model-checkingpromelaspin

Logical evaluation of "When A and B ... "

Given a statement "When the CM is idle and receives update request from the WCP, it will set ....". Some context: there can only be one type of msg in the channel i.e. it will only contain update requests from wcp.

I can think of 2 possible implementations. However, I'm not too sure as to which is the correct way.

1st Way:

    do
    :: CM_STATUS == IDLE && nempty(wcpOut) -> // remove msg from channel and set something;
    od;

2nd Way

    mtype receivedMessage;
    do
    :: CM_STATUS == IDLE -> 
        if
        :: wcpOut?receivedMessage -> // set something;
        fi;
    od;
Solution

  • The two examples are slighly different.

    do
    :: CM_STATUS == IDLE && nempty(wcpOut) -> // read msg
od;

    Here, you commit to reading the message if your state is idle and the channel wcpOut is not empty. However, what happens if the process is preempted right aver the evaluation of nempty(wcpOut), and the message is read by someone else? In that case, the process could end up being blocked.

    mtype receivedMessage;
do
:: CM_STATUS == IDLE -> 
    if
    :: wcpOut?receivedMessage -> // set something;
    fi;
od;

    Here, you commit to read a message when the state idle, so you are unable to react to a state change up until when the message is read.

    I wouldn't use either approach, except for simple examples.

    The flaw of the first method is that it does not perform the two operations atomically. The flaw of the second method is that it makes it hard to extend the behavior of your controller in the idle state by adding more conditions. (For instance, you would get the "dubious use of 'else' combined with i/o" error message if you tried to add an else branch).

    IMHO, a better option is

    do
    :: atomic{ nempty(my_channel) -> my_channel?receiveMessage; } ->
        ...
    :: empty(my_channel) -> // do something else

od;

    Instead, when you want to use message filtering, you can use message polling:

    do
    :: atomic{ my_channel?[MESSAGE_TYPE] -> my_channel?MESSAGE_TYPE } ->
        ...
    :: else -> // do something else
od;

    Whether or not you choose to join these conditions with CM_STATUS == IDLE, or you prefer to use the nested approach, is entirely up to you, unless you have reasons to believe that the CM_STATUS variable can be changed by some other process. I would almost always use the second style when it can improve readability.