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