About machine-closed Fairness Property

[Huailin]

Team,

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 wrote a simple spec to test what gonna happen when a fairness action is not Machine-Closed. And seems to me the checker will NOT do sanity check and keep updating the state. I am not very sure if my testing case is correct or not, though. 

------------------------------ MODULE Fairness ------------------------------
EXTENDS Naturals
VARIABLE x
FairnessIni == x=0
FairnessNext == x'=x+1

\*I tried to introduce an WF action that will break the NEXT safety property.
\*Please refer to Lamport's 2019 paper: Safeness, Liveness and Fairness

FairnessChaos == x'=x+2

\*  Conjunction together with Init, Safety and WF property
Fairness == FairnessIni /\ [][FairnessNext]_x /\ WF_x(FairnessChaos)

\* Put a invariance check to see if the state x is growing...
Invariance == x <100
--------------------------------------------------------------
THEOREM Fairness => []Invariance

=======================================================================

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."

[Stephan Merz]

Hello,

first, TLC will not check if your specification is machine-closed. (It is machine-closed if you only state fairness conditions for sub-actions of the next-state relation.)

Second, TLC does not take into account fairness conditions when checking invariants. (This may be interpreted as TLC silently assuming that specifications are machine-closed.) Even when you check `[]Invariance' as a temporal property rather than checking `Invariance' as an invariant, TLC will detect that your property is in fact an invariant and check it as such. However, if you check the temporal property `<>[]Invariance', TLC will verify it successfully. (You have to add an appropriate state constraint such as `x < 200' in order to ensure that TLC terminates).

Stephan

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/eac5bed6-4451-4c17-8c52-219b4fe6beb6n%40googlegroups.com.

[Leslie Lamport]

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.

--

[Huailin]

en. Our TLC is not a gcc *compiler*. So, it is our responsibility to make sure any WF or/and SF actions are sub-actions of (Init /\ NEXT). 

Thanks to Stephan and Lesie! Have a nice weekend! I really enjoy the TLA family's discussion!

Mike

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/BYAPR21MB1256A7E1AA7DDAA1A8E8F5C8B8279%40BYAPR21MB1256.namprd21.prod.outlook.com.