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

#include <spot/twaalgos/alternation.hh>

Collaboration diagram for spot::outedge_combiner:

Public Member Functions
	outedge_combiner (const twa_graph_ptr &aut)
	Construct from an alternating automaton.

bdd	operator() (unsigned st)
	Combine outgoing edges of state st.

void	new_dests (unsigned st, bdd out) const
	Compute new destinations for state st under condition out.

Detailed Description

Helper class to combine outgoing edges in alternating automata.

The idea is that you can call the operator() on some state to get a BDD representation of its outgoing edges (labels and destinations, but not acceptance marks). The BDD representation of different states can be 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 groups of destination states (in that case the conjunction of all those states are taken).

Constructor & Destructor Documentation

◆ outedge_combiner()

spot::outedge_combiner::outedge_combiner ( const twa_graph_ptr & aut )

Construct from an alternating automaton.

Member Function Documentation

◆ new_dests()

void spot::outedge_combiner::new_dests	(	unsigned	st,
		bdd	out
	)		const

Compute new destinations for state st under condition out.

Referenced by spot::states_and().

◆ operator()()

bdd spot::outedge_combiner::operator() ( unsigned st )

Combine outgoing edges of state st.

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

spot/twaalgos/alternation.hh