The following property is true with check_property but msat_check_ltlspec_bmc gives counterexample. The result of latter one seems to be correct."G (((tt >= 7) -> G ((FlagLO = FALSE)))) IN module". how do we explain this?
I tried this with slightly changed smv file. Was trying to check the existence pattern based LTL property. Check_fsm result was not run earlier. This gives a deadlock. In that case msat_check.... result seems incorrect. Now which one is correct? And what should be the correct method of verifying the model? Need to work with reals, thus trying msat commands.
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);
This is the output of 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
This is the output of a normal LTL check_property call:
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
This is the output of 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
##########################################################
The output of check_fsm tells you where the problem is: there are deadlock states in your FSM.
See 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.