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.