model-checking - 如何使用 SPIN 对转换系统进行建模

Question

我是新手。我想检查转换系统是否满足给定的 LTL 属性。但我不知道如何在 promela 中建模过渡系统。例如下图所示的转移系统有两种状态，初始状态为s0。如何检查LTL属性：<>q是否满足。有人知道如何在 promela 中描述这个问题吗？对了，spin中LTL的next算子怎么用？

Answer 1

您可以使用标签、原子块和 goto 为您的自动机建模：

bool p, q;

init
{  
  s1:
    atomic {
      p = true;
      q = false;
    }
    goto s2;

  s2:
    atomic {
      p = false;
      q = true;
    }
}

要检查您的 LTL 属性，请将ltl eventually_q { <>q };其放在文件末尾并运行 Spin 和生成的可执行文件-a。

如果您在末尾放置一个不成立的属性，例如 ，ltl always_p { []p };您将收到end state in claim reached指示该属性已被违反的消息。

关于 next-operator：它与 Spin 默认使用的偏序约简算法相冲突。使用 next-operator 的属性必须是stutter invariant，否则必须禁用部分降阶。在本手册页的末尾阅读更多内容。