#include <TwinRealTimeSystemPattern.hh>

Public Member Functions
	TwinRealTimeSystemPattern (const RealTimeSystemPattern &syspat)

const vector< Marking > &	leftFinalMarkings () const

const vector< Place > &	leftNonAdmissibleSystemPlaces () const

const vector< Marking > &	rightFinalMarkings () const

const vector< Place > &	rightNonAdmissibleSystemPlaces () const

const std::string &	seltFormula () const

Public Member Functions inherited from Diades::Petri::RealTimeSystem
	RealTimeSystem ()

void	setObservable (Event e)

void	setNonObservable (Event e)

bool	isObservable (Event e) const

void	timeDecompositionObservable ()

Public Member Functions inherited from Diades::Petri::LabelledPrioritizedTimeNet
bool	isTimeDecomposed (const Transition &t) const

const vector< TimeDecomposedTransition > &	decomposedTransitions () const

void	timeDecomposition ()

void	timeDecomposition (Event e)

const Interval &	staticInterval (const Transition &t) const

	LabelledPrioritizedTimeNet ()

virtual	~LabelledPrioritizedTimeNet ()

virtual Transition	newTransition (const set< Place > &pre, const set< Place > &post, const string &name, const Interval &interval, Event event)

virtual void	nameOfTransition2Dot (ostream &os, Transition transition) const

virtual Place	makeEventConflictFree (Place p)

virtual void	makeEventConflictFree ()

Public Member Functions inherited from Diades::Petri::LabelledPrioritizedNet
	LabelledPrioritizedNet ()

	LabelledPrioritizedNet (const LabelledPrioritizedNet &net)

LabelledPrioritizedNet &	operator= (const LabelledPrioritizedNet &net)

LabelledPrioritizedNet &	append (const LabelledPrioritizedNet &net)

	LabelledPrioritizedNet (const LabelledPrioritizedNet &lppn1, const LabelledPrioritizedNet &lppn2, const unordered_set< Event > &syncEvents)

LabelledPrioritizedNet &	merge (const LabelledPrioritizedNet &lppn1, const LabelledPrioritizedNet &lppn2, const unordered_set< Event > &syncEvents, std::unordered_map< Transition, std::list< Transition > > &lppn1SyncTrans, std::unordered_map< Transition, std::list< Transition > > &lppn2SyncTrans, std::unordered_map< Transition, std::pair< Transition, Transition > > &syncTransitions, std::unordered_map< Place, Place > &lppn1Place, std::unordered_map< Place, Place > &lppn2Place, std::unordered_map< Place, std::pair< Place, Place > > &syncPlaces)

void	setPriority (Transition t1, Transition t2)

const set< Transition > &	priorities (Transition tr) const

const set< Transition > &	reversedPriorities (Transition tr) const

void	resetPriority (Transition t1, Transition t2)

void	priorities2Dot (ostream &os) const

virtual void	deleteTransition (Transition t1)

Public Member Functions inherited from Diades::Petri::LabelledNet
Event	lambda () const

	LabelledNet ()

	LabelledNet (const LabelledNet &net)

LabelledNet &	operator= (const LabelledNet &net)

LabelledNet &	append (const LabelledNet &net)

	LabelledNet (const LabelledNet &lpn1, const LabelledNet &lpn2, const unordered_set< Event > &syncEvents)

LabelledNet &	merge (const LabelledNet &lpn1, const LabelledNet &lpn2, const unordered_set< Event > &syncEvents, std::unordered_map< Transition, std::list< Transition > > &lpn1SyncTrans, std::unordered_map< Transition, std::list< Transition > > &lpn2SyncTrans, unordered_map< Transition, std::pair< Transition, Transition >> &synchronisations, std::unordered_map< Place, Place > &lpn1Place, std::unordered_map< Place, Place > &lpn2Place, std::unordered_map< Place, std::pair< Place, Place > > &syncPlaces)

virtual Transition	newTransition (const set< Place > &pre, const set< Place > &post, const string &name, Event e)

TransitionEventIterator	beginOfTransitionWithEvent (Event event) const

TransitionEventIterator	endOfTransitionWithEvent (Event event) const

Transition	duplicateTransition (Transition t)

virtual void	net2TinaTransitionName (ostream &os, Transition trans) const

virtual void	copyLabelledNet (const LabelledNet &net, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMap, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapCopy, Diades::Graph::ConstEdgeMap< Diades::Graph::Edge > &edgeMap, Diades::Graph::EdgeMap< Diades::Graph::Edge > &edgeMapCopy)

virtual void	appendLabelledNet (const LabelledNet &net, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMap, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapCopy, Diades::Graph::ConstEdgeMap< Diades::Graph::Edge > &edgeMap, Diades::Graph::EdgeMap< Diades::Graph::Edge > &edgeMapCopy)

virtual void	mergeLabelledNet (const LabelledNet &lpn1, const LabelledNet &lpn2, const unordered_set< Event > &syncEvents, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMapLpn1, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapFromLpn1, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMapLpn2, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapFromLpn2, std::unordered_map< Transition, std::list< Transition > > &lpn1SyncTrans, std::unordered_map< Transition, std::list< Transition > > &lpn2SyncTrans, std::unordered_map< Transition, std::pair< Transition, Transition > > &syncTransitions, std::unordered_map< Place, Place > &lppn1Place, std::unordered_map< Place, Place > &lppn2Place, std::unordered_map< Place, std::pair< Place, Place > > &syncPlaces)

EventIterator	beginOfEvents () const

EventIterator	endOfEvents () const

Event	getEvent (Transition t) const

bool	containsEvent (Event event) const

Public Member Functions inherited from Diades::Petri::BoundedNet
	BoundedNet ()

	BoundedNet (const BoundedNet &net)

BoundedNet &	operator= (const BoundedNet &net)

BoundedNet &	append (const BoundedNet &net)

virtual	~BoundedNet ()

void	setName (const string &name)

const string &	name () const

unsigned int	id () const

void	setId (unsigned id)

void	clear ()

const Diades::Graph::Graph &	graph () const

Place	newPlace ()

Place	newPlace (const string &name)

void	deletePlace (Place p)

void	setLabelOfPlace (Place place, const string &label)

PlaceIterator	beginOfPlaces () const

PlaceIterator	endOfPlaces () const

size_t	numberOfPlaces () const

const string &	labelOfPlace (const Place &p) const

const string &	nameOfPlace (Place p) const

void	setNameOfPlace (Place p, const string &name)

Place	getPlace (const string &name) const

Arc	getArc (Diades::Graph::Node n1, Diades::Graph::Node n2) const

virtual bool	enables (Transition t, const Marking &marking) const

virtual bool	fire (Transition t, const Marking &marking, Marking &newMarking) const

virtual Transition	newTransition (const set< Place > &pre, const set< Place > &post)

virtual Transition	newTransition (const set< Place > &pre, const set< Place > &post, const string &name)

virtual void	setInhibition (Place p, Transition t)

const std::unordered_set< Transition > &	inhibitors (Place p) const

virtual void	unsetInhibition (Place p, Transition t)

bool	inhibits (Place p, Transition t) const

size_t	numberOfTransitions () const

size_t	numberOfArcs () const

void	addPre (Transition transition, Place place)

void	addPost (Transition transition, Place place)

ConstIterator	preTransBegin (Place place) const

ConstIterator	preTransEnd (Place place) const

ConstIterator	postTransBegin (Place place) const

ConstIterator	postTransEnd (Place place) const

ConstIterator	preBegin (Transition transition) const

ConstIterator	preEnd (Transition transition) const

ConstIterator	postBegin (Transition transition) const

ConstIterator	postEnd (Transition transition) const

TransitionIterator	beginOfTransitions () const

TransitionIterator	endOfTransitions () const

void	setNameOfTransition (Transition transition, const string &name)

const string &	nameOfTransition (Transition transition) const

Transition	transitionOfName (const string &name) const

bool	inPre (Transition t, Place p) const

bool	inPost (Transition t, Place p) const

const Marking &	initialMarking () const

Marking &	initialMarking ()

bool	isMarked () const

virtual void	net2Dot (const string &fileName) const

void	net2Tina (ostream &os) const

void	net2Tina (const string &filename) const

void	printPrettyMarking (ostream &os, const Marking &marking) const

virtual void	appendNet (const BoundedNet &net, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMap, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapCopy, Diades::Graph::ConstEdgeMap< Diades::Graph::Edge > &edgeMap, Diades::Graph::EdgeMap< Diades::Graph::Edge > &edgeMapCopy)

template<typename Iterator >
Place	mergePlaces (Iterator first, Iterator last)

Private Member Functions
void	duplicatePlaces (const RealTimeSystemPattern &syspat, unordered_map< Place, Place > &leftPlaceOf, unordered_map< Place, Place > &rightPlaceOf)

void	duplicateTransitions (const RealTimeSystemPattern &syspat, const unordered_map< Place, Place > &leftPlaceOf, const unordered_map< Place, Place > &rightPlaceOf, unordered_map< Transition, Transition > &leftTransitionOf, unordered_map< Transition, Transition > &rightTransitionOf, unordered_map< Event, unordered_set< Transition >> &leftObservableTransitions, unordered_map< Event, unordered_set< Transition >> &rightObservableTransitions)

void	mergeTransitions (unordered_map< Event, unordered_set< Transition >> &leftObservableTransitions, unordered_map< Event, unordered_set< Transition >> &rightObservableTransitions)

Transition	mergeTransition (Transition trLeft, Transition trRight)

void	computeSeltFormula ()

Private Attributes
vector< Marking >	_leftFinalMarkings

vector< Place >	_leftNonAdmissibleSystemPlaces

vector< Marking >	_rightFinalMarkings

vector< Place >	_rightNonAdmissibleSystemPlaces

std::string	_seltFormula

Additional Inherited Members
Public Types inherited from Diades::Petri::LabelledPrioritizedTimeNet
typedef ::Diades::Utils::Exception< LabelledPrioritizedTimeNet >	Exception

typedef int	Time

typedef ::Diades::Utils::Interval	Interval

Public Types inherited from Diades::Petri::LabelledNet
typedef Diades::Utils::Exception< LabelledNet >	Exception

typedef PetriEventManager::EventId	Event

typedef set< Event >::const_iterator	EventIterator

typedef unordered_set< Transition >::const_iterator	TransitionEventIterator

typedef unordered_set< Transition >::const_iterator	EventTransitionIterator

Public Types inherited from Diades::Petri::BoundedNet
enum	NodeType { P, T }

typedef Diades::Utils::Exception< BoundedNet >	Exception

typedef PerTypeIterator	TransitionIterator

typedef PerTypeIterator	PlaceIterator

typedef set< Transition >::const_iterator	TransitionEventIterator

Static Public Member Functions inherited from Diades::Petri::LabelledPrioritizedTimeNet
static string	typeName ()

Static Public Member Functions inherited from Diades::Petri::LabelledNet
static string	typeName ()

Static Public Member Functions inherited from Diades::Petri::BoundedNet
static string	typeName ()

Protected Types inherited from Diades::Petri::BoundedNet
enum	TransitionType { NotPostponable, Postponable }

Protected Member Functions inherited from Diades::Petri::LabelledPrioritizedTimeNet
virtual void	net2TinaTransitionInterval (ostream &os, Transition trans) const

virtual size_t	timeDecomposition (Transition t)

virtual Transition	shiftTransition (Transition t)

Protected Member Functions inherited from Diades::Petri::LabelledPrioritizedNet
virtual void	priorities2Tina (ostream &os) const

virtual void	net2TinaEnd (ostream &os, const string &header) const

virtual void	writeEndOfDotFile (ostream &os) const

virtual void	copyLabelledPrioritizedNet (const LabelledPrioritizedNet &net, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMap, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapCopy, Diades::Graph::ConstEdgeMap< Diades::Graph::Edge > &edgeMap, Diades::Graph::EdgeMap< Diades::Graph::Edge > &edgeMapCopy)

virtual void	appendLabelledPrioritizedNet (const LabelledPrioritizedNet &net, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMap, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapCopy, Diades::Graph::ConstEdgeMap< Diades::Graph::Edge > &edgeMap, Diades::Graph::EdgeMap< Diades::Graph::Edge > &edgeMapCopy)

virtual void	mergeLabelledPrioritizedNet (const LabelledPrioritizedNet &lppn1, const LabelledPrioritizedNet &lppn2, const unordered_set< Event > &syncEvents, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMapLppn1, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapFromLppn1, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMapLppn2, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapFromLppn2, std::unordered_map< Transition, std::list< Transition > > &lppn1SyncTrans, std::unordered_map< Transition, std::list< Transition > > &lppn2SyncTrans, std::unordered_map< Transition, std::pair< Transition, Transition > > &syncTransitions, std::unordered_map< Place, Place > &lppn1Place, std::unordered_map< Place, Place > &lppn2Place, std::unordered_map< Place, std::pair< Place, Place > > &syncPlaces)

Protected Member Functions inherited from Diades::Petri::BoundedNet
void	net2TinaWithHeader (ostream &os, const string &netHeader) const

virtual void	net2TinaTransition (ostream &os, Transition trans) const

virtual void	copyNet (const BoundedNet &net, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMap, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapCopy, Diades::Graph::ConstEdgeMap< Diades::Graph::Edge > &edgeMap, Diades::Graph::EdgeMap< Diades::Graph::Edge > &edgeMapCopy)

Protected Attributes inherited from Diades::Petri::RealTimeSystem
std::unordered_set< Event >	_observables

std::unordered_set< Event >	_unobservables

Protected Attributes inherited from Diades::Petri::BoundedNet
Diades::Graph::Graph	_graph

Diades::Graph::NodeMap< NodeType >	_nodeType

Diades::Graph::NodeMap< string >	_nameOfNode

Diades::Graph::NodeMap< string >	_labelOfNode

Diades::Graph::NodeMap< int >	_postponable

Diades::Graph::NodeMap< std::unordered_set< Transition > >	_inhibitors

Diades::Graph::NodeMap< std::unordered_set< Place > >	_inhibited

string	_name

Marking	_initialMarking

unordered_map< string, Diades::Graph::Node >	_placeOfName

unordered_map< string, Diades::Graph::Node >	_transitionOfName

Detailed Description

This class implements the twin product of a RealTimeSystemPattern

Definition at line 25 of file TwinRealTimeSystemPattern.hh.

Constructor & Destructor Documentation

◆ TwinRealTimeSystemPattern()

Diades::Petri::TwinRealTimeSystemPattern::TwinRealTimeSystemPattern ( const RealTimeSystemPattern & syspat )

Parametrized constructor

Parameters

syspat RealTimeSystemPattern Build the twin product of the RealTimeSystemPattern

Member Function Documentation

◆ computeSeltFormula()

void Diades::Petri::TwinRealTimeSystemPattern::computeSeltFormula ( )

private

Initialise the selt formula for diagnosability checking

Referenced by seltFormula().

◆ duplicatePlaces()

void Diades::Petri::TwinRealTimeSystemPattern::duplicatePlaces	(	const RealTimeSystemPattern &	syspat,
		unordered_map< Place, Place > &	leftPlaceOf,
		unordered_map< Place, Place > &	rightPlaceOf
	)

private

Initialise the set of left and right places in the Twin and the corresponding initial markings as well as the final markings. Initialise the non admissible places (left and right) in the twin

Parameters

syspat	the RealTimeSystemPattern that is used to build the Twin
leftPlaceOf	the returned place mapping (left side) leftPlaceOf[syspat_place] = left_place
rightPlaceOf	the returned place mapping (right side) rightPlaceOf[syspat_place] = right_place

Referenced by seltFormula().

◆ duplicateTransitions()

void Diades::Petri::TwinRealTimeSystemPattern::duplicateTransitions	(	const RealTimeSystemPattern &	syspat,
		const unordered_map< Place, Place > &	leftPlaceOf,
		const unordered_map< Place, Place > &	rightPlaceOf,
		unordered_map< Transition, Transition > &	leftTransitionOf,
		unordered_map< Transition, Transition > &	rightTransitionOf,
		unordered_map< Event, unordered_set< Transition >> &	leftObservableTransitions,
		unordered_map< Event, unordered_set< Transition >> &	rightObservableTransitions
	)

private

Duplicate the transitions of the RealTimeSystemPattern and decompose the observable ones to prepare them to be merged

Parameters

syspat	RealTimeSystemPattern
leftPlaceOf	the precomputed place mapping (left side) leftPlaceOf[syspat_place] = left_place
rightPlaceOf	the precomputed place mapping (right side) rightPlaceOf[syspat_place] = right_place
leftTransitionOf	the returned unobservable transition mapping (left side) leftTransitionOf[syspat_trans] = left_trans
rightTransitionOf	the returned unobservable transition mapping (right side) rightTransitionOf[syspat_trans] = right_trans
leftObservableTransitions	the returned set of left_decomposed_event observable transition (left side)
rightObservableTransitions	the returned set of right_decomposed_event observable transition (right side)

Referenced by seltFormula().

◆ leftFinalMarkings()

const vector<Marking>& Diades::Petri::TwinRealTimeSystemPattern::leftFinalMarkings ( ) const

inline

Returns: the final markings (left side)

Definition at line 50 of file TwinRealTimeSystemPattern.hh.

References _leftFinalMarkings.

◆ leftNonAdmissibleSystemPlaces()

const vector<Place>& Diades::Petri::TwinRealTimeSystemPattern::leftNonAdmissibleSystemPlaces ( ) const

inline

Returns: the set of non admissible places (left side)

Definition at line 60 of file TwinRealTimeSystemPattern.hh.

References _leftNonAdmissibleSystemPlaces.

◆ mergeTransition()

Transition Diades::Petri::TwinRealTimeSystemPattern::mergeTransition	(	Transition	trLeft,
		Transition	trRight
	)

private

Merging of the transition trLeft and trRight (associated with the observable same event)

Parameters

trLeft	left observable transition
trRight	right observable transition

Returns: the merged transition

Referenced by seltFormula().

◆ mergeTransitions()

void Diades::Petri::TwinRealTimeSystemPattern::mergeTransitions	(	unordered_map< Event, unordered_set< Transition >> &	leftObservableTransitions,
		unordered_map< Event, unordered_set< Transition >> &	rightObservableTransitions
	)

private

Merge the observable transitions (they are already decomposed). A merged transition is created for each couple of left/right transitions that are labeled with the same event leftObservableTransitions and rightObservableTransitions are cleared out as well as the transitions that they store

Parameters

leftObservableTransitions	the set of left decomposed observable transitions per event
rightObservableTransitions	the set of right decomposed observable transitions per event

Referenced by seltFormula().