Как я могу изменить псевдокод на код NuSMV?

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

Интересующие вас шаги в зависимости от вашего вопроса должны быть 1-4. Я добавил еще несколько, чтобы представить более полную картину того, чего можно достичь с помощью NuSMV.

Я использовал немного другую версию того же алгоритма, хотя основная идея та же.

ИДЕЯ: существует методика преобразования псевдокода в модель NuSMV:

1. Пометьте точки входа и выхода каждого оператора в коде:

   --     void p(iflag, turn, id) {
   -- l0:   while(true) do
   -- l1:     flag := true
   -- l2:     while iflag do
   -- l3:       if turn != id
   -- l4:         flag := false;
   -- l5:         wait until turn = id;
   -- l6:         flag := true
   -- l7:     // Critical section
   -- l8:     turn := 1 - id
   -- l9:     flag := false;
   --     }
   

   Обратите внимание, что некоторые утверждения, например. while iflag do может иметь более одной точки выхода в зависимости от значения guard: если iflag истинно, то точка выхода l3, иначе точка выхода будет l7.

2. Создайте соответствующий модуль, который принимает те же входные данные и имеет переменную состояния, оценивающую новые введенные метки.

   MODULE p(iflag, turn, id)
   VAR
     state : { l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, error };
     flag : boolean;
   

   Здесь обратите внимание, что я добавил особое состояние error. Это нужно только для того, чтобы во время определения отношения перехода для state мы не упустили ни одного правильного шага перехода. В общем случае его следует опустить, так как он не принадлежит исходному коду.

3. Определите отношение перехода для состояния:

   ASSIGN
     init(state) := l0;
     next(state) := case
       state = l0              : l1;
       state = l1              : l2;
       state = l2 & iflag      : l3;
       state = l2 & !iflag     : l7;
       state = l3 & turn != id : l4;
       state = l3 & turn = id  : l2;
       state = l4              : l5;
       state = l5 & turn != id : l5;
       state = l5 & turn = id  : l6;
       state = l6              : l2;
       state = l7              : l8;
       state = l8              : l9;
       state = l9              : l0;
       TRUE                    : error; -- if you match this then the above
                                        -- description of transitions are incomplete
     esac;
   

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

4. Добавьте отношение перехода для flag:

   init(flag) := FALSE;
   next(flag) := case
     state = l1 | state = l6 : TRUE;
     state = l4 | state = l9 : FALSE;
     TRUE                    : flag;
   esac;
   

5. Добавьте несколько определений, чтобы определить, какие разделы кода выполняются процессом:

   DEFINE
     critical_section := (state = l7);
     trying_section := (state = l1 | state = l2 | state = l3 |
                        state = l4 | state = l5 | state = l6);
   

6. Создайте основной модуль, который создает два экземпляра p:

   MODULE main ()
   VAR
     turn : {0, 1};
     p1   : p(p2.flag, turn, 0);
     p2   : p(p1.flag, turn, 1);
   
   ASSIGN
     init(turn) := 0;
     next(turn) := case
       p1.state = l8 : 1;
       p2.state = l8 : 0;
       TRUE          : turn;
     esac;
   

7. Добавьте некоторые очень типичные свойства взаимного исключения, которые будут проверены средством проверки модели:

     --*-- PROPERTIES --*--
   
   -- Safety: two processes are never in the critical section at the same time
   CTLSPEC AG !(p1.critical_section & p2.critical_section);
   
   -- Liveness: if a process is in the trying section, then sooner or later
   --           it will access the critical section.
   CTLSPEC AG (p1.trying_section -> AF p1.critical_section);
   
   -- Absence of Starvation
   CTLSPEC ! EF AG (p1.trying_section & p2.trying_section);
   
   -- Never in Error State 
   CTLSPEC AG !(p1.state = error);
   

8. Запустите инструмент

   ~$ NuSMV -int
   

   и убедитесь, что все свойства проверены:

   NuSMV > reset; read_model -i dekker.smv; go; check_property
   -- specification AG !(p1.critical_section & p2.critical_section)  is true
   -- specification AG (p1.trying_section -> AF p1.critical_section)  is true
   -- specification !(EF (AG (p1.trying_section & p2.trying_section)))  is true
   -- specification AG !(p1.state = error)  is true