[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <Stepha...@xxxxxxxxx>*Date*: Mon, 4 Aug 2014 13:52:59 +0200*References*: <85eb0aeb-0599-4dbe-8e3a-ac60d793ba94@googlegroups.com> <2d936027-2c40-4152-b58b-f94ac257148d@googlegroups.com> <e411f0d1-5396-4bf6-8cc0-ab5ba295ae19@googlegroups.com> <855e9493-9cbc-4584-9020-507facfb92b6@googlegroups.com>

"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

**Follow-Ups**:**Re: [tlaplus] Execution semantics of \/***From:*Sidharth Kshatriya

**References**:**Execution semantics of \/***From:*Sidharth Kshatriya

**Re: Execution semantics of \/***From:*Stephan Merz

**Re: Execution semantics of \/***From:*Sidharth Kshatriya

**Re: Execution semantics of \/***From:*Sidharth Kshatriya

- Prev by Date:
**Re: Execution semantics of \/** - Next by Date:
**Re: [tlaplus] Execution semantics of \/** - Previous by thread:
**Re: Execution semantics of \/** - Next by thread:
**Re: [tlaplus] Execution semantics of \/** - Index(es):