wali::wfa::Trans Class Reference

List of all members.

Public Member Functions
	Trans ()
	Trans (Key from, Key stack, Key to, sem_elem_t se)
	constructor
	Trans (const Trans &t)
	Trans (const ITrans &t)
Trans &	operator= (const Trans &t)
Trans &	operator= (const ITrans &t)
virtual	~Trans ()
virtual Trans *	copy () const
virtual Trans *	copy (Key f, Key s, Key t) const
Key	from () const throw ()
Key	from_state () const throw ()
Key	stack () const throw ()
Key	to () const throw ()
Key	to_state () const throw ()
virtual const sem_elem_t	weight () const throw ()
const sem_elem_t	getDelta () const throw ()
Key	from () throw ()
Key	from_state () throw ()
Key	stack () throw ()
Key	to () throw ()
Key	to_state () throw ()
virtual sem_elem_t	weight () throw ()
sem_elem_t	getDelta () throw ()
virtual void	setWeight (sem_elem_t w)
void	setDelta (const sem_elem_t w)
virtual void	combineTrans (ITrans *tp)
const KeyPair &	keypair () const throw ()
bool	modified () const throw ()
	return true if the transition has been modified
wpds::Config *	getConfig () const
void	setConfig (wpds::Config *c)
virtual sem_elem_t	poststar_eps_closure (sem_elem_t se)
virtual TaggedWeight	apply_post (TaggedWeight tw) const
virtual TaggedWeight	apply_pre (TaggedWeight tw) const
virtual void	applyWeightChanger (util::WeightChanger &wc)
Static Public Attributes
static int	numTrans = 0
Protected Attributes
KeyPair	kp
Key	toStateKey
sem_elem_t	se
sem_elem_t	delta
status_t	status
wpds::Config *	config
Friends
class	WFA

---

Detailed Description

A Trans is a 4-tuple of from state, stack, to state, and Weight. It represents a transition in the WFA.

Markable is to make a Trans able to be placed in a Worklist. Countable is for reference counting.

See also:

Printable

Countable

Markable

Worklist

WFA

sem_elem_t

ref_ptr

---

Constructor & Destructor Documentation

wali::wfa::Trans::Trans

(

)

Construct an empty Trans

References numTrans.

Referenced by copy().

wali::wfa::Trans::Trans	(	Key	from,
		Key	stack,
		Key	to,
		sem_elem_t	se
	)

constructor

This is used by WFA when addTrans is called.

References numTrans.

wali::wfa::Trans::Trans

(

const Trans &

t

)

References numTrans, and operator=().

wali::wfa::Trans::Trans

(

const ITrans &

t

)

References numTrans, and operator=().

wali::wfa::Trans::~Trans

(

)

[virtual]

References numTrans.

---

Member Function Documentation

Trans & wali::wfa::Trans::operator=

(

const Trans &

t

)

References config, delta, kp, se, status, toStateKey, and weight().

Referenced by Trans().

Trans & wali::wfa::Trans::operator=

(

const ITrans &

t

)

References config, delta, wali::wfa::ITrans::getConfig(), wali::wfa::ITrans::keypair(), kp, wali::wfa::ITrans::MODIFIED, wali::wfa::ITrans::modified(), wali::wfa::ITrans::SAME, se, status, wali::wfa::ITrans::to(), toStateKey, and wali::wfa::ITrans::weight().

Trans * wali::wfa::Trans::copy

(

)

const [virtual]

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

Trans * wali::wfa::Trans::copy	(	Key	f,
		Key	s,
		Key	t
	)			const [virtual]

References Trans(), and weight().

Key wali::wfa::Trans::from

(

)

const throw ()

Returns:

const Key of from state

References kp.

Referenced by copy().

Key wali::wfa::Trans::from_state

(

)

const throw ()

Returns:

const Key of from state

References kp.

Key wali::wfa::Trans::stack

(

)

const throw ()

Returns:

const Key of stack symbol

References kp.

Referenced by copy().

Key wali::wfa::Trans::to

(

)

const throw ()

Returns:

const Key of to state

References toStateKey.

Referenced by copy().

Key wali::wfa::Trans::to_state

(

)

const throw ()

Returns:

const Key of to state

References toStateKey.

virtual const sem_elem_t wali::wfa::Trans::weight

(

)

const throw () [virtual]

Returns:

const sem_elem_t of Trans

References se.

Referenced by apply_post(), apply_pre(), applyWeightChanger(), copy(), operator=(), and poststar_eps_closure().

const sem_elem_t wali::wfa::Trans::getDelta

(

)

const throw ()

Returns:

const sem_elem_t delta of Trans

delta is used in computing fixpoints

References delta.

Key wali::wfa::Trans::from

(

)

throw ()

Returns:

Key of from state

References kp.

Key wali::wfa::Trans::from_state

(

)

throw ()

Returns:

Key of from state

References kp.

Key wali::wfa::Trans::stack

(

)

throw ()

Returns:

Key of stack symbol

References kp.

Key wali::wfa::Trans::to

(

)

throw ()

Returns:

Key of to state

References toStateKey.

Key wali::wfa::Trans::to_state

(

)

throw ()

Returns:

Key of to state

References toStateKey.

virtual sem_elem_t wali::wfa::Trans::weight

(

)

throw () [virtual]

Returns:

sem_elem_t of Trans

References se.

sem_elem_t wali::wfa::Trans::getDelta

(

)

throw ()

Returns:

sem_elem_t delta of Trans

delta is used in computing fixpoints

References delta.

virtual void wali::wfa::Trans::setWeight

(

sem_elem_t

w

)

[virtual]

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

Parameters:

sem_elem_t

for new weight and delta

Returns:

void

References delta, and se.

Referenced by applyWeightChanger().

void wali::wfa::Trans::setDelta

(

const sem_elem_t

w

)

Set the delta value for the Trans.

References delta.

void wali::wfa::Trans::combineTrans

(

ITrans *

tp

)

[virtual]

Sets the weight of the Trans to be param w. The Trans's status will be set to MODIFIED if param w != this->weight(). Delta is set accordingly.

Parameters:

w

the sem_elem_t for the new weight

References delta, wali::wfa::ITrans::MODIFIED, wali::wfa::ITrans::SAME, se, status, and wali::wfa::ITrans::weight().

const KeyPair& wali::wfa::Trans::keypair

(

)

const throw ()

Return const referenct to this transitions KeyPair

The KeyPair holds the from state and stack symbol.

See also:

KeyPair

Returns:

const KeyPair reference

References kp.

bool wali::wfa::Trans::modified

(

)

const throw ()

return true if the transition has been modified

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

Returns:

true if this transition has been modified

References wali::wfa::ITrans::MODIFIED, and status.

wpds::Config * wali::wfa::Trans::getConfig

(

)

const

Returns:

A null pointer.

References config.

void wali::wfa::Trans::setConfig

(

wpds::Config *

c

)

Set this Trans's Config to c.

Returns:

void

References config.

sem_elem_t wali::wfa::Trans::poststar_eps_closure

(

sem_elem_t

se

)

[virtual]

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

References weight().

TaggedWeight wali::wfa::Trans::apply_post

(

TaggedWeight

tw

)

const [virtual]

References wali::TaggedWeight::getTag(), wali::TaggedWeight::getWeight(), and weight().

TaggedWeight wali::wfa::Trans::apply_pre

(

TaggedWeight

tw

)

const [virtual]

References wali::TaggedWeight::getTag(), wali::TaggedWeight::getWeight(), and weight().

void wali::wfa::Trans::applyWeightChanger

(

util::WeightChanger &

wc

)

[virtual]

References wali::util::WeightChanger::change_weight(), setWeight(), and weight().

---

Friends And Related Function Documentation

friend class WFA [friend]

---

Member Data Documentation

int wali::wfa::Trans::numTrans = 0 [static]

Referenced by Trans(), and ~Trans().

KeyPair wali::wfa::Trans::kp [protected]

Referenced by from(), from_state(), keypair(), operator=(), and stack().

Key wali::wfa::Trans::toStateKey [protected]

Referenced by operator=(), to(), and to_state().

sem_elem_t wali::wfa::Trans::se [mutable, protected]

Referenced by combineTrans(), operator=(), setWeight(), and weight().

sem_elem_t wali::wfa::Trans::delta [protected]

Referenced by combineTrans(), getDelta(), operator=(), setDelta(), and setWeight().

status_t wali::wfa::Trans::status [protected]

Referenced by combineTrans(), modified(), and operator=().

wpds::Config* wali::wfa::Trans::config [mutable, protected]

Used by *WPDS during pre and poststar. This is guaranteed to be NULL when not performing a reachability query.

Reimplemented in wali::wpds::LinkedTrans.

Referenced by getConfig(), operator=(), and setConfig().

---

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

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