[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Question about 'Init' in a TLA+ specification
On 9/25/22 00:25, Aman Shaikh wrote:
A TLA+ specification generally has the form Init /\ [Next]_vars; I'm ignoring
liveness properties here. However, one could as well write this in the form
FooInit /\ [FooNext]_vars if my understanding is correct. In other words, Init
and Next are not TLA+ keywords.
You are correct, Init and Next are just conventions. If they are defined, the
toolbox automatically proposes them as your specification. You can choose your
own definitions in the model checking pane if you prefer.
Given this, how does a tool like TLC know that Init (or FooInit) is the starting
state of the specification? Is it because there are no primed variables in the
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/75c19d0c-5630-8ffc-3a2f-e43dfc559bb5%40gmail.com.