A DFA with explicit states and symbolic transitions represented in ADDs. More...

Public Member Functions
std::shared_ptr< VarMgr >	var_mgr () const
	Returns the variable manager.

std::size_t	initial_state () const
	Returns the initial state of the DFA.

std::size_t	state_count () const
	Returns the number of states in the DFA.

std::vector< std::size_t >	final_states () const
	Returns the list of indices of final states of the DFA.

std::vector< CUDD::ADD >	transition_function () const
	Returns the transition function of the DFA as a vector of ADDs. More...

void	dump_dot (const std::string &filename) const
	Saves the transition function of the DFA in a .dot file. More...

Static Public Member Functions
static ExplicitStateDfaAdd	from_dfa_mona (std::shared_ptr< VarMgr > var_mgr, const ExplicitStateDfa &explicit_dfa)
	Constructs an explicit-state DFA in ADD representation from an explicit-state DFA. More...

Detailed Description

A DFA with explicit states and symbolic transitions represented in ADDs.

Member Function Documentation

void Syft::ExplicitStateDfaAdd::dump_dot ( const std::string & filename ) const

Saves the transition function of the DFA in a .dot file.

Parameters

filename The name of the file to save the transition function to.

ExplicitStateDfaAdd Syft::ExplicitStateDfaAdd::from_dfa_mona	(	std::shared_ptr< VarMgr >	var_mgr,
		const ExplicitStateDfa &	explicit_dfa
	)

static

Constructs an explicit-state DFA in ADD representation from an explicit-state DFA.

Parameters

var_mgr	The variable manager for managing transition variables.
explicit_dfa	An explicit-state DFA.

std::vector< CUDD::ADD > Syft::ExplicitStateDfaAdd::transition_function ( ) const

Returns the transition function of the DFA as a vector of ADDs.

The ADD in index i represents the transition function for state i.

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