22 #include <spot/twa/twagraph.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());
103 twa_graph_ptr remove_alternation(
const const_twa_graph_ptr& aut,
104 bool named_states =
false);
109 class SPOT_API univ_remover_state:
public state
112 std::set<unsigned> states_;
116 univ_remover_state(
const std::set<unsigned>& states);
117 univ_remover_state(
const univ_remover_state& other)
118 : states_(other.states_), is_reset_(other.is_reset_)
121 int compare(
const state* other)
const override;
122 size_t hash()
const override;
123 state* clone()
const override;
124 const std::set<unsigned>& states()
const;
125 bool is_reset()
const;
128 class SPOT_API twa_univ_remover:
public twa
132 const_twa_graph_ptr aut_;
133 std::vector<int> state_to_var_;
134 std::map<int, unsigned> var_to_state_;
138 twa_univ_remover(
const const_twa_graph_ptr& aut);
139 void allocate_state_vars();
140 const state* get_init_state()
const override;
141 twa_succ_iterator* succ_iter(
const state* s)
const override;
142 std::string format_state(
const state* s)
const override;
145 typedef std::shared_ptr<twa_univ_remover> twa_univ_remover_ptr;
164 twa_univ_remover_ptr remove_univ_otf(
const const_twa_graph_ptr& aut);
Definition: automata.hh:26