Thanks so much.AmirhosseinOn Thu, Mar 5, 2020, 11:17 AM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:Hello,--a counter-example to a temporal logic property is an infinite sequence of states such that the property is false for that sequence. For a finite-state system, such a sequence must contain a repetition of some previous state, so there is a counter-example in the form of a "lasso" (i.e., that ends in a loop). TLC displays counter-examples in this form: they always end with "back to state X" (or "stuttering", which simply is "back to the last state").StephanOn 4 Mar 2020, at 15:20, Amirhossein Sayyadabdi <amir.ahsa.2011@xxxxxxxxx> wrote: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.AmirhosseinOn Mon, Mar 2, 2020, 8:20 PM Amirhossein Sayyadabdi <amir.ahsa.2011@xxxxxxxxx> wrote:Dear Stephan, thanks so much for your valuable help.AmirhosseinOn Mon, Mar 2, 2020 at 8:12 PM Stephan Merz <stephan.merz@xxxxxxxxx> wrote: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 infinite-state, 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,StephanOn 2 Mar 2020, at 17:30, Amirhossein Sayyadabdi <amir.ahsa.2011@xxxxxxxxx> wrote: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 non-enumerable 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 BakeryWhy 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/CAKxfy0sdLdP1ocXp40hsscNt-KDLYwN8419YgZ9KBWphrhy3Cw%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/903C5BA7-4BE7-402D-B833-F29C388B7E9E%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/3043FD9B-770A-4E55-9290-0C2681592353%40gmail.com.