Как интерпретировать разницу в результатах контрольных примеров check_property & msat_check_ltlspec_bmc - PullRequest
Новая
       79

Как интерпретировать разницу в результатах контрольных примеров check_property & msat_check_ltlspec_bmc

0 голосов
/ 12 января 2019

Я создал универсальную программу SMV и проверил пару свойств LTL, используя check_property и msat_check_ltlspec_bmc. Найдено одно свойство 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 <-

Вместо этого, с проверкой модели LTL на основе msat_, я получаю следующий вывод: 

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

1 Ответ

0 голосов
/ 12 января 2019

В первом случае свойство LTL проверяется с помощью классической проверки моделей на основе таблиц. При таком подходе механизм имеет глобальное представление конечного автомата, представленного в модели, и, следовательно, он может предоставить контрпримерный след, представляющий (бесконечный) след выполнения, нарушающий данное свойство.

Во втором случае свойство 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

Следовательно, возвращаемое решение верное.

...