Promela频道“？”移除令

Question

有人能向我解释一下下面发生的事情的顺序吗？

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

所以，基本上，我理解的是，要使语句可执行，5需要在通道中。据我所知，5会因此而从通道中移除(如果它确实在通道中)。我不明白的是，5点将被移除。将在语句执行后删除5，还是在执行检查期间删除该语句。

用于接收的Promela参考链接：http://spinroot.com/spin/Man/receive.html

Answer 1

假设a_channel??5包含在某个进程P_i的主体中。

将在语句执行后删除5，或者在执行检查期间删除它。

“检查执行”是将5从通道中移除的必要条件，但不是充分条件。另一个必要条件是选择执行P_i并执行a_channel??5语句。

一个更详细的答案。

语句a_channel??5是一条语句，它是，并不总是可执行的。当 5在通道中时，它仅可执行5。(__，例如，如果5在通道中，则为，但它已被删除，例如被其他人删除，a_channel??5不再是可执行的)

每次进程P_i执行原子(一组)后，调度程序可能会决定抢占它，并允许具有一些可执行指令的其他进程P_j继续执行。

当进程P_i到达非可执行语句时，调度程序总是会立即抢占它。在这种情况下，如果没有其他进程P_j和一些可以调度执行的立即可执行指令(即著名的“无效结束状态”错误)，则为错误条件。

如果语句a_channel??5是可执行的，而process P_i被选择执行(或继续执行)，那么a_channel??5将原子化地执行，并且它会立即从通道中删除值5的(第一次出现)。