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

*From*: Saswata Paul <paulsaswata1@xxxxxxxxx>*Date*: Mon, 19 Aug 2019 13:10:10 -0700 (PDT)

Hi,

-- 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>bIt 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)' | |

OBVIOUS | |

<1> USE DEF Send, Inv, Ballots | |

<1> USE TRUE /\ TRUE | |

<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)' | |

PROVE FALSE | |

<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.

**Follow-Ups**:**Re: [tlaplus] The CASE keyword***From:*Saksham Chand

- Prev by Date:
**[tlaplus] TLA+, Event B comparison** - Next by Date:
**[tlaplus] Re: Usage of the ! operator** - Previous by thread:
**Re: [tlaplus] TLA+, Event B comparison** - Next by thread:
**Re: [tlaplus] The CASE keyword** - Index(es):