There is a simple way to write a spec that is guaranteed to be machine closed. But there are lots of other ways to do it. The tools don’t care if your spec is machine closed or not. That’s your problem.
My question is: When writing a spec, is it our HUMAN's responsibility to make sure a WF or/and SF property is Machine-Closed, or the model-check runtime will help do the sanity check and point out: Hi, dude, the WF is NOT a subaction of the NEXT...?
\*I tried to introduce an WF action that will break the NEXT safety property.
FairnessChaos == x'=x+2
\* Conjunction together with Init, Safety and WF property
Then I run the TLA+ model checker. Apparently, every time the state will go from 0 to 101, and then check! "Invariant Invariance is violated."
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/BYAPR21MB1256A7E1AA7DDAA1A8E8F5C8B8279%40BYAPR21MB1256.namprd21.prod.outlook.com.