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

Question

Мой профессор решил дать нам студент-математик код для преобразования в NuSMV, и я не могу найти помощь где-либо еще, и я читаю учебник, он всего 6 страниц и описывает только то, что делает определенное свойство. Модуль main является примером кода NuSMV, и он сказал использовать этот пример формата для написания кода psuedo. Я не знаю, как написать цикл while и установить, что должно быть правдой? а flag1 будет государством, а разворот также будет другим государством?

 while(true) do
  flag1 := true
    while flag2 do
     if turn=2
       flag1 := false;
       wait until turn = 1;
       flag1 := true
  Critical section
  turn := 2
  flag1 := false;

Answer 1

It looks like you're trying to model Dekker/Dijkstra's algorithm for mutual exclusion among two processes.

The steps of your interest, based on your question, should only be 1-4. I added some more to provide a more complete picture of what can be achieved with NuSMV.

I used a slightly different version of the same algorithm, though the underlying idea is the same.

---

IDEA: there exists a methodology for converting pseudo-code into a NuSMV model:

1. Label the entry and exit point of each statement in your code:

   --     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;
   --     }
   

   Note that some statements, eg while iflag do, might have more than one exit point depending on the value of the guard: if iflag is true, then the exit point is l3, otherwise the exit point is l7.

2. Create a corresponding module that takes the same inputs and has a state variable which evaluates to the newly introduced labels.

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

   Here, notice that i added the special state error. This is only to ensure that during the definition the transition relation for state we are not leaving out any correct transition step. In general, it should be omitted as it does not belong to the original code.

3. Define the transition relation for state:

   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;
   

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

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

   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 
   

---

ЗАМЕТКИ:

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

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

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