Re: Execution semantics of \/

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

Curious about the question I asked, I ran the following:

--------------------------------- MODULE cs ---------------------------------
EXTENDS Integers, Sequences
VARIABLES x, y

vars == << x, y >>
Init == (x = 5) /\ (y = 6)
Action1 == x' = x + 5
Action2 == y' = y + 5
Next == Action1 \/ Action2 
Spec == Init /\ [][Next]_vars

What interesting is that it seems one branch *is* taken (whether Action1 or Action2). Here I get the error
"Successor state is not completely specified by the next-state action."

My thought here is that since both actions should have been enabled, the next state assignment should have been figured out for both x and y.

On Monday, 4 August 2014 16:55:50 UTC+5:30, Sidharth Kshatriya  wrote:
> Thanks for your quick explanation. 
> 
> 
> 
> "any one of them may be executed" --> does that mean that all of them that are enabled are executed?
> 
> 
> 
> Lets take:
> 
> 
> 
> Action1 == (x' = x + 5)
> 
> Action2 == (y' = y + 5)
> 
> 
> 
> What does Next == Action1 \/ Action2 here mean? (Note that I've deliberately omitted any preconditions for both Actions so that they are always enabled)
> 
> 
> 
> Does it mean that *both* x and y increase in value by 5 or does it mean that only one of them increases in value by 5 "simultaneously" in a single time step?
> 
> 
> 
> 
> 
> On Monday, 4 August 2014 16:46:52 UTC+5:30, Stephan Merz  wrote:
> 
> > 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