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

to_parity: improve remove_false_transitions

Browse source 
* spot/twaalgos/toparity.hh (remove_false_transitions): Keep it
private.
* spot/twaalgos/toparity.cc (remove_false_transitions): Do not clone
automata without false transitions, simplify the loops, and preserve
all properties.
This commit is contained in:
Alexandre Duret-Lutz 2020-04-04 16:06:51 +02:00
parent 1db319267f
commit 0a95314dca
2 changed files with 18 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

30
spot/twaalgos/toparity.cc
View file

@ -1605,23 +1605,29 @@ to_parity_options options;
std::vector<std::string>* names; std::vector<std::string>* names;
}; // car_generator }; // car_generator
}// namespace static twa_graph_ptr
remove_false_transitions(const twa_graph_ptr a)
twa_graph_ptr {
remove_false_transitions(const twa_graph_ptr a) // Do not do anything if the automaton has no false transition
{ for (auto edge : a->edges())
if (edge.cond == bddfalse)
goto doremoval;
return a;
doremoval:
auto res_ = make_twa_graph(a->get_dict()); auto res_ = make_twa_graph(a->get_dict());
res_->copy_ap_of(a); res_->copy_ap_of(a);
for (unsigned state = 0; state < a->num_states(); ++state) res_->new_states(a->num_states());
res_->new_state(); for (auto edge : a->edges())
for (unsigned state = 0; state < a->num_states(); ++state) if (edge.cond != bddfalse)
for (auto edge : a->out(state)) res_->new_edge(edge.src, edge.dst, edge.cond, edge.acc);
if (edge.cond != bddfalse)
res_->new_edge(state, edge.dst, edge.cond, edge.acc);
res_->set_init_state(a->get_init_state_number()); res_->set_init_state(a->get_init_state_number());
res_->set_acceptance(a->get_acceptance()); res_->set_acceptance(a->get_acceptance());
res_->prop_copy(a, twa::prop_set::all());
return res_; return res_;
} }
}// namespace
twa_graph_ptr twa_graph_ptr
to_parity(const twa_graph_ptr &aut, const to_parity_options options) to_parity(const twa_graph_ptr &aut, const to_parity_options options)

4
spot/twaalgos/toparity.hh
View file

@ -77,10 +77,6 @@ namespace spot
to_parity(const twa_graph_ptr &aut, to_parity(const twa_graph_ptr &aut,
const to_parity_options options = to_parity_options()); const to_parity_options options = to_parity_options());
SPOT_API twa_graph_ptr
remove_false_transitions(const twa_graph_ptr a);
/// \ingroup twa_acc_transform /// \ingroup twa_acc_transform
/// \brief Take an automaton with any acceptance condition and return an /// \brief Take an automaton with any acceptance condition and return an
/// equivalent parity automaton. /// equivalent parity automaton.