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

[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
   /\ 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:
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.