This class models nested word automata (NWA). More...

Public Types
typedef StateStorage::ClientInfoRefPtr	ClientInfoRefPtr
	ref_ptr to a ClientInfo object
typedef StateStorage::const_iterator	StateIterator
	Iterator for traversing a set of states.
typedef SymbolStorage::const_iterator	SymbolIterator
	Iterator for traversing the set of symbols.
typedef Trans::Call	Call
	Represents a call transition.
typedef Trans::Internal	Internal
	Represents an internal transition.
typedef Trans::Return	Return
	Represents a return transition.
typedef Trans::Calls	Calls
typedef Trans::Internals	Internals
typedef Trans::Returns	Returns
typedef Trans::CallIterator	CallIterator
	Iterator to a set of calls.
typedef Trans::InternalIterator	InternalIterator
	Iterator to a set of internals.
typedef Trans::ReturnIterator	ReturnIterator
	Iterator to a set of returns.
typedef wali::relations::RelationTypedefs < State >::BinaryRelation	BinaryRelation
	Represents a binary relation on states.
Public Member Functions
	Nwa ()
	Constructs an empty NWA.
	Nwa (const Nwa &other)
	Copies 'other'.
Nwa &	operator= (const Nwa &other)
	Assigns 'other' to this NWA.
void	clear ()
	Removes all states, symbols, and transitions from this NWA.
virtual std::ostream &	marshall (std::ostream &os) const
	Marshalls the NWA as XML to the output stream os.
ClientInfoRefPtr	getClientInfo (State state) const
	access the client information associated with the given state
void	setClientInfo (State state, const ClientInfoRefPtr c)
	set the client information associated with the given state
const StateSet &	getStates () const
	Returns the set of states in the NWA.
bool	isState (State state) const
	Tests if a given state is in this NWA.
bool	addState (State state)
	Adds the given state to this NWA.
size_t	sizeStates () const
	Returns the number of states in this NWA.
State	largestState () const
	Returns the largest state ID in the automaton.
virtual bool	removeState (State state)
	Removes the given state from this NWA along with any associated transitions.
void	clearStates ()
	remove all states and transitions from the NWA
const StateSet &	getInitialStates () const
	Returns the set of initial states.
bool	isInitialState (State state) const
	test if the given state is an initial state of this NWA
bool	addInitialState (State state)
	Makes the given state an initial state in this NWA (adding it to the NWA if necessary).
size_t	sizeInitialStates () const
	Returns the number of initial states in this NWA.
bool	removeInitialState (State state)
	Removes the given state from the set of initial states.
void	clearInitialStates ()
	Clears the set of initial states.
const StateSet &	getFinalStates () const
	Returns the set of final states.
bool	isFinalState (State state) const
	test if a state with the given name is a final state
bool	addFinalState (State state)
	Makes the given state an final state in this NWA (adding it to the NWA if necessary).
size_t	sizeFinalStates () const
	Returns the number of final states in this NWA.
bool	removeFinalState (State state)
	Removes the given state from the set of final states.
void	clearFinalStates ()
	Clears the set of final states.
const SymbolSet &	getSymbols () const
	Returns the set of (non-epsilon, non-wild) symbols in this NWA.
bool	isSymbol (Symbol sym) const
	Tests whether the given symbol is a member the NWA.
bool	addSymbol (Symbol sym)
	Adds the given symbol to the NWA.
size_t	sizeSymbols () const
	Returns the number of symbols in this NWA (excluding epsilon and wild).
bool	removeSymbol (Symbol sym)
	Remove the given symbol from the NWA along with any associated transitions.
void	clearSymbols ()
	Remove all symbols and transitions from the NWA.
Trans const &	_private_get_transition_storage_ () const
	Please don't call this, in case that's not evident from the name.
void	duplicateStateOutgoing (State orig, State dup)
	duplicates the original state, but only duplicates outgoing transitions
void	duplicateState (State orig, State dup)
	duplicates the original state
void	realizeImplicitTrans (State stuckState)
	realizes all implicit transitions in the NWA
size_t	sizeTrans () const
	Returns the number of transitions in this NWA (regardless of type).
void	clearTrans ()
	Removes all transitions from this NWA.
bool	addInternalTrans (State from, Symbol sym, State to)
	Adds a internal transition to the NWA.
bool	addInternalTrans (Internal &ct)
	Adds a internal transition to the NWA.
bool	removeInternalTrans (State from, Symbol sym, State to)
	Removes the given internal transition from the NWA.
bool	removeInternalTrans (const Internal &ct)
	Removes the given internal transition from the NWA.
size_t	sizeInternalTrans () const
	Returns the number of internal transitions in this NWA.
bool	addCallTrans (State call, Symbol sym, State entry)
	Adds a call transition to the NWA.
bool	addCallTrans (Call &ct)
	Adds a call transition to the NWA.
bool	removeCallTrans (State call, Symbol sym, State entry)
	Removes the given call transition from the NWA.
bool	removeCallTrans (const Call &ct)
	Removes the given call transition from the NWA.
size_t	sizeCallTrans () const
	Returns the number of call transitions in this NWA.
bool	addReturnTrans (State exit, State pred, Symbol sym, State ret)
	Adds a return transition to the NWA.
bool	addReturnTrans (Return &ct)
	Adds a return transition to the NWA.
bool	removeReturnTrans (State exit, Symbol sym, State ret)
	Removes (possibly multiple) matching return transition from the NWA.
bool	removeReturnTrans (State exit, State pred, Symbol sym, State ret)
	Removes the given return transition from the NWA.
bool	removeReturnTrans (const Return &ct)
	Removes the given return transition from the NWA.
size_t	sizeReturnTrans () const
	Returns the number of return transitions in this NWA.
void	projectStates (Nwa const &first, StateSet const &prjStates)
virtual bool	isTransitionPossible (const State &src, const Symbol &sym, const State &tgt)
void	removeImplicitTransitions ()
	Detects (immediately) stuck states and removes them.
void	pruneUnreachableForward (const StateSet &sources)
	Removes states not reachable from any of the 'sources' states.
void	pruneUnreachableBackward (const StateSet &targets)
	Removes states from which none of the 'targets' are reachable.
void	pruneUnreachableInitial ()
	Removes states not reachable from any initial state.
void	pruneUnreachableFinal ()
	Removes states from which none of the final states are reachable.
void	chop ()
	Removes states not reachable from any initial state and from which none of the final states are reachable.
void	_private_star_ (Nwa const &first)
	constructs the NWA resulting from performing Kleene-* on the given NWA
void	_private_determinize_ (Nwa const &nondet)
	constructs a deterministic NWA that is equivalent to the given NWA.
void	_private_intersect_ (Nwa const &first, Nwa const &second)
	constructs the NWA which is the intersection of the given NWAs
bool	_private_isDeterministic_ () const
	tests whether this NWA is deterministic
virtual void	intersectClientInfoCall (Nwa const &first, State call1, State entry1, Nwa const &second, State call2, State entry2, Symbol resSym, State resSt)
	Intersects client information for the target of a call transition.
virtual void	intersectClientInfoInternal (Nwa const &first, State src1, State tgt1, Nwa const &second, State src2, State tgt2, Symbol resSym, State resSt)
	Intersects client information for the target of an internal transition.
virtual void	intersectClientInfoReturn (Nwa const &first, State exit1, State call1, State ret1, Nwa const &second, State exit2, State call2, State ret2, Symbol resSym, State resSt)
	Intersects client information for the target of a return transition.
virtual bool	stateIntersect (Nwa const &first, State state1, Nwa const &second, State state2, State &resSt, ClientInfoRefPtr &resCI)
	Intersect states.
virtual bool	transitionIntersect (Nwa const &first, Symbol sym1, Nwa const &second, Symbol sym2, Symbol &resSym)
	Intersect symbols.
virtual void	mergeClientInfo (Nwa const &nwa, BinaryRelation const &binRel, State resSt, ClientInfoRefPtr &resCI)
	Merges clientInfo for determinize.
virtual void	mergeClientInfoCall (Nwa const &nwa, BinaryRelation const &binRelCall, BinaryRelation const &binRelEntry, State callSt, Symbol resSym, State resSt, ClientInfoRefPtr &resCI)
	Merges clientInfo for determinize for the target of a call transition.
virtual void	mergeClientInfoInternal (Nwa const &nwa, BinaryRelation const &binRelSource, BinaryRelation const &binRelTarget, State sourceSt, Symbol resSym, State resSt, ClientInfoRefPtr &resCI)
	Merges clientInfo for determinize for the target of an internal transition.
virtual void	mergeClientInfoReturn (Nwa const &nwa, BinaryRelation const &binRelExit, BinaryRelation const &binRelCall, BinaryRelation const &binRelReturn, State exitSt, State callSt, Symbol resSym, State resSt, ClientInfoRefPtr &resCI)
	Merges clientInfo for determinize for the target of a return transition.
wali::wpds::WPDS	_private_NwaToPdsReturns_ (WeightGen const &wg) const
wali::wpds::WPDS	_private_NwaToBackwardsPdsReturns_ (WeightGen const &wg) const
wali::wpds::WPDS	_private_NwaToPdsCalls_ (WeightGen const &wg, ref_ptr< wali::wpds::Wrapper > wrapper) const
wali::wpds::WPDS	_private_NwaToBackwardsPdsCalls_ (WeightGen const &wg) const
bool	_private_isEmpty_ () const
	tests whether the language accepted by this NWA is empty
const char *	toStringGdb () const
wali::wfa::WFA	prestar (wali::wfa::WFA const &input, WeightGen const &wg) const
	perform the prestar reachability query defined by the given WFA
virtual wali::wfa::WFA	prestar (wali::wfa::WFA const &input, WeightGen const &wg, ref_ptr< wali::Worklist< wali::wfa::ITrans > > worklist) const
	perform the prestar reachability query defined by the given WFA
void	prestar (wali::wfa::WFA const &input, wali::wfa::WFA &output, WeightGen const &wg) const
	perform the prestar reachability query defined by the given WFA
virtual void	prestar (wali::wfa::WFA const &input, wali::wfa::WFA &output, WeightGen const &wg, ref_ptr< wali::Worklist< wali::wfa::ITrans > > worklist) const
	perform the prestar reachability query defined by the given WFA
wali::wfa::WFA	poststar (wali::wfa::WFA const &input, WeightGen const &wg) const
	perform the poststar reachability query defined by the given WFA
virtual wali::wfa::WFA	poststar (wali::wfa::WFA const &input, WeightGen const &wg, ref_ptr< wali::Worklist< wali::wfa::ITrans > > wl) const
	perform the poststar reachability query defined by the given WFA
void	poststar (wali::wfa::WFA const &input, wali::wfa::WFA &output, WeightGen const &wg) const
	perform the poststar reachability query defined by the given WFA
virtual void	poststar (wali::wfa::WFA const &input, wali::wfa::WFA &output, WeightGen const &wg, ref_ptr< wali::Worklist< wali::wfa::ITrans > > worklist) const
	perform the poststar reachability query defined by the given WFA
virtual std::ostream &	print (std::ostream &o) const
	print the NWA
virtual std::ostream &	print_dot (std::ostream &o, std::string title, bool abbrev=true) const
	print the NWA in dot format
bool	operator== (const Nwa &other) const
	tests whether this NWA is equivalent to the NWA 'other'
void	addAllStates (StateStorage addStateSet)
	add all the states in the given StateSet to the NWA
void	addAllInitialStates (StateStorage addStateSet)
	adds all of the states in the given StateSet to the initial state set associated with this NWA
void	addAllFinalStates (StateStorage addStateSet)
	adds all of the final states in the given StateSet to the final state set associated with this NWA
void	addAllSymbols (SymbolStorage addSymbolSet)
	add the given symbols to the NWA
StateIterator	beginStates () const
	provide access to the beginning of the state set
StateIterator	endStates () const
	provide access to the end of the state set
StateIterator	beginInitialStates () const
	provide access to the beginning of the initial state set
StateIterator	endInitialStates () const
	provide access to the end of the initial state set
StateIterator	beginFinalStates () const
	provide access to the beginning of the final state set
StateIterator	endFinalStates () const
	provide access to the end of the final state set
SymbolIterator	beginSymbols () const
	provide access to the beginning of the symbol set
SymbolIterator	endSymbols () const
	provide access to the end of the symbol set
CallIterator	beginCallTrans () const
	provide access to the beginning of the call transition set
CallIterator	endCallTrans () const
	provide access to the end of the call transition set
InternalIterator	beginInternalTrans () const
	provide access to the beginning of the internal transition set
InternalIterator	endInternalTrans () const
	provide access to the end of the internal transition set
ReturnIterator	beginReturnTrans () const
	provide access to the beginning of the return transition set
ReturnIterator	endReturnTrans () const
	provide access to the end of the return transition set
bool	isMemberNondet (NestedWord const &word) const
	Determines whether word is in the language of the given NWA.
void	combineWith (Nwa const &rhs)
	Adds all states, symbols, and transitions from 'rhs' to 'this'.
Protected Member Functions
void	epsilonClosure (StateSet *newPairs, State sp) const
	computes the epsilon closure of the given state
void	epsilonClosure (std::set< StatePair > *newPairs, StatePair sp, Nwa const &first, Nwa const &second) const
	computes the epsilon closure of the given states in their respective NWAs
State	makeKey (BinaryRelation const &R) const
	returns the state corresponding to the given binary relation
Protected Attributes
StateStorage	states
SymbolStorage	symbols
Trans	trans

Detailed Description

This class models nested word automata (NWA).

Note: StName must be a unique identifier for states.

Member Typedef Documentation

typedef StateStorage::ClientInfoRefPtr opennwa::Nwa::ClientInfoRefPtr

ref_ptr to a ClientInfo object

typedef StateStorage::const_iterator opennwa::Nwa::StateIterator

Iterator for traversing a set of states.

Dereferences to a 'State'. (This is used for the set of states, set of initial states, and set of accepting states.)

typedef SymbolStorage::const_iterator opennwa::Nwa::SymbolIterator

Iterator for traversing the set of symbols.

Dereferences to a 'Symbol'

typedef Trans::Call opennwa::Nwa::Call

Represents a call transition.

Has the following fields: Call::first The call site (a State) Call::second The symbol (a Symbol) Call::third The entry (a State)

typedef Trans::Internal opennwa::Nwa::Internal

Represents an internal transition.

Has the following fields: Internal::first The source state (a State) Internal::second The symbol (a Symbol) Internal::third The target state (a State)

typedef Trans::Return opennwa::Nwa::Return

Represents a return transition.

Has the following fields: Return::first The exit site (a State) Return::second The call predecessor (a State) Return::third The symbol (a Symbol) Return::fourth The return site (a State)

typedef Trans::Calls opennwa::Nwa::Calls

typedef Trans::Internals opennwa::Nwa::Internals

typedef Trans::Returns opennwa::Nwa::Returns

typedef Trans::CallIterator opennwa::Nwa::CallIterator

Iterator to a set of calls.

Dereferences to a 'Call'.

typedef Trans::InternalIterator opennwa::Nwa::InternalIterator

Iterator to a set of internals.

Dereferences to an 'Internal'

typedef Trans::ReturnIterator opennwa::Nwa::ReturnIterator

Iterator to a set of returns.

Dereferences to a 'Return'

typedef wali::relations::RelationTypedefs<State>::BinaryRelation opennwa::Nwa::BinaryRelation

Represents a binary relation on states.

There are a couple possibilities for a concrete type for this, depending on whether you are using the (very experimental) BuDDY support or just std::maps. See the appropriate version of RelationOps.hpp.

Constructor & Destructor Documentation

opennwa::Nwa::Nwa ( )

Constructs an empty NWA.

opennwa::Nwa::Nwa ( const Nwa & other )

Copies 'other'.

Does not share structure.

Will clone the client info objects. TODO-RELEASE

Member Function Documentation

Nwa & opennwa::Nwa::operator= ( const Nwa & other )

Assigns 'other' to this NWA.

Does not share structure.

Will clone the client info objects. TODO-RELEASE

References clear(), states, symbols, and trans.

void opennwa::Nwa::clear ( )

Removes all states, symbols, and transitions from this NWA.

erases all data from the NWA

This method restore's the NWA to its default state: the stuck state with no symbols or transitions.

References clearStates(), and clearSymbols().

Referenced by _private_determinize_(), _private_intersect_(), _private_star_(), operator=(), and opennwa::nwa_pds::WpdsToNwa().

std::ostream & opennwa::Nwa::marshall ( std::ostream & os ) const [virtual]

Marshalls the NWA as XML to the output stream os.

References opennwa::details::TransitionStorage::beginCall(), opennwa::details::TransitionStorage::beginInternal(), opennwa::details::TransitionStorage::beginReturn(), beginStates(), beginSymbols(), opennwa::details::TransitionStorage::endCall(), opennwa::details::TransitionStorage::endInternal(), opennwa::details::TransitionStorage::endReturn(), endStates(), endSymbols(), isFinalState(), isInitialState(), key2str, trans, opennwa::details::SymbolStorage::XMLNameAttr(), and opennwa::details::SymbolStorage::XMLSymbolTag().

Nwa::ClientInfoRefPtr opennwa::Nwa::getClientInfo ( State state ) const

access the client information associated with the given state

This method provides access to the client information associated with the given state.

Parameters:

-

state: the state whose client information to retrieve

Returns:: the client information associated with the given state

Parameters:

-

state: the state whose client information to retrieve

Returns:: the client information associated with the given state

References opennwa::details::StateStorage::getClientInfo(), and states.

Referenced by _private_NwaToBackwardsPdsCalls_(), _private_NwaToBackwardsPdsReturns_(), _private_NwaToPdsCalls_(), _private_NwaToPdsReturns_(), and _private_star_().

void opennwa::Nwa::setClientInfo	(	State	state,
		const ClientInfoRefPtr	c
	)

set the client information associated with the given state

This method sets the client information associated with the given state to the client information provided.

Parameters:

	-	state: the state whose client information to set
	-	c: the desired client information for the given state
	-	state: the state whose client information to set
	-	c: the desired client information for the given state

References opennwa::details::StateStorage::setClientInfo(), and states.

const StateSet & opennwa::Nwa::getStates ( ) const

Returns the set of states in the NWA.

provides access to all states in the NWA

Returns:: The set of all states; a set of all states

References opennwa::details::StateStorage::getStates(), and states.

Referenced by pruneUnreachableBackward(), and pruneUnreachableForward().

bool opennwa::Nwa::isState ( State state ) const

Tests if a given state is in this NWA.

test if a given state is a state of this NWA

Parameters:

-

state: the state to check

Returns:: true if the given state is a member of this NWA

Parameters:

-

state: the state to check

Returns:: true if the given state is a state of this NWA

References opennwa::details::StateStorage::isState(), and states.

Referenced by _private_star_(), duplicateState(), duplicateStateOutgoing(), removeCallTrans(), removeInternalTrans(), and removeReturnTrans().

bool opennwa::Nwa::addState ( State state )

Adds the given state to this NWA.

add the given state to this NWA

If the state is already a member of this NWA. returns false. Otherwise, returns true.

Parameters:

-

state: the state to add

Returns:: 'false' if the state already exists in the NWA, 'true' otherwise

Parameters:

-

state: the state to add

Returns:: false if the state already exists in the NWA, true otherwise

References opennwa::details::StateStorage::addState(), and states.

Referenced by _private_determinize_(), _private_intersect_(), addCallTrans(), addInternalTrans(), and addReturnTrans().

size_t opennwa::Nwa::sizeStates ( ) const

Returns the number of states in this NWA.

returns the number of states associated with this NWA

Foo bar

Returns:: the number of states in this NWA; the number of states associated with this NWA

References opennwa::details::StateStorage::sizeStates(), and states.

State opennwa::Nwa::largestState ( ) const

Returns the largest state ID in the automaton.

Returns:: the largest state ID in the automaton

References opennwa::details::StateStorage::largestState(), and states.

Referenced by _private_determinize_().

bool opennwa::Nwa::removeState ( State state ) [virtual]

Removes the given state from this NWA along with any associated transitions.

returns the number of states associated with this NWA

This removes 'state' from the set of initial and final states as well as the set of all states. It also removes any transitions (of any type) with 'state' as a component.

If 'state' is not present, this command is a no-op (except for the return value). The return value indicates whether the state was actually removed.

Parameters:

-

state: the state to remove

Returns:: false if the state did not exist in the NWA, true otherwise

Note: This method simply calls sizeStates( ). It is here to make the transition from using PDS to using NWA easier.

Returns:: the number of states associated with this NWAremove the given state from this NWA

Parameters:

-

state: the state to remove

Returns:: false if the state does not exist in the NWA, true otherwise

References opennwa::details::StateStorage::removeState(), opennwa::details::TransitionStorage::removeTransWith(), states, and trans.

Referenced by _private_intersect_(), projectStates(), pruneUnreachableBackward(), pruneUnreachableForward(), and removeImplicitTransitions().

void opennwa::Nwa::clearStates ( )

remove all states and transitions from the NWA

remove all states from the NWA

This method removes all states and transitions from the NWA.

References opennwa::details::StateStorage::clearStates(), clearTrans(), and states.

Referenced by clear().

const StateSet & opennwa::Nwa::getInitialStates ( ) const

Returns the set of initial states.

obtain the states in the initial state set

(Note: An NWA can have an unbounded number of inital states.)

Returns:: the set of inital states associated with the NWA; set of inital states associated with the NWA

References opennwa::details::StateStorage::getInitialStates(), and states.

Referenced by print_dot(), and pruneUnreachableInitial().

bool opennwa::Nwa::isInitialState ( State state ) const

test if the given state is an initial state of this NWA

Parameters:

-

state: the state to check

Returns:: true if the given state is an initial state, false otherwise

References opennwa::details::StateStorage::isInitialState(), and states.

Referenced by _private_star_(), isMemberNondet(), and marshall().

bool opennwa::Nwa::addInitialState ( State state )

Makes the given state an initial state in this NWA (adding it to the NWA if necessary).

make the given state an initial state in this NWA

This method checks whether 'state' is in the state set of this NWA. If the state is not present, it is added to the automaton. In either case, the given state is then added to the set of initial states for the NWA.

Returns whether the state was added to the set of initial states. (The return value is 'true' if it was not already an initial state regardless of whether it needed to be added to the machine or not.)

Parameters:

-

state: the state to add to initial state set

Returns:: false if the state already exists in the initial state set of the NWA

Parameters:

-

state: the state to add to initial state set

Returns:: false if the state already exists in the initial state set of the NWA

References opennwa::details::StateStorage::addInitialState(), and states.

Referenced by _private_determinize_(), _private_intersect_(), and _private_star_().

size_t opennwa::Nwa::sizeInitialStates ( ) const

Returns the number of initial states in this NWA.

returns the number of initial states associated with this NWA

Returns:: the number of initial states in this NWA; the number of initial states associated with this NWA

References opennwa::details::StateStorage::sizeInitialStates(), and states.

Referenced by _private_isDeterministic_(), _private_isEmpty_(), and opennwa::query::getSomeAcceptedWordInternal().

bool opennwa::Nwa::removeInitialState ( State state )

Removes the given state from the set of initial states.

remove the given state from the initial state set of this NWA

If 'state' is not already an initial state, this function is a no-op (except for the return value), even if 'state' is not in the NWA at all.

The return value indicates whether 'state' was an initial state.

(This method does not remove any transitions from the NWA, nor does it remove the state from the NWA entirely.)

Parameters:

-

state: the state to remove from the initial state set

Returns:: false if the state does not exist in the initial state set of this NWA

Parameters:

-

state: the state to remove from the initial state set

Returns:: false if the state does not exist in the initial state set of this NWA

References opennwa::details::StateStorage::removeInitialState(), and states.

void opennwa::Nwa::clearInitialStates ( )

Clears the set of initial states.

remove all states from the initial state set of the NWA

(This function does not remove any states or transitions from the automaton, it just affects the set of initial states.)

References opennwa::details::StateStorage::clearInitialStates(), and states.

Referenced by _private_star_().

const StateSet & opennwa::Nwa::getFinalStates ( ) const

Returns the set of final states.

obtain the final states in this NWA

(Note: An NWA can have an unbounded number of inital states.)

Returns:: the set of inital states associated with the NWA; set of all final states associated with this NWA

References opennwa::details::StateStorage::getFinalStates(), and states.

Referenced by print_dot(), and pruneUnreachableFinal().

bool opennwa::Nwa::isFinalState ( State state ) const

test if a state with the given name is a final state

This method tests whether the given state is in the final state set of the NWA.

Parameters:

-

state: the state to check

Returns:: true if the given state is a final state

Parameters:

-

state: the state to check

Returns:: true if the given state is a final state

References opennwa::details::StateStorage::isFinalState(), and states.

Referenced by _private_intersect_(), _private_isEmpty_(), isMemberNondet(), marshall(), and removeImplicitTransitions().

bool opennwa::Nwa::addFinalState ( State state )

Makes the given state an final state in this NWA (adding it to the NWA if necessary).

make the given state a final state

This method checks whether 'state' is in the state set of this NWA. If the state is not present, it is added to the automaton. In either case, the given state is then added to the set of final states for the NWA.

Returns whether the state was added to the set of final states. (The return value is 'true' if it was not already a final state regardless of whether it needed to be added to the machine or not.)

Parameters:

-

state: the state to add to final state set

Returns:: false if the state already exists in the final state set of the NWA

Parameters:

-

state: the state to add to final state set

Returns:: false if the state already exists in the final state set of the NWA

References opennwa::details::StateStorage::addFinalState(), and states.

Referenced by _private_determinize_(), _private_intersect_(), and _private_star_().

size_t opennwa::Nwa::sizeFinalStates ( ) const

Returns the number of final states in this NWA.

returns the number of final states associated with this NWA

Returns:: the number of final states in this NWA; the number of final states associated with this NWA

References opennwa::details::StateStorage::sizeFinalStates(), and states.

Referenced by _private_isEmpty_().

bool opennwa::Nwa::removeFinalState ( State state )

Removes the given state from the set of final states.

remove the given state from the final state set of the NWA

If 'state' is not already an final state, this function is a no-op (except for the return value), even if 'state' is not in the NWA at all.

The return value indicates whether 'state' was an final state.

(This method does not remove any transitions from the NWA, nor does it remove the state from the NWA entirely.)

Parameters:

-

state: the state to remove from the final state set

Returns:: false if the state does not exist in the final state set of this NWA

Parameters:

-

state: the state to remove from the final state set

Returns:: false if the state does not exist in the final state set of the NWA

References opennwa::details::StateStorage::removeFinalState(), and states.

void opennwa::Nwa::clearFinalStates ( )

Clears the set of final states.

remove all states from the final state set of the NWA

(This function does not remove any states or transitions from the automaton, it just affects the set of final states.)

References opennwa::details::StateStorage::clearFinalStates(), and states.

Referenced by _private_star_().

const std::set< Symbol > & opennwa::Nwa::getSymbols ( ) const

Returns the set of (non-epsilon, non-wild) symbols in this NWA.

obtain all symbols in this NWA

Note: Not all symbols need to be used on a transition. (This function will still return them.)

Returns:: set of all symbols in this NWA; set of all symbols associated with this NWA

References opennwa::details::SymbolStorage::getSymbols(), and symbols.

bool opennwa::Nwa::isSymbol ( Symbol sym ) const

Tests whether the given symbol is a member the NWA.

test if the given symbol is associated with the NWA

This returns 'false' for EPSILON and WILD, even if they are used on a transition.

Parameters:

-

sym: the symbol to check

Returns:: true if the given symbol is associated with the NWA

Parameters:

-

sym: the symbol to check

Returns:: true if the given symbol is associated with the NWA

References opennwa::details::SymbolStorage::isSymbol(), and symbols.

Referenced by removeCallTrans(), removeInternalTrans(), and removeReturnTrans().

bool opennwa::Nwa::addSymbol ( Symbol sym )

Adds the given symbol to the NWA.

add the given symbol to the NWA

If 'sym' is already present in the NWA, this function is a no-op. It is also a no-op if 'sym' is either 'EPSILON' or 'WILD'.

The return value indicates whether 'sym' was added.

Parameters:

-

sym: the symbol to add

Returns:: false if the symbol is already associated with the NWA

Parameters:

-

sym: the symbol to add

Returns:: false if the symbol is already associated with the NWA

References opennwa::details::SymbolStorage::addSymbol(), and symbols.

Referenced by addCallTrans(), addInternalTrans(), and addReturnTrans().

size_t opennwa::Nwa::sizeSymbols ( ) const

Returns the number of symbols in this NWA (excluding epsilon and wild).

returns the number of symbols associated with this NWA

Symbols in the automaton are counted regardless of whether they are used to label any transitions. Neither 'EPSILON' nor 'WILD' are included in this count at all, regardless of whether they are used to label transitions or not.

Returns:: The number of symbols in this NWA

Note: The epsilon symbol is included in this count.

Returns:: the number of symbols associated with this NWA

References opennwa::details::SymbolStorage::sizeSymbols(), and symbols.

bool opennwa::Nwa::removeSymbol ( Symbol sym )

Remove the given symbol from the NWA along with any associated transitions.

remove the given symbol from the NWA

Removes 'sym' from the symbol set of the NWA as well as any transitions that have 'sym' as the symbol component.

If 'sym' is not present, this command is a no-op; the return value indicates whether this was the case.

Parameters:

-

sym: the symbol to remove

Returns:: false if the symbols was not in the NWA

Parameters:

-

sym: the symbol to remove

Returns:: false if the symbols is not associated with the NWA

References opennwa::EPSILON, opennwa::details::SymbolStorage::removeSymbol(), opennwa::details::TransitionStorage::removeTransSym(), symbols, trans, and opennwa::WILD.

void opennwa::Nwa::clearSymbols ( )

Remove all symbols and transitions from the NWA.

remove all symbols associated with the NWA

This method removes all symbols and all transitions from the NWA. It does not touch any states.

(Note: this also removes all transitions labeled with 'EPSILON' and 'WILD' even though this perhaps needn't be the case.)

References opennwa::details::SymbolStorage::clearSymbols(), clearTrans(), and symbols.

Referenced by clear().

Trans const& opennwa::Nwa::_private_get_transition_storage_ ( ) const

Please don't call this, in case that's not evident from the name.

It's const, so you won't break the NWA, but I make no guarantees it'll be around in future versions.

References trans.

void opennwa::Nwa::duplicateStateOutgoing	(	State	orig,
		State	dup
	)

duplicates the original state, but only duplicates outgoing transitions

This method assigns to the duplicate state all the state properties of the original state and duplicates all outgoing transitions of the original state for the duplicate state. Further, any self-loop outgoing transitions that the original state are not only duplicated as self-loop transitions for the duplicate state, but the duplicate state also has transitions to the original state for each such transition.

Parameters:

	-	orig: the name of the original state, i.e. the state to duplicate
	-	dup: the name of the duplicate state
	-	orig: the name of the original state, i.e. the state to duplicate
	-	dup: the name of the duplicate state

References opennwa::details::StateStorage::addState(), opennwa::details::StateStorage::dupState(), opennwa::details::TransitionStorage::dupTransOutgoing(), isState(), states, and trans.

void opennwa::Nwa::duplicateState	(	State	orig,
		State	dup
	)

duplicates the original state

This method assigns to the duplicate state all the state properties of the original state and duplicates all transitions of the original state for the duplicate state. Further, any self-loop transitions that the original state are not only duplicated as self-loop transitions for the duplicate state, but the duplicate state also has transitions to and from the original state for each such transition.

Parameters:

	-	orig: the name of the original state, i.e. the state to duplicate
	-	dup: the name of the duplicate state
	-	orig: the name of the original state, i.e. the state to duplicate
	-	dup: the name of the duplicate state

References opennwa::details::StateStorage::addState(), opennwa::details::StateStorage::dupState(), opennwa::details::TransitionStorage::dupTrans(), isState(), states, and trans.

void opennwa::Nwa::realizeImplicitTrans ( State stuck )

realizes all implicit transitions in the NWA

This method makes explicit all transitions in the NWA by adding the given stuckState (if necessary) then any transitions to the stuck state for each state/symbol(excluding epsilon) pair for which no outgoing edge(one of each kind-call,internal,return) from that state is labeled with that symbol.

References addCallTrans(), addInternalTrans(), addReturnTrans(), beginReturnTrans(), beginStates(), beginSymbols(), opennwa::details::TransitionStorage::callExists(), endReturnTrans(), endStates(), endSymbols(), opennwa::EPSILON, opennwa::details::TransitionStorage::internalExists(), trans, and opennwa::WILD.

size_t opennwa::Nwa::sizeTrans ( ) const

Returns the number of transitions in this NWA (regardless of type).

returns the number of transitions associated with this NWA

Returns:: the number of transitions in this NWA; the number of transitions associated with this NWA

References opennwa::details::TransitionStorage::size(), and trans.

void opennwa::Nwa::clearTrans ( )

Removes all transitions from this NWA.

remove all transitions from the NWA

This function does not remove any states or symbols.

References opennwa::details::TransitionStorage::clear(), and trans.

Referenced by clearStates(), and clearSymbols().

bool opennwa::Nwa::addInternalTrans	(	State	from,
		Symbol	sym,
		State	to
	)

Adds a internal transition to the NWA.

add an internal transition to the NWA

If the internal transition is already present, this function is a no-op (other than the return value). The return value indicates whether the transition was successfully added.

Note: 'sym' cannot be EPSILON.

Parameters:

	-	from: the state the edge departs from
	-	sym: the symbol labeling the edge
	-	to: the state the edge arrives to

Returns:: false if the internal transition already exists in the NWA

Parameters:

	-	from: the state the edge departs from
	-	sym: the symbol labeling the edge
	-	to: the state the edge arrives to

Returns:: false if the internal transition already exists in the NWA

References opennwa::details::TransitionStorage::addInternal(), addState(), addSymbol(), and trans.

Referenced by _private_determinize_(), _private_intersect_(), _private_star_(), opennwa::EpsilonTransitionInserter::operator()(), realizeImplicitTrans(), and opennwa::nwa_pds::WpdsToNwa().

bool opennwa::Nwa::addInternalTrans ( Internal & it )

Adds a internal transition to the NWA.

add an internal transition to the NWA

If the internal transition is already present, this function is a no-op (other than the return value). The return value indicates whether the transition was successfully added.

Parameters:

-

ct: the internal transition to add

Returns:: false if the internal transition already exists in the NWA

Parameters:

-

it: internal transition to add to the NWA

Returns:: false if the internal transition already exists in the NWA

References opennwa::details::TransitionStorage::addInternal(), addState(), addSymbol(), opennwa::details::TransitionStorage::getInternalSym(), opennwa::details::TransitionStorage::getSource(), opennwa::details::TransitionStorage::getTarget(), and trans.

bool opennwa::Nwa::removeInternalTrans	(	State	from,
		Symbol	sym,
		State	to
	)

Removes the given internal transition from the NWA.

remove an internal transition from the NWA

Removes the specified internal transition from the NWA, if present. If it was not present, this function is a no-op (apart from the return value). The return value indicates whether the transition was successfully removed.

Parameters:

	-	from: the state the edge departs from
	-	sym: the symbol labeling the edge
	-	to: the state the edge arrives to

Returns:: false if the internal transition does not exist in the NWA

Parameters:

	-	from: the state the edge departs from
	-	sym: the symbol labeling the edge
	-	to: the state the edge arrives to

Returns:: false if the internal transition does not exist in the NWA

References opennwa::EPSILON, isState(), isSymbol(), opennwa::details::TransitionStorage::removeInternal(), trans, and opennwa::WILD.

bool opennwa::Nwa::removeInternalTrans ( const Internal & it )

Removes the given internal transition from the NWA.

remove an internal transition from the NWA

Removes the specified internal transition from the NWA, if present. If it was not present, this function is a no-op (apart from the return value). The return value indicates whether the transition was successfully removed.

Parameters:

-

ct: the internal transition to remove

Returns:: false if the internal transition does not exist in the NWA

Parameters:

-

it: the internal transition to remove

Returns:: false if the internal transition does not exist in the NWA

References opennwa::details::TransitionStorage::getInternalSym(), opennwa::details::TransitionStorage::getSource(), opennwa::details::TransitionStorage::getTarget(), isState(), isSymbol(), opennwa::details::TransitionStorage::removeInternal(), and trans.

size_t opennwa::Nwa::sizeInternalTrans ( ) const

Returns the number of internal transitions in this NWA.

returns the number of internal transitions associated with this NWA

Returns:: the number of internal transitions in this NWA; the number of internal transitions associated with this NWA

References opennwa::details::TransitionStorage::sizeInternal(), and trans.

bool opennwa::Nwa::addCallTrans	(	State	from,
		Symbol	sym,
		State	to
	)

Adds a call transition to the NWA.

add a call transition to the NWA

If the call transition is already present, this function is a no-op (other than the return value). The return value indicates whether the transition was successfully added.

Note: 'sym' cannot be EPSILON.

Parameters:

	-	call: the state the edge departs from
	-	sym: the symbol labeling the edge
	-	entry: the state the edge arrives to

Returns:: false if the call transition already exists in the NWA

Parameters:

	-	from: the state the edge departs from
	-	sym: the symbol labeling the edge
	-	to: the state the edge arrives to

Returns:: false if the call transition already exists in the NWA

References opennwa::details::TransitionStorage::addCall(), addState(), addSymbol(), opennwa::EPSILON, and trans.

Referenced by _private_determinize_(), _private_intersect_(), _private_star_(), opennwa::CallReturnTransitionInserter::operator()(), realizeImplicitTrans(), and opennwa::nwa_pds::WpdsToNwa().

bool opennwa::Nwa::addCallTrans ( Call & ct )

Adds a call transition to the NWA.

add a call transition to the NWA

If the call transition is already present, this function is a no-op (other than the return value). The return value indicates whether the transition was successfully added.

Parameters:

-

ct: the call transition to add

Returns:: false if the call transition already exists in the NWA

Parameters:

-

ct: the call transition to add

Returns:: false if the call transition already exists in the NWA

References opennwa::details::TransitionStorage::addCall(), addState(), addSymbol(), opennwa::EPSILON, opennwa::details::TransitionStorage::getCallSite(), opennwa::details::TransitionStorage::getCallSym(), opennwa::details::TransitionStorage::getEntry(), and trans.

bool opennwa::Nwa::removeCallTrans	(	State	from,
		Symbol	sym,
		State	to
	)

Removes the given call transition from the NWA.

remove a call transition from the NWA

Removes the specified call transition from the NWA, if present. If it was not present, this function is a no-op (apart from the return value). The return value indicates whether the transition was successfully removed.

Parameters:

	-	call: the state the edge departs from
	-	sym: the symbol labeling the edge
	-	entry: the state the edge arrives to

Returns:: false if the call transition does not exist in the NWA

Parameters:

	-	from: the state the edge departs from
	-	sym: the symbol labeling the edge
	-	to: the state the edge arrives to

Returns:: false if the call transition does not exist in the NWA

References opennwa::EPSILON, isState(), isSymbol(), opennwa::details::TransitionStorage::removeCall(), and trans.

bool opennwa::Nwa::removeCallTrans ( const Call & ct )

Removes the given call transition from the NWA.

remove a call transition from the NWA

Removes the specified call transition from the NWA, if present. If it was not present, this function is a no-op (apart from the return value). The return value indicates whether the transition was successfully removed.

Parameters:

-

ct: the call transition to remove

Returns:: false if the call transition does not exist in the NWA

Parameters:

-

ct: the call transition to remove

Returns:: false if the call transition does not exist in the NWA

References opennwa::EPSILON, opennwa::details::TransitionStorage::getCallSite(), opennwa::details::TransitionStorage::getCallSym(), opennwa::details::TransitionStorage::getEntry(), isState(), isSymbol(), opennwa::details::TransitionStorage::removeCall(), and trans.

size_t opennwa::Nwa::sizeCallTrans ( ) const

Returns the number of call transitions in this NWA.

returns the number of call transitions associated with this NWA

Returns:: the number of call transitions in this NWA; the number of call transitions associated with this NWA

References opennwa::details::TransitionStorage::sizeCall(), and trans.

bool opennwa::Nwa::addReturnTrans	(	State	from,
		State	pred,
		Symbol	sym,
		State	to
	)

Adds a return transition to the NWA.

add a return transition to the NWA

If the return transition is already present, this function is a no-op (other than the return value). The return value indicates whether the transition was successfully added.

Note: 'sym' cannot be EPSILON.

Parameters:

	-	exit: the state the edge departs from
	-	sym: the symbol labeling the edge
	-	ret: the state the edge arrives to

Returns:: false if the return transition already exists in the NWA

Parameters:

	-	from: the state the edge departs from
	-	pred: the state from which the call was initiated
	-	sym: the symbol labeling the edge
	-	to: the state the edge arrives to

Returns:: false if the return transition already exists in the NWA

References opennwa::details::TransitionStorage::addReturn(), addState(), addSymbol(), opennwa::EPSILON, and trans.

Referenced by _private_determinize_(), _private_intersect_(), _private_star_(), opennwa::CallReturnTransitionInserter::operator()(), realizeImplicitTrans(), and opennwa::nwa_pds::WpdsToNwa().

bool opennwa::Nwa::addReturnTrans ( Return & rt )

Adds a return transition to the NWA.

add a return transition to the NWA

If the return transition is already present, this function is a no-op (other than the return value). The return value indicates whether the transition was successfully added.

Parameters:

-

ct: the return transition to add

Returns:: false if the return transition already exists in the NWA

Parameters:

-

rt: return transition to add to the NWA

Returns:: false if the return transition already exists in the NWA

References opennwa::details::TransitionStorage::addReturn(), addState(), addSymbol(), opennwa::EPSILON, opennwa::details::TransitionStorage::getCallSite(), opennwa::details::TransitionStorage::getExit(), opennwa::details::TransitionStorage::getReturnSite(), opennwa::details::TransitionStorage::getReturnSym(), and trans.

bool opennwa::Nwa::removeReturnTrans	(	State	from,
		Symbol	sym,
		State	to
	)

Removes (possibly multiple) matching return transition from the NWA.

remove a return transition from the NWA

Removes any return transition in the NWA with the given 'exit' state, symbol, and 'ret'urn state. If none were present, this function is a no-op (apart from the return value). The return value indicates whether any transition was successfully removed.

Parameters:

	-	exit: the state the edge departs from
	-	sym: the symbol labeling the edge
	-	to: the state the edge arrives to

Returns:: false if the return transition does not exist in the NWA

Parameters:

	-	from: of the state the edge departs from
	-	sym: the symbol labeling the edge
	-	to: the state the edge arrives to

Returns:: false if the return transition does not exist in the NWA

References opennwa::EPSILON, opennwa::details::TransitionStorage::getCallSites(), isState(), isSymbol(), opennwa::details::TransitionStorage::removeReturn(), and trans.

bool opennwa::Nwa::removeReturnTrans	(	State	from,
		State	pred,
		Symbol	sym,
		State	to
	)

Removes the given return transition from the NWA.

remove a return transition from the NWA

Removes the specified return transition from the NWA, if present. If it was not present, this function is a no-op (apart from the return value). The return value indicates whether the transition was successfully removed.

Parameters:

	-	exit: the state the edge departs from
	-	sym: the symbol labeling the edge
	-	to: the state the edge arrives to

Returns:: false if the return transition does not exist in the NWA

Parameters:

	-	from: the state the edge departs from
	-	pred: the state from which the call was initiated
	-	sym: the symbol labeling the edge
	-	to: the state the edge arrives to

Returns:: false if the return transition does not exist in the NWA

References opennwa::EPSILON, isState(), isSymbol(), opennwa::details::TransitionStorage::removeReturn(), and trans.

bool opennwa::Nwa::removeReturnTrans ( const Return & rt )

Removes the given return transition from the NWA.

remove a return transition from the NWA

Removes the specified return transition from the NWA, if present. If it was not present, this function is a no-op (apart from the return value). The return value indicates whether the transition was successfully removed.

Parameters:

-

ct: the return transition to remove

Returns:: false if the return transition does not exist in the NWA

Parameters:

-

rt: the return transition to remove

Returns:: false if the return transition does not exist in the NWA

References opennwa::EPSILON, opennwa::details::TransitionStorage::getCallSite(), opennwa::details::TransitionStorage::getExit(), opennwa::details::TransitionStorage::getReturnSite(), opennwa::details::TransitionStorage::getReturnSym(), isState(), isSymbol(), opennwa::details::TransitionStorage::removeReturn(), and trans.

size_t opennwa::Nwa::sizeReturnTrans ( ) const

Returns the number of return transitions in this NWA.

returns the number of return transitions associated with this NWA

Returns:: the number of return transitions in this NWA; the number of return transitions associated with this NWA

References opennwa::details::TransitionStorage::sizeReturn(), and trans.

void opennwa::Nwa::projectStates	(	Nwa const &	first,
		StateSet const &	prjStates
	)

References beginStates(), endStates(), removeState(), states, symbols, and trans.

bool opennwa::Nwa::isTransitionPossible	(	const State &	src,
		const Symbol &	sym,
		const State &	tgt
	)			`[virtual]`

Referenced by _private_intersect_().

void opennwa::Nwa::removeImplicitTransitions ( )

Detects (immediately) stuck states and removes them.

Detects stuck states and removes them, leaving the transitions implicit. (It only figures this for states that have no outgoing transitions other than itself; you can still have a SCC that acts as a stuck state.)

void opennwa::Nwa::pruneUnreachableForward ( const StateSet & sources )

Removes states not reachable from any of the 'sources' states.

References opennwa::details::TransitionStorage::getCallSite(), opennwa::query::getEntries(), opennwa::details::TransitionStorage::getExit(), opennwa::details::TransitionStorage::getReturns(), opennwa::details::TransitionStorage::getReturnSite(), getStates(), opennwa::query::getTargets(), removeState(), and trans.

Referenced by pruneUnreachableInitial().

void opennwa::Nwa::pruneUnreachableBackward ( const StateSet & targets )

Removes states from which none of the 'targets' are reachable.

References opennwa::details::TransitionStorage::getCallSite(), opennwa::query::getCallSites(), opennwa::details::TransitionStorage::getExit(), opennwa::details::TransitionStorage::getReturns(), opennwa::details::TransitionStorage::getReturnSite(), opennwa::query::getSources(), getStates(), removeState(), and trans.

Referenced by pruneUnreachableFinal().

void opennwa::Nwa::pruneUnreachableInitial ( )

Removes states not reachable from any initial state.

References getInitialStates(), and pruneUnreachableForward().

Referenced by chop().

void opennwa::Nwa::pruneUnreachableFinal ( )

Removes states from which none of the final states are reachable.

References getFinalStates(), and pruneUnreachableBackward().

Referenced by chop().

void opennwa::Nwa::chop ( )

Removes states not reachable from any initial state and from which none of the final states are reachable.

References pruneUnreachableFinal(), and pruneUnreachableInitial().

void opennwa::Nwa::_private_star_ ( Nwa const & first )

constructs the NWA resulting from performing Kleene-* on the given NWA

Parameters:

-

first: the NWA to perform Kleene-* on

void opennwa::Nwa::_private_determinize_ ( Nwa const & nondet )

constructs a deterministic NWA that is equivalent to the given NWA.

Parameters:

-

nondet: the NWA to determinize

References addCallTrans(), addFinalState(), addInitialState(), addInternalTrans(), addReturnTrans(), addState(), beginFinalStates(), beginInitialStates(), beginStates(), beginSymbols(), wali::relations::buddyInit(), clear(), wali::relations::compose(), DECLARE, endFinalStates(), endInitialStates(), endStates(), endSymbols(), opennwa::EPSILON, opennwa::details::TransitionStorage::getCalls(), opennwa::details::TransitionStorage::getInternals(), opennwa::details::TransitionStorage::getReturns(), opennwa::construct::intersect(), largestState(), makeKey(), wali::relations::merge(), mergeClientInfo(), mergeClientInfoCall(), mergeClientInfoInternal(), mergeClientInfoReturn(), wali::relations::project_symbol_3(), wali::relations::project_symbol_4(), relations, opennwa::details::StateStorage::setClientInfo(), states, trans, wali::relations::transitive_closure(), wali::relations::union_(), and opennwa::WILD.

void opennwa::Nwa::_private_intersect_	(	Nwa const &	first,
		Nwa const &	second
	)

constructs the NWA which is the intersection of the given NWAs

Parameters:

	-	first: the NWA to intersect with 'second'
	-	second: the NWA to intersect with 'first'

bool opennwa::Nwa::_private_isDeterministic_ ( ) const

tests whether this NWA is deterministic

Returns:: true if this NWA is deterministic, false otherwise

void opennwa::Nwa::intersectClientInfoCall	(	Nwa const &	first,
		State	call1,
		State	entry1,
		Nwa const &	second,
		State	call2,
		State	entry2,
		Symbol	resSym,
		State	resSt
	)			`[virtual]`

Intersects client information for the target of a call transition.

intersects client information

This method intersects the client information associated with the states 'entry1' and 'entry2' given that the transition that is being created is a call transition with the given symbol using the information in the given states and sets the resulting client information.

Note: This method should only be used to intersect client information for states immediately following a call transition.

This function is called during the exceution of 'constructintersect'. (This is an instance of the "template method" design pattern.)

Parameters:

	-	first: the NWA in which to look up the client information for 'call1' and 'entry1'
	-	call1: the call site associated with the first entry whose client information to intersect
	-	entry1: the first entry point whose client information to intersect
	-	second: the NWA in which to look up the client information for 'call2' and 'entry2'
	-	call2: the call site associated with the second entry whose client information to intersect
	-	entry2: the second entry point whose client information to intersect
	-	resSym: the symbol associated with the transition that is being created
	-	resSt: the state which will receive the computed client information
	-	first: the NWA in which to look up the client information for 'call1' and 'entry1'
	-	call1: the call site associated with the first entry whose client information to intersect
	-	entry1: the first entry point whose client information to intersect
	-	second: the NWA in which to look up the client information for 'call2' and 'entry2'
	-	call2: the call site associated with the second entry whose client information to intersect
	-	entry2: the second entry point whose client information to intersect
	-	resSym: the symbol associated with the transition that is being created
	-	resSt: the state which will receive the computed client information

Referenced by _private_intersect_().

void opennwa::Nwa::intersectClientInfoInternal	(	Nwa const &	first,
		State	src1,
		State	tgt1,
		Nwa const &	second,
		State	src2,
		State	tgt2,
		Symbol	resSym,
		State	resSt
	)			`[virtual]`

Intersects client information for the target of an internal transition.

intersects client information

This method intersects the client information associated with the states 'tgt1' and 'tgt2' given that the transition that is being created is an internal transition with the given symbol using the information in the given states and returns the resulting client information. Note: This method should only be used to intersect client information for states immediately following an internal transition.

This function is called during the exceution of 'constructintersect'. (This is an instance of the "template method" design pattern.)

Parameters:

	-	first: the NWA in which to look up the client information for 'src1' and 'tgt1'
	-	src1: the source associated with the first target whose client information to intersect
	-	tgt1: the first target whose client information to intersect
	-	second: the NWA in which to look up the client information for 'src2' and 'tgt2'
	-	src2: the source associated with the second target whose client information to intersect
	-	tgt2: the second target whose client information to intersect
	-	resSym: the symbol associated with the transition that is being created
	-	resSt: the state which will receive the computed client information
	-	first: the NWA in which to look up the client information for 'src1' and 'tgt1'
	-	src1: the source associated with the first target whose client information to intersect
	-	tgt1: the first target whose client information to intersect
	-	second: the NWA in which to look up the client information for 'src2' and 'tgt2'
	-	src2: the source associated with the second target whose client information to intersect
	-	tgt2: the second target whose client information to intersect
	-	resSym: the symbol associated with the transition that is being created
	-	resSt: the state which will receive the computed client information
	-	result: the client information resulting from the intersection of 'tgt1' and 'tgt2'

Referenced by _private_intersect_().

void opennwa::Nwa::intersectClientInfoReturn	(	Nwa const &	first,
		State	exit1,
		State	call1,
		State	ret1,
		Nwa const &	second,
		State	exit2,
		State	call2,
		State	ret2,
		Symbol	resSym,
		State	resSt
	)			`[virtual]`

Intersects client information for the target of a return transition.

intersects client information

This method intersects the client information associated with the states 'ret1' and 'ret2' given that the transition that is being created is a return transition with the given symbol using the information in the given states and returns the resulting client information. Note: This method should only be used to intersect client information for states immediately following a return transition.

This function is called during the exceution of 'constructintersect'. (This is an instance of the "template method" design pattern.)

Parameters:

	-	first: the NWA in which to look up the client information for 'exit1', 'call1', and 'ret1'
	-	exit1: the exit point associated with the first return site whose client information to intersect
	-	call1: the call site associated with the first return site whose client information to intersect
	-	ret1: the first return site whose client information to intersect
	-	second: the NWA in which to look up the client information for 'exit2', 'call2', and 'ret2'
	-	exit2: the exit point associated with the second return site whose client information to intersect
	-	call2: the call site associated with the second return site whose client information to intersect
	-	ret2: the second return site whose client information to intersect
	-	resSym: the symbol associated with the transition that is being created
	-	resSt: the state which will receive the computed client information
	-	first: the NWA in which to look up the client information for 'exit1', 'call1', and 'ret1'
	-	exit1: the exit point associated with the first return site whose client information to intersect
	-	call1: the call site associated with the first return site whose client information to intersect
	-	ret1: the first return site whose client information to intersect
	-	second: the NWA in which to look up the client information for 'exit2', 'call2', and 'ret2'
	-	exit2: the exit point associated with the second return site whose client information to intersect
	-	call2: the call site associated with the second return site whose client information to intersect
	-	ret2: the second return site whose client information to intersect
	-	resSym: the symbol associated with the transition that is being created
	-	resSt: the state which will receive the computed client information
	-	result: the client information resulting from the intersection of 'ret1' and 'ret2'

Referenced by _private_intersect_().

bool opennwa::Nwa::stateIntersect	(	Nwa const &	first,
		State	state1,
		Nwa const &	second,
		State	state2,
		State &	resSt,
		ClientInfoRefPtr &	resCI
	)			`[virtual]`

Intersect states.

intersect states

This method determines whether the given states can be intersected and returns the result in the reference parameter 'resSt'.

This function is called during the exceution of 'constructintersect'. (This is an instance of the "template method" design pattern.)

Parameters:

	-	first: the NWA in which to look up information about 'state1'
	-	state1: the first state to intersect
	-	second: the NWA in which to look up information about 'state2'
	-	state2: the second state to intersect
	-	resSt: the state that results from performing the intersection
	-	resCI: the client info that results from performing the intersection
	-	first: the NWA in which to look up information about 'state1'
	-	state1: the first state to intersect
	-	second: the NWA in which to look up information about 'state2'
	-	state2: the second state to intersect
	-	resSt: the state that results from performing the intersection

References wali::getKey().

Referenced by _private_intersect_().

bool opennwa::Nwa::transitionIntersect	(	Nwa const &	first,
		Symbol	sym1,
		Nwa const &	second,
		Symbol	sym2,
		Symbol &	resSym
	)			`[virtual]`

Intersect symbols.

intersect symbols

This method performs the intersection of the given symbols and returns the result in the reference parameter 'resSym'.

This function is called during the exceution of 'constructintersect'. (This is an instance of the "template method" design pattern.)

Parameters:

	-	first: the NWA in which to look up information about 'sym1'
	-	sym1: the first symbol to intersect
	-	second: the NWA in which to look up information about 'sym2'
	-	sym2: the second symbol to intersect
	-	resSym: the symbol that results from performing the intersection
	-	first: the NWA in which to look up information about 'sym1'
	-	sym1: the first symbol to intersect
	-	second: the NWA in which to look up information about 'sym2'
	-	sym2: the second symbol to intersect
	-	resSym: the symbol that results from performing the intersection

References opennwa::EPSILON, and opennwa::WILD.

Referenced by _private_intersect_().

virtual void opennwa::Nwa::mergeClientInfo	(	Nwa const &	nwa,
		BinaryRelation const &	binRel,
		State	resSt,
		ClientInfoRefPtr &	resCI
	)			`[virtual]`

Merges clientInfo for determinize.

This method merges the client info for the given states and returns the result in the reference parameter 'resCI'.

This function is called during the exceution of 'constructdeterminize'. (This is an instance of the "template method" design pattern.)

Parameters:

	-	nwa: the NWA in which to look up information about the states
	-	binRel: the states to merge
	-	resSt: the state resulting from the merge
	-	resCI: the client info that results from performing the merge

Referenced by _private_determinize_().

virtual void opennwa::Nwa::mergeClientInfoCall	(	Nwa const &	nwa,
		BinaryRelation const &	binRelCall,
		BinaryRelation const &	binRelEntry,
		State	callSt,
		Symbol	resSym,
		State	resSt,
		ClientInfoRefPtr &	resCI
	)			`[virtual]`

Merges clientInfo for determinize for the target of a call transition.

This method merges the client info for the given entry states given that the transition that is being created is a call transition with the given symbol using the information in the given states and returns the result in the reference parameter 'resCI'.

Parameters:

	-	nwa: the NWA in which to look up information about the states
	-	binRelCall: the states that compose the call site for this call transition
	-	binRelEntry: the states to merge that compose the entry point for this call transition
	-	callSt: the call site of the transition that is being created
	-	resSym: the symbol associated with the transition that is being created
	-	resSt: the state resulting from the merge
	-	resCI: the client info that results from performing the merge

Referenced by _private_determinize_().

virtual void opennwa::Nwa::mergeClientInfoInternal	(	Nwa const &	nwa,
		BinaryRelation const &	binRelSource,
		BinaryRelation const &	binRelTarget,
		State	sourceSt,
		Symbol	resSym,
		State	resSt,
		ClientInfoRefPtr &	resCI
	)			`[virtual]`

Merges clientInfo for determinize for the target of an internal transition.

This method merges the client info for the given target states given that the transition that is being created is an internal transition with the given symbol using the information in the given states and returns the result in the reference parameter 'resCI'.

This function is called during the exceution of 'constructdeterminize'. (This is an instance of the "template method" design pattern.)

Parameters:

	-	nwa: the NWA in which to look up information about the states
	-	binRelSource: the states that compose the source for this internal transition
	-	binRelTarget: the states to merge that compose the target for this internal transition
	-	sourceSt: the source of the transition that is being created
	-	resSym: the symbol associated with the transition that is being created
	-	resSt: the state resulting from the merge
	-	resCI: the client info that results from performing the merge

Referenced by _private_determinize_().

virtual void opennwa::Nwa::mergeClientInfoReturn	(	Nwa const &	nwa,
		BinaryRelation const &	binRelExit,
		BinaryRelation const &	binRelCall,
		BinaryRelation const &	binRelReturn,
		State	exitSt,
		State	callSt,
		Symbol	resSym,
		State	resSt,
		ClientInfoRefPtr &	resCI
	)			`[virtual]`

Merges clientInfo for determinize for the target of a return transition.

This method merges the client info for the given return states given that the transition that is being created is a return transition with the given symbol using the information in the given states and returns the result in the reference parameter 'resCI'.

This function is called during the exceution of 'constructdeterminize'. (This is an instance of the "template method" design pattern.)

Parameters:

	-	nwa: the NWA in which to look up information about the states
	-	binRelExit: the states that compose the exit point for this return transition
	-	binRelCall: the states that compose the call site for this return transition
	-	binRelReturn: the states to merge that compose the return site for this return transition
	-	exitSt: the exit point of the transition that is being created
	-	callSt: the call site of the transition that is being created
	-	resSym: the symbol associated with the transition that is being created
	-	resSt: the state resulting from the merge
	-	resCI: the client info that results from performing the merge

Referenced by _private_determinize_().

WPDS opennwa::Nwa::_private_NwaToPdsReturns_ ( WeightGen const & wg ) const

Referenced by opennwa::nwa_pds::NwaToWpdsReturns().

WPDS opennwa::Nwa::_private_NwaToBackwardsPdsReturns_ ( WeightGen const & wg ) const

Referenced by opennwa::nwa_pds::NwaToBackwardsWpdsReturns().

WPDS opennwa::Nwa::_private_NwaToPdsCalls_	(	WeightGen const &	wg,
		ref_ptr< wali::wpds::Wrapper >	wrapper
	)			const

Referenced by opennwa::nwa_pds::NwaToWpdsCalls().

WPDS opennwa::Nwa::_private_NwaToBackwardsPdsCalls_ ( WeightGen const & wg ) const

Referenced by opennwa::nwa_pds::NwaToBackwardsWpdsCalls().

bool opennwa::Nwa::_private_isEmpty_ ( ) const

tests whether the language accepted by this NWA is empty

This method tests whether the language accepted by this NWA is empty.

Returns:: true if the language accepted by this NWA is empty; true if the language accepted by this NWA is empty

References wali::wfa::WFA::addFinalState(), wali::wfa::WFA::addState(), wali::wfa::WFA::addTrans(), beginFinalStates(), beginInitialStates(), beginStates(), endFinalStates(), endInitialStates(), endStates(), wali::wfa::WFA::for_each(), wali::getKey(), wali::wfa::TransCounter::getNumTrans(), opennwa::nwa_pds::getProgramControlLocation(), wali::wfa::WFA::intersect(), isFinalState(), Reach::one(), poststar(), prestar(), wali::wfa::WFA::prune(), wali::wfa::WFA::setInitialState(), sizeFinalStates(), sizeInitialStates(), and Reach::zero().

const char * opennwa::Nwa::toStringGdb ( ) const

References print().

wali::wfa::WFA opennwa::Nwa::prestar	(	wali::wfa::WFA const &	input,
		WeightGen const &	wg
	)			const

perform the prestar reachability query defined by the given WFA

This method performs the prestar reachability query defined by the given WFA.

Parameters:

	-	input: the starting point of the reachability query
	-	wg: the functions to use in generating weights

Returns:: the WFA resulting from performing the prestar reachability query

Referenced by _private_isEmpty_(), and prestar().

wali::wfa::WFA opennwa::Nwa::prestar	(	wali::wfa::WFA const &	input,
		WeightGen const &	wg,
		ref_ptr< wali::Worklist< wali::wfa::ITrans > >	worklist
	)			const `[virtual]`

perform the prestar reachability query defined by the given WFA

Parameters:

	-	input: the starting point of the reachability query
	-	wg: the functions to use in generating weights

Returns:: the WFA resulting from performing the prestar reachability query

References opennwa::nwa_pds::NwaToWpdsCalls(), wali::wpds::WPDS::prestar(), and wali::wpds::WPDS::setWorklist().

void opennwa::Nwa::prestar	(	wali::wfa::WFA const &	input,
		wali::wfa::WFA &	output,
		WeightGen const &	wg
	)			const

perform the prestar reachability query defined by the given WFA

This method performs the prestar reachability query defined by the given WFA. The result of the query is stored in the 'output' parameter. Note: Any transitions in output before the query will be there after the query but will have no effect on the reachability query.

Parameters:

	-	input: the starting point of the reachability query
	-	ouput: the result of performing the reachability query
	-	wg: the functions to use in generating weights

References prestar().

void opennwa::Nwa::prestar	(	wali::wfa::WFA const &	input,
		wali::wfa::WFA &	output,
		WeightGen const &	wg,
		ref_ptr< wali::Worklist< wali::wfa::ITrans > >	worklist
	)			const `[virtual]`

perform the prestar reachability query defined by the given WFA

Note: Any transitions in output before the query will be there after the query but will have no effect on the reachability query.

Parameters:

	-	input: the starting point of the reachability query
	-	ouput: the result of performing the reachability query
	-	wg: the functions to use in generating weights

References opennwa::nwa_pds::NwaToWpdsCalls(), wali::wpds::WPDS::prestar(), and wali::wpds::WPDS::setWorklist().

wali::wfa::WFA opennwa::Nwa::poststar	(	wali::wfa::WFA const &	input,
		WeightGen const &	wg
	)			const

perform the poststar reachability query defined by the given WFA

This method performs the poststar reachability query defined by the given WFA.

Parameters:

	-	input: the starting point of the reachability query
	-	wg: the functions to use in generating weights

Returns:: the WFA resulting from performing the poststar reachability query

Referenced by _private_isEmpty_(), and poststar().

wali::wfa::WFA opennwa::Nwa::poststar	(	wali::wfa::WFA const &	input,
		WeightGen const &	wg,
		ref_ptr< wali::Worklist< wali::wfa::ITrans > >	worklist
	)			const `[virtual]`

perform the poststar reachability query defined by the given WFA

Parameters:

	-	input: the starting point of the reachability query
	-	wg: the functions to use in generating weights

Returns:: the WFA resulting from performing the poststar reachability query

References opennwa::nwa_pds::NwaToWpdsCalls(), wali::wpds::WPDS::poststar(), and wali::wpds::WPDS::setWorklist().

void opennwa::Nwa::poststar	(	wali::wfa::WFA const &	input,
		wali::wfa::WFA &	output,
		WeightGen const &	wg
	)			const

perform the poststar reachability query defined by the given WFA

This method performs the poststar reachability query defined by the given WFA. The result of the query is stored in the 'output' parameter. Note: Any transitions in output before the query will be there after the query but will have no effect on the reachability query.

Parameters:

	-	input: the starting point of the reachability query
	-	output: the result of performing the reachability query
	-	wg: the functions to use in generating weights

References poststar().

void opennwa::Nwa::poststar	(	wali::wfa::WFA const &	input,
		wali::wfa::WFA &	output,
		WeightGen const &	wg,
		ref_ptr< wali::Worklist< wali::wfa::ITrans > >	worklist
	)			const `[virtual]`

perform the poststar reachability query defined by the given WFA

Note: Any transitions in output before the query will be there after the query but will have no effect on the reachability query.

Parameters:

	-	input: the starting point of the reachability query
	-	output: the result of performing the reachability query
	-	wg: the functions to use in generating weights

References opennwa::nwa_pds::NwaToWpdsCalls(), wali::wpds::WPDS::poststar(), and wali::wpds::WPDS::setWorklist().

std::ostream & opennwa::Nwa::print ( std::ostream & o ) const [virtual]

print the NWA

This method prints out the NWA to the output stream provided.

Parameters:

-

o: the output stream to print to

Returns:: the output stream that was printed to

Parameters:

-

o: the output stream to print to

Returns:: the output stream that was printed to

References opennwa::details::TransitionStorage::print(), opennwa::details::SymbolStorage::print(), opennwa::details::StateStorage::print(), states, symbols, and trans.

Referenced by toStringGdb().

std::ostream & opennwa::Nwa::print_dot	(	std::ostream &	o,
		std::string	title,
		bool	abbrev = `true`
	)			const `[virtual]`

print the NWA in dot format

This method prints out the NWA in dot format to the output stream provided.

Parameters:

-

o: the output stream to print to

Returns:: the output stream that was printed to

Parameters:

-

o: the output stream to print to

Returns:: the output stream that was printed to

bool opennwa::Nwa::operator== ( const Nwa & other ) const

tests whether this NWA is equivalent to the NWA 'other'

This method tests the equivalence of this NWA and the NWA 'other'.

Parameters:

-

other: the NWA to compare this NWA to

Returns:: true if this NWA is equivalent to the NWA 'other'

Parameters:

-

other: the NWA to compare this NWA to

Returns:: true if this NWA is equivalent to the NWA 'other'

References states, symbols, and trans.

void opennwa::Nwa::addAllStates ( StateStorage addStateSet )

add all the states in the given StateSet to the NWA

This method adds all of the given states to the state set for the NWA.

Parameters:

	-	addStateSet: the StateSet that contains the states to add
	-	addStateSet: the StateSet that contains the states to add

References opennwa::details::StateStorage::addAllStates(), and states.

void opennwa::Nwa::addAllInitialStates ( StateStorage addStateSet )

adds all of the states in the given StateSet to the initial state set associated with this NWA

This method adds all of the states associated with the given StateSet to the initial state set associated with this NWA.

Parameters:

	-	addStateSet: the state set whose initial states to add to this NWA's initial state set
	-	addStateSet: the state set whose initial states to add to this NWA's initial state set

References opennwa::details::StateStorage::addAllInitialStates(), and states.

void opennwa::Nwa::addAllFinalStates ( StateStorage addStateSet )

adds all of the final states in the given StateSet to the final state set associated with this NWA

This method adds all of the final states associated with the given StateSet to the final state set associated with this NWA.

Parameters:

	-	addStateSet: the StateSet whose final states to add to this NWA's final state set
	-	addStateSet: the StateSet whose final states to add to this NWA's final state set

References opennwa::details::StateStorage::addAllFinalStates(), and states.

void opennwa::Nwa::addAllSymbols ( SymbolStorage addSymbolSet )

add the given symbols to the NWA

This method adds all of the given symbols to the set of symbols associated with the NWA.

Parameters:

	-	addSymbolSet: the symbols to add
	-	addSymbolSet: the symbols to add

References opennwa::details::SymbolStorage::addAllSymbols(), and symbols.

Referenced by combineWith().

Nwa::StateIterator opennwa::Nwa::beginStates ( ) const

provide access to the beginning of the state set

This method provides access to the beginning of the state set associated with this NWA.

Returns:: an iterator pointing to the beginning of the state set; an iterator pointing to the beginning of the state set

References opennwa::details::StateStorage::beginStates(), and states.

Referenced by _private_determinize_(), _private_isDeterministic_(), _private_isEmpty_(), _private_star_(), marshall(), print_dot(), projectStates(), realizeImplicitTrans(), and removeImplicitTransitions().

Nwa::StateIterator opennwa::Nwa::endStates ( ) const

provide access to the end of the state set

This method provides access to the position one past the end of the state set associated with this transition set.

Returns:: an iterator pointing just past the end of the state set; an iterator pointing just past the end of the state set

References opennwa::details::StateStorage::endStates(), and states.

Referenced by _private_determinize_(), _private_isDeterministic_(), _private_isEmpty_(), _private_star_(), marshall(), print_dot(), projectStates(), realizeImplicitTrans(), and removeImplicitTransitions().

Nwa::StateIterator opennwa::Nwa::beginInitialStates ( ) const

provide access to the beginning of the initial state set

This method provides access to the beginning of the initial state set associated with this NWA.

Returns:: an iterator pointing to the beginning of the initial state set; an iterator pointing to the beginning of the initial state set

References opennwa::details::StateStorage::beginInitialStates(), and states.

Referenced by _private_determinize_(), _private_intersect_(), _private_isEmpty_(), _private_star_(), opennwa::query::getSomeAcceptedWordInternal(), and isMemberNondet().

Nwa::StateIterator opennwa::Nwa::endInitialStates ( ) const

provide access to the end of the initial state set

This method provides access to the position one past the end of the initial state set associated with this NWA.

Returns:: an iterator pointing just past the end of the initial state set; an iterator pointing just past the end of the initial state set

References opennwa::details::StateStorage::endInitialStates(), and states.

Referenced by _private_determinize_(), _private_intersect_(), _private_isEmpty_(), _private_star_(), opennwa::query::getSomeAcceptedWordInternal(), and isMemberNondet().

Nwa::StateIterator opennwa::Nwa::beginFinalStates ( ) const

provide access to the beginning of the final state set

This method provides access to the beginning of the final state set associated with this NWA.

Returns:: an iterator pointing to the beginning of the final state set; an iterator pointing to the beginning of the final state set

References opennwa::details::StateStorage::beginFinalStates(), and states.

Referenced by _private_determinize_(), _private_isEmpty_(), _private_star_(), and opennwa::query::getSomeAcceptedWordInternal().

Nwa::StateIterator opennwa::Nwa::endFinalStates ( ) const

provide access to the end of the final state set

This method provides access to the position one past the end of the final state set associated with this NWA.

Returns:: an iterator pointing just past the end of the final state set; an iterator pointing just past the end of the final state set

References opennwa::details::StateStorage::endFinalStates(), and states.

Referenced by _private_determinize_(), _private_isEmpty_(), _private_star_(), and opennwa::query::getSomeAcceptedWordInternal().

Nwa::SymbolIterator opennwa::Nwa::beginSymbols ( ) const

provide access to the beginning of the symbol set

This method provides access to the beginning of the symbol set associated with this NWA.

Returns:: an iterator pointing to the beginning of the symbol set; an iterator pointing to the beginning of the symbol set

References opennwa::details::SymbolStorage::beginSymbols(), and symbols.

Referenced by _private_determinize_(), marshall(), and realizeImplicitTrans().

Nwa::SymbolIterator opennwa::Nwa::endSymbols ( ) const

provide access to the end of the symbol set

This method provides access to the position one past the end of the symbol set associated with NWA.

Returns:: an iterator pointing just past the end of the symbol set; an iterator pointing just past the end of the symbol set

References opennwa::details::SymbolStorage::endSymbols(), and symbols.

Referenced by _private_determinize_(), marshall(), and realizeImplicitTrans().

Nwa::CallIterator opennwa::Nwa::beginCallTrans ( ) const

provide access to the beginning of the call transition set

This method provides access to the beginning of the call transition set associated with this NWA.

Returns:: an iterator pointing to the beginning of the call transition set; an iterator pointing to the beginning of the call transition set

References opennwa::details::TransitionStorage::beginCall(), and trans.

Referenced by _private_star_(), and print_dot().

Nwa::CallIterator opennwa::Nwa::endCallTrans ( ) const

provide access to the end of the call transition set

This method provides access to the position one past the end of the call transition set associated with this NWA.

Returns:: an iterator pointing just past the end of the call transition set; an iterator pointing just past the end of the call transition set

References opennwa::details::TransitionStorage::endCall(), and trans.

Referenced by _private_star_(), and print_dot().

Nwa::InternalIterator opennwa::Nwa::beginInternalTrans ( ) const

provide access to the beginning of the internal transition set

This method provides access to the beginning of the internal transition set associated with this NWA.

Returns:: an iterator pointing to the beginning of the internal transition set; an iterator pointing to the beginning of the internal transition set

References opennwa::details::TransitionStorage::beginInternal(), and trans.

Referenced by _private_star_(), and print_dot().

Nwa::InternalIterator opennwa::Nwa::endInternalTrans ( ) const

provide access to the end of the internal transition set

This method provides access to the position one past the end of the internal transition set associated with this NWA.

Returns:: an iterator pointing just past the end of the internal transition set; an iterator pointing just past the end of the internal transition set

References opennwa::details::TransitionStorage::endInternal(), and trans.

Referenced by _private_star_(), and print_dot().

Nwa::ReturnIterator opennwa::Nwa::beginReturnTrans ( ) const

provide access to the beginning of the return transition set

This method provides access to the beginning of the return transition set associated with this NWA.

Returns:: an iterator pointing to the beginning of the return transition set; an iterator pointing to the beginning of the return transition set

References opennwa::details::TransitionStorage::beginReturn(), and trans.

Referenced by _private_star_(), print_dot(), and realizeImplicitTrans().

Nwa::ReturnIterator opennwa::Nwa::endReturnTrans ( ) const

provide access to the end of the return transition set

This method provides access to the position one past the end of the return transition set associated with this NWA.

Returns:: an iterator pointing just past the end of the return transition set; an iterator pointing just past the end of the return transition set

References opennwa::details::TransitionStorage::endReturn(), and trans.

Referenced by _private_star_(), print_dot(), and realizeImplicitTrans().

void opennwa::Nwa::epsilonClosure	(	StateSet *	newPairs,
		State	st
	)			const `[protected]`

computes the epsilon closure of the given state

computes the epsilon closure of the given states in their respective NWAs

This method computes the set of states reachable by starting at the given state and moving along epsilon transitions.

Parameters:

	-	newPairs: the set of states reachable from the initial state pair by traversing epsilon transitions
	-	sp: the starting point of the closure
	-	sp: the starting point of the closure
	-	first: the NWA that determines the transitions available to the first component of the state pair
	-	second: the NWA that determines the transitions available to the second component of the state pair

Returns:: the set of state pairs reachable from the initial state pair by traversing epsilon transitions

References opennwa::EPSILON, opennwa::details::TransitionStorage::getInternals(), opennwa::details::TransitionStorage::getTarget(), and trans.

Referenced by _private_intersect_(), epsilonClosure(), and isMemberNondet().

void opennwa::Nwa::epsilonClosure	(	std::set< StatePair > *	newPairs,
		StatePair	sp,
		Nwa const &	first,
		Nwa const &	second
	)			const `[protected]`

computes the epsilon closure of the given states in their respective NWAs

This method computes the set of state pairs reachable by starting at the given state pair and moving along epsilon transitions.

Parameters:

	-	newPairs: the set of state pairs reachable from the initial state pair by traversing epsilon transitions
	-	sp: the starting point of the closure
	-	first: the NWA that determines the transitions available to the first component of the state pair
	-	second: the NWA that determines the transitions available to the second component of the state pair
	-	sp: the starting point of the closure
	-	first: the NWA that determines the transitions available to the first component of the state pair
	-	second: the NWA that determines the transitions available to the second component of the state pair