[tlaplus] [Noob] Avoiding unnecessary variables

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?