#include <BddComponent.hh>

Public Types
typedef Diades::Utils::Exception< BddComponent >	Exception

typedef Variable::VariableVector	VariableVector

typedef Formula::FormulaVector	FormulaVector

typedef Formula	SlStates

typedef Formula	SlTransitions

typedef Formula	SlEvents

Public Member Functions
	BddComponent ()

	~BddComponent ()

void	encodeComponent (FormulaFactory &factory, const SynchronisationRules &model, const Component &component, Variable &stateVar, Variable &nextStateVar, Variable &event)

void	encodeComponent (FormulaFactory &factory, const Component &component, Variable &stateVar, Variable &nextStateVar, Variable &event)

const SlStates &	initialStates () const

const SlTransitions &	transitions () const

const SlTransitions &	transitions (const SlEvents &evt) const

const SlTransitions &	noTransitions () const

const SlTransitions &	transitions (const SlStates &sources, const SlEvents &events) const

const SlEvents &	events (std::set< Event > &events)

const SlEvents &	event (const Event &event)

const SlStates &	trigger (const SlStates &sources, const SlEvents &events) const

const SlStates &	synchronousTrigger (const SlStates &sources, const SlEvents &events) const

const SlStates &	reach (const SlStates &sources, const SlEvents &nonObservables, const SlEvents &observations)

Static Public Member Functions
static string	typeName ()

Private Member Functions
FormulaFactory &	factory ()

void	clear ()

void	encodeEventLabels (const SynchronisationRules &model, const Component &component)

void	encodeEventLabels (const Component &component)

void	encodeInitialStates (const Component &component)

void	encodeTransitions (const Component &component)

const Formula &	encodeTransition (const Component &component, const Transition &transition)

Private Attributes
FormulaVector	_behaviour

FormulaVector	_initialState

FormulaVector	_noTransitions

unordered_map< string, size_t >	_eventLabels

FormulaVector	_events

FormulaVector	_setOfEvents

VariableVector	_stateVariable

VariableVector	_nextStateVariable

VariableVector	_eventVariable

vector< reference_wrapper< FormulaFactory > >	_factory

Detailed Description

This class implements a automaton component with help of Bdds (Formula)

Definition at line 35 of file BddComponent.hh.

Member Typedef Documentation

◆ Exception

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

Definition at line 39 of file BddComponent.hh.

◆ FormulaVector

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

Definition at line 41 of file BddComponent.hh.

◆ SlEvents

typedef Formula Diades::Sdmdl::BddComponent::SlEvents

Definition at line 44 of file BddComponent.hh.

◆ SlStates

typedef Formula Diades::Sdmdl::BddComponent::SlStates

Definition at line 42 of file BddComponent.hh.

◆ SlTransitions

typedef Formula Diades::Sdmdl::BddComponent::SlTransitions

Definition at line 43 of file BddComponent.hh.

◆ VariableVector

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

Definition at line 40 of file BddComponent.hh.

Constructor & Destructor Documentation

◆ BddComponent()

Diades::Sdmdl::BddComponent::BddComponent ( )

inline

Constructor

Definition at line 65 of file BddComponent.hh.

◆ ~BddComponent()

Diades::Sdmdl::BddComponent::~BddComponent ( )

inline

Destructor

Definition at line 75 of file BddComponent.hh.

References encodeComponent(), event(), and factory().

Member Function Documentation

◆ clear()

void Diades::Sdmdl::BddComponent::clear ( )

private

Clear the component

Referenced by factory().

◆ encodeComponent() [1/2]

void Diades::Sdmdl::BddComponent::encodeComponent	(	FormulaFactory &	factory,
		const SynchronisationRules &	model,
		const Component &	component,
		Variable &	stateVar,
		Variable &	nextStateVar,
		Variable &	event
	)

Encode a component (part of a system through a SynchronisationRules's model)

Parameters

factory	the formula factory
model	the component-based model
component	the component to encode
stateVar	the state variable associated to the component to encode
nextStateVar	the next-state variable associated to the component to encode
event	the event variable

Referenced by ~BddComponent().

◆ encodeComponent() [2/2]

void Diades::Sdmdl::BddComponent::encodeComponent	(	FormulaFactory &	factory,
		const Component &	component,
		Variable &	stateVar,
		Variable &	nextStateVar,
		Variable &	event
	)

Encode a component (standalone)

Parameters

factory	the formula factory
component	the component to encode
stateVar	the state variable associated to the component to encode
nextStateVar	the next-state variable associated to the component to encode
event	the event variable