Логическая оценка «Когда А и Б ...» - PullRequest
Новая
       53

Логическая оценка «Когда А и Б ...»

2 голосов
/ 24 октября 2019

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

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

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;

1 Ответ

1 голос
/ 24 октября 2019

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

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

ИМХО , лучшим вариантом будет 

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 может быть изменена каким-либо другим процессом. Я почти всегда использовал бы второй стиль, когда он может улучшить читаемость.

...