Dear Sidharth,
you shouldn't really think of a TLA specification as being executed: it is a description of the possible behaviors of your system. (Although it turns out that TLC can effectively compute the behaviors for the subset of TLA+ that it accepts.) Then a disjunction A \/ B \/ C in the next-state relation means that the transition from the current state to the next one should satisfy (at least) one of the action formulas A, B or C. If several actions are enabled, either can one can actually happen, so "any one of them may be executed". And yes,
\E i \in 1 .. 4 : A(i)
is the same as
A(1) \/ A(2) \/ A(3) \/ A(4).
For example, think of A(i) being an action that models the input of value i to the system, then it is very reasonable to expect that the system should accept any value (in the domain of the inputs).
During verification, TLC will compute all possible branches at such a point and explore the subsequent behaviors. (That's where the state explosion problem in model checking comes from.) When evaluating the next-state relation, TLC computes the sets of all successor states (i.e., valuations of the primed variables) that make the formula true. Therefore it will indeed evaluate all the operands of a disjunction – note that this problem is different from a simple evaluation of a propositional formula to a Boolean value, since the values of the primed variables are initially unknown.
Hope this helps,
Stephan
On Monday, August 4, 2014 12:27:39 PM UTC+2, Sidharth Kshatriya wrote:
Hi Folks,I have a question regarding \/ . What does \/ mean when a system is actually executing a specification?
Say,
Next == Action1 \/ Action2 \/ Action3
Now, lets say, Action1 and Action2 might both be enabled at a particular point of execution of an algorithm (i.e. they are non interleaving). Note that each action may relate primed and unprimed variables to each other.
Now does Next step here mean that Action1 *and* Action2 will be executed? Or does it mean that the *both* may be executed or any one of them many executed?
The reason I am confused is because:
TRUE == TRUE \/ DONTCARE
TRUE == TRUE \/ FALSE
TRUE == TRUE \/ TRUE
Basically is short circuit evaluation implicit in the execution semantics? Do we evaluate all operands of an \/?
Similarly we may have:
Next == \E i \in 1..4 Action(i)
Is this the same as:
Next == Action(1) \/ Action(2) \/ Action(3) \/ Action(4)
Thanks,
Sidharth