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

Question

我的教授决定给我们数学专业的学生一个代码来转换成 NuSMV，我似乎找不到其他任何地方可以寻求帮助，我只读了 6 页的教科书，只描述了某些内容属性做。模块 main 是 NuSMV 代码的示例，他说使用该格式示例来编写伪代码。我不知道如何编写while循环并设置为真？ flag1 是一个状态，turn 还是另一个状态吗？

 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模型的方法:

标记代码中每个语句的 entry 和 exit 点：

--     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 的值，可能有多个 exit 点：如果 iflag 为真，那么出口点是l3，否则出口点是l7.

创建一个相应的模块，它采用相同的输入并且有一个状态变量计算新引入的 labels。
```
MODULE p(iflag, turn, id)
VAR
  state : { l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, error };
  flag : boolean;
```
在这里，请注意我添加了特殊状态 error。这只是为了确保在定义 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;

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

为标志添加转换关系:

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

添加一些定义来识别进程正在执行的代码部分：

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

创建一个 主模块 ，它创建两个 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;

添加一些非常典型的 互斥特性以供模型检查器验证：

  --*-- 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);

运行工具

~$ 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 和 3，有几个状态看起来是多余的。例如，总是可以折叠只有一个入口点和出口点的连续状态。我会把这个留给你作为练习。
请注意，为了简单起见，我使用了模块的同步组合。在实践中，让两个进程异步运行验证会更有意义。但是，这需要使模型比您的问题真正需要的更复杂，因此超出了我的回答范围。
如果你想了解更多关于NuSMV的信息，你可以看看它的documentation or look at the second part of this course.

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

How can i change psuedo-code to NuSMV code?

logic

model-checking

model

nusmv