28 #include <spot/twa/twagraph.hh> 35 typedef std::set<unsigned> power_state;
36 std::vector<power_state> map_;
39 states_of(
unsigned s)
const 51 mutable bool reason_is_states_;
54 unsigned max_edges = ~0
U)
55 : max_states_(max_states), max_edges_(max_edges)
59 unsigned max_states()
const 64 unsigned max_edges()
const 69 bool too_large(
const const_twa_graph_ptr& aut)
const 71 bool too_many_states = aut->num_states() > max_states_;
72 if (!too_many_states && (aut->num_edges() <= max_edges_))
75 reason_is_states_ = too_many_states;
79 std::ostream& print_reason(std::ostream&)
const;
98 SPOT_API twa_graph_ptr
102 SPOT_API twa_graph_ptr
127 SPOT_API twa_graph_ptr
128 tba_determinize(
const const_twa_graph_ptr& aut,
129 unsigned threshold_states = 0,
130 unsigned threshold_cycles = 0);
159 SPOT_API twa_graph_ptr
160 tba_determinize_check(
const twa_graph_ptr& aut,
161 unsigned threshold_states = 0,
162 unsigned threshold_cycles = 0,
164 const_twa_graph_ptr neg_aut =
nullptr);
Definition: automata.hh:26
twa_graph_ptr tgba_powerset(const const_twa_graph_ptr &aut, const output_aborter *aborter=nullptr)
Build a deterministic automaton, ignoring acceptance conditions.
Helper object to specify when an algorithm should abort its construction.
Definition: powerset.hh:47
Definition: powerset.hh:33