Какие шаги для проверки LTL с помощью инструмента SPIN?

Question

Какие шаги для проверки LTL с помощью инструмента SPIN?

Я написал модель в Spin. Я хочу проверить некоторые LTL на модели. например:

ltl L1 {<>[]Working}

в окне проверки я выбираю опцию "использовать заявку" и нажимаю "выполнить":

ltl L1: <> ([] (Working))
gcc -DMEMLIM=1024 -O2 -DXUSAFE -w -o pan pan.c

на данный момент я понятия не имею, что делать дальше...? Я пытался найти ответ с Google, но нет никаких руководств, как использовать Spin....

4

promela spin

Источник

user2015221 20 июн '13 в 07:03

2 ответа

Другие вопросы по тегам promela spin

user491216 20 июн '13 в 09:01 2013-06-20 09:01 · Answer 1 · 2013-06-20 09:01

Сохраните вашу модель, включая ltl-блок в foo.pml
spin -a foo.pml
gcc -o foo.exe pan.c (Windows)
foo.exe -a

Запуск исполняемого файла с -a является ключом, иначе свойство LTL проверяться не будет.

3

Источник

user491216 20 июн '13 в 09:01

user1286639 20 июн '13 в 16:37 2013-06-20 16:37 · Answer 2 · 2013-06-20 16:37

В окне "Проверка" после нажатия "Выполнить" должен быть результат проверки. Это выглядит так (например):

verification result:
spin -a  foo.pml
ltl ltl_0: [] (foo)
gcc -DMEMLIM=1024 -O2 -DXUSAFE -o pan pan.c
./pan -m10000  -a -c1
Pid: 21462

(Spin Version 6.2.4 -- 21 November 2012)
    + Partial Order Reduction
...

pan: elapsed time 0 seconds
No errors found -- did you verify all claims?

Вы не видите ничего из этого? Или вы видите что-то, но не можете это интерпретировать?