check_property和msat_check_ltlspec_bmc在NuXMV中的不同结果

Question

以下属性在check_property中为真，但msat_check_ltlspec_bmc给出了反例。后一个结果似乎是正确的，“G(tt >= 7) -> G ((FlagLO =FALSE)在模块中”。我们该怎么解释呢？

我尝试用稍微改变了的smv文件。试图检查基于LTL属性的存在模式。Check_fsm结果没有在早期运行。这就造成了僵局。那样的话msat_check..。结果似乎不正确。现在哪一个是正确的？验证模型的正确方法应该是什么？需要使用reals，从而尝试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

这是普通LTL check_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
##########################################################

Answer 1

check_fsm的输出告诉您问题所在:在FSM中存在死锁状态。

请参阅常见问题#011

基于BDD的LTL模型检测算法在NuSMV中实现，只对无限路径进行推理。因此，即使对于不具备安全属性的情况，也会产生一个套索形状的反例，尽管有限的路径就足够了。在进行检查时，假定转换关系的全局性和死锁的不存在，并且搜索被限制为只考虑无限路径，而忽略了导致死锁的所有路径。因此，将不会检测到导致死锁和伪造属性的有限路径。 基于SAT的有界模型检验算法也假定了转移关系的全局性和死锁的存在性，但它们都在寻找有限或无限属性的反例。因此，与基于BDD的LTL模型检查算法不同，将检测到导致死锁和伪造属性的有限路径。 这两种算法都假定了转换关系的全局性和死锁的存在，但它们并没有专门检查是否满足这些条件。用户有责任执行此检查，例如在批处理模式下发出-ctt命令行标志，或者在NuSMV shell中调用check_fsm命令。 到目前为止，在基于SAT的有界模型检查中，还没有禁止搜索有限路径的标志。但是，通过在模型中添加以下公平条件 正义是真实的； 有界模型检查算法停止寻找有限路径，并将搜索限制在无限路径上： 当NuSMV模型包含多个初始状态时，所报告的验证结果可能会发生另一个可能的差异。基于BDD的方法依赖于将LTL模型检查简化为CTL模型检查(通过表构造)。CTL模型对公平初始状态集进行普遍量化检验。因此，只有最初的公平状态才会被考虑。最初的状态可能是不公平的，而且是不被考虑的。这个选择是值得怀疑的，但CadenceSMV也显示了这一点。不同的是，基于BMC的模型检查不局限于只考虑公平的初始状态。因此，如果存在一个不公平的初始状态，并且有一条有限的路径，那么它就会发现它的公平性条件。