---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/Voting.tla
---
-------------------------------- MODULE Voting ---------------------------------
(***************************************************************************)
(* This is a high-level algorithm in which a set of processes *)
(* cooperatively choose a value. It is a high-level abstraction of the *)
(* Paxos consensus algorithm. Although I don't remember exactly what went *)
(* through my mind when I invented/discovered that algorithm, I'm pretty *)
(* sure that this spec formalizes the way I first thought of the *)
(* algorithm. It would have been very hard to find this algorithm had my *)
(* mind been distracted by the irrelevant details introduced by having the *)
(* processes communicate by messages. *)
(***************************************************************************)
EXTENDS Integers, TLAPS
(***************************************************************************)
(* For historical reasons, the processes that choose a value are called *)
(* acceptors. We now declare the set Value of values, the set Acceptors *)
(* of acceptors, and another set Quorum that is a set of sets of acceptors *)
(* called quorums. *)
(***************************************************************************)
CONSTANTS Value, Acceptor, Quorum
(***************************************************************************)
(* The following assumption asserts that Quorum is a set of subsets of the *)
(* set Acceptor, and that any two elements of Quorum have at least one *)
(* element (an acceptor) in common. Think of a quorum as a set consisting *)
(* of a majority (more than half) of the acceptors. *)
(***************************************************************************)
ASSUME /\ \A Q \in Quorum : Q \subseteq Acceptor
/\ \A Q1, Q2 \in Quorum : Q1 \cap Q2 /= {}
(***************************************************************************)
(* Ballot is a set of "ballot numbers". For simplicity, we let it be the *)
(* set of natural numbers. However, we write Ballot for that set to *)
(* distinguish ballots from natural numbers used for other purposes. *)
(***************************************************************************)
Ballot == Nat
--------------------------------------------------------------------------------
(***************************************************************************)
(* The algorithm works by having acceptors cast votes in numbered ballots. *)
(* Each acceptor can cast one or more votes, where each vote cast by an *)
(* acceptor has the form <<b, v>> indicating that the acceptor has voted *)
(* for value v in ballot number b. A value is chosen if a quorum of *)
(* acceptors have voted for it in the same ballot. *)
(* *)
(* We now declare the algorithm's variables 'votes' and 'maxBal'. For *)
(* each acceptor a, he value of votes[a] is the set of votes cast by `a'; *)
(* and maxBal[a] is an integer such that `a' will never cast any further *)
(* vote in a ballot numbered less than maxBal[a]. *)
(***************************************************************************)
VARIABLES votes, maxBal
(***************************************************************************)
(* TypeOK asserts the "types" of the two variables. They are both *)
(* functions with domain Acceptor (arrays indexed by acceptors). For any *)
(* acceptor a, the value of votes[a] a set of <<ballot, value>> pairs; and *)
(* the value of maxBal[a] is either a ballot number or -1. *)
(***************************************************************************)
TypeOK ==
/\ votes \in [Acceptor -> SUBSET (Ballot \X Value)]
/\ maxBal \in [Acceptor -> Ballot \union { - 1}]
(***************************************************************************)
(* Next comes a sequence of definitions of concepts used to explain the *)
(* algorithm. *)
(***************************************************************************)
VotedFor(a, b, v) == << b, v >> \in votes[a]
(************************************************************************)
(* True iff (if and only if) acceptor a has voted for value v in *)
(* ballot number b. *)
(************************************************************************)
ChosenAt(b, v) ==
\E Q \in Quorum: \A a \in Q: VotedFor(a, b, v)
(************************************************************************)
(* True iff a quorum of acceptors have all voted for value v in ballot *)
(* number b. *)
(************************************************************************)
chosen == {v \in Value: \E b \in Ballot: ChosenAt(b, v)}
(************************************************************************)
(* Defines `chosen' to be the set of all values v for which ChosenAt(b, *)
(* v) is true for some ballot number b. This is the definition of what *)
(* it means for a value to be chosen under which the Voting algorithm *)
(* implements the Consensus specification. *)
(************************************************************************)
DidNotVoteAt(a, b) == \A v \in Value: ~VotedFor(a, b, v)
(************************************************************************)
(* True iff acceptor `a' has not voted in ballot number. *)
(************************************************************************)
CannotVoteAt(a, b) ==
/\ maxBal[a] > b
/\ DidNotVoteAt(a, b)
(************************************************************************)
(* The algorithm will not allow acceptor `a' to vote in ballot number b *)
(* if maxBal[a] > b. Hence, CannotVoteAt(a, b) implies that `a' has *)
(* not and never will vote in ballot number b. *)
(************************************************************************)
NoneOtherChoosableAt(b, v) ==
\E Q \in Quorum:
\A a \in Q: VotedFor(a, b, v) \/ CannotVoteAt(a, b)
(************************************************************************)
(* This is true iff there is some quorum Q such that each acceptor `a' *)
(* in Q either has voted for v in ballot b or has not and never will *)
(* vote in ballot b. It implies that no value other than v has been or *)
(* ever can be chosen at ballot b. This is because for a value w to be *)
(* chosen at ballot b, all the acceptors in some quorum R must have *)
(* voted for w in ballot b. But any two ballots have an acceptor in *)
(* common, so some acceptor a in R that voted for w is in Q, and an *)
(* acceptor in Q can only have voted for v, so w must equal v. *)
(************************************************************************)
SafeAt(b, v) == \A c \in 0..(b - 1): NoneOtherChoosableAt(c, v)
(************************************************************************)
(* True iff no value other than v has been or ever will be chosen in *)
(* any ballot numbered less than b. We read SafeAt(b, v) as "v is safe *)
(* at b". *)
(************************************************************************)
(***************************************************************************)
(* This theorem asserts that every value is safe at ballot 0. *)
(***************************************************************************)
THEOREM AllSafeAtZero == \A v \in Value: SafeAt(0, v)
(***************************************************************************)
(* The following theorem asserts that NoneOtherChoosableAt means what it's *)
(* name implies. The comments after its definition essentially contain a *)
(* proof of this theorem. *)
(***************************************************************************)
THEOREM ChoosableThm ==
\A b \in Ballot, v \in Value:
ChosenAt(b, v) => NoneOtherChoosableAt(b, v)
(***************************************************************************)
(* Now comes the definition of the inductive invariant Inv that *)
(* essentially explains why the algorithm is correct. *)
(***************************************************************************)
OneValuePerBallot ==
\A a1, a2 \in Acceptor, b \in Ballot, v1, v2 \in Value:
VotedFor(a1, b, v1) /\ VotedFor(a2, b, v2) => (v1 = v2)
(************************************************************************)
(* This formula asserts that if any acceptors a1 and a2 have voted in a *)
(* ballot b, then they voted for the same value in ballot b. For *)
(* a1=a2, this implies that an acceptor can vote for at most one value *)
(* in any ballot. *)
(************************************************************************)
VotesSafe == \A a \in Acceptor, b \in Ballot, v \in Value:
VotedFor(a, b, v) => SafeAt(b, v)
(************************************************************************)
(* This formula asserts that an acceptors can have voted in a ballot b *)
(* only if that value is safe at b. *)
(************************************************************************)
(***************************************************************************)
(* The algorithm is essentially derived by ensuring that this formula Inv *)
(* is always true. *)
(***************************************************************************)
Inv == TypeOK /\ VotesSafe /\ OneValuePerBallot
(***************************************************************************)
(* This definition is used in the defining the algorithm. You should *)
(* study it and make sure you understand what it says. *)
(***************************************************************************)
ShowsSafeAt(Q, b, v) ==
/\ \A a \in Q: maxBal[a] >= b
/\ \E c \in - 1..(b - 1):
/\ (c /= - 1) => \E a \in Q: VotedFor(a, c, v)
/\ \A d \in (c + 1)..(b - 1), a \in Q: DidNotVoteAt(a, d)
(***************************************************************************)
(* This is the theorem that's at the heart of the algorithm. It shows *)
(* that if the algorithm has maintained the invariance of Inv, then the *)
(* truth of ShowsSafeAt(Q, b, v) for some quorum Q ensures that v is safe *)
(* at b, so the algorithm can let an acceptor vote for v in ballot b *)
(* knowing VotesSafe will be preserved. *)
(***************************************************************************)
THEOREM ShowsSafety ==
Inv => \A Q \in Quorum, b \in Ballot, v \in Value:
ShowsSafeAt(Q, b, v) => SafeAt(b, v)
--------------------------------------------------------------------------------
(***************************************************************************)
(* Finally, we get to the definition of the algorithm. The initial *)
(* predicate is obvious. *)
(***************************************************************************)
Init ==
/\ votes = [a \in Acceptor |-> {}]
/\ maxBal = [a \in Acceptor |-> - 1]
(***************************************************************************)
(* An acceptor `a' can increase maxBal[a] at any time. *)
(***************************************************************************)
IncreaseMaxBal(a, b) ==
/\ b > maxBal[a]
/\ maxBal' = [maxBal EXCEPT ![a] = b]
/\ UNCHANGED votes
(***************************************************************************)
(* The heart of the algorithm is the action in which an acceptor `a' votes *)
(* for a value v in ballot number b. The enabling condition contains the *)
(* following conjuncts, which ensure that the invariance of Inv is *)
(* maintained. *)
(* *)
(* - `a' cannot vote in a ballot numbered less than b *)
(* *)
(* - `a' cannot already have voted in ballot number b *)
(* *)
(* - No other acceptor can have voted for a value other than v *)
(* in ballot b. *)
(* *)
(* - Uses Theorem ShowsSafety to ensure that v is safe at b. *)
(* *)
(* In TLA+, a tuple t is a function (array) whose first element is t[1], *)
(* whose second element if t[2], and so on. Thus, a vote vt is the pair *)
(* <<vt[1], vt[2]>> *)
(***************************************************************************)
VoteFor(a, b, v) ==
/\ maxBal[a] <= 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] = votes[a] \union {<< b, v >>}]
/\ maxBal' = [maxBal EXCEPT ![a] = b]
(***************************************************************************)
(* The rest of the spec is straightforward. *)
(***************************************************************************)
Next == \E a \in Acceptor, b \in Ballot:
\/ IncreaseMaxBal(a, b)
\/ \E v \in Value: VoteFor(a, b, v)
Spec == Init /\ [][Next]_<< votes, maxBal >>
--------------------------------------------------------------------------------
(***************************************************************************)
(* This theorem asserts that Inv is an invariant of the algorithm. The *)
(* high-level steps in its proof are given. *)
(***************************************************************************)
THEOREM Invariance == Spec => []Inv
<1>1. Init => Inv
<1>2. Inv /\ [Next]_<<votes, maxBal>> => Inv'
<1>3. QED
BY <1>1, <1>2, PTL DEF Spec
--------------------------------------------------------------------------------
(***************************************************************************)
(* This INSTANCE statement imports definitions from module Consensus into *)
(* the current module. All definition in module Consensus can be expanded *)
(* to definitions containing only TLA+ primitives and the declared names *)
(* Value and chosen. To import a definition from Consensus into the *)
(* current module, we have to say what expressions from the current module *)
(* are substituted for Value and chosen. The INSTANCE statement says that *)
(* expressions of the same name are substituted for them. (Because of *)
(* this, the WITH statement is redundant.) Note that in both modules, *)
(* Value is just a declared constant. However, in the current module, *)
(* `chosen' is an expression defined in terms of the variables votes and *)
(* maxBal while it is a variable in module consensus. The "C! ==" in the *)
(* statement means that defined identifiers are imported with "C!" *)
(* prepended to their names. Thus Spec of module Consensus is imported, *)
(* with these substitutions, as C!Spec. *)
(***************************************************************************)
C == INSTANCE Consensus
WITH Value <- Value, chosen <- chosen
(***************************************************************************)
(* The following theorem asserts that the Voting algorithm implements the *)
(* Consensus specification, where the expression `chosen' of the current *)
(* module implements the variable `chosen' of Consensus. The high-level *)
(* steps of the the proof are also given. *)
(***************************************************************************)
THEOREM Implementation == Spec => C!Spec
<1>1. Init => C!Init
<1>2. Inv /\ Inv' /\ [Next]_<<votes, maxBal>> => [C!Next]_chosen
<1>3. QED
BY <1>1, <1>2, Invariance, PTL DEF Spec, C!Spec
(***************************************************************************)
(* This Voting specification comes with a TLC model named SmallModel. *)
(* That model tells TLC that Spec is the specification, that Acceptor and *)
(* Values should equal sets of model values with 3 acceptors and 2 values *)
(* and Quorums should equal the indicated set of values, and that it *)
(* should check theorems Invariance and Implementation. Observe that you *)
(* can't tell TLC simply to check those theorems; you have to tell TLC to *)
(* check the properties the theorems assert that Spec satisfies. (Instead *)
(* of telling TLC that Inv should be an invariant, you can tell it that *)
(* the spec should satisfy the temporal property []Inv.) *)
(* *)
(* Even though the constants are finite sets, the spec has infinitely many *)
(* reachable sets because a ballot number can be any element of the set *)
(* Nat of natural numbers. The model modifies the spec so it has a finite *)
(* set of reachable states by using a definition override (on the Spec *)
(* Options page) to redefine Ballot to equal 0..2. (Alternatively, we *)
(* could override the definition of Nat to equal 0..2.) *)
(* *)
(* Run TLC on the model. It should just take a couple of seconds. *)
(* *)
(* After doing that, show why the assumption that any pair of quorums has *)
(* an element in common is necessary by modifying the model so that *)
(* assumption doesn't hold. (It's best to clone SmallModel and modify the *)
(* clone.) Since TLC reports an error if an assumption isn't true, you *)
(* will have to comment out the second conjunct of the ASSUME statement, *)
(* which asserts that assumption. Comments can be written as follows: *)
(* *)
(* \* This is an end-of-line comment. *)
(* *)
(* (* This is another way to write a comment. *)
(* Note that comments can be nested. *) *)
(* *)
(* To help you see what the problem is, use the Trace Explorer on the *)
(* Error page to show the value of `chosen' in each state of the trace. *)
(***************************************************************************)
================================================================================