谁能向我解释以下发生的顺序？
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
【问题讨论】：
标签： model-checking promela spin
假设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。
【讨论】：
5的移除需要a_channel??5的执行。根据 branching 语义，执行 guard 之后会执行其主体 // do A。因此，如果进程P_i 选择了守卫a_channel??5，那么它既不能执行value_1 == value_2 也不能执行// do B，除非if 语句 包含在某个循环 中并且下次它到达同一个分支时，它会做出不同的选择。
a_channel??5 更简单的例子是看看当另一个具有副作用的表达式用作保护时会发生什么，例如x = x + 1。您是否希望 x 即使在其分支未被采用时也会增加？当然不是！作为练习，您可以使用 LTL 模型检查来正式验证这一点。