Diades::Sdmdl Namespace Reference

Namespaces
	Experimental

Classes
class	Assignment
class	BddComponent
class	BddModel
class	ComponentType
class	ComponentTypeInvalid
class	CubeGenerator
class	Event
class	EventInvalid
class	Formula
struct	FormulaBinaryOperator
class	FormulaBox
class	FormulaFactory
struct	FormulaUnaryOperator
class	Port
class	PortInvalid
class	Rule
class	RuleInvalid
class	StateNode
class	Unfolding
class	UnfoldingState
class	UnfoldingStateTable
class	Value
class	ValueFactory
class	Variable
class	VariableFactory

Typedefs
typedef Formula::FormulaVector	FormulaVector
typedef Value::ValueVector	ValueVector
typedef Variable::VariableVector	VariableVector

Functions
void	encodeCubes (int m, int n, std::vector< std::vector< int > > &result, int index)
void	printFormula (const Formula &formula, ostream &os)
template<Formula::UnaryOperator UnaryOp>
FormulaVector &	applyUnaryOperator (FormulaVector &formulas)
FormulaVector &	notF (FormulaVector &formulas)
template<Formula::BinaryOperator BinaryOp>
FormulaVector &	applyBinaryOperator (FormulaVector &formulas, const Formula &f2)
FormulaVector &	andF (FormulaVector &formulas, const Formula &f)
FormulaVector &	orF (FormulaVector &formulas, const Formula &f)
template<typename T >
ostream &	operator<< (ostream &os, const StateNode< T > &stateNode)

Typedef Documentation

FormulaVector

typedef Formula::FormulaVector Diades::Sdmdl::FormulaVector

FormulaVector vector of Formula constant references (const)

Definition at line 434 of file Formula.hh.

ValueVector

typedef Value::ValueVector Diades::Sdmdl::ValueVector

ValueVector a vector of constant Value references

Definition at line 187 of file Value.hh.

VariableVector

typedef Variable::VariableVector Diades::Sdmdl::VariableVector

VariableVector a vector of Variable references (non-const)

Definition at line 403 of file Variable.hh.

Function Documentation

andF()

FormulaVector& Diades::Sdmdl::andF ( FormulaVector &  formulas, const Formula &  f  )

inline

Apply 'and f' to every formula in the vector

Parameters

formulas	the vector of formulas
f	the formula in conjunction

Definition at line 1216 of file Formula.hh.

applyBinaryOperator()

template<Formula::BinaryOperator BinaryOp>

FormulaVector& Diades::Sdmdl::applyBinaryOperator	(	FormulaVector &	formulas,
		const Formula &	f2
	)

Definition at line 1194 of file Formula.hh.

applyUnaryOperator()

template<Formula::UnaryOperator UnaryOp>

FormulaVector& Diades::Sdmdl::applyUnaryOperator

(

FormulaVector &

formulas

)

Definition at line 1167 of file Formula.hh.

encodeCubes()

void Diades::Sdmdl::encodeCubes	(	int	m,
		int	n,
		std::vector< std::vector< int > > &	result,
		int	index
	)

Cube encoding

Parameters

m	the number of codes to get
n	the number of available bdd variables
result	the resulting set of m vectors resulting from the encoding of the m codes on the n variables
index	starting index in the n variables var[0], ..., var[n-1] (the user should call it with index = 0)

Note

the encoding has the following property: whatever m and n (such that m can be encoded with n bdd variables) any code between 1 and m is associated to only ONE cuble with the usual meaning (0,1,or 2 for any bddVariable associated to the indexes 0,...,n-1 Here is a little example: m = 6 n= 3. The result is: result[0] = [0,0,0] result[1] = [1,0,0], result[2] = [0,1,0] result[3] = [1,1,0], result[4] = [1,2,1], result[5] = [0,2,1]

This function is recursive. As written above, it should be called, as a client, with index = 0;

notF()

FormulaVector& Diades::Sdmdl::notF ( FormulaVector &  formulas )

inline

Apply not to every formula in the vector

Parameters

formulas

the vector of formulas

Definition at line 1187 of file Formula.hh.

operator<<()

template<typename T >

ostream& Diades::Sdmdl::operator<< ( ostream &  os, const StateNode< T > &  stateNode  )

inline

output stream operator on a StateNode

Definition at line 98 of file UnfoldingStateTable.hh.

References Diades::Sdmdl::StateNode< T >::children().

Referenced by Diades::Sdmdl::Rule::cubeSize(), and Diades::Sdmdl::Event::type().

orF()

FormulaVector& Diades::Sdmdl::orF ( FormulaVector &  formulas, const Formula &  f  )

inline

Apply 'or f' to every formula in the vector

Parameters

formulas	the vector of formulas
f	the formula in conjunction

Definition at line 1228 of file Formula.hh.

printFormula()

void Diades::Sdmdl::printFormula	(	const Formula &	formula,
		ostream &	os
	)

Print the formula in the output stream as the disjunction of the prime implicants

Parameters

formula	the formula to print out
os	the updated output stream