RE: [tlaplus] About machine-closed Fairness Property

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.

From: tlaplus@xxxxxxxxxxxxxxxx <tlaplus@xxxxxxxxxxxxxxxx> On Behalf Of Huailin
Sent: Saturday, May 22, 2021 11:03 PM
To: tlaplus <tlaplus@xxxxxxxxxxxxxxxx>
Subject: [tlaplus] About machine-closed Fairness Property

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

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