Как интерпретировать вывод ошибки SPIN?

Я пытаюсь смоделировать проверку простой модели Promela для следующего свойства LTL:

ltl { M[0] U M[1] }

И я получаю сообщение об ошибке, управляемое моделирование по следу ошибки дает следующий результат:

ltl ltl_0: (M[0]) U (M[1])
spin: couldn't find claim 2 (ignored) 
0 :init ini M[0] = 1             
Process Statement                M[0]       M[1]       
0 :init ini M[1] = 0             1          0          
Starting net with pid 2
0 :init ini run net()            1          0          
spin: trail ends after 4 steps
#processes: 2
  4:    proc  1 (net) petri:11 (state 13)
  4:    proc  0 (:init:) petri:25 (state 5)
2 processes created
Exit-Status 0

Теперь я не вижу, где здесь нарушается «M [0] до M [1]». M[0] устанавливается в 1 в процессе инициализации и остается таковым до тех пор, пока M[1] не станет 1. И трассировка заканчивается так рано, или я, возможно, полностью неправильно понимаю семантику «stronguntil». Я совершенно уверен, что это так... но что я делаю не так? Можно ли указать LTL в файле Promela?

Речь идет о следующей модели (простая сеть Петри):

#define nPlaces 2
#define nTransitions 2
#define inp1(x1) (x1>0) -> x1--
#define out1(x1) x1++

int M[nPlaces];
int T[nTransitions];

proctype net()
{
    do
    ::  d_step{inp1(M[0])->T[0]++;out1(M[1]);skip}
    ::  d_step{inp1(M[1])->T[1]++;out1(M[0]);skip}
    od
}
init
{
    atomic 
    {
        M[0] = 1;
        M[1] = 0;
    }
    run net();
}

ltl { M[0] U M[1] }

formal-verification promela spin model-checking
person user1101674    schedule 10.06.2013    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Ваше требование нарушено в исходном состоянии (до init использования atomic). Вот прогон проверки SPIN (pan -a) с выводом из файла следа:

ebg@ebg$ spin -a foo.pml
ltl ltl_0: (M[0]) U (M[1])
ebg@ebg$ gcc -o pan pan.c
ebg@ebg$ ./pan -a
pan:1: assertion violated  !(( !(M[0])&& !(M[1]))) (at depth 0)
pan: wrote foo.pml.trail

(Spin Version 6.2.4 -- 21 November 2012)
Warning: Search not completed
    + Partial Order Reduction

Full statespace search for:
    never claim             + (ltl_0)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 36 byte, depth reached 6, errors: 1
        4 states, stored (7 visited)
        1 states, matched
        8 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000   equivalent memory usage for states (stored*(State-vector + overhead))
    0.290   actual memory usage for states
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  128.730   total actual memory usage



pan: elapsed time 0 seconds
ebg@ebg$ spin -p -t foo.pml
ltl ltl_0: (M[0]) U (M[1])
starting claim 2
using statement merging
spin: _spin_nvr.tmp:5, Error: assertion violated
spin: text of failed assertion: assert(!((!(M[0])&&!(M[1]))))
Never claim moves to line 5 [D_STEP]
spin: trail ends after 1 steps
#processes: 1
        M[0] = 0
        M[1] = 0
        T[0] = 0
        T[1] = 0
  1:    proc  0 (:init:) foo.pml:18 (state 3)
  1:    proc  - (ltl_0) _spin_nvr.tmp:3 (state 6)
1 processes created

вы можете видеть, что ltl было переведено на: assert(!(( !(M[0])&& !(M[1])))), что означает:

  !(( !0 && !0))
  !((  1 &&  1))
  !((  1 ))
  0

и, таким образом, утверждение нарушается.

Самый простой способ избежать этой проблемы — изменить массивы на отдельные переменные. Поскольку ваши массивы имеют размер 2, это легко сделать:

int M0 = 1;
int M1 = 0;
int T0 = 0;
int T1 = 0;
/* then use as appropriate. */

При этом вы можете пропустить init и просто сделать net proctype объявленным как active proctype net ()

person GoZoner    schedule 18.06.2013
comment
Спасибо! Итак, как мне объявить действительно начальные значения? C-стиль? - person user1101674; 18.06.2013
comment
Вы имеете в виду... как я могу настроить начальное состояние, чтобы удовлетворить ltl? - person GoZoner; 18.06.2013
comment
Точно. Или лучше изменить LTL? - person user1101674; 19.06.2013

arrow_upward
1
arrow_downward

Ваша формула ltl помещается нормально. Если вы используете ispin и проверяете (не имитируете) свою программу, убедитесь, что выбрана опция «использовать утверждение». Предупреждение. По умолчанию установлено значение «не использовать никогда не заявлять или свойство ltl».

person Mackie    schedule 17.06.2013
comment
Спасибо за подсказку! Похоже, я делаю что-то не так. Но я не могу найти никакой информации о том, как установить эту опцию. Я использую jSpin (code.google.com/p/jspin), но команда параметры линии должны быть одинаковыми. - person user1101674; 18.06.2013