

Re: [tlaplus] [Noob] Avoiding unnecessary variables


I am a little bit confused as to how you pop the message from the queue. It looks like you are assigning m a value before popping (either with the existential quantifier or the Head operator). What does the Pop do then?

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


To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.