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

*From*: Andreas Recke <Andreas.Recke@xxxxxxx>*Date*: Thu, 4 Aug 2022 06:25:27 -0700 (PDT)

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

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.

**Follow-Ups**:**Re: [tlaplus] Proving termination using the "will eventually be true" logic***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Question about the value of action expressions** - Next by Date:
**Re: [tlaplus] Proving termination using the "will eventually be true" logic** - Previous by thread:
**Re: [tlaplus] Question about the value of action expressions** - Next by thread:
**Re: [tlaplus] Proving termination using the "will eventually be true" logic** - Index(es):