我的教授决定给我们数学学生一个代码来更改为 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;
看起来您正在尝试对Dekker/Dijkstra 的算法进行建模，以实现两个进程之间的互斥。
根据您的问题，您感兴趣的步骤应该仅为1-4。我添加了更多内容，以更全面地了解NuSMV可以实现的目标。
尽管基本思想相同，但我使用了相同算法的略有不同的版本。
IDEA：存在一种将伪代码转换为NuSMV模型的方法：
在代码中标记每个语句的入口和出口点：
-- 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。
创建一个相应的模块，该模块采用相同的输入，并具有一个评估新引入的标签的状态变量。
MODULE p(iflag, turn, id)
VAR
state : { l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, error };
flag : boolean;
在这里，请注意我添加了特殊状态错误。这只是为了确保在定义状态的转换关系期间我们不会遗漏任何正确的转换步骤。一般来说，它应该被省略，因为它不属于原始代码。
定义状态的转移关系：
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;
如您所见，我只是将每个入口点与相应的出口点连接起来。此外，只要为给定的入口点定义了多个出口点，我还添加了其他状态条件来确定接下来执行哪一行。
为flag添加转换关系：
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
笔记：