# Re: [tlaplus] [Noob] Avoiding unnecessary variables

Hi. Thank you for the answer.

Yes, I am aware that this will merge the three actions into one atomic action. This is actually what I wanted but didn't know how to implement.

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?

On Wednesday, February 27, 2019 at 10:42:41 AM UTC+1, Stephan Merz wrote:
Hello,

you can merge the three actions into a single one, but you should be aware that doing so changes the semantics of your specification. With separate actions, you expose states in which a value has been popped from the first queue but not yet pushed to the second queue. When you combine them, the push and pop operations take place in a single atomic transition. Whether this difference matters for what you intend to specify is up to you to decide, but it should be a conscious decision.

If you decide to combine the actions, you'll want to eliminate variables state and tempVar, as you say. One way of doing that is to make the parameter of Pop a value instead of a variable

Pop(val) ==
/\ q' = Tail(q)

and rewrite your combined action, somewhat as follows

TransferMessage ==
/\ ~ Queue1!IsEmpty
/\ \E m \in Message :
/\ Queue1!Pop(m)
/\ LET newM == process(m)  \* do the processing
IN  Queue2!Push(newM)
/\ UNCHANGED ...

Breaking somewhat the encapsulation between your modules, you may even choose to eliminate the existential quantifier and write

TransferMessage ==
/\ ~ Queue1!IsEmpty
newM == process(m)
IN  /\ Queue1!Pop(m)
/\ Queue2!Push(newM)
/\ UNCHANGED ...

Regards,
Stephan

On 27 Feb 2019, at 10:16, Michael Chonewicz <wawrzync...@xxxxxxxxx> wrote:

Hello. I'm still learning TLA+ and i came across an issue. I have a specification with two queues. Messages get put in the first queue by a thread, then taken out of it by the second thread, processed and put into the second queue. The way i came up with for doing this is the following (what the second thread does):

VARIABLES queue1, queue2, tempVar, state...Queue1 == INSTANCE InnerQueue WITH Values <- Message, q <- queue1Queue2 == INSTANCE InnerQueue WITH Values <- Message, q <- queue2...FetchMessage ==    /\ ~Queue1!IsEmpty    /\ state = "Idle"    /\ Queue1!Pop(tempVar)    /\ state' = "Processing"    /\ UNCHANGED <<...>> \* other variables unchanged    ProcessMessage ==    /\ state = "Processing"    /\ \* Do the processing    /\ state' = "Finished"        /\ UNCHANGED <<>> \* other variables unchanged    Finish==    /\ state = "Finished"   /\ Queue2!Push(tempVar)     /\ state' = "Idle"    /\ UNCHANGED <<>> \* other variables unchanged    Actions ==    \/ FetchMessage    \/ ProcessMessage    \/ Finish

With InnerQueue being defined like this:
EXTENDS SequencesCONSTANTS Values, NoValVARIABLES qInit ==     q = << >>TypeInvariant ==    q \in Seq(Values)    Push(val) ==    /\ val /= NoVal    /\ q' = Append(q, val)    Pop(var) ==    /\ var' = Head(q)    /\ q' = Tail(q)    IsEmpty ==    q = << >>

My issue is that already with such a simple bare-bones model, it takes a long time to check. I have two ideas of making it simpler and faster but i don't quite know how to do it or if its even possible:
• Merge FetchMessage, Process and Finish into one Action (eliminating tempVar and state). I tried to do this, but I cannot do anything with the result from Pop from the first queue until next step. Same thing with the processed result, i cannot push it until the next state.
• Eliminate the variable tempVar from being a part of the state. The state of this variable is unimportant as its a temporary variable. The only reason i have it in the first place is because i somehow have to return a value from the Pop.
Can any of this be done? Or maybe my thinking about this the wrong way after years of "normal" programming?

--
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...@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.