[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Does LATTICE rule work with the branch updated_enabled_cdot?
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
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
System => j=d ~> j=e
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!
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.