Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Draft
wants to merge 8 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -1269,6 +1269,13 @@
"features": [],
"models": []
},
{
"path": "specifications/Paxos/MCVotingApalache.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [],
"models": []
},
{
"path": "specifications/Paxos/Paxos.tla",
"communityDependencies": [],
Expand Down
32 changes: 32 additions & 0 deletions specifications/Paxos/MCVotingApalache.tla
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
--------------------------- MODULE MCVotingApalache -------------------------------
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Elsewhere, we recently discussed TLA+ naming conventions. MC*Apalache is really verbose. Perhaps, we want to adopt and encourage a less verbose convention? IIRC, Apalache already prefixes some operators with Apa. So how about ApaMCVoting or APAMCVoting? Would then even be the same number of chars if users want to do APAMCVoting and TLCMCVoting. On the other hand, we might just as well drop MC.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The MC prefix seems superfluous in that case. In this particular example, do you have a suggestion for the name of the specification module? Voting2.tla and ApaVoting2.tla?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ApaVoting2 and TLCVoting2 looks like a sensible convention to me. If one want to distinguish between different modes, she can add a prefix like TLCSimVoting2 to tag this module for simulation.

By the way, the VSCode extension simulates a model/config pair whenever the prefix Smoke* is used. This happens when the editor is saved. Once we establish a convention, we can integrate similar functionalities like type checking.


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(<<Int,VALUE>>);
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

===================================================================================

5 changes: 4 additions & 1 deletion specifications/Paxos/README
Original file line number Diff line number Diff line change
Expand Up @@ -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.
38 changes: 10 additions & 28 deletions specifications/Paxos/VotingApalache.tla
Original file line number Diff line number Diff line change
@@ -1,42 +1,30 @@
------------------------------- 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). *)
(* *)
(* 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 *)
lemmy marked this conversation as resolved.
Show resolved Hide resolved
(* 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(<<Int,VALUE>>);
votes,
\* @type: ACCEPTOR -> Int;
maxBal

TypeOK ==
Expand Down Expand Up @@ -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

=====================================================================================