alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

print_hoa: turn the safety checks into exceptions

Browse source 
Because when those assertions fails in Python, they crash the
interpreter.

* spot/twaalgos/hoa.cc (print_hoa): Remplace assert() by throw.
This commit is contained in:
Alexandre Duret-Lutz 2017-04-07 14:11:04 +02:00
parent 0d884d4a93
commit bf99e6c24e
1 changed files with 16 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

21
spot/twaalgos/hoa.cc
View file

@ -160,11 +160,22 @@ namespace spot
is_colored = colored && (!has_state_acc || nodeadend); is_colored = colored && (!has_state_acc || nodeadend);
// If the automaton declares that it is universal or // If the automaton declares that it is universal or
// state-based, make sure that it really is. // state-based, make sure that it really is.
assert(!aut->prop_universal().is_known() || if (aut->prop_universal().is_true() && !deterministic)
deterministic == aut->prop_universal().is_true()); throw std::runtime_error("print_hoa(): automaton is not universal"
assert(!aut->prop_complete().is_known() || " but prop_universal()==true");
complete == aut->prop_complete().is_true()); if (aut->prop_universal().is_false() && deterministic)
assert(state_acc || !aut->prop_state_acc().is_true()); throw std::runtime_error("print_hoa(): automaton is universal"
" despite prop_universal()==false");
if (aut->prop_complete().is_true() && !complete)
throw std::runtime_error("print_hoa(): automaton is not complete"
" but prop_complete()==true");
if (aut->prop_complete().is_false() && complete)
throw std::runtime_error("print_hoa(): automaton is complete"
" but prop_complete()==false");
if (aut->prop_state_acc() && !state_acc)
throw std::runtime_error("print_hoa(): automaton has "
"transition-based acceptance despite"
" prop_state_acc()==true");
} }
void number_all_ap(const const_twa_graph_ptr& aut) void number_all_ap(const const_twa_graph_ptr& aut)