Promela SPIN недоступен из-за ошибки proctype

Я новичок в SPIN и Promela, и я столкнулся с этой ошибкой, когда пытался проверить свойство живости в своих моделях.

Код ошибки:

unreached in proctype P
        (0 of 29 states)
unreached in proctype monitor
        mutex_assert.pml:39, state 1, "assert(!((mutex>1)))"
        mutex_assert.pml:42, state 2, "-end-"
        (2 of 2 states)
unreached in init
        (0 of 3 states)
unreached in claim ltl_0
        _spin_nvr.tmp:10, state 13, "-end-"
        (1 of 13 states)

pan: elapsed time 0 seconds

Код в основном представляет собой реализацию алгоритма Петерсона, и я проверил его на безопасность, и он кажется действительным. Но всякий раз, когда я пытаюсь проверить свойство живучести с помощью ltl {[]((wait -> ‹> (cs)))}, возникают указанные выше ошибки. Я не уверен, что они имеют в виду, поэтому я не знаю, как действовать дальше...

Мой код выглядит следующим образом:

#define N 3
#define wait   (P[1]@WAIT)
#define cs     (P[1]@CRITICAL)

int pos[N]; 
int step[N]; 
int enter;
byte mutex;
ltl {[]((wait -> <> (cs)))}

proctype P(int i) {
  int t;
  int k;
  WAIT:
  for (t : 1 .. (N-1)){
  pos[i] = t
  step[t] = i
  k = 0;
  do
  ::  atomic {(k != i && k < N && (pos[k] < t|| step[t] != i)) -> k++}
  ::  atomic {k == i -> k++}
  ::  atomic {k == N -> break}
  od;
  }

CRITICAL:
  atomic {mutex++;
  printf("MSC: P(%d) HAS ENTERED THE CRITICAL SECTION.\n", i);
  mutex--;}
  pos[i] = 0;
}

init {
  atomic { run P(0); }
}

cygwin promela spin mutual-exclusion model-checking
person firearian    schedule 11.10.2016    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Общий ответ

Это предупреждение о том, что некоторые состояния недоступны из-за переходов, которые никогда не выполнялись.

Как правило, это не ошибка, но рекомендуется тщательно проверять недостижимые состояния для каждого подпрограмму, которую вы смоделировали, и убедитесь, что ни одна из них не будет достижима. т.е. в случае, если модель неверна. предполагаемое поведение.

Примечание. Вы можете использовать метку end: перед определенной строкой кода, чтобы отметить действительные завершающие состояния, чтобы избавиться от этих предупреждений, например, когда ваша процедура не завершается. Подробнее здесь.

Конкретный ответ

Я не могу воспроизвести ваш вывод. В частности, запустив

~$ spin -a file.pml
~$ gcc pan.c
~$ ./a.out -a

Я получаю следующий вывод, который отличается от вашего:

(Spin Version 6.4.3 -- 16 December 2014)
    + 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 64 byte, depth reached 47, errors: 0
       41 states, stored (58 visited)
       18 states, matched
       76 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.004   equivalent memory usage for states (stored*(State-vector + overhead))
    0.288   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


unreached in proctype P
    (0 of 29 states)
unreached in init
    (0 of 3 states)
unreached in claim ltl_0
    _spin_nvr.tmp:10, state 13, "-end-"
    (1 of 13 states)

pan: elapsed time 0 seconds

В частности, мне не хватает предупреждений о недостигнутых состояниях в процессе monitor. Насколько я понимаю, судя по исходному коду, ни одно из полученных предупреждений не является проблематичным.

Либо вы используете версию Spin, отличную от моей, либо вы не включили в свой вопрос полный исходный код. В последнем случае не могли бы вы отредактировать свой вопрос и добавить код? Я обновлю свой ответ позже.

РЕДАКТИРОВАТЬ: в комментариях вы спрашиваете, что означает следующее сообщение: "недостигнуто требование ltl_0 _spin_nvr.tmp:10, состояние 13, "-end-"".

Если вы откроете файл _spin_nvr.tmp, вы увидите следующий фрагмент кода Promela, который соответствует автомату Бюхи, который принимает все и только выполнение, которое нарушает ваше свойство ltl []((wait -> ‹> (cs))).

never ltl_0 {    /* !([] ((! ((P[1]@WAIT))) || (<> ((P[1]@CRITICAL))))) */
T0_init:
    do
    :: (! ((! ((P[1]@WAIT)))) && ! (((P[1]@CRITICAL)))) -> goto accept_S4
    :: (1) -> goto T0_init
    od;
accept_S4:
    do
    :: (! (((P[1]@CRITICAL)))) -> goto accept_S4
    od;
}

Сообщение просто предупреждает вас, что выполнение этого кода никогда не достигнет последней закрывающей скобки } (состояние "-end-"), что означает, что процедура никогда не завершается.

person Patrick Trentin    schedule 12.10.2016
comment
Большое спасибо! Да, я в последний раз отредактировал свой код, прежде чем публиковать его здесь, и это, похоже, исправило его. Что означает приведенный ниже код? Я предположил, что это было частью ошибки? недостигнуто в заявке ltl_0 _spin_nvr.tmp:10, состояние 13, -end- - person firearian; 15.10.2016
comment
@firearian Я обновил свой пост, чтобы ответить на ваш вопрос. Опять же, убедитесь, что здесь нет ошибки. - person Patrick Trentin; 16.10.2016
comment
Большое спасибо! Это ответ на мой вопрос! Небольшое продолжение, если позволите. Я понимаю, что это означает, что свойство ltl успешно проверено, потому что процесс никогда не входит в never ltl_0? - person firearian; 18.10.2016
comment
@firearian Чтобы убедиться, что модель M удовлетворяет формуле LTL F, Spin генерирует автомат Бучи, соответствующий отрицание F и вычисляет его синхронное произведение с автоматами M [я упрощаю немного]. Если последний продукт содержит цикл принятия, то у вас есть контрпример к вашему свойству F. В противном случае ваша система в безопасности. В общем, строго говоря, не имеет значения, выполняете ли вы некоторые переходы автоматов Бучи, а скорее имеете ли вы выполнение по принимающему пути. - person Patrick Trentin; 18.10.2016
comment
Итак, сосредоточившись на вашем примере, это означает, что ни одно выполнение синхронного продукта вашей модели M + никогда ltl_0 никогда не переходит в состояние с пометкой accept_S4. Однако выполнение все равно проходит через состояние с кодом ::(1) -> goto T0_init (зацикливается на нем). - person Patrick Trentin; 18.10.2016
comment
Спасибо большое! Знаете ли вы документы муравьев, которые я могу прочитать, чтобы глубже понять это? Хотя я понимаю, что вы имеете в виду, я также хотел бы узнать, почему и как это работает. Спасибо еще раз! - person firearian; 19.10.2016
comment
@firearian Краткие презентации: spinroot.com/spin/Man Книги: spinroot.com/spin/books.html и документы: spinroot.com/spin/theory.html - person Patrick Trentin; 19.10.2016