[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 <- queue1 Queue2 == 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 Sequences CONSTANTS Values, NoVal VARIABLES q Init == 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?