How to model a transition system with SPIN

Question

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?

Answer 1

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;
    }
}

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.

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.

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.