22 #include <spot/twa/twagraph.hh> 74 SPOT_API twa_graph_ptr
75 degeneralize(
const const_twa_graph_ptr& a,
bool use_z_lvl =
true,
76 bool use_cust_acc_orders =
false,
77 int use_lvl_cache = 1,
78 bool skip_levels =
true,
79 bool ignaccsl =
false,
80 bool remove_extra_scc =
true);
82 SPOT_API twa_graph_ptr
83 degeneralize_tba(
const const_twa_graph_ptr& a,
bool use_z_lvl =
true,
84 bool use_cust_acc_orders =
false,
85 int use_lvl_cache = 1,
86 bool skip_levels =
true,
87 bool ignaccsl =
false,
88 bool remove_extra_scc =
true);
125 SPOT_API twa_graph_ptr
127 acc_cond::mark_t todegen);
128 SPOT_API twa_graph_ptr
151 SPOT_API acc_cond::mark_t
152 is_partially_degeneralizable(
const const_twa_graph_ptr& aut,
153 bool allow_inf =
true,
154 bool allow_fin =
true,
155 std::vector<acc_cond::mark_t> forbid = {});
173 SPOT_API std::vector<acc_cond::mark_t>
175 scc_info* si =
nullptr);
179 scc_info* si =
nullptr);
Definition: automata.hh:26
void propagate_marks_here(twa_graph_ptr &aut, scc_info *si=nullptr)
Propagate marks around the automaton.
std::vector< acc_cond::mark_t > propagate_marks_vector(const const_twa_graph_ptr &aut, scc_info *si=nullptr)
Propagate marks around the automaton.