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

[Andreas Recke <Andreas.Recke@xxxxxxx>]

Hi,

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

Andreas

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