我如何将这些更改为 NuSMV 模型中的 CTL SPEC？

我需要帮助编写这些 CTL。我还不太明白如何以 NuSMV 格式编写，希望我的代码对您有意义，因为它是不完整的 atm。

2）如果一个进程正在等待，它最终会到达其临界区

3）两个进程必须“轮流”进入临界区

4）一个进程有可能连续两次进入临界区（在另一个进程进入之前）。

5) 进程 1 连续进入临界区将至少间隔 n 个周期，其中 n 是某个常数。您应该为 n 选择一个合适的值，并且应该验证该值（即，而不是反驳）。

6) 您选择的另外 2 个重要属性

MODULE thread1(flag2,turn)
VAR
   state : {W0,F1,W1,T1,F2,Wait,F3,C1,T2,F4};
   flag1 : boolean;

ASSIGN
   init(state) := W0;
   next(state) :=
case
   state = W0                 : F1;  
   state = F1                 : W1;  
   state = W1 & flag2         : T1; 
   (state = W1) & !flag2      : C1;  
   (state = T1)&(turn = 2)    : F2;  
   (state = T1)&(turn != 2)   : W1;  
   (state = F2)               : Wait; 
   (state = Wait)&(turn = 1)  : F3;   
   (state = Wait)&(turn != 1) : Wait; 
   (state = F3)               : W1; 
   (state = C1)               : T2; 
   (state = T2)               : F4; 
   (state = F4)               : W0;
    TRUE : state;
esac;

init(flag1) := FALSE;
next(flag1) := 
case
   state = F1 | state = F3 : TRUE;  
   state = F2 | state = F4 : FALSE; 
   TRUE                    : flag1;
esac;

DEFINE
  critical := (state = C1);
  trying := (state = F1 | state = W1 | state = T1 | state = F2 |     state = Wait | state = F3);  

MODULE thread2(flag1,turn)
VAR
   state1 : {N0,N1,N2,N3,N4,Wait1,N5,Critical1,N7,N8};
   flag2 : boolean;

ASSIGN
   init(state1) := N0;
   next(state1) :=
case
   (state1 = N0)               : N1;  
   (state1 = N1)               : N2;  
   (state1 = N2) & flag1       : N3;  
   (state1 = N2) & !flag1      : Critical1;
   (state1 = N3) & (turn = 1)  : N4;  
   (state1 = N3) & (turn != 2) : N2;  
   (state1 = F4)               : Wait1; 
   (state1 = Wait1)&(turn = 2) : N5;   
   (state1 = Wait1)&(turn != 2): Wait1; 
   (state1 = N5)               : N2; 
   (state1 = Critical1)        : N7; 
   (state1 = N7)               : N8;
   (state1 = N8)               : N0;
    TRUE : state1;
esac;

init(flag2) := FALSE;
next(flag2) := 
case
   state1 = N1 | state1 = N5 : TRUE;  
   state1 = N4 | state1 = N8 : FALSE;
   TRUE                    : flag2;
esac;

DEFINE
  critical := (state1 = Critical1);
  trying := (state1 = N1 | state1 = N2 | state1 = N3 | state1 = N4 |     state1 = Wait1 | state1 = N5);  

MODULE main

VAR

turn: {1, 2};
proc1: process thread1(proc2.flag2,turn);
proc2: process thread2(proc1.flag1,turn);

ASSIGN

init(turn) := 1;
next(turn) := 
case
   proc1.state = T2 : 2;
   proc2.state1 = N7 : 1;
   TRUE : turn;
esac;

SPEC 

AG !(proc1.critical & proc2.critical); 
--two processes are never in the critical section at the same time

SPEC 
AG (proc1.trying -> AF proc1.critical);

Note:为您全面介绍CTL答案是相当不现实的。此外thisNuSMV/nuXmv 上的快速而肮脏的课程，您可能会受益于查看这些幻灯片，提供了 CTL 模型检查的理论背景。

CTL 操作员

为简单起见，假设您的程序有一个unique 初始状态.

的语义CTL运算符如下：

• AF P: in all可能的执行路径，迟早 P将true.
• AG P: in all可能的执行路径，P is always true.
• AX P: in all可能的执行路径，在next state P is true.

• A[P U Q]: in all可能的执行路径，P is true * until Q is true（至少一次）。

• EF P: 至少在一个执行路径，迟早 P将true.

• EG P: 至少在一个执行路径，P is always true.
• EX P: 至少在一个执行路径，在next state P is true.
• E[P U Q]: 至少在一个执行路径，P is true * until Q is true（至少一次）。

*: until is true也在一条路上P从来没有true，前提是Q是立即verified。 [另请参阅：弱/强直到]

如果你有multiple 初始状态，那么CTL财产如果是则成立true对于每一个初始状态.

特性：

请注意，自从您的NuSMV模型目前已损坏，这似乎是一项作业，我将为您提供一个伪代码属性的版本，并让您将其适合您自己的代码。

• 如果一个进程正在等待，那么它最终将到达其临界区

  CTLSPEC AG (proc1.waiting -> AF proc1.critical);
  

  解释：括号的内容与您阅读的句子完全相同。我添加了AG因为该属性必须明确适用于模型中的每个可能状态。如果省略它，那么模型检查器将简单地测试是否proc1.waiting -> AF proc1.critical is true在你的初始状态。

• 两个进程必须“轮流”进入临界区

  CTLSPEC AG ((proc1.critical -> AX A[!proc1.critical U proc2.critical]) &
             (proc2.critical -> AX A[!proc2.critical U proc1.critical]));
  

  解释：让我假设这种编码有效，因为两者proc1 and proc2留在临界区 for only one state。的想法proc1.critical -> AX A[!proc1.critical U proc2.critical]如下：“如果进程 1 处于临界区，那么从下一个状态开始，进程 1 永远不会（再次）处于临界区，直到进程 2 处于临界区”.

• 一个进程有可能连续两次进入临界区（在另一个进程进入之前）。

  CTLSPEC EF (proc1.critical -> EX A[!proc2.critical U proc1.critical]);
  

  解释：与上一篇类似。这里我用的是EF因为它足够财产holds就一次。

• 进程 1 连续进入临界区将至少间隔 n 个周期，其中 n 是某个常数。您应该为 n 选择一个合适的值，并且应该验证该值（即，而不是反驳）。

  edit:我删除了这个编码，因为再一想我写的公式是很多stronger比要求的。不过，我认为不可能通过E运算符，因为它会变得很多weaker比要求的。目前，除了修改模型来计算数量之外，我想不出其他可能的选择cycles， 不管什么意思。