wali::wpds::WPDS Class Reference

List of all members.

Public Member Functions
	WPDS ()
	WPDS (ref_ptr< Wrapper > wrapper)
	WPDS (const WPDS &w)
virtual	~WPDS ()
virtual void	clear ()
	Clears all rules from the WPDS.
void	setWorklist (ref_ptr< Worklist< wfa::ITrans > > wl)
	Set the worklist used for pre and poststar queries.
virtual bool	add_rule (Key from_state, Key from_stack, Key to_state, sem_elem_t se)
	create rule with no r.h.s.
virtual bool	add_rule (Key from_state, Key from_stack, Key to_state, Key to_stack1, sem_elem_t se)
	create rule with one r.h.s.
virtual bool	add_rule (Key from_state, Key from_stack, Key to_state, Key to_stack1, Key to_stack2, sem_elem_t se)
	create rule with two r.h.s.
virtual bool	replace_rule (Key from_state, Key from_stack, Key to_state, sem_elem_t se)
	create rule with no r.h.s.
virtual bool	replace_rule (Key from_state, Key from_stack, Key to_state, Key to_stack1, sem_elem_t se)
	create rule with one r.h.s.
virtual bool	replace_rule (Key from_state, Key from_stack, Key to_state, Key to_stack1, Key to_stack2, sem_elem_t se)
	create rule with two r.h.s.
virtual wfa::WFA	prestar (wfa::WFA const &input)
	Perform prestar reachability query.
virtual void	prestar (wfa::WFA const &input, wfa::WFA &output)
	Perform prestar reachability query The result of the query is stored in the parameter WFA& output.
virtual wfa::WFA	poststar (wfa::WFA const &input)
	Perform poststar reachability query.
virtual void	poststar (wfa::WFA const &input, wfa::WFA &output)
	Perform poststar reachability query.
virtual std::ostream &	print (std::ostream &o) const
	This method writes the WPDS to the passed in std::ostream parameter.
virtual std::ostream &	marshall (std::ostream &o) const
	This method marshalls the WPDS into the passed in std::ostream parameter.
virtual std::ostream &	print_dot (std::ostream &o, bool print_state=false) const
	Print the WPDS in dot format.
virtual int	count_rules () const
	Return the number of rules in the WPDS.
virtual void	for_each (ConstRuleFunctor &func) const
	apply ConstRuleFunctor to each rule in WPDS
virtual void	for_each (RuleFunctor &func)
	apply RuleFunctor to each rule in WPDS
virtual void	operator() (wfa::ITrans const *t)
	Implementation of TransFunctor.
bool	is_pds_state (wali::Key k) const
int	num_pds_states () const
const std::set< wali::Key > &	get_states () const
Key	constructCFG (std::set< Key > &entries, std::map< Key, Key > &entryState, wfa::WFA &cfg)
	Runs a poststar query on the following automaton to get one that represents the program CFG.
sem_elem_t	get_theZero ()
Static Public Attributes
static const std::string	XMLTag
Protected Types
typedef HashMap< KeyPair, Config * >	chash_t
typedef chash_t::iterator	iterator
typedef chash_t::const_iterator	const_iterator
typedef HashMap< Key, std::list< rule_t > >	r2hash_t
	r2hash_t is a map from key to list of rules.
Protected Member Functions
virtual bool	add_rule (Key from_state, Key from_stack, Key to_state, Key to_stack1, Key to_stack2, sem_elem_t se, bool replace_weight, rule_t &r)
	Actually creates the rule, hanldes the mappings, etc.
virtual bool	add_rule (Key from_state, Key from_stack, Key to_state, Key to_stack1, Key to_stack2, sem_elem_t se, rule_t &r)
	Actually creates the rule, hanldes the mappings, etc.
virtual void	setupOutput (wfa::WFA const &input, wfa::WFA &fa)
	copy relevant material from input WFA to output WFA
virtual void	unlinkOutput (wfa::WFA &fa)
	For each t fa, t->setConfig(0).
virtual void	prestarSetupFixpoint (wfa::WFA const &input, wfa::WFA &fa)
	Gets WPDS ready for fixpoint.
virtual void	prestarComputeFixpoint (wfa::WFA &fa)
	Performs the fixpoint computation.
virtual void	pre (wfa::ITrans *t, wfa::WFA &fa)
	Performs pre for 1 ITrans.
virtual void	prestar_handle_call (wfa::ITrans *t1, wfa::ITrans *t2, rule_t &r, sem_elem_t delta)
	helper method for prestar
virtual void	prestar_handle_trans (wfa::ITrans *t, wfa::WFA &ca, rule_t &r, sem_elem_t delta)
	helper method for prestar
virtual void	poststarSetupFixpoint (wfa::WFA const &input, wfa::WFA &fa)
	Gets WPDS ready for fixpoint.
virtual void	poststarComputeFixpoint (wfa::WFA &fa)
	Performs the fixpoint computation.
virtual void	post (wfa::ITrans *t, wfa::WFA &fa)
	Performs post for 1 ITrans.
virtual void	poststar_handle_eps_trans (wfa::ITrans *teps, wfa::ITrans *tprime, sem_elem_t delta)
	helper method for poststar
virtual void	poststar_handle_trans (wfa::ITrans *t, wfa::WFA &ca, rule_t &r, sem_elem_t delta)
	helper method for poststar
virtual Key	gen_state (Key state, Key stack)
	create a new temp state from two existing states
virtual Config *	make_config (Key state, Key stack)
	link input WFA transitions to Configs
virtual bool	make_rule (Config *f, Config *t, Key stk2, bool replace_weight, rule_t &r)
	Creates a rule that links two configurations.
virtual bool	make_rule (Config *f, Config *t, Key stk2, rule_t &r)
	Creates a rule that links two configurations.
virtual Config *	find_config (Key state, Key stack)
	Find config with KeyPair(state,stack).
virtual bool	get_from_worklist (wfa::ITrans *&)
	helper method for fixpoint loop
virtual void	update (Key from, Key stack, Key to, sem_elem_t se, Config *cfg)
	helper function to create and link a transition
virtual wfa::ITrans *	update_prime (Key from, wfa::ITrans *call, rule_t r, sem_elem_t delta, sem_elem_t wWithRule)
	update_prime does not need to take a Config b/c no Config will match a transition that is created here.
const chash_t &	config_map () const
chash_t &	config_map ()
Protected Attributes
ref_ptr< Wrapper >	wrapper
ref_ptr< Worklist< wfa::ITrans > >	worklist
chash_t	configs
std::set< Config * >	rule_zeroes
r2hash_t	r2hash
wfa::WFA *	currentOutputWFA
	Points to the output automaton during a pre or poststar query.
sem_elem_t	theZero
	theZero holds onto the semiring zero weight for this WPDS.
std::set< wali::Key >	pds_states

---

Member Typedef Documentation

typedef HashMap< KeyPair,Config * > wali::wpds::WPDS::chash_t [protected]

typedef chash_t::iterator wali::wpds::WPDS::iterator [protected]

typedef chash_t::const_iterator wali::wpds::WPDS::const_iterator [protected]

typedef HashMap< Key, std::list< rule_t > > wali::wpds::WPDS::r2hash_t [protected]

r2hash_t is a map from key to list of rules.

The key is the second RHS stack symbol of a rule. For example, the rule R1 = < s1,a > -> < s2, b c > will add R1 to the list that is mapped to by the stack symbol c.

---

Constructor & Destructor Documentation

wali::wpds::WPDS::WPDS

(

)

wali::wpds::WPDS::WPDS

(

ref_ptr< Wrapper >

wrapper

)

wali::wpds::WPDS::WPDS

(

const WPDS &

w

)

References for_each(), and wrapper.

wali::wpds::WPDS::~WPDS

(

)

[virtual]

References clear().

---

Member Function Documentation

void wali::wpds::WPDS::clear

(

)

[virtual]

Clears all rules from the WPDS.

References wali::HashMap< Key, Data, HashFunc, EqualFunc >::begin(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::clear(), config_map(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), pds_states, r2hash, rule_zeroes, and worklist.

Referenced by ~WPDS().

void wali::wpds::WPDS::setWorklist

(

ref_ptr< Worklist< wfa::ITrans > >

wl

)

Set the worklist used for pre and poststar queries.

References wali::waliErr, and worklist.

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

bool wali::wpds::WPDS::add_rule	(	Key	from_state,
		Key	from_stack,
		Key	to_state,
		sem_elem_t	se
	)			[virtual]

create rule with no r.h.s.

stack symbols

Returns:

true if rule existed

See also:

sem_elem_t

Key

Reimplemented in wali::wpds::ewpds::EWPDS.

Referenced by opennwa::Nwa::_private_NwaToBackwardsPdsCalls_(), opennwa::Nwa::_private_NwaToBackwardsPdsReturns_(), opennwa::Nwa::_private_NwaToPdsCalls_(), opennwa::Nwa::_private_NwaToPdsReturns_(), add_rule(), wali::wpds::RuleCopier::operator()(), and replace_rule().

bool wali::wpds::WPDS::add_rule	(	Key	from_state,
		Key	from_stack,
		Key	to_state,
		Key	to_stack1,
		sem_elem_t	se
	)			[virtual]

create rule with one r.h.s.

stack symbol

Returns:

true if rule existed

See also:

sem_elem_t

Key

Reimplemented in wali::wpds::ewpds::EWPDS.

References add_rule().

bool wali::wpds::WPDS::add_rule	(	Key	from_state,
		Key	from_stack,
		Key	to_state,
		Key	to_stack1,
		Key	to_stack2,
		sem_elem_t	se
	)			[virtual]

create rule with two r.h.s.

stack symbols

Returns:

true if rule existed

See also:

sem_elem_t

Key

Reimplemented in wali::wpds::ewpds::EWPDS.

References add_rule().

bool wali::wpds::WPDS::replace_rule	(	Key	from_state,
		Key	from_stack,
		Key	to_state,
		sem_elem_t	se
	)			[virtual]

create rule with no r.h.s.

stack symbols Replace the weight if the rule already existed

Returns:

true if rule existed

See also:

sem_elem_t

Key

Reimplemented in wali::wpds::ewpds::EWPDS.

Referenced by replace_rule().

bool wali::wpds::WPDS::replace_rule	(	Key	from_state,
		Key	from_stack,
		Key	to_state,
		Key	to_stack1,
		sem_elem_t	se
	)			[virtual]

create rule with one r.h.s.

stack symbol Replace the weight if the rule already existed

Returns:

true if rule existed

See also:

sem_elem_t

Key

Reimplemented in wali::wpds::ewpds::EWPDS.

References replace_rule().

bool wali::wpds::WPDS::replace_rule	(	Key	from_state,
		Key	from_stack,
		Key	to_state,
		Key	to_stack1,
		Key	to_stack2,
		sem_elem_t	se
	)			[virtual]

create rule with two r.h.s.

stack symbols Replace the weight if the rule already existed

Returns:

true if rule existed

See also:

sem_elem_t

Key

Reimplemented in wali::wpds::ewpds::EWPDS.

References add_rule().

virtual wfa::WFA wali::wpds::WPDS::prestar

(

wfa::WFA const &

input

)

[virtual]

Perform prestar reachability query.

Returns:

wfa::WFA

See also:

wfa::WFA

Reimplemented in wali::wpds::ewpds::EWPDS, wali::wpds::fwpds::FWPDS, and wali::wpds::fwpds::SWPDS.

Referenced by opennwa::Nwa::prestar().

virtual void wali::wpds::WPDS::prestar	(	wfa::WFA const &	input,
		wfa::WFA &	output
	)			[virtual]

Perform prestar reachability query The result of the query is stored in the parameter WFA& output.

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

Returns:

void

See also:

wfa::WFA

Reimplemented in wali::wpds::fwpds::FWPDS, and wali::wpds::fwpds::SWPDS.

virtual wfa::WFA wali::wpds::WPDS::poststar

(

wfa::WFA const &

input

)

[virtual]

Perform poststar reachability query.

Returns:

WFA

See also:

wfa::WFA

Reimplemented in wali::wpds::fwpds::FWPDS, and wali::wpds::fwpds::SWPDS.

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

virtual void wali::wpds::WPDS::poststar	(	wfa::WFA const &	input,
		wfa::WFA &	output
	)			[virtual]

Perform poststar reachability query.

The result of the query is stored in the parameter WFA& output. Any transitions in output before the query will be there after the query but will have no effect on the reachability query.

Returns:

wfa::WFA

See also:

wfa::WFA

Reimplemented in wali::wpds::fwpds::FWPDS, and wali::wpds::fwpds::SWPDS.

std::ostream & wali::wpds::WPDS::print

(

std::ostream &

o

)

const [virtual]

This method writes the WPDS to the passed in std::ostream parameter.

Implements Printable::print.

Parameters:

o

the std::ostream this is written to

Returns:

std::ostream this was written to

See also:

Printable

Reimplemented in wali::wpds::ewpds::EWPDS.

References for_each().

std::ostream & wali::wpds::WPDS::marshall

(

std::ostream &

o

)

const [virtual]

This method marshalls the WPDS into the passed in std::ostream parameter.

Marshalling simply writes the WPDS in XML form.

Returns:

std::ostream the WPDS was marshalled into

Reimplemented in wali::wpds::ewpds::EWPDS.

References for_each(), and XMLTag.

std::ostream & wali::wpds::WPDS::print_dot	(	std::ostream &	o,
		bool	print_state = false
	)			const [virtual]

Print the WPDS in dot format.

The format is a little strange: by default it does not print state information (since there is typically only one state in a WPDS), however, it can be included optionally.

Additionally, delta-0 edges are drawn as edges to nowhere (indicating "I don't know where this goes, since it is dynamic"), and delta-2 edges use the stack symbol which is pushed as the edge label, and call the top of stack symbol the state.

Printing weights is not currently supported, though it would not be difficult to add.

References for_each().

int wali::wpds::WPDS::count_rules

(

)

const [virtual]

Return the number of rules in the WPDS.

Note that this function takes time O(num rules), not constant time.

References wali::wpds::Config::begin(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::begin(), config_map(), wali::wpds::Config::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), and wali::HashMap< Key, Data, HashFunc, EqualFunc >::value().

void wali::wpds::WPDS::for_each

(

ConstRuleFunctor &

func

)

const [virtual]

apply ConstRuleFunctor to each rule in WPDS

See also:

ConstRuleFunctor

Rule

rule_t

References wali::wpds::Config::begin(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::begin(), config_map(), wali::wpds::Config::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), and wali::HashMap< Key, Data, HashFunc, EqualFunc >::value().

Referenced by constructCFG(), wali::wpds::ewpds::EWPDS::EWPDS(), marshall(), wali::wpds::ewpds::EWPDS::marshall(), wali::wpds::fwpds::SWPDS::preprocess(), print(), print_dot(), WPDS(), and opennwa::nwa_pds::WpdsToNwa().

void wali::wpds::WPDS::for_each

(

RuleFunctor &

func

)

[virtual]

apply RuleFunctor to each rule in WPDS

See also:

RuleFunctor

Rule

rule_t

References wali::wpds::Config::begin(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::begin(), config_map(), wali::wpds::Config::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), and wali::HashMap< Key, Data, HashFunc, EqualFunc >::value().

void wali::wpds::WPDS::operator()

(

wfa::ITrans const *

t

)

[virtual]

Implementation of TransFunctor.

Implements wali::wfa::ConstTransFunctor.

Reimplemented in wali::wpds::ewpds::EWPDS.

References wali::wfa::WFA::addTrans(), wali::wfa::ITrans::copy(), currentOutputWFA, wali::wfa::ITrans::from(), is_pds_state(), wali::is_strict(), wali::ref_ptr< T >::is_valid(), make_config(), wali::wfa::ITrans::print(), wali::wfa::ITrans::stack(), wali::wfa::ITrans::to(), wali::waliErr, worklist, and wrapper.

bool wali::wpds::WPDS::is_pds_state

(

wali::Key

k

)

const

References pds_states.

Referenced by operator()(), and wali::wpds::ewpds::EWPDS::operator()().

int wali::wpds::WPDS::num_pds_states

(

)

const

References pds_states.

const std::set<wali::Key>& wali::wpds::WPDS::get_states

(

)

const

References pds_states.

Key wali::wpds::WPDS::constructCFG	(	std::set< Key > &	entries,
		std::map< Key, Key > &	entryState,
		wfa::WFA &	cfg
	)

Runs a poststar query on the following automaton to get one that represents the program CFG.

Ainit = { (p, e, <p,e>) | e Procedure Entry Point }

returns the PDS state p; a map [e -> <p,e>]; and poststar(Ainit)

References wali::wfa::WFA::addTrans(), currentOutputWFA, wali::wpds::WpdsStackSymbols::entryPoints, for_each(), gen_state(), wali::wfa::WFA::getGeneration(), pds_states, poststar(), wali::wfa::WFA::setGeneration(), wali::wfa::WFA::setInitialState(), theZero, and wali::waliErr.

sem_elem_t wali::wpds::WPDS::get_theZero

(

)

References theZero.

bool wali::wpds::WPDS::add_rule	(	Key	from_state,
		Key	from_stack,
		Key	to_state,
		Key	to_stack1,
		Key	to_stack2,
		sem_elem_t	se,
		bool	replace_weight,
		rule_t &	r
	)			[protected, virtual]

Actually creates the rule, hanldes the mappings, etc.

Replace the weight if the rule already existed and replace_weight is set, otherwise take a combine of the weights

Returns:

true if rule existed

See also:

sem_elem_t

Key

Reimplemented in wali::wpds::ewpds::EWPDS.

References wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::find(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::insert(), wali::wpds::rule_t::is_valid(), wali::ref_ptr< T >::is_valid(), make_config(), make_rule(), pds_states, r2hash, rule_zeroes, and theZero.

bool wali::wpds::WPDS::add_rule	(	Key	from_state,
		Key	from_stack,
		Key	to_state,
		Key	to_stack1,
		Key	to_stack2,
		sem_elem_t	se,
		rule_t &	r
	)			[protected, virtual]

Actually creates the rule, hanldes the mappings, etc.

Returns:

true if rule existed

See also:

sem_elem_t

Key

Reimplemented in wali::wpds::ewpds::EWPDS.

References wali::HashMap< Key, Data, HashFunc, EqualFunc >::end(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::find(), wali::HashMap< Key, Data, HashFunc, EqualFunc >::insert(), wali::wpds::rule_t::is_valid(), wali::ref_ptr< T >::is_valid(), make_config(), make_rule(), pds_states, r2hash, rule_zeroes, and theZero.

virtual void wali::wpds::WPDS::setupOutput	(	wfa::WFA const &	input,
		wfa::WFA &	fa
	)			[protected, virtual]

copy relevant material from input WFA to output WFA

virtual void wali::wpds::WPDS::unlinkOutput

(

wfa::WFA &

fa

)

[protected, virtual]

For each t fa, t->setConfig(0).

Referenced by wali::wpds::ewpds::EWPDS::prestar().

virtual void wali::wpds::WPDS::prestarSetupFixpoint	(	wfa::WFA const &	input,
		wfa::WFA &	fa
	)			[protected, virtual]

Gets WPDS ready for fixpoint.

Referenced by wali::wpds::fwpds::FWPDS::prestar(), and wali::wpds::ewpds::EWPDS::prestar().

virtual void wali::wpds::WPDS::prestarComputeFixpoint

(

wfa::WFA &

fa

)

[protected, virtual]

Performs the fixpoint computation.

Reimplemented in wali::wpds::DebugWPDS.

Referenced by wali::wpds::fwpds::FWPDS::prestar(), and wali::wpds::ewpds::EWPDS::prestar().

virtual void wali::wpds::WPDS::pre	(	wfa::ITrans *	t,
		wfa::WFA &	fa
	)			[protected, virtual]

Performs pre for 1 ITrans.

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

void wali::wpds::WPDS::prestar_handle_call	(	wfa::ITrans *	t1,
		wfa::ITrans *	t2,
		rule_t &	r,
		sem_elem_t	delta
	)			[protected, virtual]

helper method for prestar

Reimplemented in wali::wpds::ewpds::EWPDS.

References wali::wfa::ITrans::to(), update(), and wali::wfa::ITrans::weight().

virtual void wali::wpds::WPDS::prestar_handle_trans	(	wfa::ITrans *	t,
		wfa::WFA &	ca,
		rule_t &	r,
		sem_elem_t	delta
	)			[protected, virtual]

helper method for prestar

virtual void wali::wpds::WPDS::poststarSetupFixpoint	(	wfa::WFA const &	input,
		wfa::WFA &	fa
	)			[protected, virtual]

Gets WPDS ready for fixpoint.

Referenced by wali::wpds::fwpds::FWPDS::poststarIGR().

virtual void wali::wpds::WPDS::poststarComputeFixpoint

(

wfa::WFA &

fa

)

[protected, virtual]

Performs the fixpoint computation.

Reimplemented in wali::wpds::DebugWPDS.

Referenced by wali::wpds::fwpds::FWPDS::poststarIGR().

virtual void wali::wpds::WPDS::post	(	wfa::ITrans *	t,
		wfa::WFA &	fa
	)			[protected, virtual]

Performs post for 1 ITrans.

Reimplemented in wali::wpds::DebugWPDS.

void wali::wpds::WPDS::poststar_handle_eps_trans	(	wfa::ITrans *	teps,
		wfa::ITrans *	tprime,
		sem_elem_t	delta
	)			[protected, virtual]

helper method for poststar

References wali::wfa::ITrans::from(), make_config(), wali::wfa::ITrans::poststar_eps_closure(), wali::wfa::ITrans::stack(), wali::wfa::ITrans::to(), and update().

virtual void wali::wpds::WPDS::poststar_handle_trans	(	wfa::ITrans *	t,
		wfa::WFA &	ca,
		rule_t &	r,
		sem_elem_t	delta
	)			[protected, virtual]

helper method for poststar

Reimplemented in wali::wpds::DebugWPDS.

Key wali::wpds::WPDS::gen_state	(	Key	state,
		Key	stack
	)			[protected, virtual]

create a new temp state from two existing states

Generate's a key representing the entry point to a procedure.

gen_state is only used by poststar

Returns:

Key for new state

References currentOutputWFA, wali::wfa::WFA::getGeneration(), and wali::getKey().

Referenced by constructCFG(), wali::wpds::ewpds::EWPDS::poststar_handle_trans(), wali::wpds::DebugWPDS::poststar_handle_trans(), and wali::wpds::fwpds::SWPDS::preprocess().

Config * wali::wpds::WPDS::make_config	(	Key	state,
		Key	stack
	)			[protected, virtual]

link input WFA transitions to Configs

Creates a Config if one does not already exist with KeyPair (state,stack).

See also:

Config

wfa::ITrans Create the Config for the state and stack KeyPair. If the Config already exists just return that.

Returns:

Config pointer

Config(state,stack)

References config_map(), find_config(), and wali::HashMap< Key, Data, HashFunc, EqualFunc >::insert().

Referenced by add_rule(), wali::wpds::ewpds::EWPDS::add_rule(), operator()(), wali::wpds::ewpds::EWPDS::operator()(), wali::wpds::DebugWPDS::post(), poststar_handle_eps_trans(), wali::wpds::ewpds::EWPDS::poststar_handle_trans(), and wali::wpds::DebugWPDS::poststar_handle_trans().

bool wali::wpds::WPDS::make_rule	(	Config *	f,
		Config *	t,
		Key	stk2,
		bool	replace_weight,
		rule_t &	r
	)			[protected, virtual]

Creates a rule that links two configurations.

If rule exists then (combines the weight if replace_weight is false) or (replace the weight if replace_weight is true)

Returns:

true if Rule already existed

See also:

Config

sem_elem_t

rule_t

If rule exists then (combines the weight if replace_weight is false) or (replace the weight if replace_weight is true) and drops the rule passed in.

Returns:

true if Rule already existed

See also:

Config

sem_elem_t

rule_t

References wali::wpds::Config::begin(), wali::wpds::Config::end(), wali::wpds::Config::insert(), wali::ref_ptr< T >::is_valid(), wali::wpds::Config::rinsert(), and wrapper.

Referenced by add_rule(), and wali::wpds::ewpds::EWPDS::add_rule().

bool wali::wpds::WPDS::make_rule	(	Config *	f,
		Config *	t,
		Key	stk2,
		rule_t &	r
	)			[protected, virtual]

Creates a rule that links two configurations.

If rule exists then combines the weight

Returns:

true if Rule already existed

See also:

Config

sem_elem_t

rule_t

If rule exists then combines the weight and drops the rule passed in.

Returns:

true if Rule already existed

See also:

Config

sem_elem_t

rule_t

References wali::wpds::Config::begin(), wali::wpds::Config::end(), wali::wpds::Config::insert(), wali::ref_ptr< T >::is_valid(), wali::wpds::Config::rinsert(), and wrapper.

Config * wali::wpds::WPDS::find_config	(	Key	state,
		Key	stack
	)			[protected, virtual]

Find config with KeyPair(state,stack).

Returns:

the Config * or 0 if it doesn't exist

See also:

Config

KeyPair

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

Referenced by make_config().

bool wali::wpds::WPDS::get_from_worklist

(

wfa::ITrans *&

t

)

[protected, virtual]

helper method for fixpoint loop

return true if wfa::ITrans was retrieved from worklist, false if worklist is empty

References worklist.

Referenced by wali::wpds::DebugWPDS::poststarComputeFixpoint(), and wali::wpds::DebugWPDS::prestarComputeFixpoint().

void wali::wpds::WPDS::update	(	Key	from,
		Key	stack,
		Key	to,
		sem_elem_t	se,
		Config *	cfg
	)			[protected, virtual]

helper function to create and link a transition

Reimplemented in wali::wpds::DebugWPDS, and wali::wpds::ewpds::EWPDS.

References currentOutputWFA, wali::wfa::WFA::insert(), wali::wfa::ITrans::modified(), wali::wfa::ITrans::setConfig(), and worklist.

Referenced by poststar_handle_eps_trans(), and prestar_handle_call().

wfa::ITrans * wali::wpds::WPDS::update_prime	(	Key	from,
		wfa::ITrans *	call,
		rule_t	r,
		sem_elem_t delta	ATTR_UNUSED,
		sem_elem_t	wWithRule
	)			[protected, virtual]

update_prime does not need to take a Config b/c no Config will match a transition that is created here.

update_prime does not need to take a Config b/c no Config will match a transition taht is created here.

The from state is not WFA.P. Therefore we do not need to add it to the worklist.

Returns:

generated transition

Reimplemented in wali::wpds::DebugWPDS, and wali::wpds::ewpds::EWPDS.

References currentOutputWFA, wali::wfa::WFA::insert(), and wali::wfa::ITrans::to().

const chash_t& wali::wpds::WPDS::config_map

(

)

const [protected]

Returns:

const chash_t reference

References configs.

Referenced by clear(), count_rules(), find_config(), for_each(), and make_config().

chash_t& wali::wpds::WPDS::config_map

(

)

[protected]

Returns:

chash_t reference

References configs.

---

Member Data Documentation

const std::string wali::wpds::WPDS::XMLTag [static]

Reimplemented in wali::wpds::DebugWPDS, wali::wpds::ewpds::EWPDS, wali::wpds::fwpds::FWPDS, and wali::wpds::fwpds::SWPDS.

Referenced by marshall().

ref_ptr<Wrapper> wali::wpds::WPDS::wrapper [protected]

Referenced by wali::wpds::ewpds::EWPDS::add_rule(), wali::wpds::ewpds::EWPDS::EWPDS(), make_rule(), operator()(), wali::wpds::ewpds::EWPDS::operator()(), and WPDS().

ref_ptr< Worklist<wfa::ITrans> > wali::wpds::WPDS::worklist [protected]

Referenced by clear(), get_from_worklist(), operator()(), wali::wpds::ewpds::EWPDS::operator()(), setWorklist(), update(), wali::wpds::ewpds::EWPDS::update(), and wali::wpds::DebugWPDS::update().

chash_t wali::wpds::WPDS::configs [protected]

Referenced by config_map().

std::set< Config * > wali::wpds::WPDS::rule_zeroes [protected]

Referenced by add_rule(), wali::wpds::ewpds::EWPDS::add_rule(), and clear().

r2hash_t wali::wpds::WPDS::r2hash [protected]

Referenced by add_rule(), wali::wpds::ewpds::EWPDS::add_rule(), and clear().

wfa::WFA* wali::wpds::WPDS::currentOutputWFA [protected]

Points to the output automaton during a pre or poststar query.

Is NULL all other times. Point

Referenced by constructCFG(), gen_state(), operator()(), wali::wpds::ewpds::EWPDS::operator()(), wali::wpds::fwpds::FWPDS::poststarIGR(), wali::wpds::fwpds::SWPDS::preprocess(), wali::wpds::fwpds::FWPDS::prestar(), wali::wpds::ewpds::EWPDS::prestar(), update(), wali::wpds::ewpds::EWPDS::update(), wali::wpds::DebugWPDS::update(), update_prime(), wali::wpds::ewpds::EWPDS::update_prime(), and wali::wpds::DebugWPDS::update_prime().

sem_elem_t wali::wpds::WPDS::theZero [protected]

theZero holds onto the semiring zero weight for this WPDS.

It is set the very first time a rule is added to the WPDS.

WARNING: FWPDS relies on theZero being valid. If you go changing theZero, fix FWPDS.

Referenced by add_rule(), wali::wpds::ewpds::EWPDS::add_rule(), constructCFG(), get_theZero(), wali::wpds::fwpds::FWPDS::poststarIGR(), wali::wpds::fwpds::SWPDS::preprocess(), and wali::wpds::fwpds::FWPDS::prestar().

std::set<wali::Key> wali::wpds::WPDS::pds_states [protected]

Referenced by add_rule(), wali::wpds::ewpds::EWPDS::add_rule(), clear(), constructCFG(), get_states(), is_pds_state(), num_pds_states(), wali::wpds::fwpds::SWPDS::preprocess(), and wali::wpds::fwpds::SWPDS::prestar().

---

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

• Source/wali/wpds/WPDS.hpp
• Source/wali/wpds/WPDS.cpp