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

[tlaplus] [noob] Liveness property not violated as expected



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

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