Checking equiv == prop1 <=> prop2 works when the two properties are invariants. Does it also work for liveness formula?H--On Thu, Jul 23, 2026 at 7:51 AM Jeff Trull <linmodemstudent@xxxxxxxxx> wrote: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?
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 visit https://groups.google.com/d/msgid/tlaplus/96df8e5c-2d02-441a-90f1-e34ee07dc101n%40googlegroups.com.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAJ-b8szWjzjQespKDeigSzyCdoSiLYiVqKD3snokVrmVTEHTsw%40mail.gmail.com.