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

问题描述

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

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)如果某个进程正在等待，它将最终到达其关键部分

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

3)这两个过程必须轮流"进入关键部分

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

4)一个流程有可能连续两次进入关键部分(在另一流程之前).

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

5)通过过程1连续进入关键部分将至少间隔n个周期，其中n是某个常数.您应该为n选择一个合适的值，并且应该对此值进行验证(即不被拒绝).

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个您选择的非平凡属性

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

推荐答案

注意:在回答中为您提供 CTL 的全面介绍是不现实的.除了在NuSMV/nuXmv上这快速而肮脏的课程之外，您可能还会受益于在这些幻灯片中，这些幻灯片为CTL模型检查提供了理论背景

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操作员

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

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

CTL 运算符的语义如下:

• AF P :所有可能的执行路径，早晚 P 将为 true .
• AG P :在所有可能的执行路径中， P 总是 true .
• AX P :在所有可能的执行路径中，在 next 状态 P 中为 true .

• A [PUQ] :在所有可能的执行路径中， P 为 true * 直到 Q 为 true (至少一次).

• 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 :至少在一个执行路径中，早晚 P true .

*:在直到 P 都不为 true 的路径上，直到为 true ，前提是 Q 立即被验证. [另请参阅:弱/强直到]

*: 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.

属性:

请注意，由于您的 NuSMV 模型当前已损坏，这似乎是一项作业，因此，我将为您提供属性的伪代码版本，并保留它给您，使它们适合您自己的代码.

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

解释:括号中的内容会在您阅读句子时对其进行精确编码.我添加了 AG ，因为该属性必须清楚地包含在模型中的每个可能状态中.如果您省略它，那么模型检查器将只测试在初始状态下proc1.waiting -> AF proc1.critical是否为 true .

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

说明:让我以为该编码有效是因为 proc1 和 proc2 都位于关键部分仅针对 一个状态. proc1.critical -> AX A[!proc1.critical U proc2.critical]的概念如下:如果进程1在关键部分中，那么从下一个状态开始，进程1将永远不会在关键部分中(再次)，直到进程2在关键部分中为止".

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

说明:与上一个类似.在这里，我使用 EF ，因为它足以满足属性持有一次.

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

通过过程1连续进入关键部分将至少间隔n个周期，其中n是某个常数.您应该为n选择一个合适的值，并且应该对此值进行验证(即不被拒绝).

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).

我删除了此编码，因为再次考虑到我编写的公式比要求的更强.但是，我认为使用 E 运算符不能削弱它，因为它会变得比所需的更弱.当时，除了修改模型以计算周期的数量之外，我想不出其他可行的选择.

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屋！