opennwa::nwa_pds Namespace Reference

Functions
wali::wpds::WPDS	NwaToWpdsReturns (Nwa const &nwa, WeightGen const &wg)
	constructs the PDS equivalent to this NWA
wali::wpds::WPDS	NwaToWpdsCalls (Nwa const &nwa, WeightGen const &wg, ref_ptr< wali::wpds::Wrapper > wrapper)
	constructs the backwards PDS equivalent to this NWA
wali::wpds::WPDS	NwaToWpdsCalls (Nwa const &nwa, WeightGen const &wg)
wali::wpds::WPDS	NwaToBackwardsWpdsReturns (Nwa const &nwa, WeightGen const &wg)
	constructs the PDS equivalent to this NWA
wali::wpds::WPDS	NwaToBackwardsWpdsCalls (Nwa const &nwa, WeightGen const &wg)
	constructs the backwards PDS equivalent to this NWA
wali::Key	getProgramControlLocation ()
	returns the default program control location for PDSs
wali::Key	getControlLocation (Key exit, Key callSite, Key returnSite)
	returns the program control location corresponding to the given states
void	WpdsToNwa (Nwa &out, const wali::wpds::WPDS &pds)
	constructs the NWA equivalent to the given PDS
NwaRefPtr	WpdsToNwa (const wali::wpds::WPDS &pds)
	constructs the NWA equivalent to the given PDS
WPDS	plusWpds (Nwa const &nwa, const wali::wpds::WPDS &base)
	constructs the WPDS which is the result of the explicit NWA plus WPDS construction from Advanced Querying for Property Checking

---

Function Documentation

WPDS opennwa::nwa_pds::NwaToWpdsReturns	(	Nwa const &	nwa,
		WeightGen const &	wg
	)

constructs the PDS equivalent to this NWA

This method constructs the PDS that is equivalent to this NWA. Note: This version keeps returns on the stack.

Parameters:

-

wg: the functions to use in generating weights

Returns:

the PDS equivalent to this NWA

References opennwa::Nwa::_private_NwaToPdsReturns_().

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

constructs the backwards PDS equivalent to this NWA

This method constructs the backwards PDS that is equivalent to this NWA. Note: This version keeps returns on the stack.

Parameters:

-

wg: the functions to use in generating weights

Returns:

the backwards PDS equivalent to this NWA

References opennwa::Nwa::_private_NwaToPdsCalls_().

Referenced by opennwa::query::getSomeAcceptedWordInternal(), NwaToWpdsCalls(), opennwa::Nwa::poststar(), and opennwa::Nwa::prestar().

wali::wpds::WPDS opennwa::nwa_pds::NwaToWpdsCalls	(	Nwa const &	nwa,
		WeightGen const &	wg
	)

References NwaToWpdsCalls().

WPDS opennwa::nwa_pds::NwaToBackwardsWpdsReturns	(	Nwa const &	nwa,
		WeightGen const &	wg
	)

constructs the PDS equivalent to this NWA

This method constructs the PDS that is equivalent to this NWA. Note: This version keeps calls on the stack.

Parameters:

-

wg: the functions to use in generating weights

Returns:

the PDS equivalent to this NWA

References opennwa::Nwa::_private_NwaToBackwardsPdsReturns_().

WPDS opennwa::nwa_pds::NwaToBackwardsWpdsCalls	(	Nwa const &	nwa,
		WeightGen const &	wg
	)

constructs the backwards PDS equivalent to this NWA

This method constructs the backwards PDS that is equivalent to this NWA. Note: This version keeps calls on the stack.

Parameters:

-

wg: the functions to use in generating weights

Returns:

the backwards PDS equivalent to this NWA

References opennwa::Nwa::_private_NwaToBackwardsPdsCalls_().

wali::Key opennwa::nwa_pds::getProgramControlLocation

(

)

returns the default program control location for PDSs

This method provides access to the default program control location for PDSs.

Returns:

the default program control location for PDSs

References wali::getKey().

Referenced by opennwa::Nwa::_private_isEmpty_(), opennwa::Nwa::_private_NwaToBackwardsPdsCalls_(), opennwa::Nwa::_private_NwaToBackwardsPdsReturns_(), opennwa::Nwa::_private_NwaToPdsCalls_(), opennwa::Nwa::_private_NwaToPdsReturns_(), getControlLocation(), and opennwa::query::getSomeAcceptedWordInternal().

wali::Key opennwa::nwa_pds::getControlLocation	(	Key	exit,
		Key	callSite,
		Key	returnSite
	)

returns the program control location corresponding to the given states

This method provides access to the program control location corresponding to the given exit point/call site/return site triple.

Parameters:

	-	exit: the exit point corresponding to this control location
	-	callSite: the call site corresponding to this control location
	-	returnSite: the return site corresponding to this control location

Returns:

the program control location corresponding to the given states

References wali::getKey(), and getProgramControlLocation().

Referenced by opennwa::Nwa::_private_NwaToBackwardsPdsCalls_(), opennwa::Nwa::_private_NwaToBackwardsPdsReturns_(), opennwa::Nwa::_private_NwaToPdsCalls_(), and opennwa::Nwa::_private_NwaToPdsReturns_().

void opennwa::nwa_pds::WpdsToNwa	(	Nwa &	out,
		const wali::wpds::WPDS &	pds
	)

constructs the NWA equivalent to the given PDS

This method constructs the NWA that is equivalent to the given PDS. The NWA's state space tracks both the PDS's state and top stack symbol; the NWA's "stack" tracks the remainder of the PDS's stack. The symbol on each transition is the from_stack portion of the corresponding PDS rule.

Let the PDS be (P, G, D). The NWA we create is (Q, Q_0, d, Q_f); d is split up into the usual (for NWAs) components d_i, d_c, and d_r.

• Q = P x G (Tracking the PDS state + top stack symbol)
• d_i = { ((q,a), a, (q',a')) | <q, a> -> <q', a'> in D }
• d_c = { ((q,a), a, (q',b)) | <q, a> -> <q', b a'> in D }
• d_r = { ((q,a), (p,b), a, (q',a')) | <q, a> -> <q', *> in D and <p, b> -> <_, _ a'> in D }

The last rule is a little funky in a couple ways. First, it has two conditions because the pop rule doesn't let you know what's on the top of the stack, and we need to figure that out from the corresponding push rule.

Second, note that the push rules we look at in the condition is totally unconstrained. This is because, with the exception of the "revealed" stack symbol a', everything that the push rule talks about concerns the call predecessor (p,b) and entry node (_,_); nothing the pop rule talks about -- q, a, or q' -- has any relation to those.

This last fact means that the NWA we construct can potentially have quadratically-many rules as the input PDS. If the PDS has M push rules and N pop rules, the NWA will have M*N return transitions.

Parameters:

-

pds: the pds to convert

Returns:

the NWA equivalent to the given PDS

References opennwa::Nwa::addCallTrans(), opennwa::Nwa::addInternalTrans(), opennwa::Nwa::addReturnTrans(), opennwa::Nwa::clear(), wali::wpds::WPDS::for_each(), wali::getKey(), wali::wpds::WpdsRules::popRules, wali::wpds::WpdsRules::pushRules, and wali::wpds::WpdsRules::stepRules.

Referenced by WpdsToNwa().

NwaRefPtr opennwa::nwa_pds::WpdsToNwa

(

const wali::wpds::WPDS &

pds

)

constructs the NWA equivalent to the given PDS

This method constructs the NWA that is equivalent to the given PDS.

Parameters:

	-	pds: the pds to convert
	-	stuck: dummy parameter

Returns:

the NWA equivalent to the given PDS

References WpdsToNwa().

wali::wpds::WPDS opennwa::nwa_pds::plusWpds	(	Nwa const &	nwa,
		const wali::wpds::WPDS &	base
	)

constructs the WPDS which is the result of the explicit NWA plus WPDS construction from Advanced Querying for Property Checking

This method constructs the WPDS which allows WPDS reachability to be used to perform property checking using this NWA and the given WPDS.

Parameters:

	-	base: the WPDS that forms the basis for the constructed WPDS
	-	nwa: the NWA to process

Returns:

the WPDS which can be used to perform property checking using PDS reachability