wali::relations Namespace Reference

Classes
struct	TernaryRelation
	This class represents a ternary relation over the set 'Subject'. More...
struct	RelationTypedefs
	This can be used in client code to hide the actual relation types. More...
struct	Component
	Private structure. More...
class	Domain
	This class represents a particular domain (set) that a given relation is over. More...
struct	BinaryRelation
	Wraps a bdd in a nice friendly package. More...
class	VectorSet
Typedefs
typedef wsr::RelationTypedefs < unsigned long > ::BinaryRelation	wsrbr
typedef wbr::RelationTypedefs < unsigned long > ::BinaryRelation	wbrbr
Functions
template<typename State >
void	compose (typename RelationTypedefs< State >::BinaryRelation &out_result, typename RelationTypedefs< State >::BinaryRelation const &r1, typename RelationTypedefs< State >::BinaryRelation const &r2)
	Composes two binary relations.
template<typename OutRelation , typename State , typename Symbol >
void	project_symbol_3 (OutRelation &out_result, std::set< Triple< State, Symbol, State > > const &delta, Symbol alpha)
	Projects out the symbol in the internal and call relation.
template<typename State >
void	merge (typename RelationTypedefs< State >::BinaryRelation &out_result, typename RelationTypedefs< State >::BinaryRelation const &r_exit, typename RelationTypedefs< State >::BinaryRelation const &r_call, typename RelationTypedefs< State >::TernaryRelation const &delta_r)
	Performs the sort of merge required for NWA return edges.
template<typename State , typename Symbol >
void	project_symbol_4 (typename RelationTypedefs< State >::TernaryRelation &out_result, std::set< Quad< State, State, Symbol, State > > const &delta, Symbol alpha)
	Projects out the symbol in the return relation.
template<typename State >
State	biggest (State s1, State s2, State s3)
template<typename State >
void	transitive_closure_no_remap (typename RelationTypedefs< State >::BinaryRelation &out_result, typename RelationTypedefs< State >::BinaryRelation const &r)
template<typename State >
void	transitive_closure (typename RelationTypedefs< State >::BinaryRelation &out_result, typename RelationTypedefs< State >::BinaryRelation const &r)
	Constructs the transitive closure of an algorithm.
template<typename Relation >
void	intersect (Relation &out_result, Relation const &r1, Relation const &r2)
	Returns the intersection of two binary relations on states.
template<typename Relation >
void	union_ (Relation &out_result, Relation const &r1, Relation const &r2)
	Returns the union of two binary relations on states.
Quad< int, int, int, int >	getFddNumbers (unsigned int largest)
void	buddyInit ()
void	compose (BinaryRelation &out_result, BinaryRelation const &r1, BinaryRelation const &r2)
	Composes two binary relations.
void	merge (BinaryRelation &out_result, BinaryRelation const &r_exit, BinaryRelation const &r_call, TernaryRelation const &delta_r)
	Performs the sort of merge required for NWA return edges.
template<typename State , typename Symbol >
void	project_symbol_4 (TernaryRelation &out_result, std::set< Quad< State, State, Symbol, State > > const &delta, Symbol alpha)
	Projects out the symbol in the return relation.
template<typename Relation >
void	transitive_closure (Relation &out_result, Relation const &r)
	Constructs the transitive closure of an algorithm.
void	intersect (BinaryRelation &out_result, BinaryRelation const &r1, BinaryRelation const &r2)
	Returns the intersection of two binary relations on states.
void	union_ (BinaryRelation &out_result, BinaryRelation const &r1, BinaryRelation const &r2)
	Returns the union of two binary relations on states.
void	counter (char *vals, int size)
int	bdd_rel_size (::bdd b, int factor)
template<typename OutRelation , typename State , typename Symbol >
void	project_symbol_3_set (OutRelation &out_result, std::set< Triple< State, Symbol, State > > const &delta, Symbol alpha)
	Projects out the symbol in the internal and call relation.
Variables
int	count

---

Typedef Documentation

typedef wsr::RelationTypedefs<unsigned long>::BinaryRelation wali::relations::wsrbr

typedef wbr::RelationTypedefs<unsigned long>::BinaryRelation wali::relations::wbrbr

---

Function Documentation

template<typename State >

void wali::relations::compose	(	typename RelationTypedefs< State >::BinaryRelation &	out_result,
		typename RelationTypedefs< State >::BinaryRelation const &	r1,
		typename RelationTypedefs< State >::BinaryRelation const &	r2
	)

Composes two binary relations.

{ (x,z) | (x,y) r1, (y,z) r2}

Parameters: out_result: The relational composition of r1 and r2 r1: relation 1 r2: relation 2

Referenced by opennwa::Nwa::_private_determinize_(), and compose().

template<typename OutRelation , typename State , typename Symbol >

void wali::relations::project_symbol_3	(	OutRelation &	out_result,
		std::set< Triple< State, Symbol, State > > const &	delta,
		Symbol	alpha
	)

Projects out the symbol in the internal and call relation.

{(source, target) | (source, alpha, target) delta}

Parameters: out_result: The relation delta restricted to alpha delta: Internals or calls relation alpha: Alphabet symbol to select and project

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

template<typename State >

void wali::relations::merge	(	typename RelationTypedefs< State >::BinaryRelation &	out_result,
		typename RelationTypedefs< State >::BinaryRelation const &	r_exit,
		typename RelationTypedefs< State >::BinaryRelation const &	r_call,
		typename RelationTypedefs< State >::TernaryRelation const &	delta_r
	)

Performs the sort of merge required for NWA return edges.

{(q, q') | (q,q1) r_call, (q1,q2) r_exit, (q2,q1,q') delta}

Parameters: out_result: The relational composition of R1 and R2 r_exit: The relation at the exit node r_call: The relation at the call node delta_r: The return transition relation with the alphabet symbol projected out

References wali::relations::TernaryRelation< Subject >::equal_range().

Referenced by opennwa::Nwa::_private_determinize_(), and merge().

template<typename State , typename Symbol >

void wali::relations::project_symbol_4	(	typename RelationTypedefs< State >::TernaryRelation &	out_result,
		std::set< Quad< State, State, Symbol, State > > const &	delta,
		Symbol	alpha
	)

Projects out the symbol in the return relation.

{(source, pred, target) | (source, pred, alpha, target) delta}

Parameters: out_result: The ternary relation delta restricted to alpha delta: Return relation alpha: Alphabet symbol to select and project

References wali::relations::TernaryRelation< Subject >::insert().

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

template<typename State >

State wali::relations::biggest	(	State	s1,
		State	s2,
		State	s3
	)

Referenced by transitive_closure(), and transitive_closure_no_remap().

template<typename State >

void wali::relations::transitive_closure_no_remap	(	typename RelationTypedefs< State >::BinaryRelation &	out_result,
		typename RelationTypedefs< State >::BinaryRelation const &	r
	)

References biggest().

template<typename State >

void wali::relations::transitive_closure	(	typename RelationTypedefs< State >::BinaryRelation &	out_result,
		typename RelationTypedefs< State >::BinaryRelation const &	r
	)

Constructs the transitive closure of an algorithm.

TODO: Right now we break the abstraction and assume State is a (reasonably small) integer.

{ (p, q) | p R* q} or however you want to denote it

Parameters: out_result: The transitive closure of r r: The source relation

References wali::relations::BinaryRelation::insert().

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

template<typename Relation >

void wali::relations::intersect	(	Relation &	out_result,
		Relation const &	r1,
		Relation const &	r2
	)

Returns the intersection of two binary relations on states.

Parameters: out_result: The intersection of r1 and r2 r1: One binary relation on states r2: Another binary relation on states

Referenced by intersect().

template<typename Relation >

void wali::relations::union_	(	Relation &	out_result,
		Relation const &	r1,
		Relation const &	r2
	)

Returns the union of two binary relations on states.

Parameters: out_result: The union of r1 and r2 r1: One binary relation on states r2: Another binary relation on states

Referenced by opennwa::Nwa::_private_determinize_(), and union_().

Quad<int, int, int, int> wali::relations::getFddNumbers

(

unsigned int

largest

)

Referenced by wali::relations::Domain::Domain().

void wali::relations::buddyInit

(

)

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

void wali::relations::compose	(	BinaryRelation &	out_result,
		BinaryRelation const &	r1,
		BinaryRelation const &	r2
	)

Composes two binary relations.

{ (x,z) | (x,y) r1, (y,z) r2}

Parameters: out_result: The relational composition of r1 and r2 r1: relation 1 r2: relation 2

References wali::relations::BinaryRelation::bdd, wali::relations::BinaryRelation::check(), compose(), and wali::relations::BinaryRelation::set.

void wali::relations::merge	(	BinaryRelation &	out_result,
		BinaryRelation const &	r_exit,
		BinaryRelation const &	r_call,
		TernaryRelation const &	delta_r
	)

Performs the sort of merge required for NWA return edges.

{(q, q') | (q,q1) r_call, (q1,q2) r_exit, (q2,q1,q') delta}

Parameters: out_result: The relational composition of R1 and R2 r_exit: The relation at the exit node r_call: The relation at the call node delta_r: The return transition relation with the alphabet symbol projected out

References wali::relations::TernaryRelation< Subject >::bdd, wali::relations::BinaryRelation::bdd, wali::relations::TernaryRelation< Subject >::check(), wali::relations::BinaryRelation::check(), merge(), wali::relations::TernaryRelation< Subject >::set, and wali::relations::BinaryRelation::set.

template<typename State , typename Symbol >

void wali::relations::project_symbol_4	(	TernaryRelation &	out_result,
		std::set< Quad< State, State, Symbol, State > > const &	delta,
		Symbol	alpha
	)

Projects out the symbol in the return relation.

{(source, pred, target) | (source, pred, alpha, target) delta}

Parameters: out_result: The ternary relation delta restricted to alpha delta: Return relation alpha: Alphabet symbol to select and project

References wali::relations::TernaryRelation< Subject >::bdd, wali::relations::TernaryRelation< Subject >::check(), and wali::relations::TernaryRelation< Subject >::set.

template<typename Relation >

void wali::relations::transitive_closure	(	Relation &	out_result,
		Relation const &	r
	)

Constructs the transitive closure of an algorithm.

TODO: Right now we break the abstraction and assume State is a (reasonably small) integer.

{ (p, q) | p R* q} or however you want to denote it

Parameters: out_result: The transitive closure of r r: The source relation

References biggest().

void wali::relations::intersect	(	BinaryRelation &	out_result,
		BinaryRelation const &	r1,
		BinaryRelation const &	r2
	)

Returns the intersection of two binary relations on states.

Parameters: out_result: The intersection of r1 and r2 r1: One binary relation on states r2: Another binary relation on states

References wali::relations::BinaryRelation::bdd, wali::relations::BinaryRelation::check(), intersect(), and wali::relations::BinaryRelation::set.

void wali::relations::union_	(	BinaryRelation &	out_result,
		BinaryRelation const &	r1,
		BinaryRelation const &	r2
	)

Returns the union of two binary relations on states.

Parameters: out_result: The union of r1 and r2 r1: One binary relation on states r2: Another binary relation on states

References wali::relations::BinaryRelation::bdd, wali::relations::BinaryRelation::check(), wali::relations::BinaryRelation::set, and union_().

void wali::relations::counter	(	char *	vals,
		int	size
	)

References count.

int wali::relations::bdd_rel_size	(	::bdd	b,
		int	factor
	)

template<typename OutRelation , typename State , typename Symbol >

void wali::relations::project_symbol_3_set	(	OutRelation &	out_result,
		std::set< Triple< State, Symbol, State > > const &	delta,
		Symbol	alpha
	)

Projects out the symbol in the internal and call relation.

{(source, target) | (source, alpha, target) delta}

Parameters: out_result: The relation delta restricted to alpha delta: Internals or calls relation alpha: Alphabet symbol to select and project

---

Variable Documentation

int wali::relations::count

Referenced by opennwa::details::Label::containsSymbol(), and counter().