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 Bakery
Why is this happening? I have indicated Spec as the temporal formula in Model Overview page.
Amirhossein