From 26a45828b3d43a5e886c379103a5982233d9b13f Mon Sep 17 00:00:00 2001
From: Giuliano Losa <giuliano@losa.fr>
Date: Sun, 21 Jan 2024 07:50:34 -0800
Subject: [PATCH] update README and add VotingApalache to manifest.json

Signed-off-by: Giuliano Losa <giuliano@losa.fr>
---
 manifest.json               | 7 +++++++
 specifications/Paxos/README | 6 +++++-
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/manifest.json b/manifest.json
index fa336cc3..9459c587 100644
--- 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
index c6022b6f..ab0fcc90 100644
--- 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.
-   
\ No newline at end of file
+   
+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.