Re: [tlaplus] How does TLC know which action is the Init action?

Stephan

On 23 Oct 2023, at 22:36, jayaprabhakar k <jayaprabhakar@xxxxxxxxx> wrote:

More questions on the syntax.

For the common form of the spec,

Init == count = 0

Next == count' = count + 1

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

Here, wouldn't the Init state be true only at the initialization, and ever since any next state operation takes place, that modifies count, then Init predicate is false forever.
Then, wouldn't this Spec evaluate to false in every behavior?

On Mon, 23 Oct 2023 at 10:55, jayaprabhakar k <jayaprabhakar@xxxxxxxxx> wrote:
Got it. Thanks.

On Mon, 23 Oct 2023 at 10:07, Hillel Wayne <hwayne@xxxxxxxxx> wrote:
Yup, that's fine, as long as the conjunction of the two predicates fully specifies all variables. So you might do something like
Spec == MachineInit /\ WorldInit /\ [][Next]_vars
Or
Spec == Init /\ DebugInit /\ [][Next]_vars
H
On 10/23/2023 12:03 PM, jayaprabhakar k wrote:
Does that mean, if I have the Spec defined as something like,

Spec == Predicate1 /\ [][Next]_vars /\ WF_vars(Next) /\ Predicate2
Is it still valid? (Because /\ is commutative)

What are the requirements for a valid init step? For example, any predicate with no unprimed variable. Is that required and is it sufficient?

Similarly, what if there are two predicates that follow the same requirements, would it be a valid TLA+ spec?

Thanks,
JP

On Mon, 23 Oct 2023 at 02:45, Stephan Merz <stephan.merz@xxxxxxxxx> wrote:
TLC parses the temporal formula, Init is a state predicate and Next is the [1] action that appears within the sub formula [][A]_v.

Stephan

[1] Although in TLA+ it is OK to write specifications that contain more complex formulas, such as [][A]_v /\ [][B]_w, TLC only accepts temporal formulas that contain a single sub-formula of that form.

On 23 Oct 2023, at 11:09, jayaprabhakar k <jayaprabhakar@xxxxxxxxx> wrote:

In TLC we can specify the behavioral spec as a temporal formula spec, and that is typically defined as

Spec === Init /\ [][Next]_vars /\ WF_vars(Next)

In this case,
How does TLC know Init is the init function? And more specifically, how does it know Init must happen before any Next operation occurs?
Is it by the order in which they are defined or by convention like if the name is Init etc?

Thanks,
JP

--
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/CA%2Bt%3DSiKL660Kjkn-aX13y-BytRqaUTCwXf6asFAO3X54e2vKfA%40mail.gmail.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/80431D21-1526-4D57-88CF-DA5078E43506%40gmail.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/CA%2Bt%3DSi%2Bviw5N8D5-WkHkmw8TRsjZ%2Btexn3ZHimXgk0rso_iJ7g%40mail.gmail.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/4a02b4c1-052e-4bbf-ab2f-ac874eb90723%40gmail.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/CA%2Bt%3DSiJ%2BVgKUw2drRMV0oFkXN%2BAdV6hUEDgQLrgoXBOmozqZeA%40mail.gmail.com.