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

[tlaplus] Proving termination using the "will eventually be true" logic


I am still a beginner with TLAPS andI am trying to prove  an algorithm which
works in TLC, but appears to be a bit more complicated to work on. So I decided
on 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 > 0
2) assume that a j \in Int exists for which WillTerminate is false
3) show that if 2 is true, then it will be true for j-1
4) 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 as
surrogate 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 regards

P.S.: here is the spec

---------------------------- MODULE FinallyZero ----------------------------
EXTENDS Integers, Naturals, TLC, TLAPS

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/eb93e2f8-57ae-4da1-aa52-3d878107773dn%40googlegroups.com.