# [tlaplus] Re: [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 it 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:16:58 AM UTC+1, Michael Chonewicz 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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.