Diades::Sdmdl::Experimental::BddStateMachine Class Reference

#include <BddStateMachine.hh>

Public Types
using	Exception = Diades::Utils::Exception< BddStateMachine >
using	VariableVector = Variable::VariableVector
using	FormulaVector = Formula::FormulaVector
using	SlStates = Formula
using	SlTransitions = Formula
using	SlEvents = Formula
using	Event = size_t

Public Member Functions
	BddStateMachine ()
FormulaFactory &	setFormulaFactory (FormulaFactory &factory)
FormulaFactory &	resetInternalFormulaFactory ()
const Variable &	eventVariable () const
Variable &	eventVariable ()
Variable &	setEventVariable (Variable &event)
Variable &	stateVariable ()
const Variable &	stateVariable () const
Variable &	setStateVariable (Variable &stateVar)
Variable &	nextStateVariable ()
const Variable &	nextStateVariable () const
Variable &	setNextStateVariable (Variable &nextStateVar)
	~BddStateMachine ()
const SlStates &	initialStates () const
const SlStates &	addInitialStates (const SlStates &newInitialStates)
const SlStates &	setInitialStates (const SlStates &newInitialStates)
const SlEvents &	addEvent (Event evt)
const SlEvents &	event (const Value &eventValue) const
const SlEvents &	event (Event evt) const
const SlEvents &	sources (const Value &sourceStateValue) const
template<typename ValueIterator >
const SlEvents &	sources (ValueIterator first, ValueIterator last) const
const SlEvents &	targets (const Value &targetStateValue) const
template<typename ValueIterator >
const SlEvents &	targets (ValueIterator first, ValueIterator last) const
const SlTransitions &	addTransitions (const SlTransitions &transition)
const SlTransitions &	transitions () const
const SlTransitions &	transitions (const SlEvents &event) const
const SlTransitions &	noTransitions () const
const SlTransitions &	transitions (const SlStates &sources, const SlEvents &events) const
const SlEvents &	events () const
template<typename EventIterator >
const SlEvents &	events (EventIterator first, EventIterator last)
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)
FormulaFactory &	factory ()
void	clear ()

Static Public Member Functions
static string	typeName ()

Private Attributes
FormulaVector	_behaviour
FormulaVector	_initialState
FormulaVector	_noTransitions
std::unordered_map< std::string, FormulaVector >	_eventOfValue
std::unordered_map< Event, FormulaVector >	_formulaOfEvent
FormulaVector	_events
FormulaVector	_setOfEvents
VariableVector	_stateVariable
VariableVector	_nextStateVariable
VariableVector	_eventVariable
FormulaFactory	_internalFactory
std::vector< std::reference_wrapper< FormulaFactory > >	_factory

Detailed Description

A BddStateMachine represents a finite state automata with help of Binary Decision Diagram

Definition at line 32 of file BddStateMachine.hh.

Member Typedef Documentation

Event

_events a SlEvents Formula per Diades::Sdmdl::Experimental::BddStateMachine::Event

Parameters

Event

classical Event type (i.e. size_t)

Definition at line 82 of file BddStateMachine.hh.

Exception

using Diades::Sdmdl::Experimental::BddStateMachine::Exception = Diades::Utils::Exception<BddStateMachine>

Definition at line 49 of file BddStateMachine.hh.

FormulaVector

using Diades::Sdmdl::Experimental::BddStateMachine::FormulaVector = Formula::FormulaVector

Definition at line 59 of file BddStateMachine.hh.

SlEvents

using Diades::Sdmdl::Experimental::BddStateMachine::SlEvents = Formula

Definition at line 77 of file BddStateMachine.hh.

SlStates

using Diades::Sdmdl::Experimental::BddStateMachine::SlStates = Formula

Definition at line 65 of file BddStateMachine.hh.

SlTransitions

using Diades::Sdmdl::Experimental::BddStateMachine::SlTransitions = Formula

Definition at line 71 of file BddStateMachine.hh.

VariableVector

VariableVector vector of Variables as defined in Diades::Sdmdl::Experimental::BddStateMachine::VariableVector

Definition at line 54 of file BddStateMachine.hh.

Constructor & Destructor Documentation

BddStateMachine()

Diades::Sdmdl::Experimental::BddStateMachine::BddStateMachine ( )

inline

Default Constructor, create an empty machine based on the internal factory. To make an effective BddStateMachine then use setEvent/State/NextState/Variable methods and then reset the internal factory. Another way to do is to setup an external factory encoding the Event/State/NextState/Variable and then call setFormulaFactory(FormulaFactory & factory)

Definition at line 158 of file BddStateMachine.hh.

References Diades::Sdmdl::FormulaFactory::isFalse(), and setInitialStates().

~BddStateMachine()

Diades::Sdmdl::Experimental::BddStateMachine::~BddStateMachine ( )

inline

Destructor

Definition at line 338 of file BddStateMachine.hh.

References Diades::Sdmdl::FormulaFactory::destroy().

Member Function Documentation

addEvent()

const SlEvents& Diades::Sdmdl::Experimental::BddStateMachine::addEvent ( Event  evt )

inline

Add an event

Parameters

evt

an Event

Returns

the Formula that encodes the Event

Definition at line 381 of file BddStateMachine.hh.

References eventVariable(), factory(), and Diades::Sdmdl::Variable::getValue().

Referenced by Diades::Sdmdl::Experimental::encodeEvent().

addInitialStates()

const SlStates& Diades::Sdmdl::Experimental::BddStateMachine::addInitialStates

(

const SlStates &

newInitialStates

)

Add initial states to the current ones

Parameters

newInitialStates

a new set of initial states

Returns

the new set of initial states

Referenced by Diades::Sdmdl::Experimental::encodeInitialStates(), and initialStates().

addTransitions()

const SlTransitions& Diades::Sdmdl::Experimental::BddStateMachine::addTransitions ( const SlTransitions &  transition )

inline

Add transitions to the machine

Parameters

transitions

new transitions

Returns

the set of transitions of the machine

Definition at line 501 of file BddStateMachine.hh.

Referenced by Diades::Sdmdl::Experimental::encodeTransitions().

clear()

void Diades::Sdmdl::Experimental::BddStateMachine::clear

(

)

Clear the StateMachine

Referenced by Diades::Sdmdl::Experimental::encode(), and factory().

event() [1/2]

const SlEvents& Diades::Sdmdl::Experimental::BddStateMachine::event ( const Value &  eventValue ) const

inline

Parameters

eventValue

a Value of the Variable encoding Events

Returns

the SlEvents encoding the Event of this Value

Definition at line 401 of file BddStateMachine.hh.

References Diades::Sdmdl::Value::label().

Referenced by Diades::Sdmdl::Experimental::encodeTransitions(), events(), runGlobalDiagnosisProblem(), and transitions().

event() [2/2]

const SlEvents& Diades::Sdmdl::Experimental::BddStateMachine::event ( Event  evt ) const

inline

Parameters

eventValue

an Event encoded in the Variable encoding Events

Returns

the SlEvents encoding the Event

Definition at line 412 of file BddStateMachine.hh.

events() [1/2]

const SlEvents& Diades::Sdmdl::Experimental::BddStateMachine::events ( ) const

inline

Returns

the formula corresponding to the set of events

Definition at line 559 of file BddStateMachine.hh.

Referenced by events(), and transitions().

events() [2/2]

template<typename EventIterator >

const SlEvents& Diades::Sdmdl::Experimental::BddStateMachine::events ( EventIterator  first, EventIterator  last  )

inline

Returns

the formula corresponding to the set of events

Definition at line 568 of file BddStateMachine.hh.

References current, event(), events(), factory(), reach(), sources(), synchronousTrigger(), and trigger().

eventVariable() [1/2]

const Variable& Diades::Sdmdl::Experimental::BddStateMachine::eventVariable ( ) const

inline

Returns

the Variable encoding the events (const)

Definition at line 242 of file BddStateMachine.hh.

Referenced by addEvent(), Diades::Sdmdl::Experimental::encodeTransitions(), and resetInternalFormulaFactory().

eventVariable() [2/2]

Variable& Diades::Sdmdl::Experimental::BddStateMachine::eventVariable ( )

inline

Returns

the Variable encoding the events

Definition at line 251 of file BddStateMachine.hh.

factory()

FormulaFactory& Diades::Sdmdl::Experimental::BddStateMachine::factory ( )

inline

Definition at line 623 of file BddStateMachine.hh.

References clear(), and require.

Referenced by addEvent(), Diades::Sdmdl::Experimental::encodeInitialStates(), Diades::Sdmdl::Experimental::encodeTransitions(), events(), and runGlobalDiagnosisProblem().

initialStates()

const SlStates& Diades::Sdmdl::Experimental::BddStateMachine::initialStates ( ) const

inline

Returns

the set of initial states

Definition at line 350 of file BddStateMachine.hh.

References addInitialStates(), and require.

nextStateVariable() [1/2]

Variable& Diades::Sdmdl::Experimental::BddStateMachine::nextStateVariable ( )

inline

Returns

the Variable encoding the target states

Definition at line 306 of file BddStateMachine.hh.

Referenced by Diades::Sdmdl::Experimental::encodeTransitions(), resetInternalFormulaFactory(), and targets().

nextStateVariable() [2/2]

const Variable& Diades::Sdmdl::Experimental::BddStateMachine::nextStateVariable ( ) const

inline

Returns

the Variable encoding the target states (const)

Definition at line 315 of file BddStateMachine.hh.

noTransitions()

const SlTransitions& Diades::Sdmdl::Experimental::BddStateMachine::noTransitions

(

)

const

Returns

the no-effective transition move formula. From any state, it stays in that state

Note that this method is lazy. As long as noTransitions() is not called, the noTransition formula is not computed.

Referenced by transitions().

reach()

const SlStates& Diades::Sdmdl::Experimental::BddStateMachine::reach	(	const SlStates &	sources,
		const SlEvents &	nonObservables,
		const SlEvents &	observations
	)

Parameters

sources
nonObservables
observations

Returns

the set of target states that can be reached after observing one of the observations after sequence of nonObservable events from the set sources.

Referenced by events(), and runGlobalDiagnosisProblem().

resetInternalFormulaFactory()

FormulaFactory& Diades::Sdmdl::Experimental::BddStateMachine::resetInternalFormulaFactory ( )

inline

Set the internal factory to be the one to use. This factory is cleared first. Any reference to an external factory is lost but this factory remains unchanged. The factory will be initialised depending on the availabity of the state/nextState/event Variables

Returns

the internal factory

Definition at line 206 of file BddStateMachine.hh.

References eventVariable(), Diades::Sdmdl::FormulaFactory::isFalse(), nextStateVariable(), Diades::Sdmdl::FormulaFactory::reset(), setInitialStates(), and stateVariable().

Referenced by Diades::Sdmdl::Experimental::encode().

setEventVariable()

Variable& Diades::Sdmdl::Experimental::BddStateMachine::setEventVariable ( Variable &  event )

inline

set the Variable that encodes the events

Parameters

event

the Variable

Returns

the given Variable

Postcondition

the current factory IS NOT UPDATED, if required please use resetInternalFormulaFactory() to do so

Definition at line 263 of file BddStateMachine.hh.

Referenced by Diades::Sdmdl::Experimental::encode().

setFormulaFactory()

FormulaFactory& Diades::Sdmdl::Experimental::BddStateMachine::setFormulaFactory ( FormulaFactory &  factory )

inline

Set the formula factory to an external one. If a factory was already is use, two cases hold: it is the internal one it remains unchanged but no mor reference on it. If it was an external one, the reference is lost but it remains unchanged

Parameters

factory

the external factory to use

Returns

the given factory

Precondition

IMPORTANT: factory MUST ALREADY ENCODE the state/nextState/event variable of this BddStateMachine

Definition at line 191 of file BddStateMachine.hh.

setInitialStates()

const SlStates& Diades::Sdmdl::Experimental::BddStateMachine::setInitialStates ( const SlStates &  newInitialStates )

inline

Set initial states

Parameters

newInitialStates

a new set of initial states

Returns

the new set of initial states

Definition at line 369 of file BddStateMachine.hh.

Referenced by BddStateMachine(), and resetInternalFormulaFactory().

setNextStateVariable()

Variable& Diades::Sdmdl::Experimental::BddStateMachine::setNextStateVariable ( Variable &  nextStateVar )

inline

set the Variable that encodes the target states

Parameters

nextStateVar

the Variable

Returns

the given Variable

Postcondition

the current factory IS NOT UPDATED, if required please use resetInternalFormulaFactory() to do so

Definition at line 327 of file BddStateMachine.hh.

Referenced by Diades::Sdmdl::Experimental::encode().

setStateVariable()

Variable& Diades::Sdmdl::Experimental::BddStateMachine::setStateVariable ( Variable &  stateVar )

inline

set the Variable that encodes the source states

Parameters

stateVar

the Variable

Returns

the given Variable

Postcondition

the current factory IS NOT UPDATED, if required please use resetInternalFormulaFactory() to do so

Definition at line 295 of file BddStateMachine.hh.

Referenced by Diades::Sdmdl::Experimental::encode().

sources() [1/2]

const SlEvents& Diades::Sdmdl::Experimental::BddStateMachine::sources ( const Value &  sourceStateValue ) const

inline

Source state encoding

Parameters

sourceStateValue

Value of the state Variable

Returns

the encoding of stateVar=sourceStateValue

Definition at line 423 of file BddStateMachine.hh.

References stateVariable().

Referenced by events(), runGlobalDiagnosisProblem(), and sources().

sources() [2/2]

template<typename ValueIterator >

const SlEvents& Diades::Sdmdl::Experimental::BddStateMachine::sources ( ValueIterator  first, ValueIterator  last  ) const

inline

Source state encoding of a range

Parameters

begin	first ValueIterator of the range
end	ValueIterator after the last Value of the range

Returns

the encoding of stateVar=sourceStateValue_begin and ... and stateVar=sourceStateValue_end-1

Definition at line 435 of file BddStateMachine.hh.

References current, and sources().

stateVariable() [1/2]

Variable& Diades::Sdmdl::Experimental::BddStateMachine::stateVariable ( )

inline

Returns

the Variable encoding the source states

Definition at line 274 of file BddStateMachine.hh.

Referenced by Diades::Sdmdl::Experimental::encodeInitialStates(), Diades::Sdmdl::Experimental::encodeTransitions(), resetInternalFormulaFactory(), and sources().

stateVariable() [2/2]

const Variable& Diades::Sdmdl::Experimental::BddStateMachine::stateVariable ( ) const

inline

Returns

the Variable encoding the source states (const)

Definition at line 283 of file BddStateMachine.hh.

synchronousTrigger()

const SlStates& Diades::Sdmdl::Experimental::BddStateMachine::synchronousTrigger	(	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 transition that leads to the target state. If the events do not belong to the state machine return the current states.

Referenced by events().

targets() [1/2]

const SlEvents& Diades::Sdmdl::Experimental::BddStateMachine::targets ( const Value &  targetStateValue ) const

inline

Target state encoding

Parameters

targetStateValue

Value of the state Variable

Returns

the encoding of nextStateVar=targetStateValue

Definition at line 462 of file BddStateMachine.hh.

References nextStateVariable().

Referenced by targets().

targets() [2/2]

template<typename ValueIterator >

const SlEvents& Diades::Sdmdl::Experimental::BddStateMachine::targets ( ValueIterator  first, ValueIterator  last  ) const

inline

Target state encoding of a range

Parameters

begin	first ValueIterator of the range
end	ValueIterator after the last Value of the range

Returns

the encoding of nextStateVar=targetStateValue_begin and ... and stateVar=tagertStateValue_end-1

Definition at line 475 of file BddStateMachine.hh.

References current, and targets().

transitions() [1/3]

const SlTransitions& Diades::Sdmdl::Experimental::BddStateMachine::transitions ( ) const

inline

Returns

the set of transitions of the machine

Definition at line 515 of file BddStateMachine.hh.

References require.

transitions() [2/3]

const SlTransitions& Diades::Sdmdl::Experimental::BddStateMachine::transitions ( const SlEvents &  event ) const

inline

Parameters

event

an SlEvents

Returns

the set of transitions that are triggered by this SlEvents

Definition at line 527 of file BddStateMachine.hh.

References event(), noTransitions(), and require.

transitions() [3/3]

const SlTransitions& Diades::Sdmdl::Experimental::BddStateMachine::transitions ( const SlStates &  sources, const SlEvents &  events  ) const

inline

Parameters

sources	SlStates (source states)
events	SlEvents

Returns

the set of transitions sources - events -> targets

Definition at line 549 of file BddStateMachine.hh.

References events(), and require.

trigger()

const SlStates& Diades::Sdmdl::Experimental::BddStateMachine::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().

typeName()

static string Diades::Sdmdl::Experimental::BddStateMachine::typeName ( )

inlinestatic

Returns

the namae of the class

See also

Exception

Definition at line 41 of file BddStateMachine.hh.

Member Data Documentation

_behaviour

FormulaVector Diades::Sdmdl::Experimental::BddStateMachine::_behaviour

private

Definition at line 88 of file BddStateMachine.hh.

_eventOfValue

std::unordered_map<std::string, FormulaVector> Diades::Sdmdl::Experimental::BddStateMachine::_eventOfValue

private

Definition at line 105 of file BddStateMachine.hh.

_events

FormulaVector Diades::Sdmdl::Experimental::BddStateMachine::_events

private

Definition at line 116 of file BddStateMachine.hh.

_eventVariable

Diades::Sdmdl::Experimental::BddStateMachine::_eventVariable[0] is the Variable that is used to encode the events

private

Definition at line 134 of file BddStateMachine.hh.

_factory

Diades::Sdmdl::Experimental::BddStateMachine::_factory[0] is a reference of the current FormulaFactory that is

mutableprivate

in used. It might be the internal factory or an external one.

Definition at line 145 of file BddStateMachine.hh.

_formulaOfEvent

std::unordered_map<Event, FormulaVector> Diades::Sdmdl::Experimental::BddStateMachine::_formulaOfEvent

private

Definition at line 110 of file BddStateMachine.hh.

_initialState

FormulaVector Diades::Sdmdl::Experimental::BddStateMachine::_initialState

private

Definition at line 92 of file BddStateMachine.hh.

_internalFactory

FormulaFactory Diades::Sdmdl::Experimental::BddStateMachine::_internalFactory

private

Definition at line 139 of file BddStateMachine.hh.

_nextStateVariable

Diades::Sdmdl::Experimental::BddStateMachine::_nextStateVariable[0] is the Variable that is used to encode the target state

private

of a transition

Definition at line 130 of file BddStateMachine.hh.

_noTransitions

FormulaVector Diades::Sdmdl::Experimental::BddStateMachine::_noTransitions

mutableprivate

Definition at line 99 of file BddStateMachine.hh.

_setOfEvents

FormulaVector Diades::Sdmdl::Experimental::BddStateMachine::_setOfEvents

private

Definition at line 120 of file BddStateMachine.hh.

_stateVariable

Diades::Sdmdl::Experimental::BddStateMachine::_stateVariable[0] is the Variable that is used to encode the source state

private

of a transition

Definition at line 125 of file BddStateMachine.hh.

---

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

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