#include <EncodedInstance.hh>

Public Types
typedef Diades::Graph::Graph	Fsm

typedef Diades::Graph::Node	State

typedef Diades::Graph::Edge	Trans

typedef Diades::Graph::NodeMap< Formula >	StateFormulaMap

typedef Diades::Graph::NodeIterator	StateIterator

typedef Diades::Graph::EdgeIterator	TransIterator

typedef EncodedInstanceData::AssertionIterator	AssertionIterator

Public Member Functions
	EncodedInstance ()
	the Node associated to the EncodedInstance More...

	EncodedInstance (EncodedInstanceData *data)

	EncodedInstance (const EncodedInstance &instance)

EncodedInstance &	operator= (const EncodedInstance &instance)

Formula	getFormula (State state) const

Formula	getStateFormula (State state) const

Formula	getConfigurationFormula (State state) const

Node	nodeInstance () const

bool	valid () const

bool	operator== (const EncodedInstance &instance)

bool	operator!= (const EncodedInstance &instance)

bool	operator< (const EncodedInstance &instance)

State	initialState ()

const string &	logs () const

State	getState (Formula formula) const

StateIterator	stateBegin () const

StateIterator	stateEnd () const

TransIterator	transBegin () const

TransIterator	transEnd () const

void	getNextStates (State state, const Event &event, set< State > &successors)

const Event &	getEvent (Trans t) const

AssertionIterator	assertionBegin () const

AssertionIterator	assertionEnd () const

Private Attributes
EncodedInstanceData *	_data

Detailed Description

This class represents the result of a Node encoding into a constraint automaton

Definition at line 215 of file EncodedInstance.hh.

Member Typedef Documentation

◆ AssertionIterator

typedef EncodedInstanceData::AssertionIterator Diades::Altarica::EncodedInstance::AssertionIterator

Definition at line 224 of file EncodedInstance.hh.

◆ Fsm

typedef Diades::Graph::Graph Diades::Altarica::EncodedInstance::Fsm

Definition at line 218 of file EncodedInstance.hh.

◆ State

typedef Diades::Graph::Node Diades::Altarica::EncodedInstance::State

Definition at line 219 of file EncodedInstance.hh.

◆ StateFormulaMap

typedef Diades::Graph::NodeMap<Formula> Diades::Altarica::EncodedInstance::StateFormulaMap

Definition at line 221 of file EncodedInstance.hh.

◆ StateIterator

typedef Diades::Graph::NodeIterator Diades::Altarica::EncodedInstance::StateIterator

Definition at line 222 of file EncodedInstance.hh.

◆ Trans

typedef Diades::Graph::Edge Diades::Altarica::EncodedInstance::Trans

Definition at line 220 of file EncodedInstance.hh.

◆ TransIterator

typedef Diades::Graph::EdgeIterator Diades::Altarica::EncodedInstance::TransIterator

Definition at line 223 of file EncodedInstance.hh.

Constructor & Destructor Documentation

◆ EncodedInstance() [1/3]

Diades::Altarica::EncodedInstance::EncodedInstance ( )

inline

the Node associated to the EncodedInstance

Definition at line 230 of file EncodedInstance.hh.

◆ EncodedInstance() [2/3]

Diades::Altarica::EncodedInstance::EncodedInstance ( EncodedInstanceData * data )

inline

Definition at line 231 of file EncodedInstance.hh.

◆ EncodedInstance() [3/3]

Diades::Altarica::EncodedInstance::EncodedInstance ( const EncodedInstance & instance )

inline

Definition at line 232 of file EncodedInstance.hh.

Member Function Documentation

◆ assertionBegin()

AssertionIterator Diades::Altarica::EncodedInstance::assertionBegin ( ) const

inline

Returns: an iterator on the first assertion

Definition at line 429 of file EncodedInstance.hh.

References Diades::Altarica::EncodedInstanceData::assertionBegin().

◆ assertionEnd()

AssertionIterator Diades::Altarica::EncodedInstance::assertionEnd ( ) const

inline

Returns: an iterator on assertions (end)

Definition at line 436 of file EncodedInstance.hh.

References Diades::Altarica::EncodedInstanceData::assertionEnd(), Diades::Altarica::createEncodedNode(), Diades::Altarica::export2dot(), and Diades::Altarica::unfold().

◆ getConfigurationFormula()

Formula Diades::Altarica::EncodedInstance::getConfigurationFormula ( State state ) const

inline

Parameters

state a State

Returns: the configuration Formula associated the given State

Definition at line 275 of file EncodedInstance.hh.

References Diades::Altarica::EncodedInstanceData::getConfigurationFormula().

◆ getEvent()

const Event& Diades::Altarica::EncodedInstance::getEvent ( Trans t ) const

inline

Parameters

t	a transition

Returns: the event assoiated to the transition t

Definition at line 420 of file EncodedInstance.hh.

References Diades::Altarica::EncodedInstanceData::getEvent().

◆ getFormula()

Formula Diades::Altarica::EncodedInstance::getFormula ( State state ) const

inline

Parameters

state a State

Returns: the Formula associated the given State

Definition at line 247 of file EncodedInstance.hh.

References Diades::Altarica::EncodedInstanceData::getFormula().

◆ getNextStates()

void Diades::Altarica::EncodedInstance::getNextStates	(	State	state,
		const Event &	event,
		set< State > &	successors
	)

inline

Parameters

state	a State
event	an Event
the	resulting set of State resulting from the trigger of the Event event, empty set otherwise

Definition at line 410 of file EncodedInstance.hh.

References Diades::Altarica::EncodedInstanceData::getNextStates().

◆ getState()

State Diades::Altarica::EncodedInstance::getState ( Formula formula ) const

inline

Parameters

formula a Formula

Returns: the State associated the given Formula (linear in the number of states)

Definition at line 360 of file EncodedInstance.hh.

References Diades::Altarica::EncodedInstanceData::getState().

◆ getStateFormula()

Formula Diades::Altarica::EncodedInstance::getStateFormula ( State state ) const

inline

Parameters

state a State

Returns: the state Formula associated the given State

Definition at line 259 of file EncodedInstance.hh.

References Diades::Altarica::EncodedInstanceData::getStateFormula().

◆ initialState()

State Diades::Altarica::EncodedInstance::initialState ( )

inline

Returns: the initial state of the instance

Definition at line 337 of file EncodedInstance.hh.

References Diades::Altarica::EncodedInstanceData::initialState().

◆ logs()

const string& Diades::Altarica::EncodedInstance::logs ( ) const

inline

Returns: the logs of the EncodedInstance

Definition at line 350 of file EncodedInstance.hh.

References Diades::Altarica::EncodedInstanceData::logs().

◆ nodeInstance()

Node Diades::Altarica::EncodedInstance::nodeInstance ( ) const

inline

Returns: the associated Node

Definition at line 290 of file EncodedInstance.hh.

References Diades::Altarica::EncodedInstanceData::nodeInstance().

◆ operator!=()

bool Diades::Altarica::EncodedInstance::operator!= ( const EncodedInstance & instance )

inline

Parameters

instance a EncodedInstance

Returns: true if the two instances are not equal (reference equality)

Definition at line 320 of file EncodedInstance.hh.

◆ operator<()

bool Diades::Altarica::EncodedInstance::operator< ( const EncodedInstance & instance )

inline

Parameters

instance a EncodedInstance

Returns: true if the instance is lower than the other one (reference comparison)

Definition at line 329 of file EncodedInstance.hh.

References _data.

◆ operator=()

EncodedInstance& Diades::Altarica::EncodedInstance::operator= ( const EncodedInstance & instance )

inline

Definition at line 234 of file EncodedInstance.hh.

References _data.

◆ operator==()

bool Diades::Altarica::EncodedInstance::operator== ( const EncodedInstance & instance )

inline

Parameters

instance a EncodedInstance

Returns: true if the two instances are equal (reference equality)

Definition at line 310 of file EncodedInstance.hh.

References _data.

◆ stateBegin()

StateIterator Diades::Altarica::EncodedInstance::stateBegin ( ) const

inline

Returns: an iterator on the states (begin)

Definition at line 375 of file EncodedInstance.hh.

References Diades::Altarica::EncodedInstanceData::stateBegin().

◆ stateEnd()

StateIterator Diades::Altarica::EncodedInstance::stateEnd ( ) const

inline

Returns: an iterator on the states (end)

Definition at line 383 of file EncodedInstance.hh.

References Diades::Altarica::EncodedInstanceData::stateEnd().

◆ transBegin()

TransIterator Diades::Altarica::EncodedInstance::transBegin ( ) const

inline

Returns: an iterator on the transitions (begin)

Definition at line 391 of file EncodedInstance.hh.

References Diades::Altarica::EncodedInstanceData::transBegin().

◆ transEnd()

TransIterator Diades::Altarica::EncodedInstance::transEnd ( ) const

inline

Returns: an iterator on the transitions (end)

Definition at line 399 of file EncodedInstance.hh.

References Diades::Altarica::EncodedInstanceData::transEnd().

◆ valid()

bool Diades::Altarica::EncodedInstance::valid ( ) const

inline

Returns: true if the EncodedInstance is valid (that is _data != 0)

Definition at line 301 of file EncodedInstance.hh.

Member Data Documentation

◆ _data

EncodedInstanceData* Diades::Altarica::EncodedInstance::_data

private

Definition at line 227 of file EncodedInstance.hh.

Referenced by operator<(), operator=(), and operator==().

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

include/diades/altarica/EncodedInstance.hh

Public Types

Public Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ AssertionIterator

◆ Fsm

◆ State

◆ StateFormulaMap

◆ StateIterator

◆ Trans

◆ TransIterator

Constructor & Destructor Documentation

◆ EncodedInstance() [1/3]

◆ EncodedInstance() [2/3]

◆ EncodedInstance() [3/3]

Member Function Documentation

◆ assertionBegin()

◆ assertionEnd()

◆ getConfigurationFormula()

◆ getEvent()

◆ getFormula()

◆ getNextStates()

◆ getState()

◆ getStateFormula()

◆ initialState()

◆ logs()

◆ nodeInstance()

◆ operator!=()

◆ operator<()

◆ operator=()

◆ operator==()

◆ stateBegin()

◆ stateEnd()

◆ transBegin()

◆ transEnd()

◆ valid()

Member Data Documentation

◆ _data