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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 9 May 2023 09:00:14 +0200*References*: <f247500f-7679-4f68-8d62-920b5f2f945bn@googlegroups.com> <BABF7502-A395-446E-A96E-2B17215767A1@gmail.com> <e045407f-998b-487c-a37f-286d7883f1a6n@googlegroups.com> <d60e90ec-1339-4d45-9260-4f7cb183028cn@googlegroups.com> <C0478BD4-0471-4F7F-8BFB-545A746CDEBA@gmail.com> <e51ccec9cb234989a80188b356122b36@tu-dresden.de> <4426543A-87C0-4669-8F13-BA14F4668BDF@gmail.com> <11d676cd-52cf-4c6c-b5da-0c77c0190582n@googlegroups.com> <fd4f7b70-9b92-4fd2-a15e-d4d94f8c897dn@googlegroups.com>

In fact, Init is a predicate (a Boolean _expression_), so << Init >> is a sequence containing a Boolean. Also, writing Init \in { Init } simply evaluates to TRUE and is therefore not helpful. Your original specification Init /\ [][Next]_vars (where vars is the tuple of all variables of your specification) is of the right form, assuming that it contains conditions var = ... or var \in ... for every variable var. TLC will interpret such conditions and use them for constructing the initial states. Have you actually followed an introduction to TLA+ such as Lamport's video lectures? Did you take the time to play with TLA+ specifications available online before writing your own spec from scratch? Although members of the TLA+ Google group are generally willing to help you with the problems that you encounter, it appears to me that this approach to correcting errors one by one is much less efficient than investing some time in learning how to use the language and its tools. 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/4181E31D-2B41-4AF1-A4CA-D6A567A6F1A3%40gmail.com. |

**References**:**[tlaplus] Parser Error***From:*Sara Zain

**Re: [tlaplus] Parser Error***From:*Stephan Merz

**Re: [tlaplus] Parser Error***From:*hwa...@xxxxxxxxx

**Re: [tlaplus] Parser Error***From:*Sara Zain

**Re: [tlaplus] Parser Error***From:*Stephan Merz

**Re: [tlaplus] Parser Error***From:*Sara Zain

**Re: [tlaplus] Parser Error***From:*Stephan Merz

**Re: [tlaplus] Parser Error***From:*Sara Zain

**Re: [tlaplus] Parser Error***From:*Jones Martins

- Prev by Date:
**Re: [tlaplus] Liveness only when a certain condition holds** - Next by Date:
**Re: [tlaplus] Liveness only when a certain condition holds** - Previous by thread:
**Re: [tlaplus] Parser Error** - Next by thread:
**[tlaplus] Help with UI(?) problem working through TwoPhase lecture in course** - Index(es):