[noob] Liveness property not violated as expected

[Michael Chonewicz]

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

[Jay Parlar]

On Monday, 1 April 2019 06:15:17 UTC-4, Michael Chonewicz wrote:

Spec ==
    /\ Init
    /\ LivenessSpec
    /\ [][Next]_variables 

There are generally two separate parts to liveness checking, and I think you might be conflating them.

First, you must specify appropriate fairness conditions (via WF_ and/or SF_). This determines which parts of your specification are fair, and the particular kind of fairness.

The second is specifying temporal properties that you want TLC to check. When you specify a temporal property, you add it to the "Properties" listing in the model checker. 

If you don't specify a temporal property, then TLC won't check for liveness, and thus you won't see any violations. 

Your second version of the code places a `~>` inside of `LivenessSpec`, which really throws me for a loop, and it's where I'm getting the idea that you might be conflating the two things. If you want LivenessSpec to have a `~>` in it, then don't add it as a conjunct to the `Spec`.

Jay P.

[Michael Chonewicz]

Thank you for your answer! 

I see. So if i understand this correctly, fairness conditions are not liveness properties that are checked for (which actually makes sense now that i think about it). So my LivenessSpec doesn't actually do any liveness checking. To do that, I have to add the actual liveness property (the second version of my LivenessSpec) to the model. But one question remains, whats wrong with my second version? I don't understand the error. How could i make the ReceiveMsg(msg) ~> ResultCallback(result) action into a temporal formula or a state predicate?

[Jay Parlar]

On Monday, 1 April 2019 16:44:51 UTC-4, Michael Chonewicz wrote:

I see. So if i understand this correctly, fairness conditions are not liveness properties that are checked for (which actually makes sense now that i think about it). So my LivenessSpec doesn't actually do any liveness checking. To do that, I have to add the actual liveness property (the second version of my LivenessSpec) to the model.

Yep!

 

But one question remains, whats wrong with my second version? I don't understand the error. How could i make the ReceiveMsg(msg) ~> ResultCallback(result) action into a temporal formula or a state predicate?

I can't say for certain, because you didn't include your entire original spec, but my guess is that either `ReceiveMsg` or `ResultCallback` are actions, i.e., they used primed variables. 

Jay P.

 

[Michael Chonewicz]

Ah, so thats what it was! Thank you. I have modified ReceiveMsg to look like this:

ReceiveCallback(msg) ==
    TRUE


ReceiveMsg(msg) ==
    /\ MsgQueue!Push(msg)
    /\ UNCHANGED <<proc1Queue, resultQueue>>
    /\ ReceiveCallback(msg)

And used ReceiveCallback in the liveness instead of ReceiveMsg:

LivenessSpec ==
    /\ \A msg \in Message :

        \E result \in ResultssForMsg(msg) :
            ReceiveCallback(msg) ~> ResultCallback(result)

The ResultCallback already looked like ReceiveCallback above. This fixed the compile issue. Then i removed the old LivenessSpec from my Spec completely(not even fairness is left):

Spec ==
    /\ Init
\*    /\ FairnessSpec
    /\ [][Next]_variables

and lastly added the LivenessSpec (the version with the leads-to operator) as a property of the model in TLC. My hopes were that the spec would crash this time. It did check the liveness, but unfortunately, still no crash. 

Could it be that during model checking, even though a message M is lost during the BrokenCallback step, M at some point will be put into the system again and processed correctly, leading to the liveness condition being satisfied in the end? Technically every message should be unique (ReceiveMsg is only called once for a message during the entire life of the system), but I'm not entirely sure if the model checker violates this rule.  

[Jay Parlar]

On Tuesday, 2 April 2019 05:50:36 UTC-4, Michael Chonewicz wrote:

Ah, so thats what it was! Thank you. I have modified ReceiveMsg to look like this:

ReceiveCallback(msg) ==
    TRUE


And used ReceiveCallback in the liveness instead of ReceiveMsg:

LivenessSpec ==
    /\ \A msg \in Message :
        \E result \in ResultssForMsg(msg) :
            ReceiveCallback(msg) ~> ResultCallback(result)

The ResultCallback already looked like ReceiveCallback above. This fixed the compile issue. Then i removed the old LivenessSpec from my Spec completely(not even fairness is left):

If I'm understanding correctly, you're saying that `ReceiveCallback` and `ResultCallback` are _both_ just equivalent to TRUE?

If that's the case, then the temporal property is trivially satisfied for every behaviour. It comes down to `TRUE -> TRUE`.

Or have I misunderstood?

Jay P.

[Michael Chonewicz]

Yes, they are both TRUE. My understanding was that ReceiveCallback(msg) ~> ResultCallback(result) assures that a call to the ReceiveCallback will eventually lead to ResultCallback. But it doesn't matter what i do with the message inside of these actions, so I just return TRUE. My thinking was that if ResultCallback never gets called, it cannot be TRUE, thus failing the liveness condition. 

This does seem sketchy now that you have pointed it out, but I dont really know what i could put in there, since the only purpose of those actions was to use them in the LivenessSpec. Maybe you know how else i could solve this?

[Stephan Merz]

Stepping back a bit, it appears to me that you'd like to check a property of the form

  A ~> B

where A and B are both actions. Such a formula is not syntactically well-formed in TLA (although it is indeed stuttering invariant). TLA allows such a formula to be written only if A and B are temporal formulas, including state predicates. You can work around this limitation by adding variables done_A and done_B that are initialized to FALSE and set to true whenever A and B happen. Then check the property

  done_A ~> done_B

(Since your actual actions take parameters the details are a bit more complicated and you may need to use functions but I think you get the idea.)

In practice, you won't actually need to introduce these helper variables because the system state probably already contains enough information to tell you when A and B occurred. The overall idea is to replace the actions by suitable state predicates.

Hope this helps,

Stephan

--
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...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Michael Chonewicz]

Yes, thank you, it does help. I think i can implement this, but i still have one doubt. 

As i mentioned before, technically, every Message is unique throughout the entire lifetime of the system. I dont know how to specify my model value messages like that. I suspect, that what might happen is for example: The system receives message m1, then looses it, which would violate the liveness property. But then after a while, TLC inputs m1 again, which this time is not lost, thus satisfying the liveness property in the end. Can i somehow prevent that from happening? Is that even an issue?

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.

[Stephan Merz]

You could keep a history of messages that the system has seen at some point and add a precondition to the message input action that requires the message not to be an element of that message history.

However, I speculate (without having seen your spec) that this is not necessary for what you are trying to verify: presumably there is no fairness condition for inputting a new message (since it would constrain the environment rather than the system that you are specifying), so the execution in which m1 is input and then lost (and in which m1 never reappears) is a valid counter-example that should be found by TLC.

Stephan

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.

[Michael Chonewicz]

Thank you, that makes perfect sense. My problem here was that i was confusing liveness properties and fairness, and that i didn't really understand how the ~> operator works. I thought of it as "left action being called leads to right action being called" instead of "the right condition being true leads to the left condition being true". Thanks a lot for the help! 

[Michael Chonewicz]

Actually, i have one tiny problem left, my fairness specification doesn't work, and my spec fails due to stuttering. The fairness spec is as simple as it can get:

variables == <<msgQueue, proc1Queue, resultQueue>>

FairnessSpec == WF_<<variables>>(Callback)\*Same Callback as in the code above

However, in the counterexample produced by TLC, Callback is never called. I am not entirely sure what the variables in weak fairness spec do, and i havent been able to find any information on it, but i have tried setting it to all the variables in the spec, just the variables modified by Callback and the variables not modified by Callback, all with the same result. What could be the issue? If its not visible to the naked eye i can provide the full specification.

Sorry for wasting your time with all these easy questions, i wish TLA+ was more popular on StackOverflow, its such an amazing tool!

[Stephan Merz]

This indicates that the action <<Callback>>_variables is not enabled at the state at which the counter-examples ends with stuttering. Please feel free to send me the spec off-line if you can't figure it out.

Regards,

Stephan

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.

[Michael Chonewicz]

With insightful help from Stephan Merz, I realized that the issues were:

• Not knowing what the subscript variables in fairness mean. WF_<<v1, v2>>(A) means that A /\ <<v1', v2'>> # <<v1, v2>> must happen if its forever enabled. This is particularly important when A contains UNCHANGED <<v1, v2>>, meaning that the action never changes these variables and fairness cannot be asserted. Its generally best to have all the variables in the underscore for fairness.
• Dismissing a completely different counter-example as a different version of the same one. In my specification I didn't set fairness of other actions, and confused that counter-example with the one originating from the first bullet point.

Big kudos to Stephan!