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

[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
   /\ state = "Finished"
\ Queue2!Push(tempVar)
    /\ state' = "Idle"
   /\ UNCHANGED <<>> \* other variables unchanged
Actions ==
   \/ FetchMessage
   \/ ProcessMessage
   \/ Finish

With InnerQueue being defined like this:
EXTENDS Sequences



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?

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.