Вопросы с тегами [nuxmv]

0

голосов
0

ответ
6

Просмотры

Ошибка: Невозможно построить FSM BDD с бесконечной точностью переменных

Я только что установил nuXmv и хотел попробовать на пример выращивания счетчика целочисленным из папки примеров. Когда я пытаюсь запустить команду: build_model, я получаю сообщение об ошибке: «файл взросление встречного integer.smv: строке 30: Невозможно построить Знает ли кто, как исправить эту ошибку Спасибо заранее взросления борьбы с целым числом?. SMV файл: МОДУЛЬ главного государственный ВАРА: {s0, s1, s2, s3}; VAR C: целое число; ВАР Пт: реальный; ASSIGN инициализации (состояние): = s0; следующее (состояние): = случай, STATE = s0: S1; состояние = S1: S2; состояние = s2 и с <Пт: с2; состояние = с2 & с> = Пт: s3, состояние = s3: S1; TRUE: состояние; ESAC; INIT (с): = 0; следующая (с ): = (состояние = с2 и в следующем (состояние) = с2) (с + 1) :( 0); INIT (Lim): = 2; следующий (Lim): = (состояние = s3 & следующим (состояние) = ? s1) (Lim + 1) :( Пт); INVARSPEC с <3; INVARSPEC с <4; INVARSPEC с <5; INVARSPEC с <6; INVARSPEC с <20; LTLSPEC GF (состояние = s3);
Alex
1

голосов
1

ответ
0

Просмотры

Different results from check_property and msat_check_ltlspec_bmc in NuXMV

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 State: 1.2 State: 1.3 State: 1.4 State: 1.5 State: 1.6 State: 1.7 State: 1.8 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 ##########################################################
Ranjana N
3

голосов
0

ответ
114

Просмотры

Внутреннее представление перечислимых типов в NuSMV / NuXMV

почему существует значительная выпадающая производительность при представляющем 16-разрядном целом числе в качестве переменной Intervall (-32768..32767) по сравнению с фиксированной длиной битовых массивов? Проверка предварительно обработанная модель NuSMV / NuXMV можно наблюдать, что типы интервалов преобразуются в перечисления. Статистику BDD однако не показывает соответствующую informaton.
optional