update README and add VotingApalache to manifest.json

nano-o · nano-o · commit 35a250f0c693 · 2024-01-21T07:50:34.000-08:00
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.

Original file line number	Diff line number	Diff line change
`@@ -1262,6 +1262,13 @@`
`1262`	`1262`	`}`
`1263`	`1263`	`]`
`1264`	`1264`	`},`
	`1265`	`+ {`
	`1266`	`+ "path": "specifications/Paxos/VotingApalache.tla",`
	`1267`	`+ "communityDependencies": [],`
	`1268`	`+ "tlaLanguageVersion": 2,`
	`1269`	`+ "features": [],`
	`1270`	`+ "models": []`
	`1271`	`+ },`
`1265`	`1272`	`{`
`1266`	`1273`	`"path": "specifications/Paxos/Paxos.tla",`
`1267`	`1274`	`"communityDependencies": [],`