1 
A: if
   :: q?a -> ...
   :: else -> ...
   fi

请注意，这种类型的代码内置了竞争条件。例如，在决定消息接收操作将不可执行之前，该进程应该等待多长时间？可以通过使用消息轮询操作来避免该问题，例如，如下所示：

以上引用来自http://spinroot.com/spin/Man/else.html

我无法理解这种论点。只是 Spin 可以决定q?a：如果q是空的，那么它是可执行的。否则，它正在阻塞。

给定的参数引发了竞争条件。

但是，我可以提出同样的论点：

byte x = 1;
A: if 
   :: x == 2 -> ...
   :: else -> ...
   fi

从 Spin 的角度来看，这没问题。但是，我在问，例如，在决定 的值x不会被其他进程增加之前，该进程应该等待多长时间？

4

1 回答 1

1

关于 Promela 的语义和选择结构的论证是合理的。请注意，对于选择，如果可以执行多个保护语句，则将不确定地选择其中一个。这反过来意味着语义选择（即使它可以非确定性地执行保护）需要确定在调用选择语句时哪些保护是可执行的。

在考虑选择和消息接收的语义时，关于竞态条件的问题可能更有意义。请注意，这种情况下的竞争条件意味着选择的输出可能取决于它需要调用接收的时间（即它是否在通道中存在消息的点完成）。更具体地说，对于选择语句，在可行守卫方面不应有歧义。现在，消息接收只有在通道不为空时才从通道中获取消息（否则，它无法完成执行并等待）。因此，关于receive的语义，在实际执行之前是否可以执行是不清楚的。反过来，else如果接收不可执行，则应该执行。然而，由于else仅当不可执行时才应执行?，因此要知道程序是否else可执行，程序需要知道未来（或确定它应该等待多长时间才能知道这一点，从而引发竞争条件）。

请注意，该参数不适用于您的第二个示例：

byte x = 1;
A: if 
   :: x == 2 -> ...
   :: else -> ...
   fi

从这里开始，回答是否else符合条件不需要等待（也不知道未来），因为程序可以在任何时候确定是否x == 2。

于 2017-03-28T03:54:57.017 回答