From a9a134cdf37bb1380b4007b9752db0ae8897e238 Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Sat, 20 Jan 2024 21:35:25 -0800 Subject: [PATCH 1/8] Add version of Voting.tla that can be analyzed by Apalache. This includes an inductive invariant that establishes consistency. Signed-off-by: Giuliano Losa --- specifications/Paxos/VotingApalache.tla | 129 ++++++++++++++++++++++++ 1 file changed, 129 insertions(+) create mode 100644 specifications/Paxos/VotingApalache.tla diff --git a/specifications/Paxos/VotingApalache.tla b/specifications/Paxos/VotingApalache.tla new file mode 100644 index 00000000..f5bad2c2 --- /dev/null +++ b/specifications/Paxos/VotingApalache.tla @@ -0,0 +1,129 @@ +------------------------------- MODULE VotingApalache ------------------------------- + +(***********************************************************************************) +(* 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 give concrete definitions for the constants *) +(* *) +(* * We fix the number of ballots *) +(* *) +(* * We add the necessary type annotation on variables *) +(* *) +(* * We rewrite SafeAt and ShowsSafeAt to avoid ranges of integers with *) +(* non-constant bounds (which `^Apalache^' does not support). *) +(* *) +(* Ideally, we would have instantiated Voting.tla, made the appropriate *) +(* substitutions, and reused the rest. However, the presence of TLAPS proofs in *) +(* Consensus.tla and Voting.tla seem to make `^Apalache^' fail. *) +(* *) +(* We also give an inductive invariant that proves the Safety property. On a *) +(* desktop computer bought in 2022, `^Apalache^' takes 1 minute and 45 seconds to *) +(* check that the invariant is inductive when there are for 3 values, 3 processes, *) +(* and 4 ballots. Instructions to run `^Apalache^' appear at the end of the *) +(* specification. *) +(***********************************************************************************) + +EXTENDS Integers, FiniteSets + +Value == {"V1_OF_VALUE","V2_OF_VALUE","V3_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 == 3 \* 1m45s with MaxBal=3 +Ballot == 0..MaxBal \* NOTE: has to be finite for `^Apalache^' because it is used as the domain of a function + +VARIABLES + \* @type: ACCEPTOR -> Set(<>); + votes, + \* @type: ACCEPTOR -> Int; + maxBal + +TypeOK == + /\ votes \in [Acceptor -> SUBSET (Ballot\times Value)] + /\ maxBal \in [Acceptor -> Ballot\cup {-1}] + +VotedFor(a, 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 {<>}] + /\ maxBal' = [maxBal EXCEPT ![a] = b] + +Next == \E a \in Acceptor, b \in Ballot : + \/ IncreaseMaxBal(a, b) + \/ \E v \in Value : VoteFor(a, b, v) + +(********************************************************************************) +(* 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 : + <> \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 + +\* To install `^Apalache,^' see the `^Apalache^' website at `^https://apalache.informal.systems/^' +\* To check that the invariant holds initially, run: +\* ${APALACHE_HOME}/script/run-docker.sh check --init=Init --inv=Invariant --length=0 VotingApalache.tla +\* To check that the invariant is preserved, run: +\* ${APALACHE_HOME}/script/run-docker.sh check '--tuning-options=search.invariantFilter=1->.*' --init=Invariant --inv=Invariant --length=1 VotingApalache.tla + +===================================================================================== From 528db1d1f6ff56470febc2c332bbec284183109d Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Sun, 21 Jan 2024 07:42:50 -0800 Subject: [PATCH 2/8] remove comment above reusing Voting.tla Signed-off-by: Giuliano Losa --- specifications/Paxos/VotingApalache.tla | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/specifications/Paxos/VotingApalache.tla b/specifications/Paxos/VotingApalache.tla index f5bad2c2..354e100a 100644 --- a/specifications/Paxos/VotingApalache.tla +++ b/specifications/Paxos/VotingApalache.tla @@ -8,19 +8,15 @@ (* *) (* * We fix the number of ballots *) (* *) -(* * We add the necessary type annotation on variables *) +(* * We add the necessary type annotations on variables *) (* *) (* * We rewrite SafeAt and ShowsSafeAt to avoid ranges of integers with *) (* non-constant bounds (which `^Apalache^' does not support). *) (* *) -(* Ideally, we would have instantiated Voting.tla, made the appropriate *) -(* substitutions, and reused the rest. However, the presence of TLAPS proofs in *) -(* Consensus.tla and Voting.tla seem to make `^Apalache^' fail. *) -(* *) -(* We also give an inductive invariant that proves the Safety property. On a *) -(* desktop computer bought in 2022, `^Apalache^' takes 1 minute and 45 seconds to *) -(* check that the invariant is inductive when there are for 3 values, 3 processes, *) -(* and 4 ballots. Instructions to run `^Apalache^' appear at the end of the *) +(* 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. Instructions to run `^Apalache^' appear at the end of the *) (* specification. *) (***********************************************************************************) @@ -34,7 +30,7 @@ Quorum == { {"A1_OF_ACCEPTOR","A3_OF_ACCEPTOR"}, {"A2_OF_ACCEPTOR","A3_OF_ACCEPTOR"}} -MaxBal == 3 \* 1m45s with MaxBal=3 +MaxBal == 2 Ballot == 0..MaxBal \* NOTE: has to be finite for `^Apalache^' because it is used as the domain of a function VARIABLES From 26a45828b3d43a5e886c379103a5982233d9b13f Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Sun, 21 Jan 2024 07:50:34 -0800 Subject: [PATCH 3/8] update README and add VotingApalache to manifest.json Signed-off-by: Giuliano Losa --- 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. From 681565c9bd1de49d8f7c4522aeaab24a9fb4c0ba Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Sun, 21 Jan 2024 18:07:11 -0800 Subject: [PATCH 4/8] Mention that Apalache is installed in the devcontainer Signed-off-by: Giuliano Losa --- specifications/Paxos/VotingApalache.tla | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/specifications/Paxos/VotingApalache.tla b/specifications/Paxos/VotingApalache.tla index 354e100a..83049448 100644 --- a/specifications/Paxos/VotingApalache.tla +++ b/specifications/Paxos/VotingApalache.tla @@ -20,7 +20,7 @@ (* specification. *) (***********************************************************************************) -EXTENDS Integers, FiniteSets +EXTENDS Integers Value == {"V1_OF_VALUE","V2_OF_VALUE","V3_OF_VALUE"} Acceptor == {"A1_OF_ACCEPTOR","A2_OF_ACCEPTOR","A3_OF_ACCEPTOR"} @@ -116,10 +116,11 @@ Invariant == /\ NoVoteAfterMaxBal /\ Consistency -\* To install `^Apalache,^' see the `^Apalache^' website at `^https://apalache.informal.systems/^' +\* 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_HOME}/script/run-docker.sh check --init=Init --inv=Invariant --length=0 VotingApalache.tla +\* apalache-mc check --init=Init --inv=Invariant --length=0 VotingApalache.tla \* To check that the invariant is preserved, run: -\* ${APALACHE_HOME}/script/run-docker.sh check '--tuning-options=search.invariantFilter=1->.*' --init=Invariant --inv=Invariant --length=1 VotingApalache.tla +\* apalache-mc check '--tuning-options=search.invariantFilter=1->.*' --init=Invariant --inv=Invariant --length=1 VotingApalache.tla ===================================================================================== From fe909ede13a9dfe367b4ba14b42dbdf679140d77 Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Mon, 22 Jan 2024 08:12:26 -0800 Subject: [PATCH 5/8] Add forgotten definition of Spec Signed-off-by: Giuliano Losa --- specifications/Paxos/VotingApalache.tla | 2 ++ 1 file changed, 2 insertions(+) diff --git a/specifications/Paxos/VotingApalache.tla b/specifications/Paxos/VotingApalache.tla index 83049448..3655f23c 100644 --- a/specifications/Paxos/VotingApalache.tla +++ b/specifications/Paxos/VotingApalache.tla @@ -90,6 +90,8 @@ Next == \E a \in Acceptor, b \in Ballot : \/ IncreaseMaxBal(a, b) \/ \E v \in Value : VoteFor(a, b, v) +Spec == Init /\ [][Next]_<> + (********************************************************************************) (* Next, we define an inductive invariant that shows consistency. We reuse *) (* definitions from Voting.tla and add the property NoVoteAfterMaxBal, which is *) From b95e74b135058fc103bb4ce817cc066dc759ba79 Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Mon, 22 Jan 2024 08:28:10 -0800 Subject: [PATCH 6/8] Use a separate MC file for checking VotingApalache with Apalache Signed-off-by: Giuliano Losa --- manifest.json | 7 +++++ specifications/Paxos/MCVotingApalache.tla | 32 +++++++++++++++++++ specifications/Paxos/README | 5 ++- specifications/Paxos/VotingApalache.tla | 38 ++++++----------------- 4 files changed, 53 insertions(+), 29 deletions(-) create mode 100644 specifications/Paxos/MCVotingApalache.tla diff --git a/manifest.json b/manifest.json index 9459c587..06c002a3 100644 --- a/manifest.json +++ b/manifest.json @@ -1269,6 +1269,13 @@ "features": [], "models": [] }, + { + "path": "specifications/Paxos/MCVotingApalache.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, { "path": "specifications/Paxos/Paxos.tla", "communityDependencies": [], diff --git a/specifications/Paxos/MCVotingApalache.tla b/specifications/Paxos/MCVotingApalache.tla new file mode 100644 index 00000000..0d0a7788 --- /dev/null +++ b/specifications/Paxos/MCVotingApalache.tla @@ -0,0 +1,32 @@ +--------------------------- MODULE MCVotingApalache ------------------------------- + +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: has to be finite for `^Apalache^' because it is used as the domain of a function + +VARIABLES + \* @type: ACCEPTOR -> Set(<>); + votes, + \* @type: ACCEPTOR -> Int; + maxBal + +INSTANCE VotingApalache + +\* 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 + +=================================================================================== + diff --git a/specifications/Paxos/README b/specifications/Paxos/README index ab0fcc90..d363ffb5 100644 --- a/specifications/Paxos/README +++ b/specifications/Paxos/README @@ -32,5 +32,8 @@ MCPaxos VotingApalache A version of the Voting specification that can be analyzed - the the Apalache model-checker. Also contains an inductive + by the Apalache model-checker. Also contains an inductive invariant that Apalache can verify for small system sizes. +MCVotingApalache + Specification used to model-check VotingApalache with the + Apalache model-checker. diff --git a/specifications/Paxos/VotingApalache.tla b/specifications/Paxos/VotingApalache.tla index 3655f23c..0c874dcf 100644 --- a/specifications/Paxos/VotingApalache.tla +++ b/specifications/Paxos/VotingApalache.tla @@ -1,14 +1,10 @@ ------------------------------- MODULE VotingApalache ------------------------------- (***********************************************************************************) -(* This is a version of Voting.tla that can be analyzed by the `^Apalache^' *) -(* model-checker. Here are the differences compared to Voting.tla: *) +(* 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 give concrete definitions for the constants *) -(* *) -(* * We fix the number of ballots *) -(* *) -(* * We add the necessary type annotations on variables *) +(* * We make Ballot a constant in order to be able to substitute a finite set. *) (* *) (* * We rewrite SafeAt and ShowsSafeAt to avoid ranges of integers with *) (* non-constant bounds (which `^Apalache^' does not support). *) @@ -16,27 +12,19 @@ (* 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. Instructions to run `^Apalache^' appear at the end of the *) -(* specification. *) +(* ballots. For model-checking with `^Apalache,^'see `^MCVotingApalache.tla^'. *) (***********************************************************************************) EXTENDS Integers -Value == {"V1_OF_VALUE","V2_OF_VALUE","V3_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: has to be finite for `^Apalache^' because it is used as the domain of a function +CONSTANTS + Value, + Acceptor, + Quorum, + Ballot VARIABLES - \* @type: ACCEPTOR -> Set(<>); votes, - \* @type: ACCEPTOR -> Int; maxBal TypeOK == @@ -117,12 +105,6 @@ Invariant == /\ OneValuePerBallot /\ NoVoteAfterMaxBal /\ Consistency - -\* 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 VotingApalache.tla -\* To check that the invariant is preserved, run: -\* apalache-mc check '--tuning-options=search.invariantFilter=1->.*' --init=Invariant --inv=Invariant --length=1 VotingApalache.tla +Invariant_ == Invariant ===================================================================================== From 05ebed1d6cf2b31aa0c13c1973bd17681693d12d Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Mon, 22 Jan 2024 08:39:54 -0800 Subject: [PATCH 7/8] improve comments Signed-off-by: Giuliano Losa --- specifications/Paxos/MCVotingApalache.tla | 8 +++++++- specifications/Paxos/VotingApalache.tla | 3 ++- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/specifications/Paxos/MCVotingApalache.tla b/specifications/Paxos/MCVotingApalache.tla index 0d0a7788..6ac50f79 100644 --- a/specifications/Paxos/MCVotingApalache.tla +++ b/specifications/Paxos/MCVotingApalache.tla @@ -1,5 +1,11 @@ --------------------------- MODULE MCVotingApalache ------------------------------- +(*********************************************************************************) +(* 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"} @@ -11,7 +17,7 @@ Quorum == { {"A2_OF_ACCEPTOR","A3_OF_ACCEPTOR"}} MaxBal == 2 -Ballot == 0..MaxBal \* NOTE: has to be finite for `^Apalache^' because it is used as the domain of a function +Ballot == 0..MaxBal \* NOTE: we have to make this a finite set for `^Apalache^' VARIABLES \* @type: ACCEPTOR -> Set(<>); diff --git a/specifications/Paxos/VotingApalache.tla b/specifications/Paxos/VotingApalache.tla index 0c874dcf..e5b1595f 100644 --- a/specifications/Paxos/VotingApalache.tla +++ b/specifications/Paxos/VotingApalache.tla @@ -4,7 +4,8 @@ (* 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. *) +(* * 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). *) From fb0b1d80c1888951462fcf51db93d88f34f75e87 Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Mon, 22 Jan 2024 09:06:10 -0800 Subject: [PATCH 8/8] rename files Signed-off-by: Giuliano Losa --- manifest.json | 4 ++-- .../Paxos/{MCVotingApalache.tla => ApaVoting2.tla} | 4 ++-- specifications/Paxos/README | 8 ++++---- specifications/Paxos/{VotingApalache.tla => Voting2.tla} | 5 ++--- 4 files changed, 10 insertions(+), 11 deletions(-) rename specifications/Paxos/{MCVotingApalache.tla => ApaVoting2.tla} (93%) rename specifications/Paxos/{VotingApalache.tla => Voting2.tla} (95%) diff --git a/manifest.json b/manifest.json index 06c002a3..f9da5ef7 100644 --- a/manifest.json +++ b/manifest.json @@ -1263,14 +1263,14 @@ ] }, { - "path": "specifications/Paxos/VotingApalache.tla", + "path": "specifications/Paxos/Voting2.tla", "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], "models": [] }, { - "path": "specifications/Paxos/MCVotingApalache.tla", + "path": "specifications/Paxos/ApaVoting2.tla", "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], diff --git a/specifications/Paxos/MCVotingApalache.tla b/specifications/Paxos/ApaVoting2.tla similarity index 93% rename from specifications/Paxos/MCVotingApalache.tla rename to specifications/Paxos/ApaVoting2.tla index 6ac50f79..af7a79e1 100644 --- a/specifications/Paxos/MCVotingApalache.tla +++ b/specifications/Paxos/ApaVoting2.tla @@ -1,4 +1,4 @@ ---------------------------- MODULE MCVotingApalache ------------------------------- +--------------------------- MODULE ApaVoting2 ------------------------------- (*********************************************************************************) (* In this module we instantiate VotingApalache with small constants in order to *) @@ -25,7 +25,7 @@ VARIABLES \* @type: ACCEPTOR -> Int; maxBal -INSTANCE VotingApalache +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. diff --git a/specifications/Paxos/README b/specifications/Paxos/README index d363ffb5..231e6c05 100644 --- a/specifications/Paxos/README +++ b/specifications/Paxos/README @@ -30,10 +30,10 @@ MCPaxos for the user to write such specs, essentially producing them itself from the models defined by the user. -VotingApalache +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. -MCVotingApalache - Specification used to model-check VotingApalache with the - Apalache model-checker. +ApaVoting2 + Specification used to model-check Voting2 with the Apalache + model-checker. diff --git a/specifications/Paxos/VotingApalache.tla b/specifications/Paxos/Voting2.tla similarity index 95% rename from specifications/Paxos/VotingApalache.tla rename to specifications/Paxos/Voting2.tla index e5b1595f..3fcbf8f0 100644 --- a/specifications/Paxos/VotingApalache.tla +++ b/specifications/Paxos/Voting2.tla @@ -1,4 +1,4 @@ -------------------------------- MODULE VotingApalache ------------------------------- +------------------------------- MODULE Voting2 ------------------------------- (***********************************************************************************) (* This is a version of `^Voting.tla^' that can be analyzed by the `^Apalache^' *) @@ -13,7 +13,7 @@ (* 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 `^MCVotingApalache.tla^'. *) +(* ballots. For model-checking with `^Apalache,^'see `^ApaVoting2.tla^'. *) (***********************************************************************************) EXTENDS Integers @@ -106,6 +106,5 @@ Invariant == /\ OneValuePerBallot /\ NoVoteAfterMaxBal /\ Consistency -Invariant_ == Invariant =====================================================================================