如何在 NuSMV 模型中将这些更改为 CTL SPEC? [英] How can i change these into CTL SPEC in NuSMV model?

查看：16
本文介绍了如何在 NuSMV 模型中将这些更改为 CTL SPEC?的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！

问题描述

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

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

3)两个进程必须轮流"进入临界区

4)一个进程有可能连续两次进入临界区(在另一个进程之前).

5) 进程 1 进入临界区的连续条目将被至少 n 个周期分隔，其中 n 是某个常数.你应该为 n 选择一个合适的值，这个值应该被验证(即，不被反驳).

6) 2 个更重要的属性供您选择 

MODULE thread1(flag2,turn)无功功率状态:{W0,F1,W1,T1,F2,Wait,F3,C1,T2,F4};标志1:布尔值；分配初始化(状态):= W0；下一个(状态):=案件状态 = W0 : F1;状态 = F1 : W1;状态 = W1 &标志2:T1；(状态 = W1) &!flag2 : C1;(state = T1)&(turn = 2) : F2;(state = T1)&(turn != 2) : W1;(状态= F2):等待；(状态 = 等待)&(转 = 1) : F3;(state = Wait)&(turn != 1) : Wait;(状态= F3):W1；(状态= C1):T2；(状态 = T2) : F4;(状态 = F4) : W0;真:状态；esac;init(flag1) := FALSE;下一个(标志1):=案件状态 = F1 |状态 = F3:真；状态 = F2 |状态 = F4:假；真:标志1；esac;定义关键:=(状态= C1)；尝试 := (state = F1 | state = W1 | state = T1 | state = F2 | state = Wait | state = F3);MODULE thread2(flag1,turn)无功功率状态 1 : {N0,N1,N2,N3,N4,Wait1,N5,Critical1,N7,N8};标志2:布尔值；分配初始化(状态1):= N0；下一个(状态1):=案件(state1 = N0) : N1;(state1 = N1) : N2;(state1 = N2) &标志1:N3；(state1 = N2) &!flag1 : 临界 1;(state1 = N3) &(转 = 1) : N4;(state1 = N3) &(转！= 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;真:状态 1；esac;init(flag2) := FALSE;下一个(标志2):=案件状态 1 = N1 |状态 1 = N5:真；状态 1 = N4 |状态 1 = N8:假；真:标志2；esac;定义临界 := (state1 = Critical1);尝试 := (state1 = N1 | state1 = N2 | state1 = N3 | state1 = N4 | state1 = Wait1 | state1 = N5);模块主无功功率转:{1, 2};proc1: 进程线程1(proc2.flag2,turn);proc2: 进程线程2(proc1.flag1,turn);分配初始化(转):= 1；下一个(转):=案件proc1.state = T2 : 2;proc2.state1 = N7:1；真:转；esac;规格AG !(proc1.critical & proc2.critical);--两个进程永远不会同时处于临界区规格AG(proc1.trying -> AF proc1.critical)；

解决方案

注意: 在回答中全面介绍 CTL 是很不现实的.除了

<小时>

属性:

请注意，由于您的 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 因为它足以持有一次属性.

  • 进程 1 进入临界区的连续条目将被至少 n 个周期分隔，其中 n 是某个常数.你应该为 n 选择一个合适的值，这个值应该被验证(即，不被反驳).

    我删除了这个编码，因为我再次认为我写的公式比要求的强.但是，我认为用 E 操作符来削弱它是不可能的，因为它会变得比要求的弱.目前，除了修改您的模型以计算 周期 的数量之外，我想不出可能的替代方案，无论这意味着什么.

I need help writing these CTL. I don't reall understand how to write in NuSMV format yet, hopefully my code will make sense to you since it is incomplete atm.

2)If a process is waiting, it will eventually get to its critical section

3)The two processes must 'take turns' entering the critical section

4)It is possible for one process to get into the critical section twice in succession (before the other process does).

5)Successive entries into a critical section by process 1 will be separated by at least n cycles, where n is some constant. You should choose an appropriate value for n, and this one should be verified (i.e., not disproven).

6)2 more non-trivial properties of your choice 

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: giving you a comprehensive introduction to CTL in an answer is quite unrealistic. In addition to this quick and dirty course on NuSMV/nuXmv, you might benefit from looking at these slides, which provide a theoretical background on CTL Model Checking.

CTL OPERATORS

Assume that for simplicity your program has a unique initial state.

The semantics of the CTL operators is the following:

  • AF P: in all possible execution paths, sooner or later P will be true.
  • AG P: in all possible execution paths, P is always true.
  • AX P: in all possible execution paths, in the next state P is true.

  • A[P U Q]: in all possible execution paths, P is true * until Q is true (at least once).

  • EF P: in at least one execution path, sooner or later P will be true.

  • EG P: in at least one execution path, P is always true.
  • EX P: in at least one execution path, in the next state P is true.
  • E[P U Q]: in at least one execution path, P is true * until Q is true (at least once).

*: until is true also on a path in which P is never true, provided that Q is immediately verified. [Also, see: weak/strong until]

If you have multiple initial states, then the CTL property holds if it is true for every initial state.

Properties:

Note that since your NuSMV model is currently broken and this appears to be a homework, I will provide you with a pseudo-code version of the properties and leave it to you to fit them on your own code.

  • if a process is waiting, then it will eventually get to its critical section

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

    explanation: the content of the parenthesis encodes exactly the sentence as you read it. I added AG because the property must clearly hold for every possible state in your model. If you omit it, then the model checker will simply test whether proc1.waiting -> AF proc1.critical is true in your initial state(s).

  • the two processes must 'take turns' entering the critical section

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

    explanation: let me premise that this encoding works because both proc1 and proc2 stay in the critical section for only one state. The idea of proc1.critical -> AX A[!proc1.critical U proc2.critical] is the following: "if process 1 is in the critical section, then starting from the next state process 1 will never be in the critical section (again) until when process 2 is in the critical section".

  • It is possible for one process to get into the critical section twice in succession (before the other process does).

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

    explanation: similar to the previous one. Here I use EF because it suffices the property holds just once.

  • Successive entries into a critical section by process 1 will be separated by at least n cycles, where n is some constant. You should choose an appropriate value for n, and this one should be verified (i.e., not disproven).

    edit: I removed this encoding because on a second thought the formula I wrote is much stronger than required. However, I don't think it's possible to weaken it with the E operator, as it would become much weaker than required. At the time being I can't think of a possible alternative other than modify your model to count the number of cycles, whatever that means.

这篇关于如何在 NuSMV 模型中将这些更改为 CTL SPEC?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！

查看全文
相关文章
其他开发最新文章
热门教程
热门工具
登录 关闭
扫码关注1秒登录
发送“验证码”获取 | 15天全站免登陆