关于Promela通道接收操作元素移除时机的技术问询

我来给你掰扯清楚这段Promela代码的执行逻辑，尤其是你关心的通道元素5的移除时机问题——这确实是Promela里容易踩坑的细节。

首先先拆解这段代码的核心结构：这是一个非确定性选择的if语句，包含两个分支：

• 第一个分支：a_channel??5 -> // do A，这是带值匹配的通道接收操作，只有当通道a_channel的队首元素恰好是5时，这个分支才具备可执行资格；
• 第二个分支：value_1 == value_2 -> // do B，这是普通的布尔条件判断，只要等式成立，分支就可选。

接下来重点说执行顺序和你最关心的移除时机：
Promela的if语句执行分两个关键阶段，通道元素的移除是在第一阶段就完成的，不是等分支代码执行完：

1. 可执行性检查阶段
   Spin会同时评估所有分支的可执行条件：

   • 对于第二个分支，就是简单判断value_1和value_2是否相等，这个过程没有任何副作用，不会修改任何变量或通道；
   • 对于第一个分支的a_channel??5，这个匹配检查是原子性的操作：一旦Spin检测到a_channel的队首元素是5，会立刻把这个5从通道中移除，同时标记这个分支为“可执行”；如果队首不是5，这个分支就直接被排除。

2. 分支选择与执行阶段
   当所有分支的可执行性检查完成后，Spin会从所有标记为“可执行”的分支里随机选一个执行（这就是Promela的非确定性特性）：

   • 如果选中第一个分支，就执行// do A里的代码；
   • 如果选中第二个分支，就执行// do B里的代码。

这里有个很容易误解的点：如果两个分支都具备可执行性（比如通道队首是5，同时value_1 == value_2成立），哪怕最后Spin选了第二个分支去执行do B，那个5也已经在检查阶段被移除了——不会因为没走第一个分支就留在通道里。

举个直观的例子：假设a_channel初始内容是[5, 3]，且value_1等于value_2。进入if语句后，Spin检查第一个分支时会立刻把5从通道里删掉，通道变成[3]；然后Spin可以随机选do A或者do B，不管选哪个，5都已经不在通道里了。

内容的提问来源于stack exchange，提问作者Rajdeep