forked from tlaplus/Examples
-
Notifications
You must be signed in to change notification settings - Fork 0
/
ApaVoting.tla
52 lines (38 loc) · 1.38 KB
/
ApaVoting.tla
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
--------------------------- MODULE ApaVoting -------------------------------
EXTENDS Integers
CONSTANT
\* @type: Set(VALUE);
Value,
\* @type: Set(ACCEPTOR);
Acceptor,
\* @type: Set(Set(ACCEPTOR));
Quorum
MaxBal == 2
ApaBallot == 0..MaxBal
VARIABLES
\* @type: ACCEPTOR -> Set(<<Int,VALUE>>);
votes,
\* @type: ACCEPTOR -> Int;
maxBal
INSTANCE Voting
\* SafeAt and ShowsSafeAt, as defined in Voting.tla, using non-constant integer ranges that are not supported by Apalache. We therefore rewrite them without using ranges:
ApaSafeAt(b, v) == \A c \in Ballot : c < b => NoneOtherChoosableAt(c, v)
ApaShowsSafeAt(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)
\* The indutive invariant:
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
===================================================================================