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;
103 SPOT_API twa_graph_ptr
107 std::vector<unsigned>* accepting_sinks =
nullptr);
108 SPOT_API twa_graph_ptr
111 std::vector<unsigned>* accepting_sinks =
nullptr);
134 SPOT_API twa_graph_ptr
136 unsigned threshold_states = 0,
137 unsigned threshold_cycles = 0);
166 SPOT_API twa_graph_ptr
168 unsigned threshold_states = 0,
169 unsigned threshold_cycles = 0,
171 const_twa_graph_ptr neg_aut =
nullptr);
Helper object to specify when an algorithm should abort its construction.
Definition: powerset.hh:48
twa_graph_ptr tgba_powerset(const const_twa_graph_ptr &aut, power_map &pm, bool merge=true, const output_aborter *aborter=nullptr, std::vector< unsigned > *accepting_sinks=nullptr)
Build a deterministic automaton, ignoring acceptance conditions.
Definition: automata.hh:27
twa_graph_ptr tba_determinize(const const_twa_graph_ptr &aut, unsigned threshold_states=0, unsigned threshold_cycles=0)
Determinize a TBA using the powerset construction.
twa_graph_ptr tba_determinize_check(const twa_graph_ptr &aut, unsigned threshold_states=0, unsigned threshold_cycles=0, formula f=nullptr, const_twa_graph_ptr neg_aut=nullptr)
Determinize a TBA and make sure it is correct.
Definition: powerset.hh:34