如何使用SPIN为过渡系统建模 [英] How to model a transition system with SPIN

问题描述

我是新手.我想检查过渡系统是否满足给定的LTL属性.但是我不知道如何在promela中为过渡系统建模. 例如，下面显示的转换系统具有两个状态，初始状态为s0. 如何检查是否满足LTL属性:<> q.有人知道如何在预言中描述这个问题吗?顺便问一下，如何在自旋中使用LTL的下一个运算符?

I am new to spin. I want to check whether a transition system satisfies the given LTL property. But I don't know how to model a transition system in promela. For example, the transition system shown below has two states, and the initial state is s0. How to check whether the LTL property: <>q is satisfied. Does anybody know how to describe this problem in promela? By the way, how to use the next operator of LTL in spin?

推荐答案

您可以使用标签，原子块和gotos对自动机建模:

You can model your automata by using labels, atomic blocks and gotos:

bool p, q;

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

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

要检查LTL属性，请将ltl eventually_q { <>q };放在文件末尾，然后使用-a运行Spin和生成的可执行文件.

To check your LTL property, place ltl eventually_q { <>q }; at the end of your file and run Spin and the generated executable with -a.

如果放置的属性不结尾，例如ltl always_p { []p };，则会收到消息end state in claim reached，表明该属性已被违反.

If you place a property that doesn't hold at the end, for example, ltl always_p { []p };, you'll get the message end state in claim reached that indicates that the property has been violated.

关于next-operator:它与Spin默认使用的部分降阶算法冲突.使用next-operator的属性必须是不变口吃，否则，必须禁用部分排序.在此手册页末尾了解更多信息.

About the next-operator: It is in conflict with the partial order reduction algorithm that Spin uses per default. Properties using the next-operator must be stutter invariant, otherwise, partial order reduction must be disabled. Read more at the end of this man page.

这篇关于如何使用SPIN为过渡系统建模的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！