The initial condition is just that: the predicate is only evaluated in the initial state.
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?
Got it. Thanks.
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
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 subformula of that form.
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%3DSiKL660KjknaX13yBytRqaUTCwXf6asFAO3X54e2vKfA%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/80431D2115264D5788CFDA5078E43506%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%2Bviw5N8D5WkHkmw8TRsjZ%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/4a02b4c1052e4bbfab2fac874eb90723%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.

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/9E16FF02E5D54BF3AE1A360F028CB53E%40gmail.com.
