Hello. I am still learning TLA+ and I'm now playing with liveness properties. I have a system in which Messages come in, are put in a queue(1), then taken out of the queue(msgQueue) and processed for the first time(2), and put in another queue(Proc1Queue). Then, the result of the processing is taken out of the queue, processed again(3) and put in another queue(resultQueue). Finally, the result is taken out of the resultQueue, and passed to an action ResultCallback(4). Here are the relevant parts:
Process ==
/\ ~MsgQueue!IsEmpty
/\ \E m \in Message :
/\ MsgQueue!Pop(m)
/\ LET processedMsg == m \*For now nothing to process
IN Proc1Queue!Push(processedMsg)
/\ UNCHANGED <<resultQueue>>
Process2 ==
/\ ~Proc1Queue!IsEmpty
/\ \E m \in Message :
/\ Proc1Queue!Pop(m)
/\ LET possibleResults == ResultsForMsg(m)
IN \E result \in possibleResults : ResultQueue!Push(result)
/\ UNCHANGED <<msgQueue>>
Callback ==
/\ ~ResultQueue!IsEmpty
/\ \E m \in Message :
\E result \in ResultsForMsg(m) :
/\ ResultQueue!Pop(result)
/\ ResultCallback(result)
/\ UNCHANGED <<msgQueue, proc1Queue>>
BrokenCallback ==
/\ ~ResultQueue!IsEmpty
/\ \E m \in Message :
\E result \in ResultsForMsg(m) :
/\ ResultQueue!Pop(result)
/\ UNCHANGED <<msgQueue, proc1Queue>>
Next ==
\/ \E msg \in Message : ReceiveMsg(msg) \* 1
\/ Process \* 2
\/ Process2 \* 3
\/ Callback \* 4
\/ BrokenCallback
LivenessSpec ==
/\ \A msg \in Message :
\E result \in ResultsForMsg(msg) :
WF_<<variables>>(ResultCallback(result))
Spec ==
/\ Init
/\ LivenessSpec
/\ [][Next]_variables
I tried adding the liveness property to assure that for every message that comes in, ResultCallback gets called for it, with whatever Result( ResultsForMsg just generates a set of all possible results). Then i added the BrokenCallback action, which consumes a message, but does not call the callback- which should violate the liveness property. But it doesn't. There is no difference during model checking.
I have also tried specifying my liveness property like this:
LivenessSpec ==
/\ \A msg \in Message :
\E result \in ResultsForMsg(msg) :
ReceiveMsg(msg) ~> ResultCallback(result)
but this doesn't work for some reason that I dont understand. The error says "Action used where only temporal formula or state predicate allowed". How could i turn
ReceiveMsg(msg) ~> ResultCallback(result)
into a formula or state predicate? If its not possible, then what am I doing wrong in the first liveness specification?
For the model checking, i set the messages to be a model value set (not symmetric).