Re: [tlaplus] Question about 'Init' in a TLA+ specification

["'Martin Riener' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

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

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