如何解释 check_property & msat_check_ltlspec_bmc 反例结果的差异

Question

我创建了一个通用的 SMV 程序并使用 check_property 和 msat_check_ltlspec_bmc 检查了一对 LTL 属性。一个属性被发现是 true 与两个命令。相反，另一个属性给出了第一个命令和一个单一状态的 14 状态的反例后一个命令的反例。

问：为什么第二个反例只有一个状态，应该如何解释？

MODULE Seq_19(T_41, T_41_PRESENT)
    VAR
            _next_t : { Init_46_idle, LO_51_idle, BO_73_idle, State_120_idle, LOSense_118, BOSense_115, TransitionSegment_125 };
        FlagLO : boolean;
        FlagBO : boolean;
        tt : -256..255;

    DEFINE
        LOOut_68 := 
            case
                (_next_t = LOSense_118) : TRUE;
                TRUE : FALSE;
            esac;
        BOOut_84 := 
            case
                (_next_t = BOSense_115) : 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;
                TRUE : FALSE;
            esac;
        guard_LOSense_118 := (tt > 5);
        guard_BOSense_115 := (tt > 10);
        guard_TransitionSegment_125 := TRUE;

    ASSIGN
        init(_next_t) := { Init_46_idle, LOSense_118 };
        init(FlagLO) := FALSE;
        init(FlagBO) := FALSE;
        init(tt) := 0;

    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 };
    TRANS _next_t in { BO_73_idle, BOSense_115 }
         -> 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 = Init_46_idle)
         -> next(tt) = (tt + 1) &
            next(FlagLO) = FlagLO &
            next(FlagBO) = FlagBO;
    TRANS (_next_t = LO_51_idle)
         -> next(tt) = (tt + 1) &
            next(FlagLO) = FlagLO &
            next(FlagBO) = FlagBO;
    TRANS (_next_t = BO_73_idle)
         -> next(tt) = (tt + 1) &
            next(FlagLO) = FlagLO &
            next(FlagBO) = FlagBO;
    TRANS (_next_t = State_120_idle)
         -> next(FlagLO) = FlagLO &
            next(FlagBO) = FlagBO &
            next(tt) = tt;
    TRANS (_next_t = LOSense_118)
         -> next(FlagLO) = TRUE &
            next(tt) = (tt + 1) &
            next(FlagBO) = FlagBO;
    TRANS (_next_t = BOSense_115)
         -> next(FlagBO) = TRUE &
            next(tt) = (tt + 1) &
            next(FlagLO) = FlagLO;
    TRANS (_next_t = TransitionSegment_125)
         -> next(FlagLO) = FlagLO &
            next(FlagBO) = FlagBO &
            next(tt) = tt;

    INVAR ((_next_t = LOSense_118) -> guard_LOSense_118)
    INVAR ((_next_t = BOSense_115) -> guard_BOSense_115)
    INVAR ((_next_t = TransitionSegment_125) -> guard_TransitionSegment_125)
    INVAR ((_next_t = Init_46_idle) -> !(guard_LOSense_118))
    INVAR ((_next_t = LO_51_idle) -> !(guard_BOSense_115))
    INVAR ((_next_t = BO_73_idle) -> !(guard_TransitionSegment_125))
    INVAR ((_next_t = State_120_idle) -> TRUE)

   MODULE main
    VAR
        T_41 : -256..255;
        T_41_PRESENT : boolean;
        module : Seq_19(T_41,T_41_PRESENT);

通过标准 LTL 模型检查，我得到以下输出：

nuXmv > read_model -i Seq19-1210063772855777412.smv
nuXmv > go
nuXmv > check_property -l -p "G (!(((FlagLO = TRUE) & (tt < 5)))) IN module"
-- specification  G !(FlagLO = TRUE & tt < 5) IN module is true
nuXmv > check_property -l -p "G (!(((FlagLO = FALSE) & (tt < 5)))) IN module"
-- specification  G !(FlagLO = FALSE & tt < 5) IN module is false
-- as demonstrated by the following execution sequence
Trace Description: LTL 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.guard_TransitionSegment_125 = TRUE
    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 <-
    module.tt = 1
  -> State: 1.3 <-
    module.tt = 2
  -> State: 1.4 <-
    module.tt = 3
  -> State: 1.5 <-
    module.tt = 4
  -> State: 1.6 <-
    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
  -> State: 1.9 <-
    module.tt = 8
  -> State: 1.10 <-
    module.tt = 9
  -> State: 1.11 <-
    module.tt = 10
  -> State: 1.12 <-
    module._next_t = BOSense_115
    module.tt = 11
    module.guard_BOSense_115 = TRUE
    module.BOOut_84_PRESENT = TRUE
    module.BOOut_84 = TRUE
  -> State: 1.13 <-
    module._next_t = TransitionSegment_125
    module.FlagBO = TRUE
    module.tt = 12
    module.BOOut_84_PRESENT = FALSE
    module.BOOut_84 = FALSE
  -- Loop starts here
  -> State: 1.14 <-
    module._next_t = State_120_idle
  -> State: 1.15 <-

相反，使用基于 msat_ 的 LTL 模型检查，我得到以下输出：

nuXmv > reset
nuXmv > read_model -i Seq19-1210063772855777412.smv
nuXmv > go_msa
nuXmv > msat_check_ltlspec_bmc -p "G (!(((FlagLO = TRUE) & (tt < 5)))) 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
-- no counterexample found with bound 7
-- no counterexample found with bound 8
-- no counterexample found with bound 9
-- no counterexample found with bound 10
nuXmv > msat_check_ltlspec_bmc -p "G (!(((FlagLO = FALSE) & (tt < 5)))) IN module"
-- specification  G !(FlagLO = FALSE & tt < 5) 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.guard_TransitionSegment_125 = TRUE
    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

Answer 1

在第一种情况下，LTL 属性使用经典的基于 Tableau 的模型检查进行检查。通过这种方法，引擎具有模型中表示的有限状态机的全局视图，因此它可以提供一个反例跟踪，表示违反给定属性.[=12= 的（无限）执行跟踪]

在第二种情况下，LTL 属性使用有界模型检查进行检查，这意味着引擎通过考虑越来越长的执行跟踪来推进搜索，并且缺乏对有限状态机表示的全局视图该模型。因此，该引擎返回的反例总是包含一些（有限的）最小长度的执行轨迹。

在给定的代码示例中，属性 G (!(((FlagLO = FALSE) & (tt < 5)))) IN module 在执行跟踪的第一个状态中已经被违反：

  -> 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.guard_TransitionSegment_125 = TRUE
    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

因此，返回的解是正确的。

如何解释 check_property & msat_check_ltlspec_bmc 反例结果的差异

How to interpret the differnce in results of check_property & msat_check_ltlspec_bmc counterexamples

model-checking

nuxmv