Проверка модели LTL с помощью SPIN

Чтобы сгенерировать автомат Бючи из формулы LTL, вы можете использовать ltl2ba инструмент. Инструмент может предоставить графическое представление автомата Buchi или его кодовую версию Promela, как в следующем примере:

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

Вы также можете использовать Spin для создания Promela версии Buchi Automaton с помощью команды:

~$ spin -f "LTL_FORMULA"

например:

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

Однако, в отличие от ltl2ba, Spin не упрощает автомат Бучи при создании исходного кода, что иногда затрудняет интерпретацию его вывода; например, попробуйте запустить spin -f "([] q0) && (<> ! q0)" и сравните автомат вывода с тем, который получен с помощью ltl2ba.

ИЗМЕНИТЬ

Теперь вы можете использовать gltl2ba в сочинении для ltl2ba веб-сайт, например:

~$ 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
}