Различные результаты из check_property и msat_check_ltlspec_bmc в NuXMV

Question

Следующее свойство верно для check_property, но msat_check_ltlspec_bmc дает контрпример. Результат последнего кажется правильным. "Модуль G (((tt> = 7) -> G ((FlagLO = FALSE)))) IN". как мы можем это объяснить?

Я пробовал это с немного измененным 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

Алгоритмы проверки модели LTL на основе BDD, реализованные по причине NuSMV только о бесконечных путях. Таким образом, даже для свойства безопасности, которое делает не удерживается, генерируется лассообразный контрпример, хотя конечного пути будет достаточно. Во время проверки предполагается, что совокупность переходного отношения и отсутствие тупиков, и поиск ограничен, чтобы рассматривать только бесконечные пути, игнорируя все пути, ведущие к тупику. Таким образом, конечный путь, ведущий к тупик и фальсификация свойства не будут обнаружены.

Алгоритмы проверки ограниченной модели на основе SAT также предполагают совокупность отношения перехода и отсутствия тупиков, но они ищет контрпример для данного свойства, которое либо конечный или бесконечный. Таким образом, в отличие от модели LTL на основе BDD алгоритмы проверки, конечный путь, ведущий к тупику и фальсификация свойства будет обнаружена.

Оба алгоритма предполагают совокупность отношения перехода и отсутствие тупиков, но они специально не проверяют эти условия выполняются. Пользователь несет ответственность за выполнение эта проверка, например, выдача флага командной строки -ctt в пакетном режиме, или вызвав команду check_fsm в оболочке NuSMV.

До сих пор нет флага для отключения поиска конечного пути в рамках SAT проверка ограниченной модели. Тем не менее, добавив в смоделировать следующее справедливое условие справедливости

СПРАВЕДЛИВОЕ ИСТИНА;

алгоритмы проверки ограниченной модели перестают искать конечный путь и ограничить поиск только бесконечными путями:

Другая возможная разница в сообщенных результатах проверки может произойдет, когда модель NuSMV содержит более одного начального состояния. Подход, основанный на BDD, основан на сокращении проверки модели LTL к проверке модели CTL (посредством построения таблиц). Проверка модели CTL повсеместно количественно определить множество справедливых начальных состояний. Таким образом, только начальные состояния, которые являются справедливыми, считаются. Там может быть начальный состояния, которые несправедливы, и они не рассматриваются. Этот выбор может быть сомнительным, но это также показывает CadenceSMV. Иными словами, BMC проверка на основе модели не ограничивает рассмотрение только справедливой начальной состояния. Таким образом, если существует начальное состояние, которое не является справедливым и из которого существует конечный путь, нарушает условия справедливости его найду его.