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
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
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.
--
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/C18C5AA0-789D-4EA0-B031-6BCC9F065790%40gmail.com.
|