From 528db1d1f6ff56470febc2c332bbec284183109d Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Sun, 21 Jan 2024 07:42:50 -0800 Subject: [PATCH] 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