如何将伪代码更改为 NuSMV 代码？

Question

我的教授决定给我们数学学生一个代码来更改为 NuSMV，我似乎无法在其他任何地方寻求帮助，我只阅读了 6 页的教科书，并且只描述了某些属性的作用。模块 main 是 NuSMV 代码的一个示例，他说使用该格式示例来编写伪代码。 我不知道如何编写 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

您似乎正在尝试对 Dekker/Dijkstra 的算法进行建模，以实现两个进程之间的互斥。

根据您的问题，您感兴趣的步骤应该仅为1-4。我添加了更多内容，以便更全面地了解使用 NuSMV 可以实现的目标。

虽然基本思想相同，但我使用了相同算法的稍微不同的版本。

---

IDEA：存在一种将伪代码转换为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，可能有多个 exit 点，具体取决于 guard 的值：如果 iflag 为真，则 exit点是l3，否则退出点是l7。

2. 创建一个对应的模块，它采用相同的输入，并有一个state变量，该变量评估新引入的标签时间>。

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

   在这里，请注意我添加了特殊状态错误。这只是为了确保在定义 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;
   

   如您所见，我只是将每个入口点与相应的出口点连接起来。此外，如果为给定的入口点定义了多个出口点，我还添加了其他状态条件来确定行 接下来执行。

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 
   

---

注意事项：

1. 如果您仔细查看步骤 1 和 3，您会发现有几个状态是多余的。例如，总是可以折叠只有一个入口和出口点的连续状态。我会把这个留给你作为练习。

2. 请注意，为了简单起见，我使用了模块的同步组合。在实践中，通过让两个进程异步运行，验证会更有意义。但是，这需要使模型比您的问题真正需要的更复杂，因此超出了我的回答范围。

3. 如果你想了解更多关于NuSMV的信息，你可以看看它的documentation或者看看这个course的第二部分。