#include <RealTimeSystemPattern.hh>

Public Member Functions
	RealTimeSystemPattern (const RealTimeSystem &system, const Pattern &pattern)

const vector< Marking > &	finalMarkings () const

const vector< Place > &	nonAdmissibleSystemPlaces () 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)

Protected Member Functions
void	copyPlaces (const BoundedNet &net, RealTimeSystemPattern::PlaceIterator first, RealTimeSystemPattern::PlaceIterator end, const string &prefix, unordered_map< Place, Place > &mapping)

void	setFinalMarkings (const vector< Marking > &patFinalMarkings, unordered_map< Place, Place > &mapping)

void	copySystemTransitions (const RealTimeSystem &system, unordered_map< Place, Place > &mappingSystem, unordered_map< Transition, Transition > &mappingTransitionSystem, const Pattern &pattern, unordered_map< unsigned, std::vector< size_t > > &decomposedTransitionsForEvent)

void	computeTransitionProducts (const RealTimeSystem &system, const Pattern &pattern, const unordered_map< Place, Place > &mappingPattern, const unordered_map< unsigned, std::vector< size_t > > &decomposedTransitionsForEvent)

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
vector< Marking >	_finalMarkings

vector< Place >	_nonAdmissibleSystemPlaces

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

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 }

Detailed Description

This class implements the product between a RealTimeSystem and an untimed Pattern

Definition at line 26 of file RealTimeSystemPattern.hh.

Constructor & Destructor Documentation

◆ RealTimeSystemPattern()

Diades::Petri::RealTimeSystemPattern::RealTimeSystemPattern	(	const RealTimeSystem &	system,
		const Pattern &	pattern
	)

Constructor

Parameters

system	a RealTimeSystem
pattern	a Pattern (untimed Pattern)

Member Function Documentation

◆ computeTransitionProducts()

void Diades::Petri::RealTimeSystemPattern::computeTransitionProducts	(	const RealTimeSystem &	system,
		const Pattern &	pattern,
		const unordered_map< Place, Place > &	mappingPattern,
		const unordered_map< unsigned, std::vector< size_t > > &	decomposedTransitionsForEvent
	)

protected

Parameters

system	The RealTimeSystem to copy
pattern	The Pattern to copy
mappingPattern	the precomputed place mapping[pattern_place]=copy
decomposedTransitionsForEvent	the set of decomposed transitions of the system associated with each event of the Pattern

◆ copyPlaces()

void Diades::Petri::RealTimeSystemPattern::copyPlaces	(	const BoundedNet &	net,
		RealTimeSystemPattern::PlaceIterator	first,
		RealTimeSystemPattern::PlaceIterator	end,
		const string &	prefix,
		unordered_map< Place, Place > &	mapping
	)

protected

Copy places and set the initial marking accordingly

Parameters

net	the net that contains the places to copy
first	the iterator on the first place to copy
end	the 'after the last place to copy' iterator
prefix	a prefix to add to any copied place name
mapping	the returned mapping mapping[copied_place]=copy

◆ copySystemTransitions()

void Diades::Petri::RealTimeSystemPattern::copySystemTransitions	(	const RealTimeSystem &	system,
		unordered_map< Place, Place > &	mappingSystem,
		unordered_map< Transition, Transition > &	mappingTransitionSystem,
		const Pattern &	pattern,
		unordered_map< unsigned, std::vector< size_t > > &	decomposedTransitionsForEvent
	)

protected

Copy the system transition (inhibitions + priorities) in the RealTimeSystemPattern net

Parameters

system	the RealTimeSystem to copy
mappingSystem	the precomputed mapping[system_place]=copy
mappingTransitionSystem	the returned transition mapping mappingTransitionSystem[systrans] = copy (note that if systrans has to be timed decomposed then 'copy' becomes the 'event' transition from the decomposition
pattern	the Pattern that is used in the product
decomposedTransitionsForEvent	the returned mapping that associates for each event of the Pattern the set of decomposed transitions in the system (their index in the decomposedTransitions())

◆ finalMarkings()

const vector<Marking>& Diades::Petri::RealTimeSystemPattern::finalMarkings ( ) const

inline

Returns: the final marking of the current product

Definition at line 109 of file RealTimeSystemPattern.hh.

References _finalMarkings.

◆ nonAdmissibleSystemPlaces()

const vector<Place>& Diades::Petri::RealTimeSystemPattern::nonAdmissibleSystemPlaces ( ) const

inline

Returns: the set of non admissible system places

Definition at line 119 of file RealTimeSystemPattern.hh.

References _nonAdmissibleSystemPlaces.

◆ setFinalMarkings()

void Diades::Petri::RealTimeSystemPattern::setFinalMarkings	(	const vector< Marking > &	patFinalMarkings,
		unordered_map< Place, Place > &	mapping
	)

protected

Parameters

patFinalMarkings	the final markings of the Pattern
mapping	the mapping between the places of the Pattern and the current net

Set as final in the current net the places that are set as final in the Pattern

Member Data Documentation

◆ _finalMarkings

vector<Marking> Diades::Petri::RealTimeSystemPattern::_finalMarkings

protected

Definition at line 29 of file RealTimeSystemPattern.hh.

Referenced by finalMarkings().

◆ _nonAdmissibleSystemPlaces

vector<Place> Diades::Petri::RealTimeSystemPattern::_nonAdmissibleSystemPlaces

protected

Definition at line 30 of file RealTimeSystemPattern.hh.

Referenced by nonAdmissibleSystemPlaces().

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

/home/yannick/laas/redmine/tools/diades/include/diades/petri/RealTimeSystemPattern.hh

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ RealTimeSystemPattern()

Member Function Documentation

◆ computeTransitionProducts()

◆ copyPlaces()

◆ copySystemTransitions()

◆ finalMarkings()

◆ nonAdmissibleSystemPlaces()

◆ setFinalMarkings()

Member Data Documentation

◆ _finalMarkings

◆ _nonAdmissibleSystemPlaces