| Hello Andreas, thank you for using TLAPS and for your question about termination proofs. Let me first point out that the current distribution of TLAPS only supports proofs of safety properties. In particular, it has no support for reasoning about ENABLED, which in turn underlies the definition of fairness formulas, and the latter are a prerequisite for any proofs of liveness properties. However, if you are brave enough to install a development version of TLAPS [1], below is a proof of the theorem you were after. As you found out, you cannot apply priming to arbitrary temporal formulas but only to state predicates. Also, as stated above, use of the fairness condition is important for this proof, and therefore it is useful to simplify the predicate ENABLED <<Next>>_vars and replace it by the simple state predicate i>0. As you'll see, there are still a few rough edges in the proof, such as having to hide intermediate definitions before applying the induction rule, or inferring <1>3 from <1>2, which requires a mix of quantifier and temporal logic reasoning. Nevertheless, I hope that this example will give you an overall idea of how to write liveness proofs. Best regards, Stephan [1] The proof below was checked using the updated_enabled_cdot branch at https://github.com/tlaplus/tlapm/tree/updated_enabled_cdot, but I believe that the version at the master branch should also have worked. ---------------------------- MODULE FinallyZero ----------------------------
-- EXTENDS Integers, Naturals, TLC, TLAPS, NaturalsInduction CONSTANTS N ASSUME NAssumption == N \in Int /\ N > 0 VARIABLES i vars == <<i>> Init == i = N Next == i > 0 /\ i' = i-1 Spec == Init /\ [][Next]_vars /\ WF_vars(Next) \* Type Invariant TypeOk == i \in Int /\ i >= 0 \* Termination Termination == i=0 \* Will terminate invariant WillTerminate == <>(i=0) \* Complete Invariant (* not an invariant because it has a "<>" subformula *) Inv == TypeOk /\ WillTerminate (* The formula is not level-correct, as SANY points out. You cannot prime arbitrary temporal formulas in TLA, only state predicates. THEOREM NextFinishes == ASSUME ~WillTerminate /\ Next => ~WillTerminate' PROVE FALSE BY PTL DEF WillTerminate, Next *) ------------------------------------------------------------------------------ (* Proof of the algorithm. *) (* Let's start by showing type correctness. *) LEMMA Typing == Spec => []TypeOk <1>1. Init => TypeOk BY NAssumption DEF Init, TypeOk <1>2. TypeOk /\ [Next]_vars => TypeOk' BY DEF TypeOk, Next, vars <1>. QED BY <1>1, <1>2, PTL DEF Spec (* Now let's rewrite the enabledness condition that occurs as part of the fairness hypothesis to a simple state predicate. *) LEMMA EnabledNext == ASSUME TypeOk PROVE (ENABLED <<Next>>_vars) <=> i > 0 \* any Next step changes vars: here type correctness is relevant <1>1. <<Next>>_vars <=> Next BY DEF TypeOk, Next, vars \* therefore the ENABLED conditions are equivalent <1>2. (ENABLED <<Next>>_vars) <=> ENABLED Next BY <1>1, ENABLEDrules \* The method ExpandENABLED replaces ENABLED by explicit quantification. <1>. QED BY <1>2, ExpandENABLED DEF Next, vars (* We can now prove termination by induction. *) THEOREM Terminate == Spec => <>Termination <1>. DEFINE BSpec == []TypeOk /\ [][Next]_vars /\ WF_vars(Next) P(n) == [](i=n => <>Termination) <1>1. SUFFICES BSpec => <>Termination BY Typing, PTL DEF Spec <1>2. BSpec => \A n \in Nat : P(n) <2>1. BSpec => P(0) <3>1. i=0 => Termination BY DEF Termination <3>. QED BY <3>1, PTL <2>2. ASSUME NEW n \in Nat PROVE (BSpec => P(n)) => (BSpec => P(n+1)) <3>1. i=n+1 /\ [Next]_vars => (i=n+1)' \/ (i=n)' BY DEF Next, vars <3>2. i=n+1 /\ <<Next>>_vars => (i=n)' BY DEF Next, vars <3>3. TypeOk /\ i=n+1 => ENABLED <<Next>>_vars BY EnabledNext <3>4. BSpec => [](i=n+1 => <>(i=n)) BY <3>1, <3>2, <3>3, PTL DEF BSpec <3>. QED BY <3>4, PTL <2>. HIDE DEF BSpec, P <2>. QED BY <2>1, <2>2, NatInduction <1>3. BSpec => \A n \in Nat : i=n => <>Termination <2>. SUFFICES ASSUME NEW n \in Nat PROVE BSpec => (i=n => <>Termination) OBVIOUS <2>1. BSpec => P(n) BY <1>2 <2>. QED BY <2>1, PTL <1>4. BSpec => \E n \in Nat : i=n <2>1. TypeOk => \E n \in Nat : i=n BY DEF TypeOk <2>. QED BY <2>1, PTL DEF BSpec <1>. QED BY <1>3, <1>4 =============================================================================
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/B3061F52-42BE-4607-A7E5-D0594F1D878A%40gmail.com. |