[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] The CASE keyword


  In the example of hierarchical proofs in the TLAPS tutorial (https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Hierarchical_proofs.html), the two possible actions of Next are considered in the proof using the CASE keyword:

Next == \/ /\ x < y /\ y' = y - x /\ x' = x \/ /\ y < x /\ x' = x-y /\ y' = y

 THEOREM NextProperty == InductiveInvariant /\ Next => InductiveInvariant'
<1> SUFFICES ASSUME InductiveInvariant, Next PROVE InductiveInvariant' <1> USE DEF InductiveInvariant, Next <1>1 (x < y) \/ (y < x) <1>a CASE x < y <1>b CASE y < x <1>2 QED BY <1>1, <1>a, <1>b

It is quite intuitive because this can be read as "the two separate cases that can occur in the next step.".

However, in the proof for Paxos (https://github.com/tlaplus/v1-tlapm/blob/master/examples/paxos/Paxos.tla), in the proof of the intermediate Lemma SafeAtStable, the different cases that can happen in the next state are expressed by using ASSUME keyword:

Next == \/ \E b \in Ballots : Phase1a(b) \/ Phase2a(b)
\/ \E a \in Acceptors : Phase1b(a) \/ Phase2b(a)

LEMMA SafeAtStable == Inv /\ Next /\ TypeOK' =>
\A v \in Values, b \in Ballots:
SafeAt(v, b) => SafeAt(v, b)'
<1> SUFFICES ASSUME Inv, Next, TypeOK',
NEW v \in Values, NEW b \in Ballots, SafeAt(v, b)
PROVE SafeAt(v, b)'
<1> USE DEF Send, Inv, Ballots
<1>1. ASSUME NEW bb \in Ballots, Phase1a(bb)
PROVE SafeAt(v, b)'
BY <1>1, SMT DEF SafeAt, Phase1a, VotedForIn, WontVoteIn
<1>2. ASSUME NEW a \in Acceptors, Phase1b(a)
PROVE SafeAt(v, b)'
BY <1>2, QuorumAssumption, SMTT(60) DEF TypeOK, SafeAt, WontVoteIn, VotedForIn, Phase1b
<1>3. ASSUME NEW bb \in Ballots, Phase2a(bb)
PROVE SafeAt(v, b)'
BY <1>3, QuorumAssumption, SMT DEF TypeOK, SafeAt, WontVoteIn, VotedForIn, Phase2a
<1>4. ASSUME NEW a \in Acceptors, Phase2b(a)
PROVE SafeAt(v, b)'
<2>1. PICK m \in msgs : Phase2b(a)!(m)
BY <1>4 DEF Phase2b
<2>2 \A aa \in Acceptors, bb \in Ballots, vv \in Values :
VotedForIn(aa, vv, bb) => VotedForIn(aa, vv, bb)'
BY <2>1 DEF TypeOK, VotedForIn
<2>3. \A aa \in Acceptors, bb \in Ballots : maxBal[aa] > bb => maxBal'[aa] > bb
BY <2>1 DEF TypeOK
<2>4. ASSUME NEW aa \in Acceptors, NEW bb \in Ballots,
WontVoteIn(aa, bb), NEW vv \in Values,
VotedForIn(aa, vv, bb)'
<3> DEFINE mm == [type |-> "2b", val |-> vv, bal |-> bb, acc |-> aa]
<3>1. mm \notin msgs
BY <2>4 DEF WontVoteIn, VotedForIn
<3>2. mm \in msgs'
<4>1. PICK m1 \in msgs' :
/\ m1.type = "2b"
/\ m1.val = vv
/\ m1.bal = bb
/\ m1.acc = aa
BY <2>4 DEF VotedForIn
<4>. QED BY <4>1 DEF TypeOK, Messages \* proved by Zenon
<3>3. aa = a /\ m.bal = bb
BY <2>1, <3>1, <3>2 DEF TypeOK
<3>. QED
BY <2>1, <2>4, <3>3 DEF Phase2b, WontVoteIn, TypeOK
<2>5 \A aa \in Acceptors, bb \in Ballots : WontVoteIn(aa, bb) => WontVoteIn(aa, bb)'
BY <2>3, <2>4 DEF WontVoteIn
<2> QED
BY <2>2, <2>5, QuorumAssumption DEF SafeAt
My question is: Has the ASSUME construct been used in the proof of SafeAtStable because Next is a disjunction of two existential quantifiers? Or could this have been written using the CASE keyword somehow?

Thank you

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8ff72031-c37d-4fad-b2eb-e50f6ab32ac4%40googlegroups.com.