NuSMV CTL规范

Question

这些天我开始学习NuSMV。我有这样的代码：

 MODULE main

 VAR

 state: {a,b,c,d,e};   
 ASSIGN

 init(state) := a; 

 next(state) := case

            (state = a)  : b;

            (state = b)  : c;

            (state = c)  : d;

            (state = d)  : e;                   

            TRUE:Stages;

       esac;

我想验证的是，每次我们处于状态"a“时，下一个状态将是"b”状态。哪一个是正确的(即使我尝试了这两种方法，而且它们都给了我正确的答案)：

check_ctlspec -p "AG (state=a -> AX state=b)"

check_ctlspec -p "AF (state=a -> AX state=b)"

check_ctlspec -p "AF (state=a -> AF state=b)"  

check_ctlspec -p "AF (state=a -> state=b)"  

我的第二个问题是:在上面的模型中，不存在从状态"d“到状态"a”的转换，但是当我使用

check_ctlspec -p "AF (state=d -> AX state=a)"

结果是真的。为什么是这种情况？

Answer 1

首先，让我在您的模型中用my_var重命名my_var。这避免了将自动机的实际状态与您引入的state变量混淆。

• AG (my_var = a -> AX my_var = b)

在每一种可能执行的状态中，如果my_var等于a，那么在下一种状态下，my_var必然等于b。

此是要验证的属性。

• AF (my_var=a -> AX my_var=b)

迟早，如果my_var等于a，那么在下一个状态下，my_var必然等于b。

注意，在两种情况下，蕴涵是true：

• 前提为真，结论为真，或
• 当前提是错误的

因此，如果前提my_var=a没有被验证，那么它的含义就可以由任何状态(即除初始状态以外的任何状态)来实现。由于使用了AF，因此只需要(至少)在每个可能的执行路径上(至少)验证一种状态的含义。

从某种意义上说，这对于您想要验证的内容“太弱”。

• AF (my_var=a -> AF my_var=b)

迟早，如果my_var等于a，那么在将来的某个时候必然是这样(wrt )。my_var等于a的状态my_var变为b。

与前一个类似，这一点甚至更弱，因为它甚至没有指定my_var在什么时候与b相等。

• AF (my_var=a -> my_var=b)

注意，只有当(my_var=a -> my_var=b)为false时，隐含的my_var才是真，因为不能将my_var临时分配给a和b。然而，这个条件是由除初始状态以外的任何状态来验证的，因此再次对该属性进行微不足道的验证。

• AF (my_var=d -> AX my_var=a)

同样，这种情况太弱了，因为您使用的是AF而不是AG。它的含义由任何状态( my_var != d )都是真实的，因此对整个属性进行验证就足够了。

我想请您看看这个堆栈溢出Q/A或这些幻灯片，以了解更多关于该工具和语言的知识。