update README and add VotingApalache to manifest.json

Signed-off-by: Giuliano Losa <[email protected]>
tlaplus · Jan 21, 2024 · 26a4582 · 26a4582
1 parent 528db1d
commit 26a4582
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 1 deletion.
diff --git a/manifest.json b/manifest.json
@@ -1262,6 +1262,13 @@
             }
           ]
         },
+        {
+          "path": "specifications/Paxos/VotingApalache.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
         {
           "path": "specifications/Paxos/Paxos.tla",
           "communityDependencies": [],

diff --git a/specifications/Paxos/README b/specifications/Paxos/README
@@ -29,4 +29,8 @@ MCPaxos
   three specifications above.  The Toolbox makes it unnecessary
   for the user to write such specs, essentially producing them
   itself from the models defined by the user.
-
+
+VotingApalache
+  A version of the Voting specification that can be analyzed
+  the the Apalache model-checker. Also contains an inductive
+  invariant that Apalache can verify for small system sizes.