|No. There are infinitely many successor states satisfying x'=x+5 (with arbitrary values for y'), and there are infinitely many satisfying y'=y+5 (with arbitrary values for x'). Among all these, there is of course the state satisfying x'=x+5 /\ y'=y+5. However, verifying a specification means analyzing all its possible executions, not just an arbitrary one. One general principle of TLA+ is that nothing is assumed and everything is explicit, so if this is the successor state that you have in mind, you have to define your next-state relation using conjunction.|
If you intend to model non-deterministic choice between your two actions, you'd typically write
Action1 == x' = x+5 /\ y' = y
Action2 == y' = y+5 /\ x' = x
Next == Action1 \/ Action2
and you can see that the two actions cannot occur simultaneously in any behavior satisfying Next
. But TLA+ lets you structure your specification as you consider it most natural, and it can be perfectly reasonable to have conjunctions of action formulas in a next-state relation.
Thanks things are much clearer now. I understand how things should work in TLA+ now. But I want to pursue a line of thought here:
ActionC == Action1 \/ Action2 == (x' = x + 5) \/ (y' = y + 5)
Now there aren't any preconditions (so both branches of the disjunction are "enabled") and since both branches of the disjunction are evaluated, the combined action should mean that ActionC means that *both* x' and y' get increased by 5...
Yes, its true that I can use a conjunction if I want both actions to be taken. But here my main point is that when the preconditions are satisfied (or there aren't any preconditions) for both branches of a *disjunction* then it should be a sort of "composition" of both Action1 and Action2? Yeah, its sounds strange but I hope you understand my point here.
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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.