spot  2.3.3
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
Public Member Functions | List of all members
spot::outedge_combiner Class Reference

Helper class combine outgoing edges in alternating automata. More...

#include <spot/twaalgos/alternation.hh>

Collaboration diagram for spot::outedge_combiner:
Collaboration graph

Public Member Functions

 outedge_combiner (const twa_graph_ptr &aut)
 
bdd operator() (unsigned st)
 
void new_dests (unsigned st, bdd out) const
 

Detailed Description

Helper class combine outgoing edges in alternating automata.

The idea is that you can 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).


The documentation for this class was generated from the following file:

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Tue Apr 11 2017 13:40:04 for spot by doxygen 1.8.8