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
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+u...@googlegroups.com.
To post to this group, send email to
tla...@xxxxxxxxxxxxxxxx.
Visit this group at
https://groups.google.com/group/tlaplus.
For more options, visit
https://groups.google.com/d/optout.