22#include <spot/twa/twagraph.hh>
23#include <spot/twaalgos/powerset.hh>
46 class SPOT_API outedge_combiner
49 const twa_graph_ptr& aut_;
50 std::map<unsigned, int> state_to_var;
51 std::map<int, unsigned> var_to_state;
54 outedge_combiner(
const twa_graph_ptr& aut);
56 bdd operator()(
unsigned st);
57 void new_dests(
unsigned st, bdd out)
const;
72 unsigned states_and(
const twa_graph_ptr& aut, I begin, I end)
75 throw std::runtime_error
76 (
"state_and() expects an non-empty list of states");
77 outedge_combiner combiner(aut);
78 bdd combination = bddtrue;
80 combination &= combiner(*begin++);
81 unsigned new_s = aut->new_state();
82 combiner.new_dests(new_s, combination);
88 unsigned states_and(
const twa_graph_ptr& aut,
89 const std::initializer_list<T>& il)
91 return states_and(aut, il.begin(), il.end());
107 twa_graph_ptr remove_alternation(
const const_twa_graph_ptr& aut,
108 bool named_states =
false,
109 const output_aborter* aborter =
nullptr);
114 class SPOT_API univ_remover_state:
public state
117 std::set<unsigned> states_;
121 univ_remover_state(
const std::set<unsigned>& states);
122 univ_remover_state(
const univ_remover_state& other)
123 : states_(other.states_), is_reset_(other.is_reset_)
126 int compare(
const state* other)
const override;
127 size_t hash()
const override;
128 state* clone()
const override;
129 const std::set<unsigned>& states()
const;
130 bool is_reset()
const;
133 class SPOT_API twa_univ_remover:
public twa
137 const_twa_graph_ptr aut_;
138 std::vector<int> state_to_var_;
139 std::map<int, unsigned> var_to_state_;
143 twa_univ_remover(
const const_twa_graph_ptr& aut);
144 void allocate_state_vars();
145 const state* get_init_state()
const override;
146 twa_succ_iterator* succ_iter(
const state* s)
const override;
147 std::string format_state(
const state* s)
const override;
150 typedef std::shared_ptr<twa_univ_remover> twa_univ_remover_ptr;
169 twa_univ_remover_ptr remove_univ_otf(
const const_twa_graph_ptr& aut);
Definition automata.hh:27