Hi,
Don't think too procedurally: TLA+ is a logic, and an action is a constraint on pairs of states. There is no notion of temporal order ("before" or "after") inside an atomic transition. In your original specification, you used a state variable for storing the value popped from the queue. If you want to get rid of that state variable, you'll typically introduce a bound (logical) variable using an existential quantifier (as in my first suggestion) or a LET (as in the second one). In contrast, the current content of the queue is part of the system configuration and is therefore represented by a state variable q. Transitions involving the Pop operation must respect the constraint that the value of q after the transition (q') equals the tail of the value before the transition (q), which procedurally corresponds to an assignment q := Tail(q). Stephan 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+unsubscribe@xxxxxxxxxxxxxxxx. To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout. |