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

*From*: Andreas Recke <Andreas.Recke@xxxxxxx>*Date*: Thu, 15 Sep 2022 12:37:35 -0700 (PDT)

Hi,

I am trying to set up a liveness proof.

I was able to use the WF1 rule successfully, but going farther did not work.

I have just a simple "count down from N to 0 then stop" spec.

I know there is an example that uses NatInduction, but I want to specifically

use the LATTICE rule because I would like to set up a framework for a more

complicated spec.

But now I am stuck at this:

ASSUME d \in S /\ d > 0

[]TypeOk /\ [][Next]_vars /\ WF_vars(Next) => (G(d) ~> G(d-1))

But reformulating this to

[]TypeOk /\ [][Next]_vars /\ WF_vars(Next) => (G(d) ~> \E e \in S: e < d /\ G(e))

does not work.

Moreover, another toy example with somehow similar also failed

THEOREM SmallTest == ASSUME

NEW TEMPORAL System,

NEW VARIABLE j,

NEW CONSTANT d \in S,

NEW CONSTANT e \in S,

e = d-1,

System => j=d ~> j=d-1

PROVE

System => j=d ~> j=e

BY

PTL

NEW TEMPORAL System,

NEW VARIABLE j,

NEW CONSTANT d \in S,

NEW CONSTANT e \in S,

e = d-1,

System => j=d ~> j=d-1

PROVE

System => j=d ~> j=e

BY

PTL

As if there is a bug. Or am I making a strange mistake?

Anyway: does LATTICE work with this new branch?

Thank you again in advance!

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/37114691-5b42-42ce-a506-73ed0f5a4ea4n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Does LATTICE rule work with the branch updated_enabled_cdot?***From:*Stephan Merz

**[tlaplus] Re: Does LATTICE rule work with the branch updated_enabled_cdot?***From:*Andreas Recke

- Prev by Date:
**[tlaplus] Re: Where is the code for the state space traversal algorithm in TLC?** - Next by Date:
**Re: [tlaplus] Re: Where is the code for the state space traversal algorithm in TLC?** - Previous by thread:
**Re: [tlaplus] Where is the code for the state space traversal algorithm in TLC?** - Next by thread:
**[tlaplus] Re: Does LATTICE rule work with the branch updated_enabled_cdot?** - Index(es):