model-checking - Promela channel "??"删除命令

Question

谁能给我解释一下下面发生的事情的顺序？

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

所以基本上我的理解是，要使语句可执行，5 需要在 channel 中。我知道 5 将因此从 channel 中删除(如果它确实在 channel 中)。我不明白的是什么时候 5 会被删除。 5 是在语句执行后被移除还是在检查执行前被移除。

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

Answer 1

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

Will 5 be removed after the statement is executed or will it be removed before during the check for execution.

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

---

更详细的答案。

声明 a_channel??5 声明它并不总是可执行。它可执行仅当 5 在 channel 中时。 (例如如果 5 在 channel 中，但它已被移除 [例如被其他人]，a_channel??5 是不再可执行)

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

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

如果语句 a_channel??5 是可执行的并且进程 P_i 被选择执行(或继续执行)，则 a_channel??5 原子地 执行，并立即从 channel 中删除值5 的(第一次出现)。