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