Промела канал "??"порядок удаления - PullRequest
Новая
       55

Промела канал "??"порядок удаления

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

Может ли кто-нибудь объяснить мне порядок того, что происходит в следующем случае? 

if
 :: a_channel??5 -> // do A
 :: value_1 == value_2 -> // do B
fi;

Так что, как я понимаю, для выполнения оператора 5 должно быть в канале. Я понимаю, что 5 будет удален из канала в результате (если он действительно находится в канале). Что я не понимаю, так это когда 5 будет удалено. Будет удалено 5 после выполнения инструкции или будет удалено ранее во время проверки выполнения.

Ссылка Promela ref для получения: http://spinroot.com/spin/Man/receive.html

1 Ответ

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

Предположим, a_channel??5 содержится в теле какого-либо процесса P_i.

Будет удалено 5 после выполнения инструкции или будет удалено ранее во время проверки выполнения.

«проверка выполнения» является необходимым, но недостаточным условием для удаления 5 из канала. Другое необходимое условие: P_i выбирается для выполнения и выполняет оператор a_channel??5.

Более подробный ответ.

Оператор a_channel??5 являетсяутверждение, что это не всегда исполняемый . исполняемый только , когда 5 находится в канале. ( например , если 5 было в канале, но оно было удалено [например, кем-то другим], a_channel??5 больше не может быть выполнено)

Послекаждый раз, когда процесс P_i выполняет атомарный (набор) инструкций , планировщик может решить прервать его и разрешить некоторому другому процессу P_j с некоторым исполняемым файлом инструкция для продолжения.

Когда процесс P_i достигает неисполнимого оператора , он всегда немедленно предшествует планировщику. В этом случае возникает ошибка, если нет другого процесса P_j с какой-либо немедленно исполняемой инструкцией, которую можно запланировать на выполнение (то есть известной ошибкой «недопустимое конечное состояние») .

Если оператор a_channel??5 является исполняемым и процесс P_i выбран для выполнения (или продолжает работу), то a_channel??5 выполняет атомно и немедленно удаляет (первое вхождение) значения 5 из канала.

...