spot
2.4.1
|
Helper class combine outgoing edges in alternating automata. More...
#include <spot/twaalgos/alternation.hh>
Public Member Functions | |
outedge_combiner (const twa_graph_ptr &aut) | |
bdd | operator() (unsigned st) |
void | new_dests (unsigned st, bdd out) const |
Helper class combine outgoing edges in alternating automata.
The idea is that you can call the operator() on some state to get an BDD representation of its outgoing edges (labels and destinations, but not acceptance marks). The BDD representation of different states can combined using & or | to build a new representation of some outgoing edges that can be attached to some state with new_dests. The use of BDDs helps removing superfluous edges.
Beware that new_dests() just appends the transitions to the supplied state, it does not remove existing ones.
operator() can be called on states with universal branching (that's actually the point), and can be called on state number that designate groupes of destination states (in that case the conjunction of all those states are taken).