How does TLC know which action is the Init action?

[jayaprabhakar k]

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

 

[Stephan Merz]

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.

--
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/CA%2Bt%3DSiKL660Kjkn-aX13y-BytRqaUTCwXf6asFAO3X54e2vKfA%40mail.gmail.com.

[jayaprabhakar k]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/80431D21-1526-4D57-88CF-DA5078E43506%40gmail.com.

[Hillel Wayne]

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

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.

[jayaprabhakar k]

Got it. Thanks.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4a02b4c1-052e-4bbf-ab2f-ac874eb90723%40gmail.com.

[jayaprabhakar k]

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?

[Stephan Merz]

The initial condition is just that: the predicate is only evaluated in the initial state.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CA%2Bt%3DSiJ%2BVgKUw2drRMV0oFkXN%2BAdV6hUEDgQLrgoXBOmozqZeA%40mail.gmail.com.

[A. Jesse Jiryu Davis]

From Specifying Systems: "Formally, we define a behavior to be a sequence of states, where a state is an assignment of values to variables. We specify a system by specifying a set of possible behaviors—the ones representing a correct execution of the system." A spec is a temporal formula, which is true of a behavior if the behavior's initial state matches Init and every step matches Next. For example, in Chapter 2, specifying an "hour clock", the book says:

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9E16FF02-E5D5-4BF3-AE1A-360F028CB53E%40gmail.com.