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

Re: [tlaplus] [Noob] Avoiding unnecessary variables



Hello,

you can merge the three actions into a single one, but you should be aware that doing so changes the semantics of your specification. With separate actions, you expose states in which a value has been popped from the first queue but not yet pushed to the second queue. When you combine them, the push and pop operations take place in a single atomic transition. Whether this difference matters for what you intend to specify is up to you to decide, but it should be a conscious decision.

If you decide to combine the actions, you'll want to eliminate variables state and tempVar, as you say. One way of doing that is to make the parameter of Pop a value instead of a variable

Pop(val) ==
  /\ val = Head(q)
  /\ q' = Tail(q)

and rewrite your combined action, somewhat as follows

TransferMessage == 
  /\ ~ Queue1!IsEmpty
  /\ \E m \in Message :
        /\ Queue1!Pop(m)
        /\ LET newM == process(m)  \* do the processing
           IN  Queue2!Push(newM)
  /\ UNCHANGED ...
  
Breaking somewhat the encapsulation between your modules, you may even choose to eliminate the existential quantifier and write

TransferMessage == 
  /\ ~ Queue1!IsEmpty
  /\ LET m == Head(queue1)
         newM == process(m)
     IN  /\ Queue1!Pop(m)
         /\ Queue2!Push(newM)
  /\ UNCHANGED ...


Regards,
Stephan


On 27 Feb 2019, at 10:16, Michael Chonewicz <wawrzynchonewicz@xxxxxxxxx> 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?

--
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.

--
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.