Hello,
a counterexample to a temporal logic property is an infinite sequence of states such that the property is false for that sequence. For a finitestate system, such a sequence must contain a repetition of some previous state, so there is a counterexample in the form of a "lasso" (i.e., that ends in a loop). TLC displays counterexamples in this form: they always end with "back to state X" (or "stuttering", which simply is "back to the last state").
Stephan
Hello,
When I try to check liveness properties (for example, Termination property in Bakery algorithm) I get an error trace that ends in: "Back to state X" where X is a previous state that most of its values are the same as the last state.
Please note that I have restricted the while(true) instruction to a few counts and I have also limited the number possible values to be chosen for tickets.
My question is: why does the error trace say this: Back to state X? Does this cause an infinite loop that violates liveness?
Please help me.
Dear Stephan, thanks so much for your valuable help.
Amirhossein
Hello,
TLC can only verify finite instances of specifications, and in particular all quantifier bounds have to be finite sets. The statements following labels e3 and exit contain quantification over Nat (or infinite subsets of Nat), which TLC cannot evaluate. Moreover, the introductory comments explicitly state that this specification of the Bakery algorithm is "more elegant and easy to prove, but less efficient to model check".
You can override Nat by a finite set such as `0 .. 10' in Additional Spec Options > Definition Override in the TLC pane, but you should be aware that the Bakery algorithm is intrinsically infinitestate, even for a finite set of participants. In particular, overriding Nat may introduce deadlocks in the algorithm because no number larger than the current maximum can be chosen.
Hope this helps, Stephan
Hi everyone, I have taken the TLA+ spec of the bakery algorithm from [1] and I am trying to run the model checker on it, with no success. I have deleted the comment containing the PlusCal code along with those parts related to the proof system. The spec is currently in attachment file. This is the exception that TLC throws when I run it with N = 4 or 3:
TLC threw an unexpected exception. This was probably caused by an error in the spec or model. See the User Output or TLC Console for clues to what happened. The exception was a java.lang.RuntimeException : TLC encountered a nonenumerable quantifier bound Nat. line 65, col 31 to line 65, col 33 of module Bakery The error occurred when TLC was evaluating the nested expressions at the following positions: 0. Line 64, column 13 to line 71, column 56 in Bakery 1. Line 64, column 16 to line 64, column 30 in Bakery 2. Line 65, column 16 to line 70, column 53 in Bakery 3. Line 65, column 19 to line 67, column 53 in Bakery 4. Line 65, column 22 to line 66, column 54 in Bakery
Why is this happening? I have indicated Spec as the temporal formula in Model Overview page.
Amirhossein

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/CAKxfy0sdLdP1ocXp40hsscNtKDLYwN8419YgZ9KBWphrhy3Cw%40mail.gmail.com.
<bakery_raw_tla.txt>

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/903C5BA74BE7402DB833F29C388B7E9E%40gmail.com.

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/CAKxfy0tahdZyjuYthzQpXRRgoY%3D9xY7LCZh7S0a8ptvqTftPaQ%40mail.gmail.com.

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/3043FD9B770A4E5592900C2681592353%40gmail.com.
