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

*From*: philippe.queinnec.pro@xxxxxxxxx*Date*: Mon, 25 Mar 2019 03:53:27 -0700 (PDT)

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.

**Follow-Ups**:**[tlaplus] Re: Proving false with fairness***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] Re: Understand symmetric set** - Next by Date:
**Re: [tlaplus] Re: Why is this temporal property violated?** - Previous by thread:
**Re: [tlaplus] Understand symmetric set** - Next by thread:
**[tlaplus] Re: Proving false with fairness** - Index(es):