TODO:

Should state_map_t have type HashMap< Key , ref_ptr<State> > This allows for automatic collection of States via HashMap State objects can escape the WFA (.

Public Types
enum	query_t { INORDER, REVERSE, MAX }
	query_t determines how the weights are extended during path_summary. More...
typedef wali::HashMap< KeyPair, TransSet >	kp_map_t
typedef wali::HashMap< Key, State * >	state_map_t
typedef wali::HashMap< Key, TransSet >	eps_map_t
typedef std::set< State *, State >	StateSet_t
typedef wali::HashMap< Key, StateSet_t >	PredHash_t
Public Member Functions
	WFA (query_t q=INORDER)
	WFA (const WFA &rhs)
WFA &	operator= (const WFA &rhs)
virtual	~WFA ()
virtual void	clear ()
	Remove all transitions from the WFA.
Key	set_initial_state (Key key)
	set initial state
Key	setInitialState (Key key)
	set initial state
Key	initial_state () const
	Return the initial state.
Key	getInitialState () const
	Return the initial state.
bool	isInitialState (Key key) const
	Test if param key is the initial state.
void	add_final_state (Key key)
	Add parameter key to the set of final states.
void	addFinalState (Key key)
	Add parameter key to the set of final states.
bool	isFinalState (Key key) const
	Return true if parameter key is a final state.
query_t	setQuery (query_t newQuery)
	Set the WFA query mode.
query_t	getQuery () const
size_t	getGeneration () const
void	setGeneration (size_t g)
	Set the generation to have the value of param g.
virtual sem_elem_t	getSomeWeight () const
	Get a weight from the WFA.
virtual void	addTrans (Key p, Key g, Key q, sem_elem_t se)
	Add transition (p,g,q) to the WFA.
virtual void	addTrans (ITrans *t)
	Add Trans t to the WFA.
virtual void	erase (Key from, Key stack, Key to)
	erase Trans
virtual bool	eraseState (Key q)
	erase State q and all of its outgoing transitions It does not remove incoming transitions -- *that has to be done by the client*.
virtual bool	find (Key p, Key g, Key q, Trans &t)
	return true if transition matching (p,g,q) exists and copy that transition into the ref parameter t
virtual void	for_each (TransFunctor &tf)
	invoke TransFunctor tf on each Trans
virtual void	for_each (ConstTransFunctor &tf) const
	invoke ConstTransFunctor on each Trans
virtual WFA	intersect (WFA &fa)
	Intersect this with parameter fa.
virtual void	intersect (WFA &fa, WFA &dest)
	Intersect this with parameter fa.
WFA	intersect (WeightMaker &wmaker, WFA &fa)
	Intersect this with parameter fa and return the result by value.
virtual void	intersect (WeightMaker &wmaker, WFA &fa, WFA &dest)
	Intersect this with parameter fa.
virtual void	path_summary ()
	Performs path summary.
virtual regex::regex_t	toRegex ()
	Computes a regular expression for the automaton.
virtual void	path_summary (Worklist< State > &wl)
	Performs path summary with the specified Worklist.
virtual void	path_summary (sem_elem_t wt)
	Performs path summary.
virtual void	prune ()
	Prunes the WFA.
virtual void	filter (Key stk)
	Intersects the WFA with <init_state, (stk ^*)> that essentially removes transitions and calls prune.
virtual void	filter (std::set< Key > &stkset)
	Intersects the WFA with { <init_state, (stk ^*)> \| stk stkset } This essentially removes transitions and calls prune.
virtual void	duplicateStates (std::set< Key > &st, WFA &output) const
	For every state s st, rename it to s'.
virtual std::ostream &	print (std::ostream &) const
	Write the WFA to the std::ostream parameter, implements Printable::print.
virtual std::ostream &	print_dot (std::ostream &o, bool print_weights=false) const
	Print WFA in dot format.
virtual std::ostream &	marshall (std::ostream &o) const
	marshall WFA in XML
virtual std::ostream &	marshallState (std::ostream &o, Key key) const
ITrans *	insert (ITrans *tnew)
	inserts tnew into the WFA
TransSet	match (Key p, Key y)
	Returns a TransSet containing all transitions matching (p,y,?) in the WFA.
void	addState (Key key, sem_elem_t zero)
	Create a State * for the key Key.
const State *	getState (Key name) const
State *	getState (Key name)
const std::set< Key > &	getStates () const
const std::set< Key > &	getFinalStates () const
size_t	numStates () const
Static Public Attributes
static const std::string	XMLTag
static const std::string	XMLQueryTag
static const std::string	XMLInorderTag
static const std::string	XMLReverseTag
Protected Member Functions
void	setupFixpoint (Worklist< State > &wl, PredHash_t &preds)
	setupFixpoint clears each states markable flag and sets the states weight to zero
void	setupFixpoint (Worklist< State > &wl, PredHash_t &preds, sem_elem_t wtFinal)
	setupFixpoint clears each states markable flag and sets the states weight to zero, and weight of final states to wtFinal (or ONE if NULL)
virtual ITrans *	find (Key p, Key g, Key q)
ITrans *	eraseTransFromMaps (Key from, Key stack, Key to)
	Erases the specified Trans(from,stack,to) from the kpmap and epsmap.
ITrans *	eraseTransFromKpMap (Key from, Key stack, Key to)
	Erases the specified Trans(from,stack,to) from the kpmap.
ITrans *	eraseTransFromKpMap (ITrans *terase)
ITrans *	eraseTransFromEpsMap (ITrans *terase)
	Erases the specified Trans(from,stack,to) from the epsmap.
bool	eraseState (State *state)
	Erases the State 'state' from the WFA and all transitions that go to or from the State.
virtual void	path_summary (Worklist< State > &wl, sem_elem_t wt)
	Performs path summary with the specified Worklist Initializes the weight on the final state to wt (can be useful for efficiency in some cases).
regex::regex_t	TarjanBasicRegex ()
	Uses Tarjan's algorithm to build a regular expression for this WFA.
Protected Attributes
kp_map_t	kpmap
state_map_t	state_map
	< map from KeyPair to list of trans
eps_map_t	eps_map
	< map from key to State
Key	init_state
	< map from "to state" to list of eps trans ending in "to state"
std::set< Key >	F
	< initial state of WFA
std::set< Key >	Q
	< set of final states
query_t	query
	< set of all states
size_t	generation
	< determine the extend order for path_summary
Friends
class	::wali::wpds::WPDS
class	::wali::wpds::DebugWPDS
class	::wali::wpds::ewpds::EWPDS
class	::wali::wpds::fwpds::FWPDS
class	::wali::wpds::fwpds::SWPDS

Detailed Description

TODO:

Should state_map_t have type HashMap< Key , ref_ptr<State> > This allows for automatic collection of States via HashMap State objects can escape the WFA (.

See also:: WPDS).

Member Typedef Documentation

typedef wali::HashMap< KeyPair, TransSet > wali::wfa::WFA::kp_map_t

typedef wali::HashMap< Key , State * > wali::wfa::WFA::state_map_t

typedef wali::HashMap< Key , TransSet > wali::wfa::WFA::eps_map_t

typedef std::set< State*,State > wali::wfa::WFA::StateSet_t

typedef wali::HashMap< Key,StateSet_t > wali::wfa::WFA::PredHash_t

Member Enumeration Documentation

enum wali::wfa::WFA::query_t

query_t determines how the weights are extended during path_summary.

INORDER is the normal each state's weight is the combine of all outgoing transitions's weights extended by the "to" state. REVERSE reverses this. INORDER corresponds to a prestar query while REVERSE corresponds to a poststar query when used with WPDS

Enumerator:

INORDER
REVERSE
MAX

Constructor & Destructor Documentation

wali::wfa::WFA::WFA ( query_t q = INORDER )

References MAX, query, and wali::waliErr.

wali::wfa::WFA::WFA ( const WFA & rhs )

References operator=().

wali::wfa::WFA::~WFA ( ) [virtual]

References clear().

Member Function Documentation

WFA & wali::wfa::WFA::operator= ( const WFA & rhs )

References addState(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::begin(), clear(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), F, for_each(), generation, init_state, query, and state_map.

Referenced by WFA().

void wali::wfa::WFA::clear ( ) [virtual]

Remove all transitions from the WFA.

Reimplemented in wali::wfa::epr::EPA.

References wali::HashMap< Key, Data, HashFunc, EqualFunc >::begin(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::clear(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), eps_map, F, for_each(), init_state, kpmap, Q, and state_map.

Referenced by intersect(), operator=(), wali::wpds::fwpds::SWPDS::poststar(), and ~WFA().

Key wali::wfa::WFA::set_initial_state ( Key key )

set initial state

A WFA has 1 initial state. This method will set it to the key parameter

Parameters:

key

the key for the desired initial state

Returns:: Key that is the old initial stat

References setInitialState().

Referenced by opennwa::query::getSomeAcceptedWordInternal().

Key wali::wfa::WFA::setInitialState ( Key key )

set initial state

A WFA has 1 initial state. This method will set it to the key parameter

Parameters:

key

the key for the desired initial state

Returns:: Key that is the old initial stat

References init_state.

Referenced by opennwa::Nwa::_private_isEmpty_(), wali::wpds::WPDS::constructCFG(), duplicateStates(), intersect(), wali::wpds::fwpds::SWPDS::poststar(), wali::wpds::fwpds::SWPDS::preprocess(), wali::wpds::fwpds::SWPDS::prestar(), and set_initial_state().

Key wali::wfa::WFA::initial_state ( ) const

Return the initial state.

Returns:: Key for the initial state

References init_state.

Referenced by intersect().

Key wali::wfa::WFA::getInitialState ( ) const

Return the initial state.

Returns:: Key for the initial state

References init_state.

Referenced by wali::wfa::epr::EPA::apply(), duplicateStates(), filter(), intersect(), wali::wpds::fwpds::SWPDS::poststar(), wali::wpds::fwpds::SWPDS::prestar(), prune(), and TarjanBasicRegex().

bool wali::wfa::WFA::isInitialState ( Key key ) const

Test if param key is the initial state.

Returns:: true if key == WFA::initial_state()

References init_state.

Referenced by marshallState(), and print_dot().

void wali::wfa::WFA::add_final_state ( Key key )

Add parameter key to the set of final states.

References F.

Referenced by opennwa::query::getSomeAcceptedWordInternal().

void wali::wfa::WFA::addFinalState ( Key key )

Add parameter key to the set of final states.

References F.

Referenced by opennwa::Nwa::_private_isEmpty_(), duplicateStates(), intersect(), wali::wpds::fwpds::SWPDS::poststar(), and wali::wpds::fwpds::SWPDS::prestar().

bool wali::wfa::WFA::isFinalState ( Key key ) const

Return true if parameter key is a final state.

References F.

Referenced by marshallState(), print_dot(), and setupFixpoint().

WFA::query_t wali::wfa::WFA::setQuery ( WFA::query_t newQuery )

Set the WFA query mode.

Returns:: the old query mode

References query.

Referenced by intersect(), wali::wpds::fwpds::SWPDS::poststar(), and wali::wpds::fwpds::SWPDS::prestar().

WFA::query_t wali::wfa::WFA::getQuery ( ) const

Returns:: WFA query mode

The query mode effects how weights are extended during path summary.

See also:: WFA::query_t

References query.

Referenced by intersect().

size_t wali::wfa::WFA::getGeneration ( ) const

Returns:: The current generation

Each WFA keeps a generation, which is the number of times a reachability query has been invoked on the WFA.

References generation.

Referenced by wali::wpds::WPDS::constructCFG(), duplicateStates(), wali::wpds::WPDS::gen_state(), wali::wpds::fwpds::SWPDS::poststar(), wali::wpds::fwpds::SWPDS::preprocess(), wali::wpds::fwpds::SWPDS::prestar(), and wali::graph::SummaryGraph::summaryPoststar().

void wali::wfa::WFA::setGeneration ( size_t g )

Set the generation to have the value of param g.

Returns:: void

References generation.

Referenced by wali::wpds::WPDS::constructCFG(), duplicateStates(), wali::wpds::fwpds::SWPDS::poststar(), wali::wpds::fwpds::SWPDS::preprocess(), and wali::wpds::fwpds::SWPDS::prestar().

sem_elem_t wali::wfa::WFA::getSomeWeight ( ) const [virtual]

Get a weight from the WFA.

This is to get hold of the weight domain class

See also:: sem_elem_t

Returns:: a weight on some transition in the WFA

References wali::wfa::TransSet::begin(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::begin(), wali::wfa::TransSet::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), and kpmap.

void wali::wfa::WFA::addTrans	(	Key	p,
		Key	g,
		Key	q,
		sem_elem_t	se
	)			`[virtual]`

Add transition (p,g,q) to the WFA.

add trans (p,g,q,se) to WFA Default creates a basic Trans object.

See also:: Key; sem_elem_t

Referenced by opennwa::Nwa::_private_isEmpty_(), wali::wpds::WPDS::constructCFG(), opennwa::query::getSomeAcceptedWordInternal(), intersect(), wali::wpds::WPDS::operator()(), wali::wpds::ewpds::EWPDS::operator()(), wali::wpds::fwpds::SWPDS::preprocess(), and wali::graph::SummaryGraph::summaryPoststar().

void wali::wfa::WFA::addTrans ( ITrans * t ) [virtual]

Add Trans t to the WFA.

add ITrans*t to WFA Takes care of adding states and calling insert.

See also:: wali::wfa::Trans

This method (actually insert) assumes ownership of the memory pointed to by the ITrans* t.

References insert().

void wali::wfa::WFA::erase	(	Key	from,
		Key	stack,
		Key	to
	)			`[virtual]`

erase Trans

Removes Trans (from,stack,to) from the WFA if it exists.

References wali::wfa::State::eraseTrans(), eraseTransFromMaps(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::find(), and state_map.

Referenced by filter(), and prune().

bool wali::wfa::WFA::eraseState ( Key q ) [virtual]

erase State q and all of its outgoing transitions It does not remove incoming transitions -- that has to be done by the client.

This does not delete the wfa::State object. The destructor will take care of reclaiming memory.

Returns:: true if it was sucessful

References wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::find(), and state_map.

Referenced by prune().

bool wali::wfa::WFA::find	(	Key	p,
		Key	g,
		Key	q,
		Trans &	t
	)			`[virtual]`

return true if transition matching (p,g,q) exists and copy that transition into the ref parameter t

If a Trans matching (p,g,q) exists then it is copied into the passed in reference "Trans & t". This way the user is not given and handle to the WFA's internal Trans * pointer and deleting all transitions associated with this WFA when it is deleted is safe. However, because the weight of this transition is a sem_elem_t (ref_ptr< SemElem >) modifying the weight from the Trans & t will result in modification of the weight on the interal Trans * object.

Returns:: bool true if transition matching (p,g,q) exists

See also:: Trans; SemElem; sem_elem_t

Referenced by wali::wfa::epr::EPA::apply().

void wali::wfa::WFA::for_each ( TransFunctor & tf ) [virtual]

invoke TransFunctor tf on each Trans

References wali::HashMap< Key, Data, HashFunc, EqualFunc >::begin(), wali::wfa::TransSet::each(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), wali::wfa::State::getTransSet(), and state_map.

Referenced by opennwa::Nwa::_private_isEmpty_(), clear(), duplicateStates(), intersect(), marshall(), operator=(), wali::wpds::fwpds::FWPDS::poststarIGR(), wali::wpds::fwpds::FWPDS::prestar(), print(), print_dot(), and prune().

void wali::wfa::WFA::for_each ( ConstTransFunctor & tf ) const [virtual]

invoke ConstTransFunctor on each Trans

References wali::HashMap< Key, Data, HashFunc, EqualFunc >::begin(), wali::wfa::TransSet::each(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), wali::wfa::State::getTransSet(), and state_map.

WFA wali::wfa::WFA::intersect ( WFA & fa ) [virtual]

Intersect this with parameter fa.

This is a wrapper for intersect( WeightMaker&,WFA& ) that passes the WeightMaker KeepBoth.

See also:: wali::wfa::WeightMaker; wali::wfa::KeepBoth

Intersect this with parameter fa. This is a wrapper for intersect( WeightMaker&,WFA& ) that passes the WeightMaker KeepBoth.

See also:: WeightMaker

Referenced by opennwa::Nwa::_private_isEmpty_(), wali::wfa::epr::EPA::buildEPA(), and intersect().

void wali::wfa::WFA::intersect	(	WFA &	fa,
		WFA &	dest
	)			`[virtual]`

Intersect this with parameter fa.

This is a wrapper for intersect( WeightMaker&,WFA&,WFA& ) that passes the WeightMaker KeepBoth. Result is stored in dest.

See also:: wali::wfa::WeightMaker; wali::wfa::KeepBoth

References intersect().

WFA wali::wfa::WFA::intersect	(	WeightMaker &	wmaker,
		WFA &	fa
	)

Intersect this with parameter fa and return the result by value.

The parameter WeightMaker determines how intersection should join the weights on matching transitions.

See also:: wali::wfa::WeightMaker

References intersect().

void wali::wfa::WFA::intersect	(	WeightMaker &	wmaker,
		WFA &	fa,
		WFA &	dest
	)			`[virtual]`

Intersect this with parameter fa.

The result is stored in parameter dest. Parameter dest is cleared before any results are stored. The parameter WeightMaker determines how intersection should join the weights on matching transitions.

NOTE: For now this means (dest != this) && (dest != fa).

References addFinalState(), addState(), addTrans(), wali::wfa::TransSet::begin(), wali::wfa::StackHasher::begin(), clear(), wali::wfa::TransSet::end(), wali::wfa::StackHasher::end(), F, for_each(), wali::wfa::ITrans::from(), getInitialState(), wali::getKey(), getQuery(), getState(), initial_state(), wali::wfa::WeightMaker::make_weight(), setInitialState(), setQuery(), wali::wfa::ITrans::stack(), wali::wfa::StackHasher::stackmap, wali::wfa::ITrans::to(), wali::waliErr, and wali::wfa::State::weight().

void wali::wfa::WFA::path_summary ( ) [virtual]

Performs path summary.

Simply calls the path_summary with the default Worklist provided by WALi.

Referenced by opennwa::query::getSomeAcceptedWordInternal(), and path_summary().

regex::regex_t wali::wfa::WFA::toRegex ( ) [virtual]

Computes a regular expression for the automaton.

The regex, when evaluated, produces a weight that is equal to calling path_summary and then getting the weight on the initial state. I.e.,

fa.toRegex().solve(); <==> fa.path_summary(); fa.getState( fa.getInitialState() )->weight();

References TarjanBasicRegex().

void wali::wfa::WFA::path_summary ( Worklist< State > & wl ) [virtual]

Performs path summary with the specified Worklist.

References path_summary().

void wali::wfa::WFA::path_summary ( sem_elem_t wt ) [virtual]

Performs path summary.

Simply calls the path_summary with the default Worklist provided by WALi. Initializes the weight on the final state to wt (can be useful for efficiency in some cases)

References path_summary().

void wali::wfa::WFA::prune ( ) [virtual]

Prunes the WFA.

This removes any transitions that are not in the (getInitialState(),F) chop.

References wali::wfa::TransSet::begin(), wali::wfa::TransSet::clear(), wali::DefaultWorklist< T >::empty(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), wali::wfa::TransSet::end(), wali::wfa::TransSet::erase(), erase(), eraseState(), eraseTransFromEpsMap(), eraseTransFromKpMap(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::find(), for_each(), FOR_EACH_FINAL_STATE, FOR_EACH_STATE, wali::wfa::ITrans::from(), wali::DefaultWorklist< T >::get(), getInitialState(), getState(), wali::wfa::State::getTransSet(), wali::wfa::State::name(), wali::DefaultWorklist< T >::put(), setupFixpoint(), wali::wfa::ITrans::stack(), wali::wfa::State::tag, wali::wfa::ITrans::to(), and wali::wfa::TransZeroWeight::zeroWeightTrans.

Referenced by opennwa::Nwa::_private_isEmpty_(), wali::wfa::epr::EPA::buildEPA(), and filter().

void wali::wfa::WFA::filter ( Key stk ) [virtual]

Intersects the WFA with <init_state, (stk ^*)> that essentially removes transitions and calls prune.

void wali::wfa::WFA::filter ( std::set< Key > & stkset ) [virtual]

Intersects the WFA with { <init_state, (stk ^*)> | stk stkset } This essentially removes transitions and calls prune.

References wali::wfa::State::begin(), wali::wfa::State::end(), erase(), wali::wfa::ITrans::from(), getInitialState(), getState(), kpmap, prune(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::size(), wali::wfa::ITrans::stack(), and wali::wfa::ITrans::to().

void wali::wfa::WFA::duplicateStates	(	std::set< Key > &	st,
		WFA &	output
	)			const `[virtual]`

For every state s st, rename it to s'.

Then add epsilon transition from s to s' and perform the epsilon closure. This uses WFA::getGeneration() to produce the renamed states. Returns the result in "output"

References addFinalState(), F, for_each(), getGeneration(), getInitialState(), wali::getKey(), setGeneration(), and setInitialState().

std::ostream & wali::wfa::WFA::print ( std::ostream & o ) const [virtual]

Write the WFA to the std::ostream parameter, implements Printable::print.

Parameters:

o

the std::ostream this is written to

Returns:: std::ostream WFA was written to

See also:: Printable

Implements wali::Printable.

References wali::HashMap< Key, Data, HashFunc, EqualFunc >::begin(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), F, for_each(), init_state, wali::key2str(), Q, and state_map.

std::ostream & wali::wfa::WFA::print_dot	(	std::ostream &	o,
		bool	print_weights = `false`
	)			const `[virtual]`

Print WFA in dot format.

References wali::HashMap< Key, Data, HashFunc, EqualFunc >::begin(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), for_each(), isFinalState(), isInitialState(), wali::key2str(), and state_map.

Referenced by wali::wpds::DebugWPDS::poststarComputeFixpoint().

std::ostream & wali::wfa::WFA::marshall ( std::ostream & o ) const [virtual]

marshall WFA in XML

References F, for_each(), init_state, INORDER, marshallState(), MAX, query, REVERSE, XMLQueryTag, and XMLTag.

std::ostream & wali::wfa::WFA::marshallState	(	std::ostream &	o,
		Key	key
	)			const `[virtual]`

References getState(), isFinalState(), isInitialState(), wali::key2str(), wali::wfa::State::weight(), wali::wfa::State::XMLFinalTag, wali::wfa::State::XMLInitialTag, wali::wfa::State::XMLNameTag, and wali::wfa::State::XMLTag.

Referenced by marshall().

ITrans * wali::wfa::WFA::insert ( ITrans * tnew )

inserts tnew into the WFA

This method inserts Trans * tnew into the WFA. If a transition told matching (p,g,q) of tnew already exists, then tnew is combined into told.

Warning:: : Note that insert assumes ownership of the passed in parameter tnew; : insert does assumes the states of tnew are already in the WFA. If they are not path_summary and other methods might fail

Returns:: pointer to real transition

References addState(), wali::wfa::ITrans::combineTrans(), wali::wfa::TransSet::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), eps_map, wali::wfa::TransSet::find(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::find(), wali::wfa::ITrans::from(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::insert(), wali::wfa::ITrans::keypair(), kpmap, wali::wfa::ITrans::print(), Q, wali::wfa::ITrans::stack(), state_map, wali::wfa::ITrans::to(), wali::waliErr, and wali::wfa::ITrans::weight().

Referenced by addTrans(), wali::wfa::TransDuplicator::operator()(), wali::wfa::TransCopier::operator()(), wali::wpds::fwpds::SWPDS::prestar(), wali::wpds::WPDS::update(), wali::wpds::ewpds::EWPDS::update(), wali::wpds::DebugWPDS::update(), wali::wpds::WPDS::update_prime(), wali::wpds::ewpds::EWPDS::update_prime(), and wali::wpds::DebugWPDS::update_prime().

TransSet wali::wfa::WFA::match	(	Key	p,
		Key	y
	)

Returns a TransSet containing all transitions matching (p,y,?) in the WFA.

See also:: TransSet

References wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::find(), and kpmap.

Referenced by wali::wfa::epr::EPA::apply(), and opennwa::query::getSomeAcceptedWordInternal().

void wali::wfa::WFA::addState	(	Key	key,
		sem_elem_t	zero
	)

Create a State * for the key Key.

References wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::find(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::insert(), Q, and state_map.

Referenced by opennwa::Nwa::_private_isEmpty_(), insert(), intersect(), and operator=().

const State * wali::wfa::WFA::getState ( Key name ) const

Returns:: const pointer to underlying State object or NULL if no such state exists.

Note:: This may throw an exception in the future

References wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::find(), and state_map.

Referenced by wali::wfa::epr::EPA::apply(), filter(), opennwa::query::getSomeAcceptedWordInternal(), intersect(), marshallState(), wali::wpds::DebugWPDS::post(), wali::wpds::DebugWPDS::poststar_handle_trans(), wali::wpds::fwpds::SWPDS::prestar(), prune(), wali::graph::SummaryGraph::SummaryGraph(), wali::graph::SummaryGraph::summaryPoststar(), and TarjanBasicRegex().

State * wali::wfa::WFA::getState ( Key name )

Returns:: pointer to underlying State object or NULL if no such state exists.

Parameters:

name

the key for this State

Note:: This may throw an exception in the future

References wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::find(), and state_map.

const std::set< Key > & wali::wfa::WFA::getStates ( ) const

References Q.

Referenced by wali::wpds::fwpds::SWPDS::prestar(), wali::graph::SummaryGraph::SummaryGraph(), and wali::graph::SummaryGraph::summaryPoststar().

const std::set< Key > & wali::wfa::WFA::getFinalStates ( ) const

References F.

Referenced by wali::wpds::fwpds::SWPDS::poststar(), and wali::wpds::fwpds::SWPDS::prestar().

size_t wali::wfa::WFA::numStates ( ) const

References Q.

void wali::wfa::WFA::setupFixpoint	(	Worklist< State > &	wl,
		PredHash_t &	preds
	)			`[protected]`

setupFixpoint clears each states markable flag and sets the states weight to zero

Referenced by path_summary(), and prune().

void wali::wfa::WFA::setupFixpoint	(	Worklist< State > &	wl,
		PredHash_t &	preds,
		sem_elem_t	wtFinal
	)			`[protected]`

setupFixpoint clears each states markable flag and sets the states weight to zero, and weight of final states to wtFinal (or ONE if NULL)

References wali::wfa::State::begin(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::begin(), wali::wfa::State::delta(), wali::wfa::State::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::find(), wali::ref_ptr< T >::get_ptr(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::insert(), isFinalState(), wali::wfa::State::name(), wali::Worklist< T >::put(), state_map, wali::wfa::ITrans::to(), wali::Markable::unmark(), and wali::wfa::State::weight().

ITrans * wali::wfa::WFA::find	(	Key	p,
		Key	g,
		Key	q
	)			`[protected, virtual]`

References wali::wfa::TransSet::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), wali::wfa::TransSet::find(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::find(), and kpmap.

ITrans * wali::wfa::WFA::eraseTransFromMaps	(	Key	from,
		Key	stack,
		Key	to
	)			`[protected]`

Erases the specified Trans(from,stack,to) from the kpmap and epsmap.

A null return value means no transition existed.

Returns:: the Trans* that was removed from the maps

References eraseTransFromEpsMap(), and eraseTransFromKpMap().

Referenced by erase(), and eraseState().

ITrans * wali::wfa::WFA::eraseTransFromKpMap	(	Key	from,
		Key	stack,
		Key	to
	)			`[protected]`

Erases the specified Trans(from,stack,to) from the kpmap.

A null return value means no transition existed.

Returns:: the Trans* that was removed from the KpMap

Referenced by eraseTransFromMaps(), and prune().

ITrans * wali::wfa::WFA::eraseTransFromKpMap ( ITrans * terase ) [protected]

References wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::find(), wali::wfa::ITrans::keypair(), and kpmap.

ITrans * wali::wfa::WFA::eraseTransFromEpsMap ( ITrans * terase ) [protected]

Erases the specified Trans(from,stack,to) from the epsmap.

A false return value means no transition existed.

Returns:: true if a transition was erased from EpsMap

References wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), eps_map, wali::HashMap< Key, Data, HashFunc, EqualFunc >::find(), wali::wfa::ITrans::stack(), and wali::wfa::ITrans::to().

Referenced by eraseTransFromMaps(), and prune().

bool wali::wfa::WFA::eraseState ( State * state ) [protected]

Erases the State 'state' from the WFA and all transitions that go to or from the State.

Returns:: true

References wali::wfa::State::begin(), wali::wfa::State::clearTransSet(), wali::wfa::State::end(), eraseTransFromMaps(), wali::wfa::ITrans::from(), wali::wfa::State::name(), wali::wfa::ITrans::print(), Q, wali::wfa::ITrans::stack(), wali::wfa::ITrans::to(), and wali::waliErr.

void wali::wfa::WFA::path_summary	(	Worklist< State > &	wl,
		sem_elem_t	wt
	)			`[protected, virtual]`

Performs path summary with the specified Worklist Initializes the weight on the final state to wt (can be useful for efficiency in some cases).

References wali::wfa::State::begin(), wali::wfa::State::delta(), wali::Worklist< T >::empty(), wali::wfa::State::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::find(), wali::Worklist< T >::get(), INORDER, wali::Markable::marked(), wali::wfa::State::name(), wali::Worklist< T >::put(), query, setupFixpoint(), wali::wfa::ITrans::to(), wali::wfa::ITrans::weight(), and wali::wfa::State::weight().

wali::regex::regex_t wali::wfa::WFA::TarjanBasicRegex ( ) [protected]

Uses Tarjan's algorithm to build a regular expression for this WFA.

IIRC, it is the cubic dynamic programming algorithm.

TODO - future uses One can imagine that a regular expression for states other than the initial state is desirable. To do so, either this method should take the desired key or it should return the resultant vector.