21#include <spot/twa/twagraph.hh>
40 SPOT_API twa_graph_ptr
split_edges(
const const_twa_graph_ptr& aut);
45 template<
bool subsumed>
49 : labels_(labels), cond_(cond)
55 std::vector<bdd>::const_iterator pos_;
56 std::vector<bdd>
const& labels_;
60 iterator(
const std::vector<bdd>& labels, bdd cond)
61 : labels_(labels), cond_(cond)
63 pos_ = labels_.begin();
79 while (pos_ != labels_.end() &&
80 ((subsumed && !bdd_implies(*pos_, cond_))
81 || (!subsumed && (*pos_ & cond_) == bddfalse)))
93 bool operator==(
const iterator& other)
const
95 return pos_ == other.pos_;
98 bool operator!=(
const iterator& other)
const
100 return pos_ != other.pos_;
103 bool operator==(std::vector<bdd>::const_iterator pos)
const
108 bool operator!=(std::vector<bdd>::const_iterator pos)
const
119 std::vector<bdd>::const_iterator end()
const
121 return labels_.end();
125 const std::vector<bdd>& labels_;
167 unsigned long max_label);
194 return {basis_, label};
207 return {basis_, label};
211 unsigned basis_size()
const
213 return basis_.size();
216 const std::vector<bdd>& basis()
const
222 std::vector<bdd> basis_{bddtrue};
223 std::set<formula> aps_;
separate edges so that their labels are disjoint
Definition: split.hh:146
bool add_to_basis(const const_twa_graph_ptr &aut, unsigned long max_label)
add label(s) to a basis
edge_separator_filter< true > separate_implying(bdd label)
Separate a label.
Definition: split.hh:192
twa_graph_ptr separate_implying(const const_twa_graph_ptr &aut)
Separate an automaton.
void add_to_basis(bdd label)
add label(s) to a basis
void add_to_basis(const const_twa_graph_ptr &aut)
add label(s) to a basis
twa_graph_ptr separate_compat(const const_twa_graph_ptr &aut)
Separate an automaton.
edge_separator_filter< false > separate_compat(bdd label)
Separate a label.
Definition: split.hh:205
twa_graph_ptr split_edges(const const_twa_graph_ptr &aut)
transform edges into transitions
twa_graph_ptr separate_edges(const const_twa_graph_ptr &aut)
Make edge labels disjoints.
Definition: automata.hh:26