A: if
:: q?a -> ...
:: else -> ...
fi
请注意，争用条件内置于此类代码中。多久 例如，在决定 消息接收操作将不可执行？问题可能是 通过使用消息轮询操作来避免，例如，如下所示：
以上引文来自 http://spinroot.com/spin/Man/else.html
我无法理解这种说法。只需旋转可以决定q?a： 如果q为空，则它是可执行的。否则，它将阻塞。
给定的论点提出了竞争条件。
但是，我可以提出相同的论点：
byte x = 1;
A: if
:: x == 2 -> ...
:: else -> ...
fi
从Spin的角度来看，这是可以的。但是，我要问的是，例如，在决定x的值不会被其他进程增加之前，该过程应该等待多长时间？
关于Promela的语义和选择结构，论证是合理的。请注意，对于选择，如果多个保护语句是可执行的，则将不确定地选择其中一个。这反过来又暗示了语义，使得选择(即使它可以不确定地执行守卫)需要在调用选择语句时确定哪些守卫是可执行的。
在考虑选择和消息接收的语义时，有关竞争条件的问题可能更有意义。请注意，在这种情况下，争用条件意味着选择的输出可能取决于它需要调用接收的时间(即它是否在通道中有消息的点完成)。 更具体地说，对于选择声明，在可行的守卫方面不应有歧义。现在，仅当通道不为空时，消息接收才会从通道获取消息(否则，它无法完成执行并等待)。因此，关于接收的语义，在实际执行之前不清楚它是否可执行。反过来，如果接收不可执行，则应执行else。但是，由于else只有在?不可执行时才应执行，因此要知道else是否可执行，程序需要知道未来(或确定它应该等待多少时间才能知道这一点，从而产生竞争条件)。
请注意，该参数不适用于您的第二个示例：
byte x = 1;
A: if
:: x == 2 -> ...
:: else -> ...
fi
因为在这里，要回答else是否有资格，不需要等待(也不知道未来)，因为程序可以随时确定是否x == 2。