PROMELA 中的 skip 和 break 到底有什么区别？答案

【问题标题】：What exactly is the difference between skip and break in PROMELA?PROMELA 中的 skip 和 break 到底有什么区别？
【发布时间】：2019-05-04 13:23:12
【问题描述】：

假设我有这段 PROMELA 代码

active proctype A(){

   do
      :: !x -> break
      :: else -> skip
   od

   … //more code
}

break 和 skip 在这种情况下究竟做了什么？ break 是否打破了整个过程 A() 以便不会到达“更多代码”或只是循环？

【问题讨论】：

@AIqbalRaj 如果我不是真的需要帮助，我为什么要处理整个登录过程？那里有信息，但我还不清楚……所以我希望有人能用简单的语言向我解释。像你这样的评论并没有真正帮助任何人。
我也对答案感兴趣。

标签： model promela spin

【解决方案1】：

TLDR：

break：一个（始终可执行的）指令，它使执行跳转到包含它的最内层循环的末尾。这种类型的指令几乎适用于任何编程语言。
skip：没有效果的空（始终可执行）指令。有很多来自其他语言的no-op示例，例如python 中的pass、C 中的;（和其他）、jQuery 中的jQuery.noop() 等。

active proctype A(){

   do
      :: !x -> break
      :: else -> skip
   od

   … //more code
}

在这种情况下，一旦x 变为假，break 就会强制循环终止，而skip 只是一个空指令，明确表示在另一种情况下循环什么都不做。

来自the docs of break

姓名

break - 跳到最里面的 do 循环的末尾。

[...]

示例
L1: do
    :: t1 -> t2
    :: t3 -> break
    :: break
    od;
L2: ...
在本例中，控制在语句 t2 执行后立即到达标签 L1。控制也可以在语句 t3 执行后立即到达标签 L2，并且可选地，在一个执行步骤中，控制也可以从标签 L1 移动到标签 L2。

来自the docs of skip

姓名

skip - 一个虚拟的 nil 语句的简写。

[...]

示例
proctype A()
{
L0:   if
      :: cond1 -> goto L1 /* jump to end */
      :: else -> skip     /* skip redundant */
      fi;
      ...

L1:   skip
}
在这个例子中，标签 L1 后面的 skip 语句是必需的。在上面的选择结构中，在 else 保护之后使用 skip 语句是多余的。上面的选择可以更简洁地写成：
L0:   if 
      :: cond1 -> goto L1
      :: else
      fi;
因为 Promela 是一种异步语言，所以从不需要跳过也不会有效地在流程执行中引入延迟。在 Promela 中，根据定义，proctype 主体中任何两个后续语句执行之间总是可能存在任意且不可知的延迟。这种语义对应于并发系统设计的黄金法则，它禁止假设并发系统中异步进程的相对执行速度。

【讨论】：