Namespaces
	LocalCandidateMachine

	Projection

Classes
class	AutFileDescriptor

class	AutStateCreator

class	BeliefState

class	BeliefStateBasedStateCreator

class	BeliefStateWithSourceStateCreator

class	ComposableModel

struct	ConstManagedDdAutFA
	data structure that gathers an FA, a StateManager and a EventManager More...

struct	ConstManagedDdAutFsm
	data structure that gathers an Fsm, a StateManager and a EventManager More...

class	ControlPattern
	A control pattern is a mapping between the set of Events of a StateMachine and a Boolean. More...

class	DdAutFileDescriptor

class	DdSyncDescriptor

class	DefaultDdAutSynchronisationEventEncoder

class	DiGraphComponentStartingWith

class	EventInserter

class	EventManager

class	EventManagerPrettyPrinter

class	EventSetManager

class	EventSetManagerPrettyPrinter

class	FaultyEventStateMachine

class	FiniteAutomaton

class	LocalCandidate

class	LocalCandidatePrettyPrinter

struct	MakeAcceptingState

class	ManagedBeliefStateBasedStateCreator

class	ManagedBeliefStateBasedStateCreator< FiniteAutomaton< S, I, NS, NI >, StatePropertyCombination >

class	ManagedBeliefStateWithSourceStateCreator

class	ManagedBeliefStateWithSourceStateCreator< FiniteAutomaton< S, I, NS, NI >, StatePropertyCombination >

struct	ManagedDdAutFA
	data structure that gathers an FA, a StateManager and a EventManager More...

struct	ManagedDdAutFsm
	data structure that gathers an Fsm, a StateManager and a EventManager More...

class	ManagedEventInserter

class	ManagedStateCopy

class	ManagedStateCopy< FiniteAutomaton< S, I, NS, NI >, StateProperty >

class	ManagedStateCreation

class	ManagedStateInserter

class	ManagedSynchronisedAcceptingStateCreation

class	ManagedSynchronisedStateCreation

class	NewStateCreation

class	OnlySourceStateCreator

class	OnlySourceStateCreator< FiniteAutomaton< S, I, NS, NI > >

class	OnlyStateCreator

class	OnlyStateCreator< FiniteAutomaton< S, I, NS, NI > >

class	ParametrizedSynchronisation

class	Printer

struct	PrintEvent

struct	PrintEvent< std::string >

struct	ReadEvent

struct	ReadEvent< std::string >

class	StateCopy

class	StateCopy< FiniteAutomaton< S, I, NS, NI > >

class	StateCreation

struct	StateCreationTraits

struct	StateCreationTraits< ManagedStateCreation< T1, T2 > >

struct	StateCreationTraits< StateCreation< T1 > >

class	StateIdGenerator

class	StateInfoManagerPrettyPrinter

class	StateInserter

class	StateMachine

class	StatePropertyManager

class	StreamBasedPrinter

class	SynchronisationEvent

class	SynchronisationEventEncoder

class	SynchronisationRules

class	SynchronisationRulesEncoder

class	TransitionInserter

Typedefs
using	AutStateId = StatePropertyIdAsSizeT

using	AutEventId = std::string

using	AutFsm = StateMachine< AutStateId, AutEventId >

using	AutFsmEventInserter = EventInserter< AutFsm >

using	AutFsmStateIdGenerator = StateIdGenerator< AutFsm, Diades::Utils::IncrementGenerator< AutFsm::StatePropertyId > >

using	AutFsmStateInserter = StateInserter< AutFsmStateIdGenerator, StateCopy< AutFsm > >

using	AutFsmTransitionInserter = TransitionInserter< AutFsmStateInserter, AutFsmEventInserter >

template<typename Fsm >
using	BsPtr = typename BeliefState< Fsm >::SharedPtr

template<typename Fsm >
using	CstBsMap = CstStMap< BsPtr< Fsm > >

template<typename Fsm >
using	BsMap = StMap< BsPtr< Fsm > >

using	DdAutStateId = AutStateId

using	DdAutEventId = size_t

using	DdAutFsm = StateMachine< DdAutStateId, DdAutEventId >

using	DdAutFA = FiniteAutomaton< DdAutStateId, DdAutEventId >

using	DdAutStateLabel = StatePropertyAsStringLabel

using	DdAutEventLabel = std::string

using	DdAutStateManager = StatePropertyManager< DdAutStateLabel, DdAutStateId >

using	DdAutEventManager = EventManager< DdAutEventLabel, DdAutEventId >

using	DdAutStatePrinter = StateInfoManagerPrettyPrinter< DdAutStateLabel, DdAutStateId >

using	DdAutEventPrinter = EventManagerPrettyPrinter< DdAutEventLabel, DdAutEventId >

using	DdAutComma = Diades::Utils::StringBinaryCombination< char, ',', std::char_traits< char >, std::allocator< char > >

using	DdAutAmpersand = Diades::Utils::StringBinaryCombination< char, '&', std::char_traits< char >, std::allocator< char > >

using	DdAutBraces = Diades::Utils::StringDelimiter< char, '{', '}', std::char_traits< char >, std::allocator< char > >

using	DdAutParentheses = Diades::Utils::StringDelimiter< char, '(', ')', std::char_traits< char >, std::allocator< char > >

using	DdAutDisjunction = Diades::Utils::Disjunction< DdAutStateLabel, DdAutComma, DdAutBraces >

using	DdAutConjunction = Diades::Utils::Conjunction< DdAutStateLabel, DdAutComma, DdAutParentheses >

using	DdAutProjection = DiGraphComponentStartingWith< DdAutStateLabel, char, '\|', DdAutComma, DdAutBraces >

using	DdAutSynchronisation = Diades::Utils::Conjunction< DdAutEventLabel, DdAutAmpersand, Diades::Utils::NoDelimiter< char, std::char_traits< char >, std::allocator< char > >>

using	LocStateMap = Diades::Graph::ConstNodeMap< int >

using	ExplLocStateMap = Diades::Graph::NodeMap< int >

using	Observation = std::string

using	Observations = std::vector< Observation >

using	Observables = std::set< DdAutFA::EventPropertyId >

using	Matcher = std::unordered_map< Observation, Observables >

template<typename Fsm >
using	SafeAlt = std::unordered_map< typename Fsm::State, std::unordered_set< typename Fsm::Transition > >

using	StatePropertyIdAsSizeT = size_t

template<typename Type >
using	CstStMap = Diades::Graph::ConstNodeMap< Type >

template<typename Type >
using	StMap = Diades::Graph::NodeMap< Type >

template<typename Type >
using	CstTrMap = Diades::Graph::ConstEdgeMap< Type >

template<typename Type >
using	TrMap = Diades::Graph::EdgeMap< Type >

using	StatePropertyAsStringLabel = std::string

using	StatePropertyAsUnsigned = unsigned

using	TsFsm = DdAutFsm

using	TsFsmPtr = std::shared_ptr< TsFsm >

using	TsStMgr = DdAutStateManager

using	TsEvtMgr = DdAutEventManager

using	TsStMgrPtr = std::shared_ptr< TsStMgr >

using	TsEvtMgrPtr = std::shared_ptr< TsEvtMgr >

using	ManagedTsFsm = std::tuple< TsFsmPtr, TsStMgrPtr, TsEvtMgrPtr >

using	ManagedTsFsms = std::vector< ManagedTsFsm >

Enumerations
enum	TsConversionMode { normal, full, update }

Functions
template<typename Fsm , typename BeliefStateIterator , typename StateCreation >
bool	abstract (const Fsm &machine, Fsm &abstractedMachine, BeliefStateIterator bfBegin, BeliefStateIterator bfEnd, std::vector< typename Fsm::State > &abstractedStates, StateCreation &creator)

template<typename Fsm , typename BeliefStateIterator , typename StateCreation >
bool	abstract (const Fsm &machine, Fsm &abstractedMachine, BeliefStateIterator bfBegin, BeliefStateIterator bfEnd, StateCreation &creator)

void	transformToCandidateStateMachine (const Component &component, Lcm::EvManager &manager, Lcm::EvSetManager &setManager, Lcm::LocalStateInfoManager &locStateInfoManager, Lcm::CandidateManager &candidateManager, Lcm::Fsm &result)

template<typename Fsm >
bool	autFsmNeedEncoding (const Fsm &fsm)

template<typename Fsm >
void	autFileStateEncoding (const Fsm &fsm, Diades::Graph::ConstNodeMap< AutStateId > &encoding)

template<typename Fsm >
void	autFileStateReencoding (Fsm &fsm)

bool	fromAutFile (std::istream &stream, AutFsm &fsm)

bool	toAutFile (ostream &stream, const AutFsm &fsm, bool enforce=false)

template<typename AutFsmRange >
bool	insertAutFsms (AutFsmRange range, AutFsm &output)

template<typename Fsm >
bool	isComplete (const Fsm &machine)

template<typename Fsm >
void	complete (Fsm &machine)

bool	fsmFromDdAutFile (std::istream &stream, const ManagedDdAutFsm &mFsm)

bool	faFromDdAutFile (std::istream &stream, const ManagedDdAutFA &mFa)

bool	fsmToDdAutFile (ostream &stream, const ConstManagedDdAutFsm &mFsm)

bool	faToDdAutFile (ostream &stream, const ConstManagedDdAutFA &mFa)

bool	fsmToAutFile (ostream &stream, const DdAutFsm &fsm, const DdAutEventManager &eManager, bool enforce=false)

template<typename DdAutFsmType >
bool	generateSynchronisedDdAutEventLabels (const SynchronisationRules< DdAutFsmType > &synchro, const std::vector< DdAutEventManager > &eventManagers, DdAutEventManager &syncEventManager)

void	insertDdAutFA (const DdAutFA &sourceFsm, const DdAutStateManager &sourceStateManager, const DdAutEventManager &sourceEventManager, DdAutFA &targetFsm, DdAutStateManager &targetStateManager, DdAutEventManager &targetEventManager)

template<typename DdAutFARange , typename RangeDdAutSM , typename RangeDdAutEM >
bool	insertFiniteAutomata (DdAutFARange faRange, RangeDdAutSM smRange, RangeDdAutEM evRange, DdAutFA &result, DdAutStateManager &targetStateManager, DdAutEventManager &targetEventManager)

bool	fsmToDescriptor (const DdAutFsm &fsm, DdAutFileDescriptor &descriptor, const DdAutStateManager &sManager, const DdAutEventManager &eManager, Diades::Graph::ConstNodeMap< DdAutStateId > &encoding)

bool	fsmFromDescriptor (const DdAutFileDescriptor &descriptor, DdAutFsm &fsm, DdAutStateManager &sManager, DdAutEventManager &eManager)

bool	faToDescriptor (const DdAutFA &fa, DdAutFileDescriptor &descriptor, const DdAutStateManager &sManager, const DdAutEventManager &eManager, Diades::Graph::ConstNodeMap< DdAutStateId > &encoding)

bool	faFromDescriptor (const DdAutFileDescriptor &descriptor, DdAutFA &fa, DdAutStateManager &sManager, DdAutEventManager &eManager)

template<typename DdAutFsmType >
bool	rulesToDescriptor (const SynchronisationRules< DdAutFsmType > &rules, DdSyncDescriptor &desc)

template<typename DdAutFsmType >
bool	descriptorToRules (const DdSyncDescriptor &desc, ParametrizedSynchronisation< DdAutFsmType > &rules, std::string &errorMsg)

template<typename Fsm >
bool	isDeterministic (const Fsm &machine)

template<typename Fsm , typename StateCreator >
void	determine (const Fsm &machine, Fsm &deterministicMachine, StateCreator &creator)

template<typename _SPId , typename _ISId , typename _NSPId = NullValue<_SPId>, typename _NISId = NullValue< _ISId>>
bool	isNotChoiceState (const FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId > &fsa, typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State state, const LocStateMap &levels)
	return true if the state is definitely considered as a no-choice state More...

template<typename _SPId , typename _ISId , typename _NSPId = NullValue<_SPId>, typename _NISId = NullValue< _ISId>>
void	setLevelStateAndPropagate (const FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId > &fsa, std::list< typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State > &states, int currentLevel, LocStateMap &levels, typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State state, std::unordered_set< typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State > &tagged, std::unordered_set< typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State > &visited)
	set the level of the current state and insert its untagged predecessors in the list 'states' update the tagged and visited data structure if the state is not an initial state More...

template<typename _SPId , typename _ISId , typename _NSPId = NullValue<_SPId>, typename _NISId = NullValue< _ISId>>
bool	setLevel (const FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId > &fsa, std::list< typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State > &states, int currentLevel, LocStateMap &levels)

template<typename _SPId , typename _ISId , typename _NSPId = NullValue<_SPId>, typename _NISId = NullValue< _ISId>>
bool	levelOfChoice (const FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId > &fsa, LocStateMap &result)

template<typename Fsm >
void	extractEffectiveChoiceTransitions (Fsm &traces, const ExplLocStateMap &levelOfChoice, unordered_set< typename Fsm::Transition > &solutions)
	Extraction from the traces of A \|\| Pbar \|\| L, the set of effective choice transitions. More...

std::unordered_set< DdAutFA::Transition >	getSafeAlternatives (const DdAutFA &traces, DdAutFA::State state, const ExplLocStateMap &levelOfChoiceInTraces, const Diades::Graph::NodeMap< DdAutFA::State > &mapping, const DdAutFA &fsa, const LocStateMap &levelOfChoiceInFsa, const DdAutStateManager &sManager, const DdAutEventManager &eManager)

template<typename StateIterator >
bool	explainFromStates (StateIterator begin, StateIterator end, const DdAutFA &fsa, const DdAutStateManager &sManager, const DdAutEventManager &eManager, const Observations &observations, Observables &observables, DdAutFA &explanations, DdAutFA &traces, DdAutStateManager &sManagerExplanation, const Matcher &matcher, const LocStateMap &levelOfChoice, SafeAlt< DdAutFA > &safeAlternatives)

Matcher	initialiseMatcher (const DdAutEventManager &eManager, const std::vector< std::string > &observations)

bool	explain (const DdAutFA &fsa, const DdAutStateManager &sManager, const DdAutEventManager &eManager, const std::vector< std::string > &observations, Observables &observables, DdAutFA &explanations, DdAutFA &fullExplanations, DdAutStateManager &sManagerExplanation, std::unordered_map< DdAutFA::State, unordered_set< DdAutFA::Transition > > &safeAlternatives)

ostream &	toDotHeader (ostream &os)

template<typename StateMachine >
ostream &	toDotHeader (const StateMachine &fsm, ostream &os)

template<typename StateMachine >
ostream &	toDotInitialStates (const StateMachine &fsm, ostream &os)

template<typename StateMachine , typename PrintStateProperty >
ostream &	toDotStates (const StateMachine &fsm, const PrintStateProperty &statePrinter, ostream &os)

template<typename S , typename I , typename NS , typename NI , typename PrintStateProperty >
ostream &	toDotStates (const FiniteAutomaton< S, I, NS, NI > &fsm, const PrintStateProperty &statePrinter, ostream &os)

template<typename StateMachine >
ostream &	toDotStates (const StateMachine &fsm, ostream &os)

template<typename S , typename I , typename NS , typename NI >
ostream &	toDotStates (const FiniteAutomaton< S, I, NS, NI > &fa, ostream &os)

ostream &	toDotEnding (ostream &os)

template<typename StateMachine , typename PrintEventInfo >
ostream &	toDotTransitions (const StateMachine &fsm, const PrintEventInfo &eventPrinter, ostream &os)

template<typename StateProperty , typename EventInfo , typename PrintEventInfo >
ostream &	toDotTransitions (const FaultyEventStateMachine< StateProperty, EventInfo > &fsm, const PrintEventInfo &eventPrinter, ostream &os)

template<typename StateMachine >
ostream &	toDotTransitions (const StateMachine &fsm, ostream &os)

template<typename StateProperty , typename EventInfo >
ostream &	toDotTransitions (const FaultyEventStateMachine< StateProperty, EventInfo > &fsm, ostream &os)

template<typename StateMachine , typename PrintStateProperty , typename PrintEventInfo >
ostream &	toDot (ostream &os, const StateMachine &fsm, const PrintStateProperty &statePrinter, const PrintEventInfo &eventPrinter)

template<typename StateMachine >
ostream &	toDot (ostream &os, const StateMachine &fsm)

template<typename StateMachine >
bool	toDot (const std::string &filename, const StateMachine &fsm)

template<>
ostream &	toDot (ostream &os, const DdSyncDescriptor &descriptor)

template<typename StateProperty , typename FaultProperty >
ostream &	operator<< (ostream &os, const LocalCandidate< StateProperty, FaultProperty > &candidate)

template<typename Fsm >
bool	splitPartition (const Fsm &machine, const std::shared_ptr< BeliefState< Fsm >> bigQ0, const std::shared_ptr< BeliefState< Fsm >> bigQ1, typename Fsm::EventPropertyId littleA, std::shared_ptr< BeliefState< Fsm >> bigQ0prime, std::shared_ptr< BeliefState< Fsm >> bigQ0MinusbigQ0prime)

template<typename Fsm >
void	nerodePartition (const Fsm &machine, vector< std::shared_ptr< BeliefState< Fsm >>> &partition)

template<typename Fsm , typename StateCreator >
void	minimizeDeterministicMachine (const Fsm &machine, Fsm &minimalMachine, StateCreator &creator)

template<typename Fsm , typename StateCreator >
void	minimize (const Fsm &machine, Fsm &minimalMachine, StateCreator &creator)

template<typename Fsm , typename IsGoal >
bool	project (const Fsm &machine, Fsm &abstractMachine, IsGoal isGoal, BsMap< Fsm > &bsMap, CstStMap< typename Fsm::State > &stMap)

template<typename Fsm , typename IsGoal >
bool	project (const Fsm &machine, Fsm &abstractMachine, IsGoal isGoal)

template<typename Fsm , typename EventPropertyIdIterator >
bool	project (const Fsm &machine, Fsm &abstractMachine, EventPropertyIdIterator begin, EventPropertyIdIterator end, BsMap< Fsm > &bsMap, CstStMap< typename Fsm::State > &stMap)

template<typename Fsm , typename EventPropertyIdIterator >
bool	project (const Fsm &machine, Fsm &abstractMachine, EventPropertyIdIterator begin, EventPropertyIdIterator end)

template<typename Fsm , typename IsGoal , typename StateProperty , typename StateLabelProjection >
bool	project (const Fsm &fsm, Fsm &projectedFsm, const StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &stateManager, StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &projectionStateManager, const StateLabelProjection &projection, IsGoal isGoal, BsMap< Fsm > &bsMap, CstStMap< typename Fsm::State > &stMap)

template<typename Fsm , typename IsGoal , typename StateProperty , typename StateLabelProjection >
bool	project (const Fsm &fsm, Fsm &projectedFsm, const StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &stateManager, StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &projectionStateManager, const StateLabelProjection &projection, IsGoal isGoal)

template<typename Fsm , typename EventPropertyIdIterator , typename StateProperty , typename StateLabelProjection >
bool	project (const Fsm &fsm, Fsm &projectedFsm, const StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &stateManager, StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &projectionStateManager, const StateLabelProjection &projection, EventPropertyIdIterator begin, EventPropertyIdIterator end, BsMap< Fsm > &bsMap, CstStMap< typename Fsm::State > &stMap)

template<typename Fsm , typename EventPropertyIdIterator , typename StateProperty , typename StateLabelProjection >
bool	project (const Fsm &fsm, Fsm &projectedFsm, const StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &stateManager, StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &projectionStateManager, const StateLabelProjection &projection, EventPropertyIdIterator begin, EventPropertyIdIterator end)

template<typename Fsm , typename EventPropertyIdIterator >
bool	abstractEvents (const Fsm &machine, Fsm &abstractMachine, EventPropertyIdIterator begin, EventPropertyIdIterator end, BsMap< Fsm > &bsMap, CstStMap< typename Fsm::State > &stMap)

template<typename Fsm , typename EventPropertyIdIterator >
bool	abstractEvents (const Fsm &machine, Fsm &abstractMachine, EventPropertyIdIterator begin, EventPropertyIdIterator end)

template<typename Fsm , typename EventPropertyIdIterator , typename StateProperty , typename StateLabelProjection >
bool	abstractEvents (const Fsm &fsm, Fsm &projectedFsm, const StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &stateManager, StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &projectionStateManager, const StateLabelProjection &projection, EventPropertyIdIterator begin, EventPropertyIdIterator end, BsMap< Fsm > &bsMap, CstStMap< typename Fsm::State > &stMap)

template<typename Fsm , typename EventPropertyIdIterator , typename StateProperty , typename StateLabelProjection >
bool	abstractEvents (const Fsm &fsm, Fsm &projectedFsm, const StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &stateManager, StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &projectionStateManager, const StateLabelProjection &projection, EventPropertyIdIterator begin, EventPropertyIdIterator end)

template<typename StatePropertyId , typename EventPropertyId , typename InputIterator , typename NullStateProperty , typename NullEventProperty >
void	deleteTransition (StateMachine< StatePropertyId, EventPropertyId, NullStateProperty, NullEventProperty > &m, InputIterator first, InputIterator last)

template<typename StatePropertyId , typename EventPropertyId , typename InputIterator , typename NullStateProperty , typename NullEventProperty >
void	deleteState (StateMachine< StatePropertyId, EventPropertyId, NullStateProperty, NullEventProperty > &m, InputIterator first, InputIterator last)

template<typename StatePropertyId , typename EventPropertyId , typename InputIterator , typename Predicate , typename NullStatePropertyId = NullValue<StatePropertyId>, typename NullEventPropertyId >
void	deleteState (StateMachine< StatePropertyId, EventPropertyId, NullStatePropertyId, NullEventPropertyId > &m, InputIterator first, InputIterator last, Predicate pred)

template<typename StatePropertyId , typename EventPropertyId , typename InputIterator , typename IsNullStatePropertyId , typename IsNullEventProperty >
void	deleteTransition (StateMachine< StatePropertyId, EventPropertyId, IsNullStatePropertyId, IsNullEventProperty > &m, InputIterator first, InputIterator last)

template<typename StatePropertyId , typename EventPropertyId , typename InputIterator , typename IsNullStateProperty , typename IsNullEventProperty >
void	deleteState (StateMachine< StatePropertyId, EventPropertyId, IsNullStateProperty, IsNullEventProperty > &m, InputIterator first, InputIterator last)

template<typename StatePropertyId , typename EventPropertyId , typename InputIterator , typename Predicate , typename IsNullStateProperty , typename IsNullEventProperty >
void	deleteState (StateMachine< StatePropertyId, EventPropertyId, IsNullStateProperty, IsNullEventProperty > &m, InputIterator first, InputIterator last, Predicate pred)

template<typename StatePropertyId , typename EventPropertyId , typename InputIterator , typename Predicate , typename IsNullStateProperty , typename IsNullEventProperty , typename StatePropertyIdInsertIterator >
void	deleteState (StateMachine< StatePropertyId, EventPropertyId, IsNullStateProperty, IsNullEventProperty > &m, InputIterator first, InputIterator last, Predicate pred, StatePropertyIdInsertIterator insertIt)

template<typename Fsm , typename StateCreator >
bool	synchronize (const std::vector< typename Ptr< Fsm >::ConstP > &components, const SynchronisationRules< Fsm > &rules, Fsm &synchronisation, StateCreator &creator)

std::string	listSingleItem (const std::string &item)

std::string	startListCaretItem (const std::string &item)

std::string	endListCaretItem ()

std::string	startTree (const std::string &treeId)

std::string	endTree ()

std::string	startNestedTree ()

std::string	endNestedTree ()

std::ostream &	toTreeViewHtmlStart (std::ostream &os)

std::ostream &	toTreeViewHtmlEnd (std::ostream &os)

template<typename Fsm , typename BeliefStateIterator , typename StateIdInsertIterator >
void	trimmingTraces (Fsm &machine, BeliefStateIterator bfBegin, BeliefStateIterator bfEnd, StateIdInsertIterator insertIt)
	Trim the traces of the Fsm that does not reach the given BeliefState. More...

template<typename Fsm , typename BeliefStateIterator , typename StateIdInsertIterator >
void	trimmingUnreachableStates (Fsm &machine, BeliefStateIterator bfBegin, BeliefStateIterator bfEnd, StateIdInsertIterator insertIt)
	Trim the states that cannot be reached from the given BeliefState. More...

template<typename Fsm , typename StateIdInsertIterator >
void	trimmingUnreachableStates (Fsm &machine, StateIdInsertIterator insertIt)
	Trim the states that cannot be reached from the initial states. More...

template<typename Fsm , typename BeliefStateIterator , typename StateIdInsertIterator >
bool	trimmingDeadlockStates (Fsm &machine, BeliefStateIterator bfBegin, BeliefStateIterator bfEnd, StateIdInsertIterator insertIt)
	Trim the states are the source of a deadlock within a range of states. More...

template<typename Fsm , typename StateIdInsertIterator >
bool	trimmingDeadlockStates (Fsm &machine, StateIdInsertIterator insertIt)
	Trim the states are the source of a deadlock. More...

template<typename Fsm , typename BeliefStateIterator , typename StateIdInsertIterator , typename DisableInsertIterator >
bool	controlledTrimmingDeadlockState (Fsm &machine, ControlPattern< Fsm > &pattern, BeliefStateIterator bfBegin, BeliefStateIterator bfEnd, StateIdInsertIterator insertIt, DisableInsertIterator disableIt)
	remove deadlock states of the machine by exploiting the events that are disabled in the current ControlPattern. More...

std::streampos	nextNoWhiteSpaceCharacter (std::istream &stream, bool &ok)
	return the stream position just before the first character that is a white space (not such that std::isspace is true) More...

bool	pruneCommentsBlock (std::istream &stream, bool &ok)
	analyze the stream and look for the end of a comment block More...

bool	pruneComments (std::istream &stream, bool &ok)
	read the stream and ignore the next c-style/cpp style comments More...

bool	checkSystemIdentifier (std::string &tsName, std::string::size_type &semiColonIndex)
	check that tsName is the name of a transition_system More...

std::istream &	tsFileTransitionLabel (std::istream &stream, std::unordered_map< std::string, std::string > &events, std::string &fullEventLabel, bool &ok)
	Read the transition label in a ts-format file. More...

void	tsExtractTargetState (const std::string &rawTargetState, std::string &targetState, std::string::size_type &semiColonIndex)
	extract the target state for the raw target state More...

std::istream &	tsFileHeader (std::istream &stream, std::string &tsName, bool &ok)
	parse the Ts-format file header More...

std::istream &	tsFileTransitions (std::istream &stream, ManagedTsFsms &fsms, bool &ok, TsConversionMode mode)
	Read the transitions of a Ts-format stream. More...

std::istream &	tsFileStates (std::istream &stream, ManagedTsFsms &fsms, bool &ok)

bool	fromTsFile (std::istream &stream, ManagedTsFsms &fsms, TsConversionMode mode)
	Load a Ts file as a DdAutFsm. More...

std::string	tsPrettyEvent (const std::string &tsEvent)

template<typename TransInserter >
void	insertTransitions (TransInserter &inserter)

template<typename TransInserterIterator >
void	insertRangeOfTransitions (TransInserterIterator begin, TransInserterIterator end)

Typedef Documentation

◆ AutEventId

using Diades::Automata::Experimental::AutEventId = typedef std::string

Definition at line 39 of file AutFile.hh.

◆ AutFsm

AutFsmTransitionInserter This is the TransitionInserter associated with an Diades::Automata::Experimental::AutFsm

and mainly used in insertAutFsms

It incrementally generates AutFsm::StatePropertyId's on demand (must be initialised with 0)

and mainly used in insertAutFsms. It inserts copies of State with new StateIds

and mainly used in insertAutFsms. It inserts copies of State with new StateIds. Event are inserted via an AutFsmEventInserter

Definition at line 45 of file AutFile.hh.

◆ AutFsmEventInserter

using Diades::Automata::Experimental::AutFsmEventInserter = typedef EventInserter<AutFsm>

Definition at line 232 of file AutFile.hh.

◆ AutFsmStateIdGenerator

using Diades::Automata::Experimental::AutFsmStateIdGenerator = typedef StateIdGenerator<AutFsm, Diades::Utils::IncrementGenerator<AutFsm::StatePropertyId> >

Definition at line 239 of file AutFile.hh.

◆ AutFsmStateInserter

using Diades::Automata::Experimental::AutFsmStateInserter = typedef StateInserter<AutFsmStateIdGenerator, StateCopy<AutFsm> >

Definition at line 245 of file AutFile.hh.

◆ AutFsmTransitionInserter

using Diades::Automata::Experimental::AutFsmTransitionInserter = typedef TransitionInserter<AutFsmStateInserter,AutFsmEventInserter>

Definition at line 254 of file AutFile.hh.

◆ AutStateId

using Diades::Automata::Experimental::AutStateId = typedef StatePropertyIdAsSizeT

Definition at line 34 of file AutFile.hh.

◆ BsMap

template<typename Fsm >

using Diades::Automata::Experimental::BsMap = typedef StMap<BsPtr<Fsm> >

Definition at line 482 of file BeliefState.hh.

◆ BsPtr

template<typename Fsm >

using Diades::Automata::Experimental::BsPtr = typedef typename BeliefState<Fsm>::SharedPtr

Definition at line 466 of file BeliefState.hh.

◆ CstBsMap

template<typename Fsm >

using Diades::Automata::Experimental::CstBsMap = typedef CstStMap<BsPtr<Fsm> >

Definition at line 474 of file BeliefState.hh.

◆ CstStMap

template<typename Type >

using Diades::Automata::Experimental::CstStMap = typedef Diades::Graph::ConstNodeMap<Type>

Definition at line 1857 of file StateMachine.hh.

◆ CstTrMap

template<typename Type >

using Diades::Automata::Experimental::CstTrMap = typedef Diades::Graph::ConstEdgeMap<Type>

Definition at line 1873 of file StateMachine.hh.

◆ DdAutAmpersand

using Diades::Automata::Experimental::DdAutAmpersand = typedef Diades::Utils::StringBinaryCombination<char, '&', std::char_traits<char>, std::allocator<char> >

Definition at line 169 of file DdAutFile.hh.

◆ DdAutBraces

using Diades::Automata::Experimental::DdAutBraces = typedef Diades::Utils::StringDelimiter<char, '{', '}', std::char_traits<char>, std::allocator<char> >

Definition at line 176 of file DdAutFile.hh.

◆ DdAutComma

using Diades::Automata::Experimental::DdAutComma = typedef Diades::Utils::StringBinaryCombination<char, ',', std::char_traits<char>, std::allocator<char> >

Definition at line 163 of file DdAutFile.hh.

◆ DdAutConjunction

using Diades::Automata::Experimental::DdAutConjunction = typedef Diades::Utils::Conjunction<DdAutStateLabel, DdAutComma, DdAutParentheses>

Definition at line 195 of file DdAutFile.hh.

◆ DdAutDisjunction

using Diades::Automata::Experimental::DdAutDisjunction = typedef Diades::Utils::Disjunction<DdAutStateLabel, DdAutComma, DdAutBraces>

Definition at line 189 of file DdAutFile.hh.

◆ DdAutEventId

using Diades::Automata::Experimental::DdAutEventId = typedef size_t

Definition at line 37 of file DdAutFile.hh.

◆ DdAutEventLabel

using Diades::Automata::Experimental::DdAutEventLabel = typedef std::string

Definition at line 58 of file DdAutFile.hh.

◆ DdAutEventManager

using Diades::Automata::Experimental::DdAutEventManager = typedef EventManager<DdAutEventLabel, DdAutEventId>

Definition at line 68 of file DdAutFile.hh.

◆ DdAutEventPrinter

using Diades::Automata::Experimental::DdAutEventPrinter = typedef EventManagerPrettyPrinter<DdAutEventLabel, DdAutEventId>

Definition at line 156 of file DdAutFile.hh.

◆ DdAutFA

using Diades::Automata::Experimental::DdAutFA = typedef FiniteAutomaton<DdAutStateId, DdAutEventId>

Definition at line 47 of file DdAutFile.hh.

◆ DdAutFsm

DdAutEventPrinter EventManagerPrettyPrinter associated with a Diades::Automata::Experimental::DdAutFsm

Definition at line 42 of file DdAutFile.hh.

◆ DdAutParentheses

using Diades::Automata::Experimental::DdAutParentheses = typedef Diades::Utils::StringDelimiter<char, '(', ')', std::char_traits<char>, std::allocator<char> >

Definition at line 182 of file DdAutFile.hh.

◆ DdAutProjection

using Diades::Automata::Experimental::DdAutProjection = typedef DiGraphComponentStartingWith<DdAutStateLabel, char, '|', DdAutComma, DdAutBraces>

Definition at line 201 of file DdAutFile.hh.

◆ DdAutStateId

using Diades::Automata::Experimental::DdAutStateId = typedef AutStateId

Definition at line 32 of file DdAutFile.hh.

◆ DdAutStateLabel

using Diades::Automata::Experimental::DdAutStateLabel = typedef StatePropertyAsStringLabel

Definition at line 53 of file DdAutFile.hh.

◆ DdAutStateManager

using Diades::Automata::Experimental::DdAutStateManager = typedef StatePropertyManager<DdAutStateLabel, DdAutStateId>

Definition at line 63 of file DdAutFile.hh.

◆ DdAutStatePrinter

using Diades::Automata::Experimental::DdAutStatePrinter = typedef StateInfoManagerPrettyPrinter<DdAutStateLabel, DdAutStateId>

Definition at line 151 of file DdAutFile.hh.

◆ DdAutSynchronisation

using Diades::Automata::Experimental::DdAutSynchronisation = typedef Diades::Utils::Conjunction<DdAutEventLabel, DdAutAmpersand, Diades::Utils::NoDelimiter<char, std::char_traits<char>, std::allocator<char> >>

Definition at line 208 of file DdAutFile.hh.

◆ ExplLocStateMap

using Diades::Automata::Experimental::ExplLocStateMap = typedef Diades::Graph::NodeMap<int>

Definition at line 32 of file Explanation.hh.

◆ LocStateMap

using Diades::Automata::Experimental::LocStateMap = typedef Diades::Graph::ConstNodeMap<int>

Definition at line 30 of file Explanation.hh.

◆ ManagedTsFsm

using Diades::Automata::Experimental::ManagedTsFsm = typedef std::tuple<TsFsmPtr,TsStMgrPtr,TsEvtMgrPtr>

Definition at line 29 of file TsFile.hh.

◆ ManagedTsFsms

using Diades::Automata::Experimental::ManagedTsFsms = typedef std::vector<ManagedTsFsm>

Definition at line 30 of file TsFile.hh.

◆ Matcher

using Diades::Automata::Experimental::Matcher = typedef std::unordered_map<Observation,Observables>

Definition at line 239 of file Explanation.hh.

◆ Observables

using Diades::Automata::Experimental::Observables = typedef std::set<DdAutFA::EventPropertyId>

Definition at line 238 of file Explanation.hh.

◆ Observation

using Diades::Automata::Experimental::Observation = typedef std::string

Definition at line 236 of file Explanation.hh.

◆ Observations

using Diades::Automata::Experimental::Observations = typedef std::vector<Observation>

Definition at line 237 of file Explanation.hh.

◆ SafeAlt

template<typename Fsm >

using Diades::Automata::Experimental::SafeAlt = typedef std::unordered_map<typename Fsm::State, std::unordered_set<typename Fsm::Transition> >

Definition at line 377 of file Explanation.hh.

◆ StatePropertyAsStringLabel

using Diades::Automata::Experimental::StatePropertyAsStringLabel = typedef std::string

Definition at line 37 of file StatePropertyManager.hh.

◆ StatePropertyAsUnsigned

using Diades::Automata::Experimental::StatePropertyAsUnsigned = typedef unsigned

Definition at line 45 of file StatePropertyManager.hh.

◆ StatePropertyIdAsSizeT

using Diades::Automata::Experimental::StatePropertyIdAsSizeT = typedef size_t

Definition at line 43 of file StateMachine.hh.

◆ StMap

template<typename Type >

using Diades::Automata::Experimental::StMap = typedef Diades::Graph::NodeMap<Type>

Definition at line 1865 of file StateMachine.hh.

◆ TrMap

template<typename Type >

using Diades::Automata::Experimental::TrMap = typedef Diades::Graph::EdgeMap<Type>

Definition at line 1881 of file StateMachine.hh.

◆ TsEvtMgr

using Diades::Automata::Experimental::TsEvtMgr = typedef DdAutEventManager

Definition at line 26 of file TsFile.hh.

◆ TsEvtMgrPtr

using Diades::Automata::Experimental::TsEvtMgrPtr = typedef std::shared_ptr<TsEvtMgr>

Definition at line 28 of file TsFile.hh.

◆ TsFsm

using Diades::Automata::Experimental::TsFsm = typedef DdAutFsm

Definition at line 23 of file TsFile.hh.

◆ TsFsmPtr

using Diades::Automata::Experimental::TsFsmPtr = typedef std::shared_ptr<TsFsm>

Definition at line 24 of file TsFile.hh.

◆ TsStMgr

using Diades::Automata::Experimental::TsStMgr = typedef DdAutStateManager

Definition at line 25 of file TsFile.hh.

◆ TsStMgrPtr

using Diades::Automata::Experimental::TsStMgrPtr = typedef std::shared_ptr<TsStMgr>

Definition at line 27 of file TsFile.hh.

Enumeration Type Documentation

◆ TsConversionMode

enum Diades::Automata::Experimental::TsConversionMode

Enumerator
normal
full
update

Definition at line 21 of file TsFile.hh.

Function Documentation

◆ abstract() [1/2]

template<typename Fsm , typename BeliefStateIterator , typename StateCreation >

bool Diades::Automata::Experimental::abstract	(	const Fsm &	machine,
		Fsm &	abstractedMachine,
		BeliefStateIterator	bfBegin,
		BeliefStateIterator	bfEnd,
		std::vector< typename Fsm::State > &	abstractedStates,
		StateCreation &	creator
	)

Parameters

machine	a StateMachine
abstractMachine	the resulting abstracted StateMachine
bfBegin	the start iterator of a BeliefState<Property,EventInfo> range
bfEnd	the end iterator of a BeliefState<Property,EventInfo> range
abstractedStates	the created states of abstractMachine in the order of the BeliefState range.

Returns: true if the abstraction is a success. If not the state of the abstractedMachine is undetermined.

Precondition: machine should not be abstractedMachine [bfBegin,bfEnd) represents a set of belief states bs1, bs2, ... bsn. Each bsi is a set of State from the initial StateMachine 'machine'. The abstracted machine will contain n states. State si will represent the states of bsi. A transition t of event e between state si and sj exists in the abstracted machine iff there exists a transition t of event e between a state from bsi and a state from bsj in the original machine. The state si of the abtracted machine is initial as soon as one of the state of bsi is initial.

Definition at line 45 of file Abstract.hh.

◆ abstract() [2/2]

template<typename Fsm , typename BeliefStateIterator , typename StateCreation >

bool Diades::Automata::Experimental::abstract	(	const Fsm &	machine,
		Fsm &	abstractedMachine,
		BeliefStateIterator	bfBegin,
		BeliefStateIterator	bfEnd,
		StateCreation &	creator
	)

Parameters

machine	a StateMachine
abstractMachine	the resulting abstracted StateMachine
bfBegin	the start iterator of a BeliefState<Property,EventInfo> range
bfEnd	the end iterator of a BeliefState<Property,EventInfo> range
abstractedStates	the created states of abstractMachine in the order of the BeliefState range.

Returns: true if the abstraction is a success. If not the state of the abstractedMachine is undetermined.

Precondition: machine should not be abstractedMachine [bfBegin,bfEnd) represents a set of belief states bs1, bs2, ... bsn. Each bsi is a set of State from the initial StateMachine 'machine'. The abstracted machine will contain n states. State si will represent the states of bsi. A transition t of event e between state si and sj exists in the abstracted machine iff there exists a transition t of event e between a state from bsi and a state from bsj in the original machine. The state si of the abtracted machine is initial as soon as one of the state of bsi is initial.

Parameters

machine	a StateMachine
abstractMachine	the resulting abstracted StateMachine
bfBegin	the start iterator of a BeliefState<Property,EventInfo> range
bfEnd	the end iterator of a BeliefState<Property,EventInfo> range

Returns: true if the abstraction is a success. If not the state of the abstractedMachine is undetermined.

Precondition: machine should not be abstractedMachine [bfBegin,bfEnd) represents a set of belief states bs1, bs2, ... bsn. Each bsi is a set of State from the initial StateMachine 'machine'. The abstracted machine will contain n states. State si will represent the states of bsi. A transition t of event e between state si and sj exists in the abstracted machine iff there exists a transition t of event e between a state from bsi and a state from bsj in the original machine. The state si of the abtracted machine is initial as soon as one of the state of bsi is initial.

Definition at line 190 of file Abstract.hh.

◆ abstractEvents() [1/4]

template<typename Fsm , typename EventPropertyIdIterator >

bool Diades::Automata::Experimental::abstractEvents	(	const Fsm &	machine,
		Fsm &	abstractMachine,
		EventPropertyIdIterator	begin,
		EventPropertyIdIterator	end,
		BsMap< Fsm > &	bsMap,
		CstStMap< typename Fsm::State > &	stMap
	)

Parameters

machine	a StateMachine
abstractMachine	the resulting abstracted StateMachine
begin	the start iterator of a range of EventInfoId to abstract
end	the end iterator of a range of EventInfoId to abstract
bsMap	resulting mapping that associates a State from abstractMachine to the set of abstracted states in the initial machine
stMap	resulting mapping that associates a State of the initial machine to the state in the abstractMachine. Only initial states or states from the initial machine that are targets of a projected transition have an association. Any other states of the initial StateMachine are associated with an invalid state (as they may actually belong to several belief states of the abstracted machine).

Returns: true if the abstraction is a success. If not the state of the abstractedMachine is undetermined.

Precondition: machine should not be abstractedMachine. machine must have at least one initial state; [begin,end) represents a set of EventInfoId of the StateMachine

Postcondition: the abstractMachine only contains events from StateMachine that are not part of [begin,end)

Definition at line 720 of file Project.hh.

References Diades::Automata::Experimental::Projection::projectRange().

Referenced by abstractEvents().

◆ abstractEvents() [2/4]

template<typename Fsm , typename EventPropertyIdIterator >

bool Diades::Automata::Experimental::abstractEvents	(	const Fsm &	machine,
		Fsm &	abstractMachine,
		EventPropertyIdIterator	begin,
		EventPropertyIdIterator	end
	)

Parameters

machine	a StateMachine
abstractMachine	the resulting abstracted StateMachine
begin	the start iterator of a range of EventInfoId to abstract
end	the end iterator of a range of EventInfoId to abstract

Returns: true if the abstraction is a success. If not the state of the abstractedMachine is undetermined.

Precondition: machine should not be abstractedMachine. machine must have at least one initial state; [begin,end) represents a set of EventInfoId of the StateMachine

Postcondition: the abstractMachine only contains events from StateMachine that are not part of [begin,end)

Definition at line 757 of file Project.hh.

References abstractEvents().

◆ abstractEvents() [3/4]

template<typename Fsm , typename EventPropertyIdIterator , typename StateProperty , typename StateLabelProjection >

bool Diades::Automata::Experimental::abstractEvents	(	const Fsm &	fsm,
		Fsm &	projectedFsm,
		const StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &	stateManager,
		StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &	projectionStateManager,
		const StateLabelProjection &	projection,
		EventPropertyIdIterator	begin,
		EventPropertyIdIterator	end,
		BsMap< Fsm > &	bsMap,
		CstStMap< typename Fsm::State > &	stMap
	)

Parameters

machine	a StateMachine
abstractMachine	the resulting abstracted StateMachine
begin	the start iterator of a range of EventInfoId to project
end	the end iterator of a range of EventInfoId to project
bsMap	resulting mapping that associates a State from abstractMachine to the set of abstracted states in the initial machine
stMap	resulting mapping that associates a State of the initial machine to the state in the abstractMachine. Only initial states or states from the initial machine that are targets of a projected transition have an association. Any other states of the initial StateMachine are associated with an invalid state (as they may actually belong to several belief states of the abstracted machine).

Returns: true if the projection is a success. If not the state of the abstractedMachine is undetermined.

Precondition: machine should not be abstractedMachine. machine must have at least one initial state; [begin,end) represents a set of EventInfoId of the StateMachine

Postcondition: the abstractMachine only contains events from [begin,end)

Definition at line 791 of file Project.hh.

References Diades::Automata::Experimental::Projection::projectRange().

◆ abstractEvents() [4/4]

template<typename Fsm , typename EventPropertyIdIterator , typename StateProperty , typename StateLabelProjection >

bool Diades::Automata::Experimental::abstractEvents	(	const Fsm &	fsm,
		Fsm &	projectedFsm,
		const StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &	stateManager,
		StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &	projectionStateManager,
		const StateLabelProjection &	projection,
		EventPropertyIdIterator	begin,
		EventPropertyIdIterator	end
	)

Parameters

machine	a StateMachine
abstractMachine	the resulting abstracted StateMachine
begin	the start iterator of a range of EventInfoId to project
end	the end iterator of a range of EventInfoId to project

Returns: true if the projection is a success. If not the state of the abstractedMachine is undetermined.

Precondition: machine should not be abstractedMachine. machine must have at least one initial state; [begin,end) represents a set of EventInfoId of the StateMachine

Postcondition: the abstractMachine only contains events from [begin,end)

Definition at line 838 of file Project.hh.

References abstractEvents().

◆ autFileStateEncoding()

template<typename Fsm >

void Diades::Automata::Experimental::autFileStateEncoding	(	const Fsm &	fsm,
		Diades::Graph::ConstNodeMap< AutStateId > &	encoding
	)

autFileStateEncoding computes a compatible state encoding to store the fsm into an aut file. States in aut file must start from 0 continously to n-1 where n is the number of states

Parameters

fsm	the fsm to reencode
encoding	the resulting encoding

Definition at line 79 of file AutFile.hh.

References Diades::Graph::ConstNodeMap< T >::init().

Referenced by autFileStateReencoding().

◆ autFileStateReencoding()

template<typename Fsm >

void Diades::Automata::Experimental::autFileStateReencoding ( Fsm & fsm )

autFileStateReencoding reencodes the states of the fsm to be ready for storage into an aut file. States in aut file must start from 0 continuously to n-1 where n is the number of states

Parameters

fsm	the fsm to reencode

Definition at line 109 of file AutFile.hh.

References autFileStateEncoding(), fromAutFile(), and toAutFile().

Referenced by insertAutFsms().

◆ autFsmNeedEncoding()

template<typename Fsm >

bool Diades::Automata::Experimental::autFsmNeedEncoding ( const Fsm & fsm )

Parameters

fsm	an AutFsm or anything like an AutFsm with AutStateId as StateProperty

Returns: true if the states from the fsm have properties from [0,...n-1] where n is the number of states in the fsm

Definition at line 55 of file AutFile.hh.

◆ checkSystemIdentifier()

bool Diades::Automata::Experimental::checkSystemIdentifier	(	std::string &	tsName,
		std::string::size_type &	semiColonIndex
	)

check that tsName is the name of a transition_system

tsName is a piece of text without any space but it can be a text like 'identifier;' The idea here is to detect such a format. If ';' is present then it is removed from tsName (i.e. tsName then becomes 'identifier') and secondColonIndex returns the index where the ';' was. If ';' is not found then semiColonIndex remains unchanged (so please assign it to std::string::npos to make it as non informative).

Parameters

tsName	the text to analyze as a identifier of a transition_system. It is updated by removing ';' if such a ';' is found.
semiColonIndex	the index of the ';' if it is found in 'tsName' (unchanged otherwise)

Returns: true if an identifier for the transition_system is found at the beginning of 'tsName'

◆ complete()

template<typename Fsm >

void Diades::Automata::Experimental::complete ( Fsm & machine )

Parameters

machine The original StateMachine

Postcondition: The completion of the StateMachine.

Definition at line 58 of file Complete.hh.

Referenced by completeAut(), and completeDdaut().

◆ controlledTrimmingDeadlockState()

template<typename Fsm , typename BeliefStateIterator , typename StateIdInsertIterator , typename DisableInsertIterator >

bool Diades::Automata::Experimental::controlledTrimmingDeadlockState	(	Fsm &	machine,
		ControlPattern< Fsm > &	pattern,
		BeliefStateIterator	bfBegin,
		BeliefStateIterator	bfEnd,
		StateIdInsertIterator	insertIt,
		DisableInsertIterator	disableIt
	)

remove deadlock states of the machine by exploiting the events that are disabled in the current ControlPattern.

A ControlPattern is a mapping that associates with each event type of the Fsm whether the event type is enabled or not (i.e. disabled). This function removes the deadlock states within the range of states in bfBegin/bfEnd by looking for states in the machine with an output event that can be disabled according to the pattern and, if it is triggered, will cause the trigger of enabled events (events that cannot be disabled according to the pattern) and lead to a deadlock state from the given range. It must be noticed that by pruning states, it might create new deadlock states that must be removed. After this function returns, the machine may still have some deadlocks but these deadlocks were not in the range bfBegin/bfEnd. If the range bfBegin/bfEnd is the full range of states in the machine, the function ensures that there is no more deadlock states in the returned machine. In case, there is no solution to the problem the resulting machine becomes invalid (with no more initial states).

Parameters

[in]	machine	The Fsm that is updated
[in]	pattern	The ControlPattern in use
[in]	bfBegin	the start iterator on a range of states to visit
[in]	bfEnd	the end iterator on a range of states to visit
[out]	insertIt	an insert iterator in charge of keeping the StatePropertyId of the states that are removed.
[out]	disableIt	an insert iterator in charge of keeping the pair <StatePropertyId,Event> of disabled events that remove the deadlocks.

Returns: true the resulting machine is still valid (i.e. it has at least one initial state)

Definition at line 258 of file Trimming.hh.

References Diades::Automata::Experimental::ControlPattern< Fsm >::enabled().

Referenced by trimDdAutStates2().

◆ deleteState() [1/5]

template<typename StatePropertyId , typename EventPropertyId , typename InputIterator , typename NullStateProperty , typename NullEventProperty >

void Diades::Automata::Experimental::deleteState	(	StateMachine< StatePropertyId, EventPropertyId, NullStateProperty, NullEventProperty > &	m,
		InputIterator	first,
		InputIterator	last
	)

inline

Referenced by Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::deleteState(), insertAutFsms(), trimmingTraces(), and trimmingUnreachableStates().

◆ deleteState() [2/5]

template<typename StatePropertyId , typename EventPropertyId , typename InputIterator , typename Predicate , typename NullStatePropertyId = NullValue<StatePropertyId>, typename NullEventPropertyId >

void Diades::Automata::Experimental::deleteState	(	StateMachine< StatePropertyId, EventPropertyId, NullStatePropertyId, NullEventPropertyId > &	m,
		InputIterator	first,
		InputIterator	last,
		Predicate	pred
	)

inline

◆ deleteState() [3/5]

template<typename StatePropertyId , typename EventPropertyId , typename InputIterator , typename IsNullStateProperty , typename IsNullEventProperty >

void Diades::Automata::Experimental::deleteState	(	StateMachine< StatePropertyId, EventPropertyId, IsNullStateProperty, IsNullEventProperty > &	m,
		InputIterator	first,
		InputIterator	last
	)

inline

Definition at line 1809 of file StateMachine.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::deleteState().

◆ deleteState() [4/5]

template<typename StatePropertyId , typename EventPropertyId , typename InputIterator , typename Predicate , typename IsNullStateProperty , typename IsNullEventProperty >

void Diades::Automata::Experimental::deleteState	(	StateMachine< StatePropertyId, EventPropertyId, IsNullStateProperty, IsNullEventProperty > &	m,
		InputIterator	first,
		InputIterator	last,
		Predicate	pred
	)

inline

Definition at line 1821 of file StateMachine.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::deleteState().

◆ deleteState() [5/5]

template<typename StatePropertyId , typename EventPropertyId , typename InputIterator , typename Predicate , typename IsNullStateProperty , typename IsNullEventProperty , typename StatePropertyIdInsertIterator >

void Diades::Automata::Experimental::deleteState	(	StateMachine< StatePropertyId, EventPropertyId, IsNullStateProperty, IsNullEventProperty > &	m,
		InputIterator	first,
		InputIterator	last,
		Predicate	pred,
		StatePropertyIdInsertIterator	insertIt
	)

inline

Definition at line 1836 of file StateMachine.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::deleteState(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::getStatePropertyId().

◆ deleteTransition() [1/2]

template<typename StatePropertyId , typename EventPropertyId , typename InputIterator , typename NullStateProperty , typename NullEventProperty >

void Diades::Automata::Experimental::deleteTransition	(	StateMachine< StatePropertyId, EventPropertyId, NullStateProperty, NullEventProperty > &	m,
		InputIterator	first,
		InputIterator	last
	)

inline

STL-like algorithm

Referenced by Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::deleteTransition().

◆ deleteTransition() [2/2]

template<typename StatePropertyId , typename EventPropertyId , typename InputIterator , typename IsNullStatePropertyId , typename IsNullEventProperty >

void Diades::Automata::Experimental::deleteTransition	(	StateMachine< StatePropertyId, EventPropertyId, IsNullStatePropertyId, IsNullEventProperty > &	m,
		InputIterator	first,
		InputIterator	last
	)

inline

STL-like algorithm

Definition at line 1797 of file StateMachine.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::deleteTransition().

◆ descriptorToRules()

template<typename DdAutFsmType >

bool Diades::Automata::Experimental::descriptorToRules	(	const DdSyncDescriptor &	desc,
		ParametrizedSynchronisation< DdAutFsmType > &	rules,
		std::string &	errorMsg
	)

Parameters

desc	the descriptor
rules	the initialised set of synchronisation rules
errorMsg	updated with potential errors in no success

Returns: true if the import from the descriptor is a success Note that rules must already be initialised with a set of components that contain at least the component of the names described in the descriptor and the events from the descriptor. If not it is a failure and rules are cleared

Definition at line 456 of file DdSyncDescriptor.hh.

Referenced by synchroniseDdAut().

◆ determine()

template<typename Fsm , typename StateCreator >

void Diades::Automata::Experimental::determine	(	const Fsm &	machine,
		Fsm &	deterministicMachine,
		StateCreator &	creator
	)

Parameters

machine	The original StateMachine
deterministicMachine	The deterministic version of the original StateMachine
creator	Definition of the way the states of the deterministic machine will be created from the original machine (should be a derived class from BeliefStateBasedStateCreator)

Precondition: deterministicMachine must not be the original machine; Note that if the StateMachine does not have any initial state, it is considered as if the original StateMachine is empty. A StateMachine that has no 'specific' initial states is a StateMachine such any state can be initial, in this case machine.setAllInitialStates() must be applied first.

Postcondition: A deterministic StateMachine, if not empty, has one initial state only.

Definition at line 65 of file Determine.hh.

References require, and states.

Referenced by determineAut(), determineDdaut(), minimizeAut(), and minimizeDdaut().

◆ endListCaretItem()

std::string Diades::Automata::Experimental::endListCaretItem ( )

Referenced by writeTreeView(), and writeTreeViewTransition().

◆ endNestedTree()

std::string Diades::Automata::Experimental::endNestedTree ( )

Referenced by writeTreeView(), and writeTreeViewTransition().

◆ endTree()

std::string Diades::Automata::Experimental::endTree ( )

Referenced by writeTreeView().

◆ explain()

bool Diades::Automata::Experimental::explain	(	const DdAutFA &	fsa,
		const DdAutStateManager &	sManager,
		const DdAutEventManager &	eManager,
		const std::vector< std::string > &	observations,
		Observables &	observables,
		DdAutFA &	explanations,
		DdAutFA &	fullExplanations,
		DdAutStateManager &	sManagerExplanation,
		std::unordered_map< DdAutFA::State, unordered_set< DdAutFA::Transition > > &	safeAlternatives
	)

Definition at line 555 of file Explanation.hh.

References explainFromStates(), initialiseMatcher(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::initialStateBegin(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::initialStateEnd(), levelOfChoice(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::name(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::setName().

Referenced by explainLog().

◆ explainFromStates()

template<typename StateIterator >

bool Diades::Automata::Experimental::explainFromStates	(	StateIterator	begin,
		StateIterator	end,
		const DdAutFA &	fsa,
		const DdAutStateManager &	sManager,
		const DdAutEventManager &	eManager,
		const Observations &	observations,
		Observables &	observables,
		DdAutFA &	explanations,
		DdAutFA &	traces,
		DdAutStateManager &	sManagerExplanation,
		const Matcher &	matcher,
		const LocStateMap &	levelOfChoice,
		SafeAlt< DdAutFA > &	safeAlternatives
	)

Definition at line 382 of file Explanation.hh.

Referenced by explain().

◆ extractEffectiveChoiceTransitions()

template<typename Fsm >

void Diades::Automata::Experimental::extractEffectiveChoiceTransitions	(	Fsm &	traces,
		const ExplLocStateMap &	levelOfChoice,
		unordered_set< typename Fsm::Transition > &	solutions
	)

Extraction from the traces of A || Pbar || L, the set of effective choice transitions.

Parameters

traces	any path from the initial state to an acceptor states is a trace from A \|\| Pbar \|\| L
levelOfChoice	the level of choices on any state in traces
solutions	the returned set of effective choice transitions

Definition at line 253 of file Explanation.hh.

Referenced by explainFromStates().

◆ faFromDdAutFile()

bool Diades::Automata::Experimental::faFromDdAutFile	(	std::istream &	stream,
		const ManagedDdAutFA &	mFa
	)

import a FiniteAutomaton from a ddaut format file stream

Parameters

stream	the stream that contains the ddaut description
sManager	the manager that records the state information
eManager	the manager that records the event information

Returns: true if the import is a success not a complete

Todo:: complete the parser

See also: http://cadp.inria.fr/man/aut.html The ddaut format is an extension of the aut format

about the aut file format: The first line of an AUT file has the following syntax: des (<initial-state>, <number-of-transitions>, <number-of-states>) The "des" keywords stands for "descriptor". The <number-of-states> must be greater or equal to 1, because there is always at least one state, the initial state. State numbers range between 0 and <number-of-states> - 1. The <initial-state> is always equal to 0. The remainder of the AUT file consists of one line per transition, in an arbitrary order. Each remaining line has the following syntax: (<from-state>, <label>, <to-state>) where <from-state> and <to-state> are state numbers and where <label> can take two possible forms: <unquoted-label> consists of a character string starting with a letter, and followed by zero, one, or many letters, digits, or underscore characters. <quoted-label> consists of a character string starting with a double quote and ending with a double quote. Between these two double quotes, there can be zero, one or many printable characters; the meaning of "printable" is given by the POSIX isprint() function with locale "C" (namely, ASCII characters with decimal codes in the range from 32 to 126, bounds included). No other assumption should be made about the characters present between these two double quotes. In particular, the double quote character itself may be present, and may not necessarily be "escaped" in some way (e.g., preceded by a backslash, as in C).

About the ddaut extensions: the idea is to start from the aut format and add new fields of information: for now state, event, initial, acceptor None of this field is mandatory. There is no order. They may be several occurrence of the same field. Be as flexible as possible. None of the information in the fields has to be complete.

About state: it is a couple consisting of one integer (the id of the state) and one <label>, one couple per line. If the state is present several times, the last occurrence prevails

Referenced by insertDdAuts(), and synchroniseDdAut().

◆ faFromDescriptor()

bool Diades::Automata::Experimental::faFromDescriptor	(	const DdAutFileDescriptor &	descriptor,
		DdAutFA &	fa,
		DdAutStateManager &	sManager,
		DdAutEventManager &	eManager
	)

Parameters

descriptor
fsm	the state machine to fill
sManager	the state manager to fill
eManager	the event manager to fill

Returns: true if the initialisation of the fsm is a success

Referenced by completeDdaut(), determineDdaut(), explainFsm(), exportDdAutToDot(), Diades::CmdInterface::loadFiniteStateAutomaton(), minimizeDdaut(), projectDdaut(), tagDdAutStates2(), and trimDdAutStates2().

◆ faToDdAutFile()

bool Diades::Automata::Experimental::faToDdAutFile	(	ostream &	stream,
		const ConstManagedDdAutFA &	mFa
	)

FA To DdAutFile

Parameters

stream	the updated output stream
fa	the Finite Automaton to export
sManager	the manager that records the state information
eManager	the manager that records the event information
enforce	(encoding of the states in aut file format if needed)

Returns: true if the export is a success.

The export is not a success the finite automaton is not valid or if there is some writing issues with stream

Referenced by tagDdAutStates2(), trimDdAutStates2(), and Diades::CmdInterface::writeFiniteAutomaton().

◆ faToDescriptor()

bool Diades::Automata::Experimental::faToDescriptor	(	const DdAutFA &	fa,
		DdAutFileDescriptor &	descriptor,
		const DdAutStateManager &	sManager,
		const DdAutEventManager &	eManager,
		Diades::Graph::ConstNodeMap< DdAutStateId > &	encoding
	)

Parameters

fsm	a FiniteAutomaton
descriptor	a ddaut fsm descriptor
sManager	the state manager of the FA
eManager	the event manager of the FA

Returns: true if the conversion of the FA to the descriptor is a success

◆ fromAutFile()

bool Diades::Automata::Experimental::fromAutFile	(	std::istream &	stream,
		AutFsm &	fsm
	)

import a Component from an aut format file stream

Parameters

stream the stream that contains the aut description

Returns: true if the import is a success not a complet parser

Todo:: complete the parser

See also: http://cadp.inria.fr/man/aut.html about the aut file format: The first line of an AUT file has the following syntax: des (<initial-state>, <number-of-transitions>, <number-of-states>) The "des" keywords stands for "descriptor". The <number-of-states> must be greater or equal to 1, because there is always at least one state, the initial state. State numbers range between 0 and <number-of-states> - 1. The <initial-state> is always equal to 0. The remainder of the AUT file consists of one line per transition, in an arbitrary order. Each remaining line has the following syntax: (<from-state>, <label>, <to-state>) where <from-state> and <to-state> are state numbers and where <label> can take two possible forms: <unquoted-label> consists of a character string starting with a letter, and followed by zero, one, or many letters, digits, or underscore characters. <quoted-label> consists of a character string starting with a double quote and ending with a double quote. Between these two double quotes, there can be zero, one or many printable characters; the meaning of "printable" is given by the POSIX isprint() function with locale "C" (namely, ASCII characters with decimal codes in the range from 32 to 126, bounds included). No other assumption should be made about the characters present between these two double quotes. In particular, the double quote character itself may be present, and may not necessarily be "escaped" in some way (e.g., preceded by a backslash, as in C).

Referenced by autFileStateReencoding(), completeAut(), determineAut(), exportAutToDot(), insertAuts(), minimizeAut(), projectAut(), and runAut().

◆ fromTsFile()

bool Diades::Automata::Experimental::fromTsFile	(	std::istream &	stream,
		ManagedTsFsms &	fsms,
		TsConversionMode	mode
	)

Load a Ts file as a DdAutFsm.

This is the first function that handles ts-format that results from arc (altarica tool)

Parameters

stream	a stream that contains a ts-format transition system
fsms	the vector of managed fsms extracted from the ts file (first the global fsm followed by its component projection)
mode	normal (as in ts), full (events contain the target state), update (events contain state changes)

Returns: true is the loading is a success

Referenced by exportTsToDdAut2().

◆ fsmFromDdAutFile()

bool Diades::Automata::Experimental::fsmFromDdAutFile	(	std::istream &	stream,
		const ManagedDdAutFsm &	mFsm
	)

import a StateMachine from a ddaut format file stream

Parameters

stream	the stream that contains the ddaut description
sManager	the manager that records the state information
eManager	the manager that records the event information

Returns: true if the import is a success not a complete

Todo:: complete the parser

See also: http://cadp.inria.fr/man/aut.html The ddaut format is an extension of the aut format

about the aut file format: The first line of an AUT file has the following syntax: des (<initial-state>, <number-of-transitions>, <number-of-states>) The "des" keywords stands for "descriptor". The <number-of-states> must be greater or equal to 1, because there is always at least one state, the initial state. State numbers range between 0 and <number-of-states> - 1. The <initial-state> is always equal to 0. The remainder of the AUT file consists of one line per transition, in an arbitrary order. Each remaining line has the following syntax: (<from-state>, <label>, <to-state>) where <from-state> and <to-state> are state numbers and where <label> can take two possible forms: <unquoted-label> consists of a character string starting with a letter, and followed by zero, one, or many letters, digits, or underscore characters. <quoted-label> consists of a character string starting with a double quote and ending with a double quote. Between these two double quotes, there can be zero, one or many printable characters; the meaning of "printable" is given by the POSIX isprint() function with locale "C" (namely, ASCII characters with decimal codes in the range from 32 to 126, bounds included). No other assumption should be made about the characters present between these two double quotes. In particular, the double quote character itself may be present, and may not necessarily be "escaped" in some way (e.g., preceded by a backslash, as in C).

About the ddaut extensions: the idea is to start from the aut format and add new fields of information: for now state, event, initial, acceptor None of this field is mandatory. There is no order. They may be several occurrence of the same field. Be as flexible as possible. None of the information in the fields has to be complete.

About state: it is a couple consisting of one integer (the id of the state) and one <label>, one couple per line. If the state is present several times, the last occurrence prevails

◆ fsmFromDescriptor()

bool Diades::Automata::Experimental::fsmFromDescriptor	(	const DdAutFileDescriptor &	descriptor,
		DdAutFsm &	fsm,
		DdAutStateManager &	sManager,
		DdAutEventManager &	eManager
	)

Parameters

descriptor
fsm	the state machine to fill
sManager	the state manager to fill
eManager	the event manager to fill

Returns: true if the initialisation of the fsm is a success

Referenced by completeDdaut(), determineDdaut(), Diades::CmdInterface::loadFiniteStateMachine(), minimizeDdaut(), projectDdaut(), and runDdaut().

◆ fsmToAutFile()

bool Diades::Automata::Experimental::fsmToAutFile	(	ostream &	stream,
		const DdAutFsm &	fsm,
		const DdAutEventManager &	eManager,
		bool	enforce = `false`
	)

Fsm To AutFile

Parameters

stream	the updated output stream
fsm	the Fsm to export
eManager	the manager that records the event information
enforce	(encoding of the states in aut file format if needed)

Returns: true if the export is a success.

The export is not a success the fsm is empty or if there is more than one initial state in the Fsm. If the encoding is not forced but is incompatible then failure. This function actually converts a Fsm in ddaut file to aut file, so the state labels are simply ignored the event are the event label in the eManager.

Referenced by Diades::CmdInterface::writeFiniteAutomaton(), and Diades::CmdInterface::writeFiniteStateMachine().

◆ fsmToDdAutFile()

bool Diades::Automata::Experimental::fsmToDdAutFile	(	ostream &	stream,
		const ConstManagedDdAutFsm &	mFsm
	)

Fsm To DdAutFile

Parameters

stream	the updated output stream
fsm	the Fsm to export
sManager	the manager that records the state information
eManager	the manager that records the event information
enforce	(encoding of the states in aut file format if needed)

Returns: true if the export is a success.

The export is not a success the fsm is empty or if there is some writing issues with stream

Referenced by exportTsToDdAut2(), writeDdAutComponents(), and Diades::CmdInterface::writeFiniteStateMachine().

◆ fsmToDescriptor()

bool Diades::Automata::Experimental::fsmToDescriptor	(	const DdAutFsm &	fsm,
		DdAutFileDescriptor &	descriptor,
		const DdAutStateManager &	sManager,
		const DdAutEventManager &	eManager,
		Diades::Graph::ConstNodeMap< DdAutStateId > &	encoding
	)

Parameters

fsm	a DdAutFsm
descriptor	a ddaut fsm descriptor
sManager	the state manager of the fsm
eManager	the event manager of the fsm

Returns: true if the conversion of the DdAutFsm to the descriptor is a success

◆ generateSynchronisedDdAutEventLabels()

template<typename DdAutFsmType >

bool Diades::Automata::Experimental::generateSynchronisedDdAutEventLabels	(	const SynchronisationRules< DdAutFsmType > &	synchro,
		const std::vector< DdAutEventManager > &	eventManagers,
		DdAutEventManager &	syncEventManager
	)

Generation of a label to represent each synchronisation events involved in the rules synchro

Parameters

synchro	synchronisation rules
eventManagers	the event managers of the DdAut Fsm involved in the synchronisation
syncEventManager	the manager that is associated with the resulting synchronised fsm

Returns: true if the operation is a success

Definition at line 432 of file DdAutFile.hh.

References Diades::Automata::Experimental::SynchronisationRules< StateMachine >::beginOfSynchronisedEvents(), Diades::Automata::Experimental::SynchronisationRules< StateMachine >::endOfSynchronisedEvents(), insertDdAutFA(), and Diades::Automata::Experimental::EventManager< _Event, _EventId, NullEvent, NullEventId, Hash >::setEvent().

Referenced by synchroniseDdAut().

◆ getSafeAlternatives()

std::unordered_set<DdAutFA::Transition> Diades::Automata::Experimental::getSafeAlternatives	(	const DdAutFA &	traces,
		DdAutFA::State	state,
		const ExplLocStateMap &	levelOfChoiceInTraces,
		const Diades::Graph::NodeMap< DdAutFA::State > &	mapping,
		const DdAutFA &	fsa,
		const LocStateMap &	levelOfChoiceInFsa,
		const DdAutStateManager &	sManager,
		const DdAutEventManager &	eManager
	)

Definition at line 344 of file Explanation.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::outputTransitionBegin(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::outputTransitionEnd().

Referenced by explainFromStates().

◆ initialiseMatcher()

Matcher Diades::Automata::Experimental::initialiseMatcher	(	const DdAutEventManager &	eManager,
		const std::vector< std::string > &	observations
	)

Definition at line 525 of file Explanation.hh.

References Diades::Utils::InfoManager< _Info, _InfoId, _NullInfo, _NullInfoId, _Hash >::begin(), Diades::Utils::InfoManager< _Info, _InfoId, _NullInfo, _NullInfoId, _Hash >::end(), and Diades::Automata::Experimental::EventManager< _Event, _EventId, NullEvent, NullEventId, Hash >::getEvent().

Referenced by explain().

◆ insertAutFsms()

template<typename AutFsmRange >

bool Diades::Automata::Experimental::insertAutFsms	(	AutFsmRange	range,
		AutFsm &	output
	)

AutFsm insertion

Parameters

a	range of AutFsm
output	the AutFsm where all the AutFsm of the range have been inserted

Returns: true if success This is used by the program dd-insert, it ensures it is a compatible AutFsm as it merges the initial states. Be aware that the state encoding might not be

Definition at line 270 of file AutFile.hh.

Referenced by insertAuts().

◆ insertDdAutFA()

void Diades::Automata::Experimental::insertDdAutFA	(	const DdAutFA &	sourceFsm,
		const DdAutStateManager &	sourceStateManager,
		const DdAutEventManager &	sourceEventManager,
		DdAutFA &	targetFsm,
		DdAutStateManager &	targetStateManager,
		DdAutEventManager &	targetEventManager
	)

Insertion of a sourceFsm into a targetFsm

Parameters

sourceFsm	the Fsm to insert
sourceStateManager	the state manager associated with the source fsm
sourceEventManager	the event manager associated with the source fsm
targetFsm	the Fsm where the sourceFsm is inserted
targetStateManager	the target state manager associated with the target fsm
targetEventManager	the target event manager associated with the target fsm

Referenced by generateSynchronisedDdAutEventLabels(), and insertFiniteAutomata().

◆ insertFiniteAutomata()

template<typename DdAutFARange , typename RangeDdAutSM , typename RangeDdAutEM >

bool Diades::Automata::Experimental::insertFiniteAutomata	(	DdAutFARange	faRange,
		RangeDdAutSM	smRange,
		RangeDdAutEM	evRange,
		DdAutFA &	result,
		DdAutStateManager &	targetStateManager,
		DdAutEventManager &	targetEventManager
	)

AutFsm insertion

Parameters

a	range of AutFsm
output	the AutFsm where all the AutFsm of the range have been inserted

Returns: true if success This is used by the program dd-insert, it ensures it is a compatible AutFsm as it merges the initial states. Be aware that the state encoding might not be

Definition at line 493 of file DdAutFile.hh.

References insertDdAutFA().

Referenced by insertDdAuts().

◆ insertRangeOfTransitions()

template<typename TransInserterIterator >

void Diades::Automata::Experimental::insertRangeOfTransitions	(	TransInserterIterator	begin,
		TransInserterIterator	end
	)

Raw Insertion of a range of Finite State Machines into a single FiniteStateMachine

Parameters

fsms	range of Finite State Machines to insert
eventInserters	range of EventInserters associated to the range of Fsms The EventInserter of a given position in the range is associated with the Fsm of the same position in the fsm range. Each EventInserter is built with its source Fsm in the corresponding Fsm range and with its target being the Fsm result.
stateInserters	range of StateInserters associated to the range of Fsms The StateInserter of a given position in the range is associated with the Fsm of the same position in the fsm range.
result	the Fsm that will contain the result of the insertion of the range of fsms.

Definition at line 71 of file Union.hh.

References insertTransitions().

Referenced by insertAutFsms().

◆ insertTransitions()

template<typename TransInserter >

void Diades::Automata::Experimental::insertTransitions ( TransInserter & inserter )

Main procedure for the insertion of a StateMachine into another one

Parameters

inserter a TransitionInserter, any Transition from inserter.source() are inserted into inserter.target()

Postcondition: raw insertion

Definition at line 36 of file Union.hh.

Referenced by insertRangeOfTransitions().

◆ isComplete()

template<typename Fsm >

bool Diades::Automata::Experimental::isComplete ( const Fsm & machine )

Parameters

machine a StateMachine

Returns: true if the machine is complete i.e. any EventPropertyId is involved in at least one output transition of every state of the StateMachine

Definition at line 36 of file Complete.hh.

Referenced by nerodePartition().

◆ isDeterministic()

template<typename Fsm >

bool Diades::Automata::Experimental::isDeterministic ( const Fsm & machine )

Parameters

machine a StateMachine

Returns: true if the machine is deterministic, i.e. all the output transitions from a given state have a different EventPropertyId

Definition at line 35 of file Determine.hh.

Referenced by minimize(), minimizeAut(), and minimizeDdaut().

◆ isNotChoiceState()

template<typename _SPId , typename _ISId , typename _NSPId = NullValue<_SPId>, typename _NISId = NullValue< _ISId>>

bool Diades::Automata::Experimental::isNotChoiceState	(	const FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId > &	fsa,
		typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State	state,
		const LocStateMap &	levels
	)

return true if the state is definitely considered as a no-choice state

a state is considered as a no-choice state iff every successor of the state has the same (initialized) level of choice (such successor must exist)

Parameters

fsa	the FiniteAutomaton where the state is
state	the state to investigate
levels	the current assigned levels (-1 if not assigned)

Returns: true if the state is definitely considered as a no-choice state

Definition at line 47 of file Explanation.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::getStatePropertyId(), LP, Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::outputTransitionBegin(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::outputTransitionEnd().

Referenced by setLevel().

◆ levelOfChoice()

template<typename _SPId , typename _ISId , typename _NSPId = NullValue<_SPId>, typename _NISId = NullValue< _ISId>>

bool Diades::Automata::Experimental::levelOfChoice	(	const FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId > &	fsa,
		LocStateMap &	result
	)

Definition at line 209 of file Explanation.hh.

References LP, setLevel(), and states.

Referenced by explain(), and explainFromStates().

◆ listSingleItem()

std::string Diades::Automata::Experimental::listSingleItem ( const std::string & item )

Referenced by writeTreeView(), writeTreeViewSafeAlternative(), and writeTreeViewTransition().

◆ minimize()

template<typename Fsm , typename StateCreator >

void Diades::Automata::Experimental::minimize	(	const Fsm &	machine,
		Fsm &	minimalMachine,
		StateCreator &	creator
	)

Parameters

machine	The original StateMachine
minimalMachine	The minimal version of the original StateMachine

Precondition: minimalMachine must not be the original machine; Note that if the StateMachine does not have any initial state, it is considered as if the original StateMachine is empty. A StateMachine that has no 'specific' initial states is a StateMachine such any state can be initial, in this case machine.setAllInitialStates() must be applied first.; machine must be deterministic (no check here)

Postcondition: A minimal StateMachine, if not empty, has one initial state only.

Parameters

machine	The original StateMachine
minimalMachine	The minimal version of the original StateMachine

Precondition: minimalMachine must not be the original machine; Note that if the StateMachine does not have any initial state, it is considered as if the original StateMachine is empty. A StateMachine that has no 'specific' initial states is a StateMachine such any state can be initial, in this case machine.setAllInitialStates() must be applied first.

Postcondition: A minimal StateMachine, if not empty, has one initial state only.

Parameters

machine	The original StateMachine
minimalMachine	The minimal version of the original StateMachine
minimalStateManager	StateInfoManger of the resulting machine
disjunction	Definition of the way the minimal machine will hold the disjunction states from the original machine.

Precondition: minimalMachine must not be the original machine; the machine must be deterministic (in particular one and only one initial state)

Postcondition: A minimal StateMachine, if not empty, has one initial state only.

Definition at line 336 of file Minimize.hh.

References isDeterministic(), and minimizeDeterministicMachine().

Referenced by minimizeAut(), and minimizeDdaut().

◆ minimizeDeterministicMachine()

template<typename Fsm , typename StateCreator >

void Diades::Automata::Experimental::minimizeDeterministicMachine	(	const Fsm &	machine,
		Fsm &	minimalMachine,
		StateCreator &	creator
	)

Parameters

machine	The original deterministic StateMachine
minimalMachine	The minimal version of the original StateMachine
minimalStateManager	StateInfoManger of the resulting machine
disjunction	Definition of the way the minimal machine will hold the disjunction states from the original machine.

Precondition: minimalMachine must not be the original machine; Note that if the StateMachine does not have any initial state, it is considered as if the original StateMachine is empty. A StateMachine that has no 'specific' initial states is a StateMachine such any state can be initial, in this case machine.setAllInitialStates() must be applied first.

Postcondition: A minimal StateMachine, if not empty, has one initial state only.

Definition at line 225 of file Minimize.hh.

References nerodePartition().

Referenced by minimize().

◆ nerodePartition()

template<typename Fsm >

void Diades::Automata::Experimental::nerodePartition	(	const Fsm &	machine,
		vector< std::shared_ptr< BeliefState< Fsm >>> &	partition
	)

Nerode partition (for minimization)

Parameters

partition will contain the nerode partition of the StateMachine (required for the minimization of the StateMachine) The Nerode partition is the partition of states such that for any Q0 Q1 there is no pair of state q0 and q'0 from Q0 such that q0 - a -> q1 is a transition of 'machine' and q1 is in Q1 while q'0 - a -> q'1 is a transition of 'machine' and q'1 is NOT in Q1 Be aware that to compute the partition, it is sometimes necessary to introduce a sink state. It is implicitely represented as an empty belief state that is pushed the first in the given partition (usually as partition is called as an empty vector which means that this empty belief state, if it exists, is at index 0). For performance issues, this empty belief state is not removed.

Definition at line 114 of file Minimize.hh.

References isComplete(), and splitPartition().

Referenced by minimizeDeterministicMachine().

◆ nextNoWhiteSpaceCharacter()

std::streampos Diades::Automata::Experimental::nextNoWhiteSpaceCharacter	(	std::istream &	stream,
		bool &	ok
	)

return the stream position just before the first character that is a white space (not such that std::isspace is true)

reads the stream till it founds a character c such that std::isspace(c) is false.

Parameters

stream	the analyzed stream
ok	the updated state of the stream (not good if no such a character has not been found)

Returns: return the current stream position that is the one of the first nonwhitespace character

◆ operator<<()

template<typename StateProperty , typename FaultProperty >

ostream& Diades::Automata::Experimental::operator<<	(	ostream &	os,
		const LocalCandidate< StateProperty, FaultProperty > &	candidate
	)

operator << of a LocalCandidate<StateProperty,FaultProperty>

Parameters

os	the output stream
candidate	a LocalCandidate<StateProperty,FaultProperty>

Returns: a stream where candidate.state() is printed followed by a space and candidate.faults() (so it is only ids, NOT the associated pieces of information)

Definition at line 134 of file LocalCandidate.hh.

◆ project() [1/8]

template<typename Fsm , typename IsGoal >

bool Diades::Automata::Experimental::project	(	const Fsm &	machine,
		Fsm &	abstractMachine,
		IsGoal	isGoal,
		BsMap< Fsm > &	bsMap,
		CstStMap< typename Fsm::State > &	stMap
	)

Parameters

machine	a StateMachine
abstractMachine	the resulting abstracted StateMachine
isGoal	transition Predicate
bsMap	resulting mapping that associates a State from abstractMachine to the set of abstracted states in the initial machine
stMap	resulting mapping that associates a State of the initial machine to the state in the abstractMachine. Only initial states or states from the initial machine that are targets of a projected transition have an association. Any other states of the initial StateMachine are associated with an invalid state (as they may actually belong to several belief states of the abstracted machine).

Returns: true if the projection is a success. If not the state of the abstractedMachine is undetermined.

Precondition: machine should not be abstractedMachine. machine must have at least one initial state; isGoal is a transition Predicate over the set of transitions in machine

Postcondition: the abstractMachine only contains transitions such that the predicate is true.

Definition at line 426 of file Project.hh.

References Diades::Automata::Experimental::Projection::projectRange().

Referenced by explainFromStates(), and project().

◆ project() [2/8]

template<typename Fsm , typename IsGoal >

bool Diades::Automata::Experimental::project	(	const Fsm &	machine,
		Fsm &	abstractMachine,
		IsGoal	isGoal
	)

Parameters

machine	a StateMachine
abstractMachine	the resulting abstracted StateMachine
isGoal	transition Predicate

Returns: true if the projection is a success. If not the state of the abstractedMachine is undetermined.

Precondition: machine should not be abstractedMachine. machine must have at least one initial state; isGoal is a transition Predicate over the set of transitions in machine

Postcondition: the abstractMachine only contains transitions such that the predicate is true.

Definition at line 458 of file Project.hh.

References project().

◆ project() [3/8]

template<typename Fsm , typename EventPropertyIdIterator >

bool Diades::Automata::Experimental::project	(	const Fsm &	machine,
		Fsm &	abstractMachine,
		EventPropertyIdIterator	begin,
		EventPropertyIdIterator	end,
		BsMap< Fsm > &	bsMap,
		CstStMap< typename Fsm::State > &	stMap
	)

Parameters

machine	a StateMachine
abstractMachine	the resulting abstracted StateMachine
begin	the start iterator of a range of EventInfoId to project
end	the end iterator of a range of EventInfoId to project
bsMap	resulting mapping that associates a State from abstractMachine to the set of abstracted states in the initial machine
stMap	resulting mapping that associates a State of the initial machine to the state in the abstractMachine. Only initial states or states from the initial machine that are targets of a projected transition have an association. Any other states of the initial StateMachine are associated with an invalid state (as they may actually belong to several belief states of the abstracted machine).

Returns: true if the projection is a success. If not the state of the abstractedMachine is undetermined.

Precondition: machine should not be abstractedMachine. machine must have at least one initial state; [begin,end) represents a set of EventInfoId of the StateMachine

Postcondition: the abstractMachine only contains events from [begin,end)

Definition at line 492 of file Project.hh.

References Diades::Automata::Experimental::Projection::projectRange().

◆ project() [4/8]

template<typename Fsm , typename EventPropertyIdIterator >

bool Diades::Automata::Experimental::project	(	const Fsm &	machine,
		Fsm &	abstractMachine,
		EventPropertyIdIterator	begin,
		EventPropertyIdIterator	end
	)

Parameters

machine	a StateMachine
abstractMachine	the resulting abstracted StateMachine
begin	the start iterator of a range of EventInfoId to project
end	the end iterator of a range of EventInfoId to project

Returns: true if the projection is a success. If not the state of the abstractedMachine is undetermined.

Precondition: machine should not be abstractedMachine. machine must have at least one initial state; [begin,end) represents a set of EventInfoId of the StateMachine

Postcondition: the abstractMachine only contains events from [begin,end)

Definition at line 532 of file Project.hh.

References project().

◆ project() [5/8]

template<typename Fsm , typename IsGoal , typename StateProperty , typename StateLabelProjection >

bool Diades::Automata::Experimental::project	(	const Fsm &	fsm,
		Fsm &	projectedFsm,
		const StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &	stateManager,
		StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &	projectionStateManager,
		const StateLabelProjection &	projection,
		IsGoal	isGoal,
		BsMap< Fsm > &	bsMap,
		CstStMap< typename Fsm::State > &	stMap
	)

Parameters

machine	a StateMachine
abstractMachine	the resulting abstracted StateMachine
isGoal	transition Predicate
bsMap	resulting mapping that associates a State from abstractMachine to the set of abstracted states in the initial machine
stMap	resulting mapping that associates a State of the initial machine to the state in the abstractMachine. Only initial states or states from the initial machine that are targets of a projected transition have an association. Any other states of the initial StateMachine are associated with an invalid state (as they may actually belong to several belief states of the abstracted machine).

Returns: true if the projection is a success. If not the state of the abstractedMachine is undetermined.

Precondition: machine should not be abstractedMachine. machine must have at least one initial state; isGoal is a transition Predicate over the set of transitions in machine

Postcondition: the abstractMachine only contains transitions such that the predicate is true.

Definition at line 567 of file Project.hh.

References Diades::Automata::Experimental::Projection::projectRange().

◆ project() [6/8]

template<typename Fsm , typename IsGoal , typename StateProperty , typename StateLabelProjection >

bool Diades::Automata::Experimental::project	(	const Fsm &	fsm,
		Fsm &	projectedFsm,
		const StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &	stateManager,
		StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &	projectionStateManager,
		const StateLabelProjection &	projection,
		IsGoal	isGoal
	)

Parameters

machine	a StateMachine
abstractMachine	the resulting abstracted StateMachine
isGoal	transition Predicate

Returns: true if the projection is a success. If not the state of the abstractedMachine is undetermined.

Precondition: machine should not be abstractedMachine. machine must have at least one initial state; isGoal is a transition Predicate over the set of transitions in machine

Postcondition: the abstractMachine only contains transitions such that the predicate is true.

Definition at line 601 of file Project.hh.

References project().

◆ project() [7/8]

template<typename Fsm , typename EventPropertyIdIterator , typename StateProperty , typename StateLabelProjection >

bool Diades::Automata::Experimental::project	(	const Fsm &	fsm,
		Fsm &	projectedFsm,
		const StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &	stateManager,
		StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &	projectionStateManager,
		const StateLabelProjection &	projection,
		EventPropertyIdIterator	begin,
		EventPropertyIdIterator	end,
		BsMap< Fsm > &	bsMap,
		CstStMap< typename Fsm::State > &	stMap
	)

Parameters

machine	a StateMachine
abstractMachine	the resulting abstracted StateMachine
begin	the start iterator of a range of EventInfoId to project
end	the end iterator of a range of EventInfoId to project
bsMap	resulting mapping that associates a State from abstractMachine to the set of abstracted states in the initial machine
stMap	resulting mapping that associates a State of the initial machine to the state in the abstractMachine. Only initial states or states from the initial machine that are targets of a projected transition have an association. Any other states of the initial StateMachine are associated with an invalid state (as they may actually belong to several belief states of the abstracted machine).

Returns: true if the projection is a success. If not the state of the abstractedMachine is undetermined.

Precondition: machine should not be abstractedMachine. machine must have at least one initial state; [begin,end) represents a set of EventInfoId of the StateMachine

Postcondition: the abstractMachine only contains events from [begin,end)

Definition at line 643 of file Project.hh.

References Diades::Automata::Experimental::Projection::projectRange().

◆ project() [8/8]

template<typename Fsm , typename EventPropertyIdIterator , typename StateProperty , typename StateLabelProjection >

bool Diades::Automata::Experimental::project	(	const Fsm &	fsm,
		Fsm &	projectedFsm,
		const StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &	stateManager,
		StatePropertyManager< StateProperty, typename Fsm::StatePropertyId > &	projectionStateManager,
		const StateLabelProjection &	projection,
		EventPropertyIdIterator	begin,
		EventPropertyIdIterator	end
	)

Parameters

machine	a StateMachine
abstractMachine	the resulting abstracted StateMachine
begin	the start iterator of a range of EventInfoId to project
end	the end iterator of a range of EventInfoId to project

Returns: true if the projection is a success. If not the state of the abstractedMachine is undetermined.

Precondition: machine should not be abstractedMachine. machine must have at least one initial state; [begin,end) represents a set of EventInfoId of the StateMachine

Postcondition: the abstractMachine only contains events from [begin,end)

Definition at line 685 of file Project.hh.

References project().

◆ pruneComments()

bool Diades::Automata::Experimental::pruneComments	(	std::istream &	stream,
		bool &	ok
	)

read the stream and ignore the next c-style/cpp style comments

The input stream may start with a set of c-style/cpp style comments pruneComments will read them and ignore them. pruneComments will set the current cursor so that the next character to read is the first character that does not belong to any c-style/cpp style comments.

Parameters

stream	the input stream to analyze
ok	status of the stream (good or not good)

Returns: true if at least one comment has been detected and ignored.

◆ pruneCommentsBlock()

bool Diades::Automata::Experimental::pruneCommentsBlock	(	std::istream &	stream,
		bool &	ok
	)

analyze the stream and look for the end of a comment block

here we suppose that the stream is in a c-style comment block and we simply look for the end of the comment block. The stream is updated so that the next character to read is the one after the comment block

Parameters

stream	the stream to analyze
ok	is true if the stream is good

Returns: return true if the end of the comment block is found

◆ rulesToDescriptor()

template<typename DdAutFsmType >

bool Diades::Automata::Experimental::rulesToDescriptor	(	const SynchronisationRules< DdAutFsmType > &	rules,
		DdSyncDescriptor &	desc
	)

Parameters

rules	a set of synchronisation rules
desc	the initialised descriptor

Returns: true if the export into the descriptor is a success

Definition at line 426 of file DdSyncDescriptor.hh.

References Diades::Automata::Experimental::SynchronisationRules< StateMachine >::beginOfSynchronisedEvents(), Diades::Automata::Experimental::SynchronisationRules< StateMachine >::endOfSynchronisedEvents(), Diades::Automata::Experimental::DdSyncDescriptor::Synchronisation::insertSynchronisation(), and Diades::Automata::Experimental::DdSyncDescriptor::insertSynchronisation().

◆ setLevel()

template<typename _SPId , typename _ISId , typename _NSPId = NullValue<_SPId>, typename _NISId = NullValue< _ISId>>

bool Diades::Automata::Experimental::setLevel	(	const FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId > &	fsa,
		std::list< typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State > &	states,
		int	currentLevel,
		LocStateMap &	levels
	)

Definition at line 132 of file Explanation.hh.

References isNotChoiceState(), LP, setLevelStateAndPropagate(), and states.

Referenced by levelOfChoice().

◆ setLevelStateAndPropagate()

template<typename _SPId , typename _ISId , typename _NSPId = NullValue<_SPId>, typename _NISId = NullValue< _ISId>>

void Diades::Automata::Experimental::setLevelStateAndPropagate	(	const FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId > &	fsa,
		std::list< typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State > &	states,
		int	currentLevel,
		LocStateMap &	levels,
		typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State	state,
		std::unordered_set< typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State > &	tagged,
		std::unordered_set< typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State > &	visited
	)

set the level of the current state and insert its untagged predecessors in the list 'states' update the tagged and visited data structure if the state is not an initial state

this function is intermediate and is only used in setLevel only the current state is tagged any of its predecessors is then considered as visited

Parameters

fsa	the FiniteAutomaton where the state is
states	any non-visited predecessors of the current state will be inserted at the end of 'states'
currentLevel	the level to assign to the current state
levels	the level mapping that stores the level for each state
state	the current state to tag
tagged	the current set of tagged states that is updated with the current state
visited	the current set of visited states that is updated with the inserted predecessors

Returns: return type

Definition at line 96 of file Explanation.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::getStatePropertyId(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::inputTransitionBegin(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::inputTransitionEnd(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::isInitial(), LP, and states.

Referenced by setLevel().

◆ splitPartition()

template<typename Fsm >

bool Diades::Automata::Experimental::splitPartition	(	const Fsm &	machine,
		const std::shared_ptr< BeliefState< Fsm >>	bigQ0,
		const std::shared_ptr< BeliefState< Fsm >>	bigQ1,
		typename Fsm::EventPropertyId	littleA,
		std::shared_ptr< BeliefState< Fsm >>	bigQ0prime,
		std::shared_ptr< BeliefState< Fsm >>	bigQ0MinusbigQ0prime
	)

Split two partition elements according to the splittable property (minimization)

Parameters

bigQO	a BeliefState
bigQ1	a BeliefState
littleA	an Event
bigQ0prime	a BeliefState result of the split
bigQ0MinusbigQ0prime	a BeliefState result of the split

Returns: splittable(bigQO,bigQ1,littleA)

Does the split as follows. 1) If the states of Q0 always have an output transition labelled with a that goes to a state of Q1 then Q0 is not splittable and bigQ0prime bigQ0MinusbigQ0prime are empty belief states, returns false 2) If the states of Q0 always have an output transition labelled with a that goes to a state NOT in Q1 then Q0 is not splittable and bigQ0prime bigQ0MinusbigQ0prime are empty belief states 3) Otherwise it is splittable and bigQ0prime contains the states of Q0 that satify case 1 and bigQ0MinusbigQ0prime are the one that satisfies case 2

Note that bigQ1 may be equal to an empty belief state means that Q1 = {sink_state}. The sink_state is not explicitly represented in the StateMachine

Definition at line 50 of file Minimize.hh.

Referenced by nerodePartition().

◆ startListCaretItem()

std::string Diades::Automata::Experimental::startListCaretItem ( const std::string & item )

Referenced by writeTreeView(), and writeTreeViewTransition().

◆ startNestedTree()

std::string Diades::Automata::Experimental::startNestedTree ( )

Referenced by writeTreeView(), and writeTreeViewTransition().

◆ startTree()

std::string Diades::Automata::Experimental::startTree ( const std::string & treeId )

Referenced by writeTreeView().

◆ synchronize()

template<typename Fsm , typename StateCreator >

bool Diades::Automata::Experimental::synchronize	(	const std::vector< typename Ptr< Fsm >::ConstP > &	components,
		const SynchronisationRules< Fsm > &	rules,
		Fsm &	synchronisation,
		StateCreator &	creator
	)

Parameters

machine	The original StateMachine
minimalMachine	The minimal version of the original StateMachine
minimalStateManager	StateInfoManger of the resulting machine
disjunction	Definition of the way the minimal machine will hold the disjunction states from the original machine.

Precondition: minimalMachine must not be the original machine; the machine must be deterministic (in particular one and only one initial state)

Postcondition: A minimal StateMachine, if not empty, has one initial state only.

Definition at line 36 of file Synchronize.hh.

Referenced by Diades::Petri::Net::isPostponable(), and synchroniseDdAut().

◆ toAutFile()

bool Diades::Automata::Experimental::toAutFile	(	ostream &	stream,
		const AutFsm &	fsm,
		bool	enforce = `false`
	)

To AutFile

Parameters

stream	the updated output stream
fsm	the Fsm to export
enforce	(encoding of the states in aut file format if needed)

Returns: true if the export is a success.

The export is not a success if there is more than one initial state The initial state holds the information 0 If the information hold by the states is not from 0 to numberOfStates()-1 it is not a success. If enforce is set to true and the state encoding is not compatible then create a new compatible state encoding

Referenced by autFileStateReencoding(), and Diades::CmdInterface::writeAut().

◆ toDot() [1/4]

template<typename StateMachine , typename PrintStateProperty , typename PrintEventInfo >

ostream& Diades::Automata::Experimental::toDot	(	ostream &	os,
		const StateMachine &	fsm,
		const PrintStateProperty &	statePrinter,
		const PrintEventInfo &	eventPrinter
	)

Export in the output stream os a 'dot format' description of a StateMachine

Parameters

os	the output stream
fsm	the StateMachine
statePrinter	a Printer for StateProperty of type PrintStateProperty
eventPrinter	a Printer for EventInfo of type PrintEventInfo

Returns: the updated output stream

Definition at line 267 of file Io.hh.

References toDotEnding(), toDotHeader(), toDotInitialStates(), toDotStates(), and toDotTransitions().

Referenced by exportAutToDot(), exportDdAutToDot(), exportDdSyncToDot(), main(), toDot(), and Diades::Automata::Experimental::LocalCandidateMachine::toDotPretty().

◆ toDot() [2/4]

template<typename StateMachine >

ostream& Diades::Automata::Experimental::toDot	(	ostream &	os,
		const StateMachine &	fsm
	)

Export in the output stream as a 'dot format' description of a StateMachine without the StateProperty/EventInfo data

Parameters

os	the output stream
fsm	the StateMachine<StateProperty,EventInfo>

Returns: the updated output stream

Definition at line 290 of file Io.hh.

References toDotEnding(), toDotHeader(), toDotInitialStates(), toDotStates(), and toDotTransitions().

◆ toDot() [3/4]

template<typename StateMachine >

bool Diades::Automata::Experimental::toDot	(	const std::string &	filename,
		const StateMachine &	fsm
	)

Export in the 'dot format' description of a StateMachine without the StateProperty/EventInfo data

Parameters

filename	the output filename
fsm	the StateMachine<StateProperty,EventInfo>

Returns: the updated output stream

Definition at line 310 of file Io.hh.

References toDot().

◆ toDot() [4/4]

template<>

ostream& Diades::Automata::Experimental::toDot	(	ostream &	os,
		const DdSyncDescriptor &	descriptor
	)

inline

Parameters

os	the output stream
descriptor	a synchronisation rule descriptor

Returns: the updated output stream

Definition at line 337 of file Io.hh.

References Diades::Automata::Experimental::DdSyncDescriptor::toDot().

◆ toDotEnding()

ostream& Diades::Automata::Experimental::toDotEnding ( ostream & os )

inline

Definition at line 160 of file Io.hh.

Referenced by toDot().

◆ toDotHeader() [1/2]

ostream& Diades::Automata::Experimental::toDotHeader ( ostream & os )

inline

export in the output stream the header of a dot file

Parameters

os	the output stream

Returns: the updated output stream

Definition at line 31 of file Io.hh.

Referenced by toDot(), and toDotHeader().

◆ toDotHeader() [2/2]

template<typename StateMachine >

ostream& Diades::Automata::Experimental::toDotHeader	(	const StateMachine &	fsm,
		ostream &	os
	)

export in the output stream the header of a dot file for a StateMachine

Parameters

os	the output stream

Returns: the updated output stream

Definition at line 49 of file Io.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::name(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::numberOfStates(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::numberOfTransitions(), and toDotHeader().

◆ toDotInitialStates()

template<typename StateMachine >

ostream& Diades::Automata::Experimental::toDotInitialStates	(	const StateMachine &	fsm,
		ostream &	os
	)

export in the output stream the initial states of a StateMachine

Parameters

os	the output stream

Returns: the updated output stream

Definition at line 65 of file Io.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::initialStateBegin(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::initialStateEnd().

Referenced by toDot().

◆ toDotStates() [1/4]

template<typename StateMachine , typename PrintStateProperty >

ostream& Diades::Automata::Experimental::toDotStates	(	const StateMachine &	fsm,
		const PrintStateProperty &	statePrinter,
		ostream &	os
	)

Definition at line 83 of file Io.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::getStatePropertyId(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::stateBegin(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::stateEnd().

Referenced by toDot().

◆ toDotStates() [2/4]

template<typename S , typename I , typename NS , typename NI , typename PrintStateProperty >

ostream& Diades::Automata::Experimental::toDotStates	(	const FiniteAutomaton< S, I, NS, NI > &	fsm,
		const PrintStateProperty &	statePrinter,
		ostream &	os
	)

Definition at line 96 of file Io.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::getStatePropertyId(), Diades::Automata::Experimental::FiniteAutomaton< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::isAcceptingState(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::stateBegin(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::stateEnd().

◆ toDotStates() [3/4]

template<typename StateMachine >

ostream& Diades::Automata::Experimental::toDotStates	(	const StateMachine &	fsm,
		ostream &	os
	)

Definition at line 120 of file Io.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::getStatePropertyId(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::stateBegin(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::stateEnd().

◆ toDotStates() [4/4]

template<typename S , typename I , typename NS , typename NI >

ostream& Diades::Automata::Experimental::toDotStates	(	const FiniteAutomaton< S, I, NS, NI > &	fa,
		ostream &	os
	)

Definition at line 136 of file Io.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::getStatePropertyId(), Diades::Automata::Experimental::FiniteAutomaton< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::isAcceptingState(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::stateBegin(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::stateEnd().

◆ toDotTransitions() [1/4]

template<typename StateMachine , typename PrintEventInfo >

ostream& Diades::Automata::Experimental::toDotTransitions	(	const StateMachine &	fsm,
		const PrintEventInfo &	eventPrinter,
		ostream &	os
	)

Definition at line 170 of file Io.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::getEvent(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::transitionBegin(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::transitionEnd().

Referenced by toDot().

◆ toDotTransitions() [2/4]

template<typename StateProperty , typename EventInfo , typename PrintEventInfo >

ostream& Diades::Automata::Experimental::toDotTransitions	(	const FaultyEventStateMachine< StateProperty, EventInfo > &	fsm,
		const PrintEventInfo &	eventPrinter,
		ostream &	os
	)

Definition at line 187 of file Io.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::getEvent(), Diades::Automata::Experimental::FaultyEventStateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::isFaulty(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::transitionBegin(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::transitionEnd().

◆ toDotTransitions() [3/4]

template<typename StateMachine >

ostream& Diades::Automata::Experimental::toDotTransitions	(	const StateMachine &	fsm,
		ostream &	os
	)

Definition at line 213 of file Io.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::getEvent(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::transitionBegin(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::transitionEnd().

◆ toDotTransitions() [4/4]

template<typename StateProperty , typename EventInfo >

ostream& Diades::Automata::Experimental::toDotTransitions	(	const FaultyEventStateMachine< StateProperty, EventInfo > &	fsm,
		ostream &	os
	)

Definition at line 231 of file Io.hh.

References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::getEvent(), Diades::Automata::Experimental::FaultyEventStateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::isFaulty(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::transitionBegin(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::transitionEnd().

◆ toTreeViewHtmlEnd()

std::ostream& Diades::Automata::Experimental::toTreeViewHtmlEnd ( std::ostream & os )

Referenced by writeTreeView().

◆ toTreeViewHtmlStart()

std::ostream& Diades::Automata::Experimental::toTreeViewHtmlStart ( std::ostream & os )

Referenced by writeTreeView().

◆ transformToCandidateStateMachine()

void Diades::Automata::Experimental::transformToCandidateStateMachine	(	const Component &	component,
		Lcm::EvManager &	manager,
		Lcm::EvSetManager &	setManager,
		Lcm::LocalStateInfoManager &	locStateInfoManager,
		Lcm::CandidateManager &	candidateManager,
		Lcm::Fsm &	result
	)

Convert a Component to a StateMachine where each state holds a diagnosis information

Parameters

component	the Component to convert
manager	the EventManager that will contain the events of the Component (the events are added into the EventManager)
setManager	the LocalEventSetManager in charge in computing the EventSets of the LocalCandidate and ONLY (initialised within the function)
locSTateInfoManager	state info manager in charge of computing the information associated with a State of a Component to inject into a Candidate
candidateManager	state info manager in charge of storing the information associated with a State of a Lcm
result	the StateMachine resulting from the transformation

Referenced by runGlobalDiagnosisProblem().

◆ trimmingDeadlockStates() [1/2]

template<typename Fsm , typename BeliefStateIterator , typename StateIdInsertIterator >

bool Diades::Automata::Experimental::trimmingDeadlockStates	(	Fsm &	machine,
		BeliefStateIterator	bfBegin,
		BeliefStateIterator	bfEnd,
		StateIdInsertIterator	insertIt
	)

Trim the states are the source of a deadlock within a range of states.

This function removes every state that only leads to deadlock within a range of states (and consequently their predecessors) The StatePropertyId that are deleted are stored via an insertIterator. Be aware that this function can make the machine empty.

Parameters

machine	The Fms that is updated
bfBegin	the iterator on the first state of the BeliefState
bfEnd	the past-the-end iterator of the BeliefState
insertIt	an insert iterator in charge of keeping the StatePropertyId of the states that are removed.

Returns: true if the machine is still valid (i.e. not empty with some initial states).

Definition at line 164 of file Trimming.hh.

Referenced by trimmingDeadlockStates().

◆ trimmingDeadlockStates() [2/2]

template<typename Fsm , typename StateIdInsertIterator >

bool Diades::Automata::Experimental::trimmingDeadlockStates	(	Fsm &	machine,
		StateIdInsertIterator	insertIt
	)

Trim the states are the source of a deadlock.

This function removes every state that only leads to deadlock. The StatePropertyId that are deleted are stored via an insertIterator. Be aware that this function can make the machine empty.

Parameters

machine	The Fsm that is updated
insertIt	an insert iterator in charge of keeping the StatePropertyId of the states that are removed.

Returns: true if the machine is still valid (i.e. not empty with some initial states).

Definition at line 224 of file Trimming.hh.

References trimmingDeadlockStates().

◆ trimmingTraces()

template<typename Fsm , typename BeliefStateIterator , typename StateIdInsertIterator >

void Diades::Automata::Experimental::trimmingTraces	(	Fsm &	machine,
		BeliefStateIterator	bfBegin,
		BeliefStateIterator	bfEnd,
		StateIdInsertIterator	insertIt
	)

Trim the traces of the Fsm that does not reach the given BeliefState.

This function considers that the given Fsm only contains states that are reachable from at least one initial state. It removes every state that does not belong to a trace that finally reaches a state of the belief State.

Parameters

machine	The Fms that is updated
bfBegin	the iterator on the first state of the BeliefState
bfEnd	the past-the-end iterator of the BeliefState
insertIt	an insert iterator in charge of keeping the StatePropertyId of the states that are removed.

Definition at line 44 of file Trimming.hh.

References deleteState().

◆ trimmingUnreachableStates() [1/2]

template<typename Fsm , typename BeliefStateIterator , typename StateIdInsertIterator >

void Diades::Automata::Experimental::trimmingUnreachableStates	(	Fsm &	machine,
		BeliefStateIterator	bfBegin,
		BeliefStateIterator	bfEnd,
		StateIdInsertIterator	insertIt
	)

Trim the states that cannot be reached from the given BeliefState.

This function removes every state that cannot be reached by at least one state of the given Belief State. The StatePropertyId that are deleted are stored via an insertIterator

Parameters

machine	The Fms that is updated
bfBegin	the iterator on the first state of the BeliefState
bfEnd	the past-the-end iterator of the BeliefState
insertIt	an insert iterator in charge of keeping the StatePropertyId of the states that are removed.

Definition at line 93 of file Trimming.hh.

References deleteState().

Referenced by trimmingUnreachableStates().

◆ trimmingUnreachableStates() [2/2]

template<typename Fsm , typename StateIdInsertIterator >

void Diades::Automata::Experimental::trimmingUnreachableStates	(	Fsm &	machine,
		StateIdInsertIterator	insertIt
	)

Trim the states that cannot be reached from the initial states.

This function removes every state that cannot be reached from at least one initial state. The StatePropertyId that are deleted are stored via an insertIterator

Parameters

machine	The Fms that is updated
insertIt	an insert iterator in charge of keeping the StatePropertyId of the states that are removed.

Definition at line 140 of file Trimming.hh.

References trimmingUnreachableStates().

◆ tsExtractTargetState()

void Diades::Automata::Experimental::tsExtractTargetState	(	const std::string &	rawTargetState,
		std::string &	targetState,
		std::string::size_type &	semiColonIndex
	)

extract the target state for the raw target state

raw target state may be something like the_state; or the_state simply get the_state and set the position index of ';' if found

Parameters

rawTargetState	the raw Target State something like the_state; or the_state
targetState	the extracted state (i.e the_state)
semiColonIndex	the position index of ';' if found

◆ tsFileHeader()

std::istream& Diades::Automata::Experimental::tsFileHeader	(	std::istream &	stream,
		std::string &	tsName,
		bool &	ok
	)

parse the Ts-format file header

parse something like ' <comments> transition_system name;'

Parameters

stream	input stream to be parsed
tsName	the assigned name of the transition system found in the stream
ok	the current status of the stream (if not ok, it means the stream has the wrong format)

Returns: the analyzed stream

◆ tsFileStates()

std::istream& Diades::Automata::Experimental::tsFileStates	(	std::istream &	stream,
		ManagedTsFsms &	fsms,
		bool &	ok
	)

◆ tsFileTransitionLabel()

std::istream& Diades::Automata::Experimental::tsFileTransitionLabel	(	std::istream &	stream,
		std::unordered_map< std::string, std::string > &	events,
		std::string &	fullEventLabel,
		bool &	ok
	)

Read the transition label in a ts-format file.

In a Ts-format file a transition label is as follows 'label->' or '<evt, comp1.v1=val1, ..., compn.vn=valn>->' We extract the label and stores as label or <evt,comp1.v1=val1,...,compn.vn=valn> (i.e. skiped whitespaces)

Parameters

stream	the analyzed input stream (expecting something like 'label->' or '<evt, comp1.v1=val1, ..., compn.vn=valn>->')
eventLabel	the extracted label (i.e. label or <evt,comp1.v1=val1,...,compn.vn=valn>)
ok	true if the extraction is successful

Returns: the update input stream positioned after 'label->' or '<evt, comp1.v1=val1, ..., compn.vn=valn>->'

◆ tsFileTransitions()

std::istream& Diades::Automata::Experimental::tsFileTransitions	(	std::istream &	stream,
		ManagedTsFsms &	fsms,
		bool &	ok,
		TsConversionMode	mode
	)

Read the transitions of a Ts-format stream.

The format is as follows: state1 |- '<event1>'-> state2; |- '<event2>'-> state3; state4 |- '<event3>'-> state5; ...

Parameters

stream	the input stream to read
fsm	the Fsm where the transitions are inserted
sManager	the state manager where the state identifiers are inserted
eManager	the event manager where the event are inserted
ok	the status of the stream

Returns: the stream positionned to the first non-isspace character after the set of transitions

◆ tsPrettyEvent()

std::string Diades::Automata::Experimental::tsPrettyEvent ( const std::string & tsEvent )

Referenced by exportTsToDdAut2().

Namespaces

Classes

Typedefs

Enumerations

Functions

Typedef Documentation

◆ AutEventId

◆ AutFsm

◆ AutFsmEventInserter

◆ AutFsmStateIdGenerator

◆ AutFsmStateInserter

◆ AutFsmTransitionInserter

◆ AutStateId

◆ BsMap

◆ BsPtr

◆ CstBsMap

◆ CstStMap

◆ CstTrMap

◆ DdAutAmpersand

◆ DdAutBraces

◆ DdAutComma

◆ DdAutConjunction

◆ DdAutDisjunction

◆ DdAutEventId

◆ DdAutEventLabel

◆ DdAutEventManager

◆ DdAutEventPrinter

◆ DdAutFA

◆ DdAutFsm

◆ DdAutParentheses

◆ DdAutProjection

◆ DdAutStateId

◆ DdAutStateLabel

◆ DdAutStateManager

◆ DdAutStatePrinter

◆ DdAutSynchronisation

◆ ExplLocStateMap

◆ LocStateMap

◆ ManagedTsFsm

◆ ManagedTsFsms

◆ Matcher

◆ Observables

◆ Observation

◆ Observations

◆ SafeAlt

◆ StatePropertyAsStringLabel

◆ StatePropertyAsUnsigned

◆ StatePropertyIdAsSizeT

◆ StMap

◆ TrMap

◆ TsEvtMgr

◆ TsEvtMgrPtr

◆ TsFsm

◆ TsFsmPtr

◆ TsStMgr

◆ TsStMgrPtr

Enumeration Type Documentation

◆ TsConversionMode

Function Documentation

◆ abstract() [1/2]

◆ abstract() [2/2]

◆ abstractEvents() [1/4]

◆ abstractEvents() [2/4]

◆ abstractEvents() [3/4]

◆ abstractEvents() [4/4]

◆ autFileStateEncoding()

◆ autFileStateReencoding()

◆ autFsmNeedEncoding()

◆ checkSystemIdentifier()

◆ complete()

◆ controlledTrimmingDeadlockState()

◆ deleteState() [1/5]

◆ deleteState() [2/5]

◆ deleteState() [3/5]

◆ deleteState() [4/5]

◆ deleteState() [5/5]

◆ deleteTransition() [1/2]

◆ deleteTransition() [2/2]

◆ descriptorToRules()

◆ determine()