[tlaplus] Checking the equivalence of two formulas (video 9a)

[Jeff Trull <linmodemstudent@xxxxxxxxx>]

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.