22 #include <spot/twa/twagraph.hh> 48 const twa_graph_ptr& aut_;
49 std::map<unsigned, int> state_to_var;
50 std::map<int, unsigned> var_to_state;
55 bdd operator()(
unsigned st);
56 void new_dests(
unsigned st, bdd out)
const;
71 unsigned states_and(
const twa_graph_ptr& aut, I begin, I end)
74 throw std::runtime_error
75 (
"state_and() expects an non-empty list of states");
77 bdd combination = bddtrue;
79 combination &= combiner(*begin++);
80 unsigned new_s = aut->new_state();
81 combiner.new_dests(new_s, combination);
87 unsigned states_and(
const twa_graph_ptr& aut,
88 const std::initializer_list<T>& il)
90 return states_and(aut, il.begin(), il.end());
103 twa_graph_ptr remove_alternation(
const const_twa_graph_ptr& aut,
104 bool named_states =
false);
Definition: automata.hh:26
Helper class combine outgoing edges in alternating automata.
Definition: alternation.hh:45