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

Question

我需要帮助编写这些 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);

Answer 1

注意：在回答中给你全面介绍CTL是很不现实的。除了 this 关于 NuSMV/nuXmv 的快速而肮脏的课程之外，您还可以从提供 CTL 模型检查理论背景的 these slides 中受益。

---

CTL 操作员

假设为简单起见，您的程序具有唯一 初始状态。

CTL 运算符的语义如下：

• AF P：在所有可能的执行路径中，迟早P将为真.
• AG P：在所有可能的执行路径中，P总是 true。
• AX P：在所有可能的执行路径中，下一个状态P为true.

• A[P U Q]：在所有可能的执行路径中，P为真 * 直到 Q 为真（至少一次）。

• EF P：在至少一个执行路径中，迟早P将是是的。

• EG P：在至少一个执行路径中，P总是 true。
• EX P：在至少一个执行路径中，在下一个状态P为true em>。
• E[P U Q]：在至少一个执行路径中，P为true * 直到 strong> Q 为 true（至少一次）。

*：直到为true也在一条P永远不会true的路径上，前提是Q 立即验证。 [另见：weak/strong until]

如果您有多个 初始状态，则CTL 属性 成立，如果它是true 对于每个初始状态。

---

属性：

请注意，由于您的 NuSMV 模型目前已损坏并且这似乎是一项家庭作业，因此我将为您提供属性的 伪代码 版本并保留它让您将它们安装到您自己的代码中。

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

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

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

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

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

  解释：让我假设这种编码有效，因为 proc1 和 proc2 都位于 临界区 仅一个状态。 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 选择一个合适的值，并且这个值应该被验证（即，不被证明）。

  编辑：我删除了这个编码，因为我再次想到我写的公式比要求的要强。但是，我认为使用 E 运算符无法削弱它，因为它会变得比所需的 weaker 多得多。目前我想不出除了修改你的模型来计算 cycles 的数量之外的可能替代方案，不管这意味着什么。