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

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

Hi Aman!

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 expression?


kind regards,

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.