[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] About machine-closed Fairness Property


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

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/eac5bed6-4451-4c17-8c52-219b4fe6beb6n%40googlegroups.com.