Add version of Voting.tla that can be analyzed by Apalache.

manifest.json

@@ -1262,6 +1262,20 @@
             }
           ]
         },
+        {
+          "path": "specifications/Paxos/Voting2.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
+        {
+          "path": "specifications/Paxos/ApaVoting2.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
         {
           "path": "specifications/Paxos/Paxos.tla",
           "communityDependencies": [],

specifications/Paxos/ApaVoting2.tla

@@ -0,0 +1,38 @@
+--------------------------- MODULE ApaVoting2 -------------------------------
+
+(*********************************************************************************)
+(* In this module we instantiate VotingApalache with small constants in order to *)
+(* run the `^Apalache^' model-checker. We also give type annotations for the     *)
+(* variables, which are required by `^Apalache^'.                                *)
+(*********************************************************************************)
+
+EXTENDS Integers
+
+Value == {"V1_OF_VALUE","V2_OF_VALUE"}
+Acceptor == {"A1_OF_ACCEPTOR","A2_OF_ACCEPTOR","A3_OF_ACCEPTOR"}
+\* The quorums are the sets of 2 acceptors:
+Quorum == {
+    {"A1_OF_ACCEPTOR","A2_OF_ACCEPTOR"},
+    {"A1_OF_ACCEPTOR","A3_OF_ACCEPTOR"},
+    {"A2_OF_ACCEPTOR","A3_OF_ACCEPTOR"}}
+
+MaxBal == 2
+Ballot == 0..MaxBal \* NOTE: we have to make this a finite set for `^Apalache^'
+
+VARIABLES
+    \* @type: ACCEPTOR -> Set(<<Int,VALUE>>);
+    votes,
+    \* @type: ACCEPTOR -> Int;
+    maxBal
+
+INSTANCE Voting2
+
+\* To install `^Apalache,^' see the `^Apalache^' website at `^https://apalache.informal.systems/^'.
+\* Note that this is not necessary if you are using the devcontainer, as `^Apalache,^' is already installed.
+\* To check that the invariant holds initially, run:
+\* apalache-mc check --init=Init --inv=Invariant --length=0 MCVotingApalache.tla
+\* To check that the invariant is preserved, run:
+\* apalache-mc check '--tuning-options=search.invariantFilter=1->.*' --init=Invariant --inv=Invariant --length=1 MCVotingApalache.tla
+
+===================================================================================
+

specifications/Paxos/README

@@ -29,4 +29,11 @@ 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.
-
+
+Voting2
+  A version of the Voting specification that can be analyzed
+  by the Apalache model-checker. Also contains an inductive
+  invariant that Apalache can verify for small system sizes.
+ApaVoting2
+  Specification used to model-check Voting2 with the Apalache
+  model-checker.

specifications/Paxos/Voting2.tla

@@ -0,0 +1,110 @@
+------------------------------- MODULE Voting2 -------------------------------
+
+(***********************************************************************************)
+(* This is a version of `^Voting.tla^' that can be analyzed by the `^Apalache^'    *)
+(* model-checker. Here are the differences compared to `^Voting.tla^':             *)
+(*                                                                                 *)
+(*     * We make Ballot a constant in order to be able to substitute a finite set  *)
+(*       for model-checking with Apalache.                                         *)
+(*                                                                                 *)
+(*     * We rewrite SafeAt and ShowsSafeAt to avoid ranges of integers with        *)
+(*       non-constant bounds (which `^Apalache^' does not support).                *)
+(*                                                                                 *)
+(* We also give an inductive invariant that proves the consistency property. On a  *)
+(* desktop computer from 2022, `^Apalache^' takes 1 minute and 45 seconds to check *)
+(* that the invariant is inductive when there are 3 values, 3 processes, and 4     *)
+(* ballots. For model-checking with `^Apalache,^'see `^ApaVoting2.tla^'.           *)
+(***********************************************************************************)
+
+EXTENDS Integers
+
+CONSTANTS
+    Value,
+    Acceptor,
+    Quorum,
+    Ballot
+
+VARIABLES
+    votes,
+    maxBal
+
+TypeOK ==
+    /\ votes \in [Acceptor -> SUBSET (Ballot\times Value)]
+    /\ maxBal \in [Acceptor -> Ballot\cup {-1}]
+
+VotedFor(a, b, v) == <<b, v>> \in votes[a]
+
+ChosenAt(b, v) ==
+  \E Q \in Quorum : \A a \in Q : VotedFor(a, b, v)
+
+chosen == {v \in Value : \E b \in Ballot : ChosenAt(b, v)}
+
+DidNotVoteAt(a, b) == \A v \in Value : ~ VotedFor(a, b, v)
+
+CannotVoteAt(a, b) == /\ maxBal[a] > b
+                      /\ DidNotVoteAt(a, b)
+NoneOtherChoosableAt(b, v) ==
+   \E Q \in Quorum :
+     \A a \in Q : VotedFor(a, b, v) \/ CannotVoteAt(a, b)
+
+SafeAt(b, v) == \A c \in Ballot : c < b => NoneOtherChoosableAt(c, v)
+
+ShowsSafeAt(Q, b, v) ==
+  /\ \A a \in Q : maxBal[a] \geq b
+  \* NOTE: `^Apalache^' does not support non-constant integer ranges (e.g. we cannot write (c+1)..(b-1))
+  /\ \E c \in Ballot\cup {-1} :
+    /\ c < b
+    /\ (c # -1) => \E a \in Q : VotedFor(a, c, v)
+    /\ \A d \in Ballot : c < d /\ d < b => \A a \in Q : DidNotVoteAt(a, d)
+
+Init ==
+    /\ votes = [a \in Acceptor |-> {}]
+    /\ maxBal = [a \in Acceptor |-> -1]
+
+IncreaseMaxBal(a, b) ==
+  /\ b > maxBal[a]
+  /\ maxBal' = [maxBal EXCEPT ![a] = b]
+  /\ UNCHANGED votes
+
+VoteFor(a, b, v) ==
+    /\ maxBal[a] \leq b
+    /\ \A vt \in votes[a] : vt[1] # b
+    /\ \A c \in Acceptor \ {a} :
+         \A vt \in votes[c] : (vt[1] = b) => (vt[2] = v)
+    /\ \E Q \in Quorum : ShowsSafeAt(Q, b, v)
+    /\ votes' = [votes EXCEPT ![a] = @ \cup {<<b, v>>}]
+    /\ maxBal' = [maxBal EXCEPT ![a] = b]
+
+Next  ==  \E a \in Acceptor, b \in Ballot :
+            \/ IncreaseMaxBal(a, b)
+            \/ \E v \in Value : VoteFor(a, b, v)
+
+Spec == Init /\ [][Next]_<<votes, maxBal>>
+
+(********************************************************************************)
+(* Next, we define an inductive invariant that shows consistency. We reuse      *)
+(* definitions from Voting.tla and add the property NoVoteAfterMaxBal, which is *)
+(* needed to make the invariant inductive.                                      *)
+(********************************************************************************)
+
+VotesSafe == \A a \in Acceptor, b \in Ballot, v \in Value :
+                 VotedFor(a, b, v) => SafeAt(b, v)
+
+OneValuePerBallot ==
+    \A a1, a2 \in Acceptor, b \in Ballot, v1, v2 \in Value :
+       VotedFor(a1, b, v1) /\ VotedFor(a2, b, v2) => (v1 = v2)
+
+NoVoteAfterMaxBal == \A a \in Acceptor, b \in Ballot, v \in Value :
+    <<b,v>> \in votes[a] => /\ b <= maxBal[a]
+
+Consistency == \A v,w \in chosen : v = w
+
+\* This invariant is inductive and establishes consistency:
+Invariant ==
+  /\ TypeOK
+  /\ VotesSafe
+  /\ OneValuePerBallot
+  /\ NoVoteAfterMaxBal
+  /\ Consistency
+
+=====================================================================================