wali::wfa::ITrans Class Reference

List of all members.

Public Types
enum	status_t {   MODIFIED,   SAME }
Public Member Functions
virtual ITrans *	copy () const =0
virtual ITrans *	copy (Key fromst, Key stk, Key tost) const =0
virtual Key	from () const =0 throw ()
virtual Key	stack () const =0 throw ()
virtual Key	to () const =0 throw ()
virtual const sem_elem_t	weight () const =0 throw ()
virtual const sem_elem_t	getDelta () const =0 throw ()
virtual Key	from ()=0 throw ()
virtual Key	stack ()=0 throw ()
virtual Key	to ()=0 throw ()
virtual sem_elem_t	weight ()=0 throw ()
virtual sem_elem_t	getDelta ()=0 throw ()
virtual void	setWeight (sem_elem_t w)=0
virtual void	setDelta (const sem_elem_t w)=0
virtual void	combineTrans (ITrans *tp)=0
virtual const KeyPair &	keypair () const =0 throw ()
virtual bool	modified () const =0 throw ()
	return true if the transition has been modified
virtual wpds::Config *	getConfig () const =0
virtual void	setConfig (wpds::Config *c)=0
virtual sem_elem_t	poststar_eps_closure (sem_elem_t se)=0
virtual TaggedWeight	apply_post (TaggedWeight tw) const =0
virtual TaggedWeight	apply_pre (TaggedWeight tw) const =0
virtual void	applyWeightChanger (util::WeightChanger &wc)=0
virtual bool	equal (const ITrans &rhs) const
virtual bool	equal (const ITrans *rhs) const
virtual std::ostream &	print (std::ostream &o) const
virtual std::ostream &	marshall (std::ostream &o) const
	Print ITrans in XML to ostream o.
Static Public Attributes
static const std::string	XMLTag
static const std::string	XMLFromTag
static const std::string	XMLStackTag
static const std::string	XMLToTag

---

Detailed Description

ITrans defines the interface that an automaton transition must implement.

An automaton transition is basically a 4-tuple of (p,g,q,W), where p is a "from state", g is a "stack symbol", q is a "to state", and W is a weight, or an instance of a SemElem.

IMarkable is to make a ITrans able to be placed in a Worklist.

See also:

Printable

Markable

Worklist

WFA

sem_elem_t

ref_ptr

---

Member Enumeration Documentation

enum wali::wfa::ITrans::status_t

Enumerator:

MODIFIED
SAME

---

Member Function Documentation

virtual ITrans* wali::wfa::ITrans::copy

(

)

const [pure virtual]

Returns:

a copy of the transition

Implemented in wali::wfa::DecoratorTrans, wali::wpds::ewpds::ETrans, and wali::wpds::fwpds::LazyTrans.

Referenced by wali::wfa::epr::FunctionalWeight::FunctionalWeight(), wali::wpds::WPDS::operator()(), wali::wpds::ewpds::EWPDS::operator()(), wali::wfa::TransDuplicator::operator()(), and wali::wfa::TransCopier::operator()().

virtual ITrans* wali::wfa::ITrans::copy	(	Key	fromst,
		Key	stk,
		Key	tost
	)			const [pure virtual]

Returns:

a copy of the transition with changed states and stack

Implemented in wali::wfa::DecoratorTrans, wali::wpds::ewpds::ETrans, and wali::wpds::fwpds::LazyTrans.

virtual Key wali::wfa::ITrans::from

(

)

const throw () [pure virtual]

Returns:

const Key of from state

Implemented in wali::wfa::DecoratorTrans.

Referenced by wali::KeyOrderWorklist::compareTo(), equal(), wali::wfa::WFA::eraseState(), wali::wfa::WFA::filter(), wali::wfa::DecoratorTrans::from(), wali::wfa::WFA::insert(), wali::wfa::WFA::intersect(), marshall(), wali::wpds::WPDS::operator()(), wali::wpds::ewpds::EWPDS::operator()(), wali::wfa::TransDotty::operator()(), wali::wfa::TransDuplicator::operator()(), wali::wfa::ITransLT::operator()(), wali::wpds::DebugWPDS::post(), wali::wpds::WPDS::poststar_handle_eps_trans(), wali::wpds::ewpds::EWPDS::poststar_handle_trans(), wali::wpds::DebugWPDS::poststar_handle_trans(), print(), and wali::wfa::WFA::prune().

virtual Key wali::wfa::ITrans::stack

(

)

const throw () [pure virtual]

Returns:

const Key of stack symbol

Implemented in wali::wfa::DecoratorTrans.

Referenced by wali::PriorityWorklist::compareTo(), wali::KeyOrderWorklist::compareTo(), equal(), wali::wfa::WFA::eraseState(), wali::wfa::WFA::eraseTransFromEpsMap(), wali::wfa::WFA::filter(), wali::wfa::WFA::insert(), wali::wfa::WFA::intersect(), marshall(), wali::wpds::WPDS::operator()(), wali::wpds::ewpds::EWPDS::operator()(), wali::wfa::StackHasher::operator()(), wali::wfa::TransDotty::operator()(), wali::wfa::TransDuplicator::operator()(), wali::wfa::ITransLT::operator()(), wali::wpds::DebugWPDS::post(), wali::wpds::WPDS::poststar_handle_eps_trans(), wali::wpds::ewpds::EWPDS::poststar_handle_trans(), wali::wpds::DebugWPDS::poststar_handle_trans(), print(), wali::wfa::WFA::prune(), wali::wfa::DecoratorTrans::stack(), and wali::wfa::WFA::TarjanBasicRegex().

virtual Key wali::wfa::ITrans::to

(

)

const throw () [pure virtual]

Returns:

const Key of to state

Implemented in wali::wfa::DecoratorTrans.

Referenced by wali::wfa::epr::EPA::apply(), wali::KeyOrderWorklist::compareTo(), equal(), wali::wfa::WFA::eraseState(), wali::wfa::WFA::eraseTransFromEpsMap(), wali::wfa::WFA::filter(), wali::wfa::WFA::insert(), wali::wfa::WFA::intersect(), marshall(), wali::wpds::WPDS::operator()(), wali::wpds::ewpds::EWPDS::operator()(), wali::wfa::TransDotty::operator()(), wali::wfa::TransDuplicator::operator()(), wali::wfa::ITransLT::operator()(), wali::wfa::Trans::operator=(), wali::wfa::WFA::path_summary(), wali::wpds::DebugWPDS::post(), wali::wpds::WPDS::poststar_handle_eps_trans(), wali::wpds::ewpds::EWPDS::poststar_handle_trans(), wali::wpds::DebugWPDS::poststar_handle_trans(), wali::wpds::WPDS::prestar_handle_call(), wali::wpds::ewpds::EWPDS::prestar_handle_call(), wali::wpds::ewpds::EWPDS::prestar_handle_trans(), print(), wali::wfa::WFA::prune(), wali::wfa::WFA::setupFixpoint(), wali::wfa::WFA::TarjanBasicRegex(), wali::wfa::DecoratorTrans::to(), wali::wpds::WPDS::update_prime(), wali::wpds::ewpds::EWPDS::update_prime(), and wali::wpds::DebugWPDS::update_prime().

virtual const sem_elem_t wali::wfa::ITrans::weight

(

)

const throw () [pure virtual]

Returns:

const sem_elem_t of ITrans

Implemented in wali::wfa::DecoratorTrans, and wali::wpds::fwpds::LazyTrans.

Referenced by wali::wfa::epr::EPA::apply(), wali::wfa::Trans::combineTrans(), wali::TotalOrderWorklist::compareTo(), wali::wfa::WFA::insert(), wali::wfa::WeightMaker::make_weight(), marshall(), wali::wpds::ewpds::EWPDS::operator()(), wali::wfa::TransDotty::operator()(), wali::wfa::TransZeroWeight::operator()(), wali::wfa::Trans::operator=(), wali::wfa::WFA::path_summary(), wali::wpds::DebugWPDS::post(), wali::wpds::ewpds::EWPDS::poststar_handle_trans(), wali::wpds::DebugWPDS::poststar_handle_trans(), wali::wpds::WPDS::prestar_handle_call(), wali::wpds::ewpds::EWPDS::prestar_handle_call(), wali::wpds::ewpds::EWPDS::prestar_handle_trans(), print(), wali::wfa::WFA::TarjanBasicRegex(), wali::wfa::DecoratorTrans::weight(), and wali::wpds::Wrapper::wrap().

virtual const sem_elem_t wali::wfa::ITrans::getDelta

(

)

const throw () [pure virtual]

Returns:

const sem_elem_t delta of ITrans

delta is used in computing fixpoints

Implemented in wali::wfa::DecoratorTrans.

Referenced by wali::wfa::DecoratorTrans::getDelta(), wali::wpds::DebugWPDS::post(), and wali::wpds::DebugWPDS::poststar_handle_trans().

virtual Key wali::wfa::ITrans::from

(

)

throw () [pure virtual]

Returns:

Key of from state

Implemented in wali::wfa::DecoratorTrans.

virtual Key wali::wfa::ITrans::stack

(

)

throw () [pure virtual]

Returns:

Key of stack symbol

Implemented in wali::wfa::DecoratorTrans.

virtual Key wali::wfa::ITrans::to

(

)

throw () [pure virtual]

Returns:

Key of to state

Implemented in wali::wfa::DecoratorTrans.

virtual sem_elem_t wali::wfa::ITrans::weight

(

)

throw () [pure virtual]

Returns:

sem_elem_t of ITrans

Implemented in wali::wfa::DecoratorTrans, and wali::wpds::fwpds::LazyTrans.

virtual sem_elem_t wali::wfa::ITrans::getDelta

(

)

throw () [pure virtual]

Returns:

sem_elem_t delta of ITrans

delta is used in computing fixpoints

Implemented in wali::wfa::DecoratorTrans.

virtual void wali::wfa::ITrans::setWeight

(

sem_elem_t

w

)

[pure virtual]

Set weight and delta of this ITrans to be param [w].

Parameters:

sem_elem_t

for new weight and delta

Returns:

void

Implemented in wali::wfa::DecoratorTrans, and wali::wpds::fwpds::LazyTrans.

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

virtual void wali::wfa::ITrans::setDelta

(

const sem_elem_t

w

)

[pure virtual]

Set the delta value for the ITrans.

Implemented in wali::wfa::DecoratorTrans.

Referenced by wali::wpds::DebugWPDS::post(), and wali::wfa::DecoratorTrans::setDelta().

virtual void wali::wfa::ITrans::combineTrans

(

ITrans *

tp

)

[pure virtual]

When inserting a transition into an automaton, the WFA will check to see if the transition already exists. If so, let told be the existing transition and tnew be the transition being inserted. Then the WFA invokes: told->combineTrans( tnew )

Parameters:

ITrans*

the new ITrans to be "absorbed"

Implemented in wali::wfa::DecoratorTrans, and wali::wpds::fwpds::LazyTrans.

Referenced by wali::wfa::DecoratorTrans::combineTrans(), and wali::wfa::WFA::insert().

virtual const KeyPair& wali::wfa::ITrans::keypair

(

)

const throw () [pure virtual]

Return const referenct to this transitions KeyPair

The KeyPair holds the from state and stack symbol.

See also:

KeyPair

Returns:

const KeyPair reference

Implemented in wali::wfa::DecoratorTrans.

Referenced by wali::wfa::WFA::eraseTransFromKpMap(), wali::wfa::WFA::insert(), wali::wfa::DecoratorTrans::keypair(), and wali::wfa::Trans::operator=().

virtual bool wali::wfa::ITrans::modified

(

)

const throw () [pure virtual]

return true if the transition has been modified

A ITrans is considered modified if when its weight changes. This includes the initial creation of a ITrans object. This follows from the fact that all ITrans can be considered (abstractly) created with a weight of ZERO

Returns:

true if this transition has been modified

Implemented in wali::wfa::DecoratorTrans.

Referenced by wali::wfa::DecoratorTrans::modified(), wali::wfa::Trans::operator=(), wali::wpds::ewpds::EWPDS::poststar_handle_trans(), wali::wpds::DebugWPDS::poststar_handle_trans(), wali::wpds::WPDS::update(), wali::wpds::ewpds::EWPDS::update(), and wali::wpds::DebugWPDS::update().

virtual wpds::Config* wali::wfa::ITrans::getConfig

(

)

const [pure virtual]

Returns:

A null pointer.

Implemented in wali::wfa::DecoratorTrans.

Referenced by wali::wfa::DecoratorTrans::getConfig(), wali::wfa::Trans::operator=(), and wali::wpds::DebugWPDS::post().

virtual void wali::wfa::ITrans::setConfig

(

wpds::Config *

c

)

[pure virtual]

Set this ITrans's Config to c.

Returns:

void

Implemented in wali::wfa::DecoratorTrans.

Referenced by wali::wpds::ewpds::EWPDS::operator()(), wali::wfa::DecoratorTrans::setConfig(), wali::wpds::WPDS::update(), wali::wpds::ewpds::EWPDS::update(), and wali::wpds::DebugWPDS::update().

virtual sem_elem_t wali::wfa::ITrans::poststar_eps_closure

(

sem_elem_t

se

)

[pure virtual]

This is used by (E)WPDS::poststar during epsilon-transistion contraction. The base case is: this->weight()->extend(se)

Implemented in wali::wfa::DecoratorTrans, and wali::wpds::ewpds::ETrans.

Referenced by wali::wfa::DecoratorTrans::poststar_eps_closure(), wali::wpds::WPDS::poststar_handle_eps_trans(), and wali::wpds::ewpds::EWPDS::poststar_handle_trans().

virtual TaggedWeight wali::wfa::ITrans::apply_post

(

TaggedWeight

tw

)

const [pure virtual]

This is used by FunctionalWeight The base case is: weight tw.weight

Implemented in wali::wpds::ewpds::ETrans, and wali::wpds::fwpds::LazyTrans.

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

virtual TaggedWeight wali::wfa::ITrans::apply_pre

(

TaggedWeight

tw

)

const [pure virtual]

This is used by FunctionalWeight The base case is: tw.weight weight

Implemented in wali::wpds::ewpds::ETrans, and wali::wpds::fwpds::LazyTrans.

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

virtual void wali::wfa::ITrans::applyWeightChanger

(

util::WeightChanger &

wc

)

[pure virtual]

This is used by WeightChanger It applies the changer to all weights stored in the transition Base case is that it is applied to t->weight()

Implemented in wali::wpds::ewpds::ETrans, and wali::wpds::fwpds::LazyTrans.

bool wali::wfa::ITrans::equal

(

const ITrans &

rhs

)

const [virtual]

Returns:

true if param rhs is equal to this

References from(), stack(), and to().

Referenced by wali::wfa::ITransEq::operator()().

bool wali::wfa::ITrans::equal

(

const ITrans *

rhs

)

const [virtual]

Returns:

true if param rhs is equal to this

References from(), stack(), and to().

std::ostream & wali::wfa::ITrans::print

(

std::ostream &

o

)

const [virtual]

Print this transition to the ostream. Overrides or implements Printable::print

Returns:

std::ostream this was written to

See also:

Printable

Reimplemented in wali::wfa::DecoratorTrans, wali::wpds::ewpds::ETrans, and wali::wpds::fwpds::LazyTrans.

References from(), wali::printKey(), stack(), to(), and weight().

Referenced by wali::wfa::WFA::eraseState(), wali::wfa::WFA::insert(), wali::wfa::TransSet::insert(), wali::wpds::WPDS::operator()(), wali::wfa::TransPrinter::operator()(), wali::wpds::DebugWPDS::post(), wali::wpds::DebugWPDS::poststarComputeFixpoint(), wali::wpds::DebugWPDS::prestarComputeFixpoint(), wali::witness::WitnessTrans::prettyPrint(), wali::wfa::epr::FunctionalWeight::print(), wali::wfa::DecoratorTrans::print(), wali::wpds::DebugWPDS::update(), wali::wpds::DebugWPDS::update_prime(), and wali::witness::VisitorPrinter::visitTrans().

std::ostream & wali::wfa::ITrans::marshall

(

std::ostream &

o

)

const [virtual]

Print ITrans in XML to ostream o.

Returns:

std::ostream the marshalled ITrans was written to.

References from(), wali::key2str(), stack(), to(), weight(), XMLFromTag, XMLStackTag, XMLTag, and XMLToTag.

Referenced by wali::wfa::TransMarshaller::operator()().

---

Member Data Documentation

const std::string wali::wfa::ITrans::XMLTag [static]

Referenced by marshall().

const std::string wali::wfa::ITrans::XMLFromTag [static]

Referenced by marshall().

const std::string wali::wfa::ITrans::XMLStackTag [static]

Referenced by marshall().

const std::string wali::wfa::ITrans::XMLToTag [static]

Referenced by marshall().

---

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

• Source/wali/wfa/ITrans.hpp
• Source/wali/wfa/ITrans.cpp