[tlaplus] Does LATTICE rule work with the branch updated_enabled_cdot?

[Andreas Recke <Andreas.Recke@xxxxxxx>]

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

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.