21#include <spot/twa/twagraph.hh>
22#include <spot/twaalgos/powerset.hh>
45 class SPOT_API outedge_combiner
48 const twa_graph_ptr& aut_;
49 std::map<unsigned, int> state_to_var;
50 std::map<int, unsigned> var_to_state;
53 outedge_combiner(
const twa_graph_ptr& aut);
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");
76 outedge_combiner combiner(aut);
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());
110 twa_graph_ptr remove_alternation(
const const_twa_graph_ptr& aut,
111 bool named_states =
false,
112 const output_aborter* aborter =
nullptr,
113 bool raise_if_too_many_sets =
true);
118 class SPOT_API univ_remover_state:
public state
121 std::set<unsigned> states_;
125 univ_remover_state(
const std::set<unsigned>& states);
126 univ_remover_state(
const univ_remover_state& other)
127 : states_(other.states_), is_reset_(other.is_reset_)
130 int compare(
const state* other)
const override;
131 size_t hash()
const override;
132 state* clone()
const override;
133 const std::set<unsigned>& states()
const;
134 bool is_reset()
const;
137 class SPOT_API twa_univ_remover:
public twa
141 const_twa_graph_ptr aut_;
142 std::vector<int> state_to_var_;
143 std::map<int, unsigned> var_to_state_;
147 twa_univ_remover(
const const_twa_graph_ptr& aut);
148 void allocate_state_vars();
149 const state* get_init_state()
const override;
150 twa_succ_iterator* succ_iter(
const state* s)
const override;
151 std::string format_state(
const state* s)
const override;
154 typedef std::shared_ptr<twa_univ_remover> twa_univ_remover_ptr;
173 twa_univ_remover_ptr remove_univ_otf(
const const_twa_graph_ptr& aut);
Definition: automata.hh:26