More info about JPF testing

FedericoPonzi · Jun 15, 2024 · 2e05e79 · 2e05e79
1 parent be2f002
commit 2e05e79
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 4 deletions.
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
@@ -14,14 +14,15 @@
     - [SANY]()
     - [Java Path Finder](./codebase/jpf.md)
     - []()
-- [Learning TLA+](./learning/intro.md)
+- [Learning TLA+: Introduction](./learning/intro.md)
     - [Lamport's video tutorial]()
+    - [Hyperbook]()
     - [Example repo]()
     - [Notable repos]()
     - [Books]()
     - [TLA]()
         - [Typed Model Values]()
-    - [Pluscal]()
+    - [Pluscal](./learning/pluscal.md)
         - []()
     - [TLA+ Vs xxx](./learning/tla-comparisons.md)
     - [Config files](./learning/config-file.md)

diff --git a/src/codebase/jpf.md b/src/codebase/jpf.md
@@ -1,5 +1,9 @@
 # Java Path Finder
-Java Path Finder is a project developed by nasa for model checking Java bytecode. See [https://github.com/javapathfinder/jpf-core](https://github.com/javapathfinder/jpf-core).
+Java Path Finder is a project developed by Nasa for model checking Java bytecode. See [https://github.com/javapathfinder/jpf-core](https://github.com/javapathfinder/jpf-core).
 
-JPF is used to test some of the tla+ classes.
+JPF is used to test some of the datastructures of tlatools. These tests can be invoked by using:
+
+```
+ant -f customBuild.xml compile compile-test test-verify
+```