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

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

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

In every state of every possible execution, if my_var is equal to a then it must be necessarily the case that in the next statemy_var is equal to b.

这个是你要验证的属性。

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

Sooner or later, if my_var is equal to a then it must be necessarily the case that in the next statemy_var is equal to b.

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

当前提为真且结论为真时，或者
当前提为假时

因此，前提 my_var=a 未被验证的任何状态，即初始状态以外的任何状态，都可以简单地使蕴涵为真。由于您使用 AF，因此您需要针对每个可能的执行路径仅在（至少）一个状态上验证蕴涵。

从某种意义上说，这是"too weak"关于你要验证的。

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

Sooner or later, if my_var is equal to a then it must be necessarily the case at some point in the future (wrt. the state in which my_var is equal to a) my_var becomes equal to b.

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

AF (my_var=a -> my_var=b)

请注意，仅当 my_var=a 为假时，蕴涵 (my_var=a -> my_var=b) 才为真，因为 my_var 不能 con-temporarily 分配给 a 和 b。尽管如此，此条件可由初始状态以外的任何状态验证，因此属性再次被简单地验证。

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

同样，此条件太弱，因为您使用的是 AF 而不是 AG。 my_var != d 的任何状态都使该含义为真，因此足以验证整个属性。

我会邀请您查看此 or to these slides 以了解有关该工具和语言的更多信息。

NuSMV CTL规范

NuSMV CTL specification

ctl

nusmv