Diades::Sdmdl::BddModel Class Reference

#include <BddModel.hh>

Public Types
typedef Diades::Utils::Exception< BddModel >	Exception
typedef Diades::Automata::SynchronisationRules::ComponentVector	ComponentVector
typedef vector< BddComponent >	BddComponentVector
typedef Variable::VariableVector	VariableVector
typedef Formula::FormulaVector	FormulaVector

Public Member Functions
	BddModel (const SynchronisationRules &model, const set< Event > &observable, const set< Event > &faults)
	~BddModel ()
FormulaFactory &	formulaFactory ()
const BddComponent &	getComponent (BddComponentVector::size_type index) const
BddComponent &	getComponent (BddComponentVector::size_type index)
const SlStates &	initialStates () const
const SlEvents &	events () const
const SlTransitions &	transitions () const
const SlStates &	trigger (const SlStates &sources, const SlEvents &events) const
const SlStates &	synchronousTrigger (const SlStates &sources, const SlEvents &events)
const VariableVector &	stateVariables () const
const VariableVector &	nextStateVariables () const

Static Public Member Functions
static string	typeName ()

Private Types
typedef BddComponent::SlStates	SlStates
typedef BddComponent::SlTransitions	SlTransitions
typedef BddComponent::SlEvents	SlEvents

Private Member Functions
void	encodeStateVariables ()
void	encodeEvents ()
void	setFaults (const set< Event > &faults)
void	setObservables (const set< Event > &observable)
const SlStates &	trigger (const SlStates &sources, size_t eventIndex) const

Private Attributes
const SynchronisationRules &	_model
BddComponentVector	_bddComponents
VariableFactory *	_varFactory
FormulaFactory *	_formulas
VariableVector	_stateVariables
VariableVector	_nextStateVariables
Variable &	_event
VariableVector	_varSet
FormulaVector	_observables
FormulaVector	_isObs
FormulaVector	_faults
FormulaVector	_isFault
FormulaVector	_setOfEvents
FormulaVector	_events
vector< vector< size_t > >	_supports
vector< vector< bool > >	_booleanSupports
FormulaVector	_transitions

Detailed Description

This class implements a discrete event system as a set of BddComponent

Definition at line 32 of file BddModel.hh.

Member Typedef Documentation

BddComponentVector

typedef vector<BddComponent> Diades::Sdmdl::BddModel::BddComponentVector

Definition at line 40 of file BddModel.hh.

ComponentVector

typedef Diades::Automata::SynchronisationRules::ComponentVector Diades::Sdmdl::BddModel::ComponentVector

Definition at line 39 of file BddModel.hh.

Exception

typedef Diades::Utils::Exception<BddModel> Diades::Sdmdl::BddModel::Exception

Definition at line 38 of file BddModel.hh.

FormulaVector

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

Definition at line 42 of file BddModel.hh.

SlEvents

typedef BddComponent::SlEvents Diades::Sdmdl::BddModel::SlEvents

private

Definition at line 63 of file BddModel.hh.

SlStates

typedef BddComponent::SlStates Diades::Sdmdl::BddModel::SlStates

private

Definition at line 61 of file BddModel.hh.

SlTransitions

typedef BddComponent::SlTransitions Diades::Sdmdl::BddModel::SlTransitions

private

Definition at line 62 of file BddModel.hh.

VariableVector

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

Definition at line 41 of file BddModel.hh.

Constructor & Destructor Documentation

BddModel()

Diades::Sdmdl::BddModel::BddModel	(	const SynchronisationRules &	model,
		const set< Event > &	observable,
		const set< Event > &	faults
	)

Constructor

Parameters

model	the set of components to encode
observable	the set of observable events
faults	the set of fault events
shared	the set of shared events that a

~BddModel()

Diades::Sdmdl::BddModel::~BddModel

(

)

Destructor

Member Function Documentation

encodeEvents()

void Diades::Sdmdl::BddModel::encodeEvents ( )

private

Encode the events

Referenced by nextStateVariables().

encodeStateVariables()

void Diades::Sdmdl::BddModel::encodeStateVariables ( )

private

Encode the state variables

Referenced by nextStateVariables().

events()

const SlEvents& Diades::Sdmdl::BddModel::events ( ) const

inline

Returns

the set of initial states

Definition at line 145 of file BddModel.hh.

References synchronousTrigger(), transitions(), and trigger().

formulaFactory()

FormulaFactory& Diades::Sdmdl::BddModel::formulaFactory ( )

inline

Returns

the formula factory associated to this (and only this) BddModel

Definition at line 92 of file BddModel.hh.

References _formulas.

getComponent() [1/2]

const BddComponent& Diades::Sdmdl::BddModel::getComponent ( BddComponentVector::size_type  index ) const

inline

Parameters

index

Returns

the BddComponent of the given index.

Definition at line 104 of file BddModel.hh.

References require.

getComponent() [2/2]

BddComponent& Diades::Sdmdl::BddModel::getComponent ( BddComponentVector::size_type  index )

inline

Parameters

index

Returns

the BddComponent of the given index.

Definition at line 119 of file BddModel.hh.

References initialStates(), and require.

initialStates()

const SlStates& Diades::Sdmdl::BddModel::initialStates

(

)

const

Returns

the set of initial states

Referenced by getComponent().

nextStateVariables()

const VariableVector& Diades::Sdmdl::BddModel::nextStateVariables ( ) const

inline

Returns

the state variables (nextState version encoding the states of each BddComponent. nextStateVariables().operator[i] is the variable that encodes the state of getComponent(i) (next state version)

Definition at line 207 of file BddModel.hh.

References _nextStateVariables, encodeEvents(), encodeStateVariables(), setFaults(), setObservables(), and trigger().

setFaults()

void Diades::Sdmdl::BddModel::setFaults ( const set< Event > &  faults )

private

Encode the faults of the system

Parameters

faults

set of fault events

Referenced by nextStateVariables().

setObservables()

void Diades::Sdmdl::BddModel::setObservables ( const set< Event > &  observable )

private

Encode the observability of the system

Parameters

observable

set of observable events

Referenced by nextStateVariables().

stateVariables()

const VariableVector& Diades::Sdmdl::BddModel::stateVariables ( ) const

inline

Returns

the state variables encoding the states of each BddComponent. stateVariables().operator[i] is the variable that encodes the state of getComponent(i)

Definition at line 194 of file BddModel.hh.

References _stateVariables.

synchronousTrigger()

const SlStates& Diades::Sdmdl::BddModel::synchronousTrigger	(	const SlStates &	sources,
		const SlEvents &	events
	)

Trigger one event belonging to the set of events from the set of sources

Parameters

sources
events

Returns

the set of target states such that there exists at least one source state and one event in a component transition that leads to the target state. If the events do not belong to the components return the current states.

Referenced by events().

transitions()

const SlTransitions& Diades::Sdmdl::BddModel::transitions

(

)

const

Returns

the set of transitions

Referenced by events().

trigger() [1/2]

const SlStates& Diades::Sdmdl::BddModel::trigger	(	const SlStates &	sources,
		const SlEvents &	events
	)		const

Trigger one event belonging to the set of events from the set of sources

Parameters

sources
events

Returns

the set of target states such that there exists at least one source state and one event in a component transition that leads to the target state

Referenced by events(), and nextStateVariables().

trigger() [2/2]

const SlStates& Diades::Sdmdl::BddModel::trigger ( const SlStates &  sources, size_t  eventIndex  ) const

private

Trigger one event belonging to the set of events from the set of sources

Parameters

sources	the set of sources states
eventIndex	the index of the encoding of THE event to trigger

Returns

the set of global target states such that there exists at least one global transition from one of the source states that leads to the global target state, false otherwise

typeName()

static string Diades::Sdmdl::BddModel::typeName ( )

inlinestatic

Definition at line 37 of file BddModel.hh.

Member Data Documentation

_bddComponents

BddComponentVector Diades::Sdmdl::BddModel::_bddComponents

private

Definition at line 45 of file BddModel.hh.

_booleanSupports

vector< vector<bool> > Diades::Sdmdl::BddModel::_booleanSupports

private

Definition at line 59 of file BddModel.hh.

_event

Variable& Diades::Sdmdl::BddModel::_event

private

Definition at line 50 of file BddModel.hh.

_events

FormulaVector Diades::Sdmdl::BddModel::_events

private

Definition at line 57 of file BddModel.hh.

_faults

FormulaVector Diades::Sdmdl::BddModel::_faults

private

Definition at line 54 of file BddModel.hh.

_formulas

FormulaFactory* Diades::Sdmdl::BddModel::_formulas

private

Definition at line 47 of file BddModel.hh.

Referenced by formulaFactory().

_isFault

FormulaVector Diades::Sdmdl::BddModel::_isFault

private

Definition at line 55 of file BddModel.hh.

_isObs

FormulaVector Diades::Sdmdl::BddModel::_isObs

private

Definition at line 53 of file BddModel.hh.

_model

const SynchronisationRules& Diades::Sdmdl::BddModel::_model

private

Definition at line 44 of file BddModel.hh.

_nextStateVariables

VariableVector Diades::Sdmdl::BddModel::_nextStateVariables

private

Definition at line 49 of file BddModel.hh.

Referenced by nextStateVariables().

_observables

FormulaVector Diades::Sdmdl::BddModel::_observables

private

Definition at line 52 of file BddModel.hh.

_setOfEvents

FormulaVector Diades::Sdmdl::BddModel::_setOfEvents

private

Definition at line 56 of file BddModel.hh.

_stateVariables

VariableVector Diades::Sdmdl::BddModel::_stateVariables

private

Definition at line 48 of file BddModel.hh.

Referenced by stateVariables().

_supports

vector< vector<size_t> > Diades::Sdmdl::BddModel::_supports

private

Definition at line 58 of file BddModel.hh.

_transitions

FormulaVector Diades::Sdmdl::BddModel::_transitions

mutableprivate

Definition at line 60 of file BddModel.hh.

_varFactory

VariableFactory* Diades::Sdmdl::BddModel::_varFactory

private

Definition at line 46 of file BddModel.hh.

_varSet

VariableVector Diades::Sdmdl::BddModel::_varSet

private

Definition at line 51 of file BddModel.hh.

---

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

• /home/yannick/laas/redmine/tools/diades/include/diades/sdmdl/BddModel.hh