Логическая оценка когда A и B

Учитывая утверждение "Когда CM бездействует и получает запрос на обновление от WCP, он устанавливает ....". Некоторый контекст: в канале может быть только один тип сообщения, т. е. он будет содержать только запросы на обновление от wcp.

Я могу думать о двух возможных реализациях. Тем не менее, я не слишком уверен, что это правильный путь.

1-й способ:

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

2-й способ

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

promela spin model-checking
person Rajdeep    schedule 24.10.2019    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Два примера немного отличаются.

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

Здесь вы обязуетесь прочитать сообщение, если ваше состояние idle и канал wcpOut не пуст. Однако что произойдет, если процесс будет вытеснен сразу после оценки nempty(wcpOut), и сообщение будет прочитано кем-то другим? В этом случае процесс может быть заблокирован.

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

Здесь вы обязуетесь прочитать сообщение, когда состояние idle, поэтому вы не можете реагировать на изменение состояния до тех пор, пока сообщение не будет прочитано.

Я бы не стал использовать ни тот, ни другой подход, за исключением простых примеров.

Недостаток первого метода в том, что он не выполняет две операции атомарно. Недостаток второго метода заключается в том, что он затрудняет расширение поведения вашего контроллера в режиме ожидания state путем добавления дополнительных условий. (Например, вы получите " сомнительное использование 'else' в сочетании с сообщением об ошибке ввода-вывода, если вы попытались добавить ветку else).

ИМХО, лучший вариант

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

od;

Вместо этого, если вы хотите использовать фильтрацию сообщений, вы можно использовать опрос сообщений:

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

Решите ли вы объединить эти условия с CM_STATUS == IDLE или предпочтете использовать вложенный подход, полностью зависит от вас, если только у вас нет оснований полагать, что переменная CM_STATUS может быть изменена каким-либо другим процессом. Я бы почти всегда использовал второй стиль, когда он может улучшить читаемость.

person Patrick Trentin    schedule 24.10.2019