Checking the equivalence of two formulas (video 9a)

[Jeff Trull]

Hi folks,

I'm struggling with the tutorial at a point late in video 9a. Around 19:40 Lamport gives two temporal formulas related to liveness, and asks the viewer to "Use TLC to check their equivalence". I can't find when we were shown how to perform an equivalence check on two formulas. I made a number of unsuccessful attempts based on my beginner's understanding of how TLC works.

Finally, using a suggestion from Google AI, I changed the SPECIFICATION line of the .cfg file to be one of the specs, and added a PROPERTY listing the other, then ran the checker again with them switched. This at last behaved as I expected. This was sufficiently convoluted, however, that I suspected it was not what we were intended to do.

What is the intended action for the viewer to take to "check the equivalence" of the two temporal formulas?

[Hillel Wayne]

Checking equiv == prop1 <=> prop2 works when the two properties are invariants. Does it also work for liveness formula?

H

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/96df8e5c-2d02-441a-90f1-e34ee07dc101n%40googlegroups.com.

[Jeff Trull]

One of my experiments was to define a formula Equiv == (Spec1 <=> Spec2) in the .tla file and add PROPERTY Equiv to the .cfg file.

It resulted in the error message: TLC cannot handle the temporal formula.

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/gb7AHltMXuM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAJ-b8szWjzjQespKDeigSzyCdoSiLYiVqKD3snokVrmVTEHTsw%40mail.gmail.com.