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 = NNext == i > 0 /\ i' = i-1Spec == 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
=============================================================================On 4 Aug 2022, at 15:25, Andreas Recke <Andrea...@xxxxxxx> wrote:Hi,I am still a beginner with TLAPS andI am trying to prove an algorithm whichworks in TLC, but appears to be a bit more complicated to work on. So I decidedon a toy problem and found it very hard to prove.It is a simple algorithm that counts i from N to 0 and ends.I want to prove that it ends, i.e. WillTerminate == <>(i=0)The logic of the proof is inductive and by contradiction:1) show that Next is enabled for every i > 02) assume that a j \in Int exists for which WillTerminate is false3) show that if 2 is true, then it will be true for j-14) show that if 2 and 3 are true, then it will be true for j=0 which is a contradiction.TLC toolbox dislikes when I something like~WillTerminate /\ Next => (~WillTerminate)', because it contains action and temporal arguments.So I am stuck.Maybe TLAPS cannot work with the <> construct.An alternative is to set a "promise" that the algorithm ends to true and use this assurrogate which never changes. But this appears to be incorrect.I did not find anything how to work with this "will eventually be" temporal logic.I would appreciate if someone has an idea or comment on this.Kind regardsAndreasP.S.: here is the spec---------------------------- MODULE FinallyZero ----------------------------
EXTENDS Integers, Naturals, TLC, TLAPS
CONSTANTS N
ASSUME N > 0
VARIABLES i, expected_i
vars == <<i>>
Init == i = N /\ i \in Int /\ expected_i = 0
Next == i > 0 /\ i' = i-1 /\ UNCHANGED(expected_i)
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
Inv == TypeOk /\ WillTerminate
THEOREM NextFinishes == ASSUME ~WillTerminate /\ Next => ~WillTerminate' PROVE FALSE
BY PTL DEF WillTerminate, Next
=============================================================================
\* Modification History
\* Last modified Thu Aug 04 14:39:02 CEST 2022 by andreas
\* Created Sun Jul 31 21:38:42 CEST 2022 by andreas--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/eb93e2f8-57ae-4da1-aa52-3d878107773dn%40googlegroups.com.