[tlaplus] Proving false with fairness

[philippe.queinnec.pro@xxxxxxxxx]

Two silly cases where TLC finds that <>FALSE is a valid property of the models. The first case is correct but unexpected. The second case uses CONSTRAINT which changes the meaning of the spec w.r.t liveness.

Would it be possible for TLC to warn that the situation is dangereous?
I have been bitten by both cases in a larger model (500 lines of TLA+) and lost a lot of time because of a typo (first case) and trusting "constraint" too much (second case).

---------------- MODULE foo ----------------
VARIABLE x
Fairness == WF_x(x' = 3)
Spec == x = 0 /\ [][x' = 1]_x /\ Fairness
Ouch == <>FALSE
============================================

TLC (and TLA+ logic) correctly proves <>FALSE:
Init /\ [][Next] has a unique execution (modulo stuttering) : x=0 -> x=1
This execution does not satisfy fairness.
Thus Spec = FALSE and Spec => anything.

----------------------------------------------------------------

---------------- MODULE bar ----------------
EXTENDS Naturals
VARIABLE x
Next == x' = x + 1
Spec == x = 0 /\ [][Next]_x /\ WF_x(Next)
Constraint == x <= 2
Ouch == <>FALSE
================================================================

With CONSTRAINT Constraint, TLC proves <>FALSE:
Init /\ [][Next] and the constraint has a unique execution (modulo stuttering):
     x=0 -> x=1 -> x=2 -> x=3
It does not satisfy fairness, and Spec = FALSE.

-- 
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.