model-checking - NuXMV 中 check_property 和 msat_check_ltlspec_bmc 的结果不同
问题描述
以下属性对于 check_property 是正确的,但 msat_check_ltlspec_bmc 给出了反例。后一个的结果似乎是正确的。“G (((tt >= 7) -> G ((FlagLO = FALSE)))) IN 模块”。我们如何解释这一点?
我用稍微改变的 smv 文件尝试了这个。试图检查基于 LTL 属性的存在模式。Check_fsm 结果未早先运行。这造成了僵局。在这种情况下 msat_check.... 结果似乎不正确。现在哪一个是正确的?验证模型的正确方法应该是什么?需要使用实数,因此尝试 msat 命令。
MODULE Seq_19(T_41, T_41_PRESENT)
VAR
_next_t : { Init_46_idle, LO_51_idle, BO_73_idle, State_120_idle, TO_132_idle, LOSense_118, BOSense_115, TOSense_137, TransitionSegment_125, BOSense_141 };
FlagLO : boolean;
FlagBO : boolean;
tt : -256..255;
FlagTO : boolean;
DEFINE
LOOut_68 :=
case
(_next_t = LOSense_118) : TRUE;
TRUE : FALSE;
esac;
BOOut_84 :=
case
(_next_t = BOSense_115) : TRUE;
(_next_t = BOSense_141) : TRUE;
TRUE : FALSE;
esac;
LOOut_68_PRESENT :=
case
(_next_t = LOSense_118) : TRUE;
TRUE : FALSE;
esac;
BOOut_84_PRESENT :=
case
(_next_t = BOSense_115) : TRUE;
(_next_t = BOSense_141) : TRUE;
TRUE : FALSE;
esac;
guard_LOSense_118 := (tt > 5);
guard_BOSense_115 := (tt > 10);
guard_TOSense_137 := (tt > 8);
guard_TransitionSegment_125 := (tt > 50);
guard_BOSense_141 := (tt > 10);
ASSIGN
init(_next_t) := { Init_46_idle, LOSense_118 };
init(FlagLO) := FALSE;
init(FlagBO) := FALSE;
init(tt) := 0;
init(FlagTO) := FALSE;
TRANS _next_t in { Init_46_idle }
-> next(_next_t) in { Init_46_idle, LOSense_118 };
TRANS _next_t in { LO_51_idle, LOSense_118 }
-> next(_next_t) in { LO_51_idle, BOSense_115, TOSense_137 };
TRANS _next_t in { BO_73_idle, BOSense_115, BOSense_141 }
-> next(_next_t) in { BO_73_idle, TransitionSegment_125 };
TRANS _next_t in { State_120_idle, TransitionSegment_125 }
-> next(_next_t) in { State_120_idle };
TRANS _next_t in { TO_132_idle, TOSense_137 }
-> next(_next_t) in { TO_132_idle, BOSense_141 };
TRANS (_next_t = Init_46_idle)
-> next(tt) = (tt + 1) &
next(FlagLO) = FlagLO &
next(FlagBO) = FlagBO &
next(FlagTO) = FlagTO;
TRANS (_next_t = LO_51_idle)
-> next(tt) = (tt + 1) &
next(FlagLO) = FlagLO &
next(FlagBO) = FlagBO &
next(FlagTO) = FlagTO;
TRANS (_next_t = BO_73_idle)
-> next(tt) = (tt + 1) &
next(FlagLO) = FlagLO &
next(FlagBO) = FlagBO &
next(FlagTO) = FlagTO;
TRANS (_next_t = State_120_idle)
-> next(tt) = (tt + 1) &
next(FlagLO) = FlagLO &
next(FlagBO) = FlagBO &
next(FlagTO) = FlagTO;
TRANS (_next_t = TO_132_idle)
-> next(tt) = (tt + 1) &
next(FlagLO) = FlagLO &
next(FlagBO) = FlagBO &
next(FlagTO) = FlagTO;
TRANS (_next_t = LOSense_118)
-> next(FlagLO) = TRUE &
next(tt) = (tt + 1) &
next(FlagBO) = FlagBO &
next(FlagTO) = FlagTO;
TRANS (_next_t = BOSense_115)
-> next(FlagBO) = TRUE &
next(tt) = (tt + 1) &
next(FlagLO) = FlagLO &
next(FlagTO) = FlagTO;
TRANS (_next_t = TOSense_137)
-> next(FlagTO) = TRUE &
next(tt) = (tt + 1) &
next(FlagLO) = FlagLO &
next(FlagBO) = FlagBO;
TRANS (_next_t = TransitionSegment_125)
-> next(tt) = (tt + 1) &
next(FlagLO) = FlagLO &
next(FlagBO) = FlagBO &
next(FlagTO) = FlagTO;
TRANS (_next_t = BOSense_141)
-> next(FlagBO) = TRUE &
next(tt) = (tt + 1) &
next(FlagLO) = FlagLO &
next(FlagTO) = FlagTO;
INVAR ((_next_t = LOSense_118) -> guard_LOSense_118)
INVAR ((_next_t = BOSense_115) -> guard_BOSense_115)
INVAR ((_next_t = TOSense_137) -> guard_TOSense_137)
INVAR ((_next_t = TransitionSegment_125) -> guard_TransitionSegment_125)
INVAR ((_next_t = BOSense_141) -> guard_BOSense_141)
INVAR ((_next_t = Init_46_idle) -> !(guard_LOSense_118))
INVAR ((_next_t = LO_51_idle) -> (!(guard_BOSense_115) & !(guard_TOSense_137)))
INVAR ((_next_t = BO_73_idle) -> !(guard_TransitionSegment_125))
INVAR ((_next_t = State_120_idle) -> TRUE)
INVAR ((_next_t = TO_132_idle) -> !(guard_BOSense_141))
MODULE main
VAR
T_41 : -256..255;
T_41_PRESENT : boolean;
module : Seq_19(T_41,T_41_PRESENT);
这是的输出msat_check_ltlspec_bmc
:
nuXmv > read_model -i Seq.smv
nuXmv > go_msat
nuXmv > msat_check_ltlspec_bmc -p "G (((tt >= 7) -> G ((FlagLO = FALSE)))) IN module"
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification G (tt >= 7 -> G FlagLO = FALSE) IN module is false
-- as demonstrated by the following execution sequence
Trace Description: MSAT BMC counterexample
Trace Type: Counterexample
-> State: 1.1 <-
T_41 = -256
T_41_PRESENT = FALSE
module._next_t = Init_46_idle
module.FlagLO = FALSE
module.FlagBO = FALSE
module.tt = 0
module.FlagTO = FALSE
module.guard_BOSense_141 = FALSE
module.guard_TransitionSegment_125 = FALSE
module.guard_TOSense_137 = FALSE
module.guard_BOSense_115 = FALSE
module.guard_LOSense_118 = FALSE
module.BOOut_84_PRESENT = FALSE
module.LOOut_68_PRESENT = FALSE
module.BOOut_84 = FALSE
module.LOOut_68 = FALSE
-> State: 1.2 <-
T_41 = 255
T_41_PRESENT = TRUE
module.tt = 1
-> State: 1.3 <-
T_41 = -238
T_41_PRESENT = FALSE
module.tt = 2
-> State: 1.4 <-
T_41 = 255
T_41_PRESENT = TRUE
module.tt = 3
-> State: 1.5 <-
T_41 = -224
T_41_PRESENT = FALSE
module.tt = 4
-> State: 1.6 <-
T_41 = 255
T_41_PRESENT = TRUE
module.tt = 5
-> State: 1.7 <-
module._next_t = LOSense_118
module.tt = 6
module.guard_LOSense_118 = TRUE
module.LOOut_68_PRESENT = TRUE
module.LOOut_68 = TRUE
-> State: 1.8 <-
module._next_t = LO_51_idle
module.FlagLO = TRUE
module.tt = 7
module.LOOut_68_PRESENT = FALSE
module.LOOut_68 = FALSE
这是正常 LTLcheck_property
调用的输出:
nuXmv > go
nuXmv > check_property -l -p "G (((tt >= 7) -> G ((FlagLO = FALSE)))) IN module"
-- specification G (tt >= 7 -> G FlagLO = FALSE) IN module is true
这是的输出check_fsm
:
nuXmv > check_fsm
******** WARNING ********
Fair states set of the finite state machine is empty.
This might make results of model checking not trustable.
******** END WARNING ********
##########################################################
The transition relation is not total. A state without
successors is:
T_41 = -256
T_41_PRESENT = FALSE
module._next_t = State_120_idle
module.FlagLO = FALSE
module.FlagBO = FALSE
module.tt = 255
module.FlagTO = FALSE
The transition relation is not deadlock-free.
A deadlock state is:
T_41 = -256
T_41_PRESENT = FALSE
module._next_t = State_120_idle
module.FlagLO = TRUE
module.FlagBO = TRUE
module.tt = 255
module.FlagTO = TRUE
##########################################################
解决方案
的输出check_fsm
告诉您问题出在哪里:FSM中存在死锁状态。
请参阅常见问题解答 #011
在 NuSMV 中实现的基于 BDD 的 LTL 模型检查算法仅与无限路径有关。因此,即使对于不成立的安全属性,也会生成套索形状的反例,尽管有限路径就足够了。在进行检查时,假设转移关系的整体性和不存在死锁,并且搜索仅限于考虑无限路径,而忽略导致死锁的所有路径。因此,将不会检测到导致死锁和伪造属性的有限路径。
基于 SAT 的有界模型检查算法还假设转移关系的整体性和不存在死锁,但他们正在为给定的有限或无限属性寻找反例。因此,与基于 BDD 的 LTL 模型检查算法不同,将检测到导致死锁和伪造属性的有限路径。
两种算法都假设转移关系的整体性和不存在死锁,但它们没有专门检查是否满足这些条件。用户有责任通过例如在批处理模式下发出 -ctt 命令行标志或通过在 NuSMV shell 中调用 check_fsm 命令来执行此检查。
到目前为止,还没有标志可以禁用在基于 SAT 的有界模型检查中搜索有限路径。但是,通过在模型中添加以下正义公平条件
正义真实;
有界模型检查算法停止寻找有限路径并将搜索限制为仅无限路径:
当 NuSMV 模型包含多个初始状态时,报告的验证结果可能会发生差异。基于 BDD 的方法依赖于将 LTL 模型检查减少到 CTL 模型检查(通过画面构造)。CTL 模型检查普遍量化了一组公平的初始状态。因此,仅考虑公平的初始状态。可能存在不公平的初始状态,它们不被考虑。这种选择可能是有问题的,但 CadenceSMV 也显示了这一点。不同的是,基于 BMC 的模型检查并不局限于只考虑公平的初始状态。因此,如果存在一个不公平的初始状态,并且从中存在一条有限路径,它将违反公平条件。
推荐阅读
- java - 具有线性时间复杂度的嵌套循环?
- php - 如何解决致命错误:Uncaught PDOException: SQLSTATE[HY093]: Invalid parameter number: number of bound variables does not match number of tokens
- c# - 从数据库中读取 varbinary 列并在弹出窗口中显示
- node.js - 依赖注入错误 TSED 单元测试服务
- java - 无法从 ADB shell 启动活动
- dataframe - Julia - 数据框 - 如何使用 by() 强制转换为向量/多行值标量结果
- php - 在 laravel 5.8 中更新图像时文件输入表单的默认值
- apache - SVN 无法打开密码文件
- python - 如何在openpyxl中将列宽设置为bestFit
- javascript - 如何在每个完整的三个单词后插入换行符?