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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 2 Mar 2020 17:42:07 +0100*References*: <CAKxfy0sdLdP1ocXp40hsscNt-KDLYwN8419YgZ9KBWphrhy3Cw@mail.gmail.com>

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, Stephan
--
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. |

**Follow-Ups**:**Re: [tlaplus] Model Checking the Bakery Algorithm***From:*Amirhossein Sayyadabdi

**References**:**[tlaplus] Model Checking the Bakery Algorithm***From:*Amirhossein Sayyadabdi

- Prev by Date:
**[tlaplus] Model Checking the Bakery Algorithm** - Next by Date:
**Re: [tlaplus] Model Checking the Bakery Algorithm** - Previous by thread:
**[tlaplus] Model Checking the Bakery Algorithm** - Next by thread:
**Re: [tlaplus] Model Checking the Bakery Algorithm** - Index(es):