通过构造,以所谓的分配样式[在您的模型中使用]:
- 总是至少有一个初始状态
- 所有状态至少有一个下一个状态
- 不确定性很明显
或者,可以使用所谓的约束样式,它允许:
- 不一致
INIT
的约束,导致没有初始状态
- 不一致
TRANS
的约束,导致死锁状态(即没有任何传出转换到下一个状态的状态)
- 不确定性是隐藏的
有关更多信息,请参阅本课程的第二部分,这也适用NuSMV
于大部分内容。
某个状态没有未来状态的 FSM 的示例是:
MODULE main
VAR b : boolean;
TRANS b -> FALSE;
b
is的状态true
没有未来状态。相反,b
is的状态false
可以自行循环或转到 的状态b = true
。
您可以使用该命令check_fsm
检测死锁状态。
请注意,在某些情况下,死锁状态的存在会阻碍模型检查的正确性。例如:
常见问题解答 #007:具有顶级存在路径量词的 CTL 规范被错误地报告为违反。例如,对于下面的模型,两种规格都被报告为错误的,尽管其中一个只是对另一个的否定!我知道死锁状态可能会出现此类问题,但是使用 -ctt 运行它表示一切都很好。
MODULE main
VAR b : boolean;
TRANS next(b) = b;
CTLSPEC EF b
CTLSPEC !(EF b)
有关转换关系中死锁状态的其他严重后果,请参阅此页面。
通常,当NuSMV
说“案例条件并非详尽无遗”时,会在构造末尾添加一个带有条件的默认操作,当前面的条件都不适用时会触发该操作。默认动作最常见的选择是自循环,其编码如下:TRUE
case
MODULE main
VAR
location: {l1,l2,l3};
ASSIGN
init(location):= l1;
next(location):=
case
(location = l1): l2;
(location = l2): {l1, l3};
TRUE : location;
esac;
注意:请注意,如果有多个条件具有相同的保护,则只会使用这些条件中的第一个。出于这个原因,当在您的模型中时,location = l2
下一个值location
只能是l1
并且从不l3
。为了解决这个问题,并在 和 中进行一些不确定的选择l1
,必须列出与一组l3
值相同的条件下所有可能的未来值(即)。{l1, l3}