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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 1 Dec 2022 07:51:20 +0100*References*: <4351c96e-420c-40f5-b5b4-5ed42fa131dcn@googlegroups.com>

Your definition is perfectly fine: it defines a set of records with two fields, the second of which is a sequence. However, as the error message indicates, TLC cannot evaluate this operator because the set of these records is infinite (it may contain sequences of arbitrary length). Whether this is a problem or not depends on how you intend to use the operator: - If it only appears in an invariant, say you write "rec \in MyRec" to check that some variable always takes values in this set, then TLC will be able to evaluate this predicate (it doesn't have to enumerate the entire set MyRec to do so). - If it appears in the definition of the transition system, say your initial condition has a conjunct "rec \in MyRec" or your next-state relation contains "rec' \in MyRec" then indeed your state space can be infinite because the variable can take an arbitrary value in an infinite set, and TLC will not be able to generate the state space. In that case, you can override the definition of MyRec for TLC and restrict the allowed sequences to a finite set (restricting to fixed maximal length), and check a finite subset of the state space. See the corresponding help pages in the Toolbox. From what you write, it appears that you'll initialize the variable deterministically, so you'll write something like Init == rec = [id |-> someValue, seek |-> << >>] and in that case everything should work fine: MyRec will probably only appear in a (typing) invariant. Regards, 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/545512AE-61E3-44B9-97EF-8472C3FB5B78%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] How can I define a sequence as part of a record's fields?***From:*Alan Munirji

**References**:**[tlaplus] How can I define a sequence as part of a record's fields?***From:*Alan Munirji

- Prev by Date:
**[tlaplus] How can I define a sequence as part of a record's fields?** - Next by Date:
**[tlaplus] another simple theorem** - Previous by thread:
**[tlaplus] How can I define a sequence as part of a record's fields?** - Next by thread:
**Re: [tlaplus] How can I define a sequence as part of a record's fields?** - Index(es):