NuXMV 中 check_property 和 msat_check_ltlspec_bmc 的不同结果

Question

下面的属性对check_property是正确的，但是msat_check_ltlspec_bmc给出了反例。后一个的结果似乎是正确的。"G (((tt >= 7) -> G ((FlagLO = FALSE)))) IN module"。我们如何解释这个？

我尝试使用略微更改的 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

这是正常 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.

见FAQ #011

BDD based LTL model checking algorithms implemented in NuSMV reason only about infinite paths. Thus, even for a safety property that does not hold, a lasso-shaped counterexample is generated, although a finite path would be enough. While doing the check, it is assumed the totality of the transition relation and the absence of deadlocks, and the search is restricted to consider only infinite paths, disregarding all paths leading to a deadlock. Thus, a finite path leading to a deadlock and falsifying the property will not be detected.

SAT based bounded model checking algorithms also assume the totality of the transition relation and the absence of deadlocks, but they are looking for a counterexample for the given property that is either finite or infinite. Thus, differently from the BDD based LTL model checking algorithms, a finite path leading to a deadlock and falsifying the property will be detected.

Both algorithms assume the totality of the transition relation and the absence of deadlocks but they do not specifically check for these conditions being satisfied. It is the user responsibility to perform this check by e.g. issuing the -ctt command line flag in batch mode, or by invoking the check_fsm command in the NuSMV shell.

Up to now there is no flag to disable the search for a finite path within SAT based bounded model checking. However, by adding within the model the following justice fairness condition

JUSTICE TRUE;

the bounded model checking algorithms stop looking for a finite path and restrict the search to only infinite paths:

Another possible difference in the reported verification results can be happen when the NuSMV model contains more than one initial state. The BDD based approach relies on the reduction of LTL model checking to CTL model checking (via tableau construction). CTL model checking universally quantify over the set of fair initial states. Thus, only initial states that are fair are considered. There can be initial states that are not fair, and they are not considered. This choice can be questionable, but it is also shown by CadenceSMV. Differently, BMC based model checking does not restrict to consider only fair initial states. Thus, if there exists an initial state that is not fair and from which there is a finite path violates the fairness conditions it will find it.

NuXMV 中 check_property 和 msat_check_ltlspec_bmc 的不同结果

Different results from check_property and msat_check_ltlspec_bmc in NuXMV

model-checking

nuxmv