Promela频道“？？”移除令
Promela channel "??" removal order
谁能给我解释一下下面发生的事情的顺序？
if
:: a_channel??5 -> // do A
:: value_1 == value_2 -> // do B
fi;
基本上我的理解是，要使语句可执行，5 需要在通道中。我知道 5 将因此从频道中删除（如果它确实在频道中）。我不明白的是什么时候 5 会被删除。 5 是在语句执行后删除还是在检查执行前删除。
Promela ref link 接收：http://spinroot.com/spin/Man/receive.html
假设 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.
"check for execution"是从频道中删除5的必要但不充分条件。另一个必要的条件是选择 P_i 执行并执行语句 a_channel??5.
更详细的回答。
声明a_channel??5是声明它并不总是可执行的。它是可执行的只有当5在频道中。 （例如如果5在频道中，但它已被删除[例如被其他人]，a_channel??5不再可执行）
每次进程 P_i 执行 原子（一组）指令后 ，调度程序可能会决定抢占它并允许一些其他进程 P_j 有一些 可执行 指令继续。
当进程 P_i 到达 不可执行的 语句时，它总是立即被调度程序抢占。在这种情况下，如果没有其他进程 P_j 有一些立即 可执行的 指令可以安排执行 （即著名的"invalid end state"错误).
如果语句 a_channel??5 是可执行的并且进程 P_i 被选择执行（或继续执行），则 a_channel??5 执行 原子地 并且它立即从通道中删除值 5 的 （第一次出现）。
谁能给我解释一下下面发生的事情的顺序？
if
:: a_channel??5 -> // do A
:: value_1 == value_2 -> // do B
fi;
基本上我的理解是，要使语句可执行，5 需要在通道中。我知道 5 将因此从频道中删除（如果它确实在频道中）。我不明白的是什么时候 5 会被删除。 5 是在语句执行后删除还是在检查执行前删除。
Promela ref link 接收：http://spinroot.com/spin/Man/receive.html
假设 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.
"check for execution"是从频道中删除5的必要但不充分条件。另一个必要的条件是选择 P_i 执行并执行语句 a_channel??5.
更详细的回答。
声明a_channel??5是声明它并不总是可执行的。它是可执行的只有当5在频道中。 （例如如果5在频道中，但它已被删除[例如被其他人]，a_channel??5不再可执行）
每次进程 P_i 执行 原子（一组）指令后 ，调度程序可能会决定抢占它并允许一些其他进程 P_j 有一些 可执行 指令继续。
当进程 P_i 到达 不可执行的 语句时，它总是立即被调度程序抢占。在这种情况下，如果没有其他进程 P_j 有一些立即 可执行的 指令可以安排执行 （即著名的"invalid end state"错误).
如果语句 a_channel??5 是可执行的并且进程 P_i 被选择执行（或继续执行），则 a_channel??5 执行 原子地 并且它立即从通道中删除值 5 的 （第一次出现）。