1

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

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

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

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

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

6）您选择的更多非平凡属性

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

1 回答 1

4

注意：在答案中给您全面介绍CTL是非常不现实的。除了这个关于 NuSMV/nuXmv 的快速而肮脏的课程之外，您可能会从这些幻灯片中受益，这些幻灯片提供了 CTL 模型检查的理论背景。

CTL 运营商

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

CTL运算符的语义如下：

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

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

  • EF P：在至少一个执行路径中，P迟早 会为真。

  • EG P：在至少一个执行路径中，P始终为真。
  • EX P：在至少一个执行路径中，在下一个状态P为true。
  • E[PUQ]：在至少一个执行路径中，P为真*直到 Q为真（至少一次）。

*: until在P永远不为真的路径上也为真，前提是Q被立即验证。[另外，请参阅：弱/强直到]

如果您有多个 初始状态，则CTL 属性在每个初始状态都为真时成立。

CTL 运营商

特性：

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

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

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

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

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

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

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

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

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

    解释：和上一个类似。在这里，我使用EF，因为它足以让属性只保存一次。

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

    编辑：我删除了这种编码，因为再想想我写的公式比要求的要强得多。但是，我认为用E运算符削弱它是不可能的，因为它会变得比要求的要弱得多。目前我想不出一个可能的替代方案，除了修改你的模型来计算周期数，不管这意味着什么。

于 2016-05-31T17:19:07.930 回答