1

这些天我开始学习 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)"

结果是真的。为什么会这样？

4

1 回答 1

0

首先，让我在你state的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。

请注意，暗示在两种情况下为真：

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

因此，任何未验证前提my_var=a的状态，即除了初始状态之外的任何状态，都可以轻松地实现暗示。由于您使用AF，因此您需要仅在（至少）每个可能的执行路径的一个状态上验证暗示。

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

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

迟早，如果my_var等于，a那么它必然在未来的某个时间点（即my_var等于的状态a）my_var变为等于b。

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

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

请注意，暗示(my_var=a -> my_var=b)仅在my_var=a为假时为真，因为my_var不能同时分配给a和b。然而，这个条件由初始状态以外的任何状态验证，因此该属性再次被简单验证。

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

同样，这个条件太弱了，因为你正在使用AF而不是AG. 对于 的任何状态，其含义都是正确的my_var != d，因此对整个属性进行验证就足够了。

我会邀请您查看此堆栈溢出 Q/A或这些幻灯片，以了解有关该工具和语言的更多信息。

于 2019-05-29T21:18:37.767 回答