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

Re: [tlaplus] [Noob] Avoiding unnecessary variables



Hi,

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

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.