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

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



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

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

--
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/682b2064-00f8-4546-92e3-300868ef9f9an%40googlegroups.com.