Execution semantics of \/

[Sidharth Kshatriya <sid.ks...@xxxxxxxxx>]

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