LTL model checking with SPIN

Question

I am looking at the SPIN software. I would like to do use it to find models of LTL theories. All the manuals and tutorials talk about verifying properties of algorithms, but I am not interested in that at all. I simply want to find a models of LTL formulas (a corresponding Büchi automaton, I suppose), much like the mace4 or paradox model checkers can find models of FOL formulas. I believe that SPIN should be able to do that, but I am unable to find how in the documentation. Could somebody point to any helpful resources?

Answer 1

In order to generate a Buchi automaton from an LTL formula you can use the ltl2ba tool. The tool can provide a graphical representation of the Buchi automaton or a Promela code version of it, as in the following example:

~$ ./ltl2ba -f "([] q0) && (<> ! q0)"
never {    /* ([] q0) && (<> ! q0) */
T0_init:
    false;
}

---

You may also use Spin to generate the Promela version of the Buchi Automaton, with the command:

~$ spin -f "LTL_FORMULA"

e.g.:

~$ spin -f "[] (q1 -> ! q0)" 
never  {    /* [] (q1 -> ! q0) */
accept_init:
T0_init:
    do
    :: (((! ((q0))) || (! ((q1))))) -> goto T0_init
    od;
}

However, in contrast with ltl2ba, Spin does not seem to simplify the Buchi Automaton when generating the source code, making sometimes difficult to interpret its output; e.g. try running spin -f "([] q0) && (<> ! q0)" and compare the output automaton to that obtained with ltl2ba.

---

EDIT

You can now use gltl2ba in sostitution for ltl2ba's website, e.g.:

~$ gltl2ba.py -f "([] p0) || (<> p1)" -g

never { /* ([] p0) || (<> p1) */
T0_init:
    if
    :: (1) -> goto T0_S1
    :: (p1) -> goto accept_all
    :: (p0) -> goto accept_S2
    fi;
T0_S1:
    if
    :: (1) -> goto T0_S1
    :: (p1) -> goto accept_all
    fi;
accept_S2:
    if
    :: (p0) -> goto accept_S2
    fi;
accept_all:
    skip
}

generates the following graph: