Question about 'Init' in a TLA+ specification

[Aman Shaikh]

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. 

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

[Martin Riener]

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

[Aman Shaikh]

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

aman

[Leslie Lamport]

If you don't use the Toolbox, you have to create a configuration file for TLC.   See the chapter on TLC in "Specifying Systems".

Leslie

[Aman Shaikh]

Hi Leslie

Yes, I have read the chapter on TLC in your book (BTW I am really enjoying reading the book although at times I feel I'm really pushing the boundaries of my brain's Mathematical capability :-) ).

Usually in the config, you specify the specification to check using the SPECIFICATION statement. However, the TLC chapter in your book also mentions you can instead use INIT and NEXT statements. Is that what you're referring to?

thx

aman

[Stephan Merz]

Usually in the config, you specify the specification to check using the SPECIFICATION statement. However, the TLC chapter in your book also mentions you can instead use INIT and NEXT statements. Is that what you're referring to?

Yes: as explained in section 14.1, one can use INIT <init-pred> and NEXT <action> to declare the initial predicate and next-state action when fairness conditions are irrelevant, typically for checking safety properties. See also section 14.7.1, which contains the grammar of the configuration file.

Regards,

Stephan

On Sunday, September 25, 2022 at 1:38:01 AM UTC-4 Leslie Lamport wrote:

If you don't use the Toolbox, you have to create a configuration file for TLC.   See the chapter on TLC in "Specifying Systems".

Leslie

On Saturday, September 24, 2022 at 5:00:14 PM UTC-7 amansh...@gmail.com wrote:

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

aman

On Saturday, September 24, 2022 at 6:31:54 PM UTC-4 martin...@googlemail.com 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

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/682b2064-00f8-4546-92e3-300868ef9f9an%40googlegroups.com.