Spin unreachable in proctype -end-

Я новичок в проверке модели вращения и хотел знать, что означает эта ошибка:

unreached in proctype P1
    ex2.pml:16, state 11, "-end-"
    (1 of 11 states)
unreached in proctype P2
    ex2.pml:29, state 11, "-end-"
    (1 of 11 states)

вот мой код:

int y1, y2;
byte insideCritical;

active proctype P1(){
do
    ::true->
        y2 = y1 + 1;
        (y1 == 0 || y2 < y1);
        /* Entering critical section */
            insideCritical++;
            assert(insideCritical < 2);
            insideCritical--;
        /* Exiting critical section */
        y2 = 0;
od
}
active proctype P2(){
do
    ::true->
        y1 = y2 + 1;
        (y2 == 0 || y1 < y2);
        /* Entering critical section */
            insideCritical++;
            assert(insideCritical < 2);
            insideCritical--;
        /* Exiting critical section */
        y1 = 0;
od
}

На самом деле он не должен заканчиваться, это программа взаимного исключения, которая проверяет, не находятся ли два процесса вместе в критической секции. Означает ли ошибка, что программа не завершается? Спасибо!


process promela spin mutual-exclusion
person Javi    schedule 31.03.2014    source источник

Ответы (2)


arrow_upward
7
arrow_downward

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

active proctype P1(){
  endHere:
  do
  :: true->
    y2 = y1 + 1;
    (y1 == 0 || y2 < y1);
    /* Entering critical section */
        insideCritical++;
        assert(insideCritical < 2);
        insideCritical--;
    /* Exiting critical section */
    y2 = 0;
  od
}

Конечная метка — это любая метка, начинающаяся с «конец». Если ваш proctype заканчивается в состоянии, отмеченном таким образом, Spin не будет показывать вам эти предупреждения.

person dsteinhoefel    schedule 31.03.2014
comment
Большой! как я и думал.. Спасибо! - person Javi; 01.04.2014

arrow_upward
6
arrow_downward

Проверенный ответ - хороший; это хороший тон, чтобы быть явным, добавляя метку end соответствующим образом. Однако это не всегда возможно сделать, поэтому вы можете отключить SPIN, запустив проверку pan с флагом -n:

-n : no listing of unreached states at the end of the run
person GoZoner    schedule 09.04.2014