Re: [tlaplus] Execution semantics of \/

[Stephan Merz <Stepha...@xxxxxxxxx>]

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.

Stephan

On 04 Aug 2014, at 14:09, Sidharth Kshatriya <sid.ks...@xxxxxxxxx> wrote:

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.

Thanks,

Sidharth 

On Mon, Aug 4, 2014 at 5:22 PM, Stephan Merz <Stepha...@xxxxxxxxx> wrote:

"Any one of them may be executed" means that the next state may correspond to either action. If you want both actions to be executed then you should write Action1 /\ Action2. With a disjunction, you have a branching point with possible successors according to Action1 or Action2 (actually, an action need not determine a unique successor state, think of x' \in {"a", "b", "c"}). TLC will compute all successors that correspond to some enabled action and then continue from these, as I tried to explain previously.

TLC complains about incompletely specified successor states if it cannot determine a finite set of values for each of the primed state variables. For example, Action1 does not specify what values y may take in the successor state. According to the TLA+ semantics, it can have any value, including {}, -42, "foobar", [x \in Int |-> x*x] etc. There are uncountably many possible values, and TLC has no way of enumerating them all.

Regards,
Stephan

On 04 Aug 2014, at 13:35, Sidharth Kshatriya <sid.ks...@xxxxxxxxx> wrote:

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

--
Stephan Merz

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

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