I created a generic SMV program and checked a pair of LTL properties using both check_property and msat_check_ltlspec_bmc. One property is found to be true with both commands. The other property, instead, gives a counter-example of 14 states with the first command and a single-state
counter-example with the latter command.
Q: why the second counter-example contains only one state, and how should it be interpreted?
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);
With standard LTL model checking, I get the following output:
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 <-
Instead, with msat_-based LTL model checking, I get the following output:
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
In the first case, the LTL property is checked with classic Tableau-based Model Checking. With this approach, the engine has a global view of the Finite State Machine represented in the model, and therefore it can provide a counter-example trace representing an (infinite) execution trace violating a given property.
In the second case, the LTL property is checked with Bounded Model Checking, which means that the engine advances the search by considering increasingly longer execution traces and lacks a global view of the Finite State Machine represented in the model. As a result, the counter-example returned by this engine always consists in some (finite) execution trace of minimum length.
In the given code example, the property G (!(((FlagLO = FALSE) & (tt < 5)))) IN module is already violated in the first state of the execution trace:
-> 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
Therefore, the returned solution is correct.