Thanks Martin. I forgot to mention that I don't use the toolbox. Rather, I run TLC from the command-line. Even in that case, I am assuming TLC picks Init as the initialization _expression_. However, what if I have used some other identifier (fooInit)?
On Saturday, September 24, 2022 at 6:31:54 PM UTC-4 martin...@xxxxxxxxxxxxxx wrote:
Hi Aman!
On 9/25/22 00:25, Aman Shaikh wrote:
> Hi
>
> 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
> _expression_?
>
> thx
> aman
>
kind regards,
Martin