Diades::Sdmdl::Experimental Namespace Reference

Classes
class	Assignment
class	BddStateMachine
class	EventEncoder
class	StateInfoEncoder

Functions
template<typename StateProperty , typename FaultProperty >
BddStateMachine &	encodeTransitions (const Diades::Automata::Experimental::StateMachine< StateProperty, FaultProperty > &component, BddStateMachine &result)
template<typename StateProperty , typename FaultProperty >
BddStateMachine &	encodeEvent (const Diades::Automata::Experimental::StateMachine< StateProperty, FaultProperty > &component, BddStateMachine &result)
template<typename StateProperty , typename FaultProperty >
BddStateMachine &	encodeInitialStates (const Diades::Automata::Experimental::StateMachine< StateProperty, FaultProperty > &component, BddStateMachine &result)
template<typename StateProperty , typename FaultProperty >
BddStateMachine &	encode (const Diades::Automata::Experimental::StateMachine< StateProperty, FaultProperty > &component, Variable &stateVar, Variable &nextStateVar, Variable &event, BddStateMachine &result)
void	exportToDisjunctiveNormalForm (const Formula &formula, std::list< std::list< Assignment > > &dnf)

Function Documentation

encode()

template<typename StateProperty , typename FaultProperty >

BddStateMachine& Diades::Sdmdl::Experimental::encode	(	const Diades::Automata::Experimental::StateMachine< StateProperty, FaultProperty > &	component,
		Variable &	stateVar,
		Variable &	nextStateVar,
		Variable &	event,
		BddStateMachine &	result
	)

Definition at line 90 of file BddStateMachineEncoding.hh.

References Diades::Sdmdl::Experimental::BddStateMachine::clear(), encodeEvent(), encodeInitialStates(), encodeTransitions(), Diades::Sdmdl::Experimental::BddStateMachine::resetInternalFormulaFactory(), Diades::Sdmdl::Experimental::BddStateMachine::setEventVariable(), Diades::Sdmdl::Experimental::BddStateMachine::setNextStateVariable(), and Diades::Sdmdl::Experimental::BddStateMachine::setStateVariable().

Referenced by runGlobalDiagnosisProblem(), and Diades::Sdmdl::FormulaFactory::valid().

encodeEvent()

template<typename StateProperty , typename FaultProperty >

BddStateMachine& Diades::Sdmdl::Experimental::encodeEvent	(	const Diades::Automata::Experimental::StateMachine< StateProperty, FaultProperty > &	component,
		BddStateMachine &	result
	)

Definition at line 60 of file BddStateMachineEncoding.hh.

References Diades::Sdmdl::Experimental::BddStateMachine::addEvent(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::events().

Referenced by encode().

encodeInitialStates()

template<typename StateProperty , typename FaultProperty >

BddStateMachine& Diades::Sdmdl::Experimental::encodeInitialStates	(	const Diades::Automata::Experimental::StateMachine< StateProperty, FaultProperty > &	component,
		BddStateMachine &	result
	)

Definition at line 72 of file BddStateMachineEncoding.hh.

References Diades::Sdmdl::Experimental::BddStateMachine::addInitialStates(), Diades::Sdmdl::Experimental::BddStateMachine::factory(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::getStatePropertyId(), Diades::Sdmdl::Variable::getValue(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::initialStateBegin(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::initialStateEnd(), Diades::Sdmdl::FormulaFactory::newFormula(), and Diades::Sdmdl::Experimental::BddStateMachine::stateVariable().

Referenced by encode().

encodeTransitions()

template<typename StateProperty , typename FaultProperty >

BddStateMachine& Diades::Sdmdl::Experimental::encodeTransitions	(	const Diades::Automata::Experimental::StateMachine< StateProperty, FaultProperty > &	component,
		BddStateMachine &	result
	)

Parameters

component

the component to encode

Definition at line 32 of file BddStateMachineEncoding.hh.

References Diades::Sdmdl::Experimental::BddStateMachine::addTransitions(), Diades::Sdmdl::Experimental::BddStateMachine::event(), Diades::Sdmdl::Experimental::BddStateMachine::eventVariable(), Diades::Sdmdl::Experimental::BddStateMachine::factory(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::getEvent(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::getStatePropertyId(), Diades::Sdmdl::Variable::getValue(), Diades::Sdmdl::FormulaFactory::newFormula(), Diades::Sdmdl::Experimental::BddStateMachine::nextStateVariable(), Diades::Sdmdl::Experimental::BddStateMachine::stateVariable(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::transitionBegin(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::transitionEnd().

Referenced by encode().

exportToDisjunctiveNormalForm()

void Diades::Sdmdl::Experimental::exportToDisjunctiveNormalForm	(	const Formula &	formula,
		std::list< std::list< Assignment > > &	dnf
	)

This function transforms a Formula as a Disjunctive Normal Formula (DNF) A DNF is a disjunction of conjunctions. Each conjunction is modeled as a list of variable Assignements. So the dnf is a list of Assignment lists. In case of Formula.isFalse() the dnf list is set to be empty. In case of Formula.isTrue() the dnf list then contains one single list that is empty.

Parameters

formula	a Formula
the	result disjunctive normal form

Referenced by printSolution().