DiaDes  0.1
DIAgnosis of Discrete-Event System
Public Types | Public Member Functions | Static Public Member Functions | Protected Member Functions | Private Attributes | List of all members
Diades::Petri::LabelledPrioritizedTimeNet Class Reference

#include <LabelledPrioritizedTimeNet.hh>

Public Types

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
 

Public Member Functions

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)
 

Static Public Member Functions

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 Member Functions

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)
 

Private Attributes

Diades::Graph::ConstNodeMap< Interval > _staticInterval
 
list< Transition > _toDecompose
 
vector< TimeDecomposedTransition > _decompositions
 
Diades::Graph::ConstNodeMap< int > _decIndex
 

Additional Inherited Members

- Protected Types inherited from Diades::Petri::BoundedNet
enum  TransitionType { NotPostponable, Postponable }
 
- 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 a safe labelled time Petri net (with priorities) Each transition holds an interval. Bounds of intervals are integers. An Interval can be unbounded (+oo).

Definition at line 28 of file LabelledPrioritizedTimeNet.hh.

Member Typedef Documentation

◆ Exception

Diades::Petri::LabelledPrioritizedTimeNet::Exception
Exceptions
Exceptionexception returned by any Net

Definition at line 44 of file LabelledPrioritizedTimeNet.hh.

◆ Interval

typedef ::Diades::Utils::Interval Diades::Petri::LabelledPrioritizedTimeNet::Interval

Definition at line 48 of file LabelledPrioritizedTimeNet.hh.

◆ Time

typedef int Diades::Petri::LabelledPrioritizedTimeNet::Time

Definition at line 47 of file LabelledPrioritizedTimeNet.hh.

Constructor & Destructor Documentation

◆ LabelledPrioritizedTimeNet()

Diades::Petri::LabelledPrioritizedTimeNet::LabelledPrioritizedTimeNet ( )
inline

Default constructor: empty net A LabelledPrioritizedTimeNet is a LabelledPrioritizedNet()

Definition at line 105 of file LabelledPrioritizedTimeNet.hh.

References Diades::Petri::BoundedNet::graph(), and Diades::Graph::ConstNodeMap< T >::init().

◆ ~LabelledPrioritizedTimeNet()

virtual Diades::Petri::LabelledPrioritizedTimeNet::~LabelledPrioritizedTimeNet ( )
inlinevirtual

Destructor

Definition at line 117 of file LabelledPrioritizedTimeNet.hh.

References Diades::Petri::BoundedNet::name(), nameOfTransition2Dot(), and newTransition().

Member Function Documentation

◆ decomposedTransitions()

const vector<TimeDecomposedTransition>& Diades::Petri::LabelledPrioritizedTimeNet::decomposedTransitions ( ) const
inline

Definition at line 68 of file LabelledPrioritizedTimeNet.hh.

References _decompositions, and timeDecomposition().

◆ isTimeDecomposed()

bool Diades::Petri::LabelledPrioritizedTimeNet::isTimeDecomposed ( const Transition &  t) const
inline
Parameters
ta Transition of the current net
Returns
true if t doe not require any time decomposition

Definition at line 63 of file LabelledPrioritizedTimeNet.hh.

◆ makeEventConflictFree() [1/2]

virtual Place Diades::Petri::LabelledPrioritizedTimeNet::makeEventConflictFree ( Place  p)
virtual

Make the place p "event conflict-free"

Parameters
pthe Place
Returns
the Place Suppose that Place p is involved in the preset of at least two transitions (conflict) AND at least one of them is labelled with an effective event (not a lambda) then place p is NOT "event conflict-free". For the transitions involving place p in their preset and labelled with an effective event, we perform a transition shift. Finally, if place p was not "event conflict-free", it becomes "event conflict-free" as place p is then involved only into lambda-transitions
See also
shiftTransition

◆ makeEventConflictFree() [2/2]

virtual void Diades::Petri::LabelledPrioritizedTimeNet::makeEventConflictFree ( )
virtual

Call makeEventConflictFree on any place

Referenced by net2TinaTransitionInterval().

◆ nameOfTransition2Dot()

virtual void Diades::Petri::LabelledPrioritizedTimeNet::nameOfTransition2Dot ( ostream &  os,
Transition  transition 
) const
virtual

Output the transition as a dot-readable string in the stream os

Parameters
osthe output stream
transitionthe Transition to print out

Reimplemented from Diades::Petri::LabelledNet.

Referenced by ~LabelledPrioritizedTimeNet().

◆ net2TinaTransitionInterval()

virtual void Diades::Petri::LabelledPrioritizedTimeNet::net2TinaTransitionInterval ( ostream &  os,
Transition  trans 
) const
inlineprotectedvirtual

Output the transition interval as a TINA-readable string in the stream os

Parameters
osthe output stream
transthe Transition to print out

Reimplemented from Diades::Petri::BoundedNet.

Definition at line 159 of file LabelledPrioritizedTimeNet.hh.

References makeEventConflictFree(), shiftTransition(), and timeDecomposition().

◆ newTransition()

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

Creation of a new Transition

Parameters
prethe preset
postthe postset
namethe name
intervalthe static Interval (positive, bounded or not, integers bounds)
eventthe Event associated with the Transition
Returns
the newly created Transition
Precondition
the static Interval is positive, bounded or not, integers bounds
Postcondition
If the transition is not associated with an interval [0,+oo[, it is then added to the pool of transitions that may require a time decomposition

Referenced by ~LabelledPrioritizedTimeNet().

◆ shiftTransition()

virtual Transition Diades::Petri::LabelledPrioritizedTimeNet::shiftTransition ( Transition  t)
protectedvirtual

Transition "shifting"

Parameters
Transitiont Perform the following operation
  • Suppose transition t is of event e and static interval I
  • Add a transition t1 of event lambda and static interval I with pre(t1) = pre(t)
  • Add a new place p and then post(t1) = p
  • Add a transition t2 of event e and static interval [0,0], pre(t2) = { p } and post(t2) = post(t)
  • priorities involving t are duplicated on transition t1.
  • remove transition t
Returns
Transition t2

Referenced by net2TinaTransitionInterval().

◆ staticInterval()

const Interval& Diades::Petri::LabelledPrioritizedTimeNet::staticInterval ( const Transition &  t) const
inline
Parameters
ta Transition of the net
Returns
the static time interval of Transition t (denoted $ I_S(t) $). Here $ I_S(t) $ is an interval bounded by integers only. It can be bounded or not. Intervals are always positive.

Definition at line 97 of file LabelledPrioritizedTimeNet.hh.

◆ timeDecomposition() [1/3]

void Diades::Petri::LabelledPrioritizedTimeNet::timeDecomposition ( )

Perform the time decomposition of any transition that is set to be time-decomposed

Referenced by decomposedTransitions(), and net2TinaTransitionInterval().

◆ timeDecomposition() [2/3]

void Diades::Petri::LabelledPrioritizedTimeNet::timeDecomposition ( Event  e)

Perform the time decomposition of any transition that is set to be time-decomposed and that is associated with Event e

Parameters
ean Event
See also
TimeDecomposedTransition

◆ timeDecomposition() [3/3]

virtual size_t Diades::Petri::LabelledPrioritizedTimeNet::timeDecomposition ( Transition  t)
protectedvirtual

Perform the time decomposition of a transition

Parameters
tthe Transition to decompose
Returns
the index where the TimeDecomposedTransition is stored
See also
TimeDecomposedTransition

◆ typeName()

static string Diades::Petri::LabelledPrioritizedTimeNet::typeName ( )
inlinestatic
Returns
the absolute name of this class

Definition at line 36 of file LabelledPrioritizedTimeNet.hh.

Member Data Documentation

◆ _decIndex

Diades::Graph::ConstNodeMap<int> Diades::Petri::LabelledPrioritizedTimeNet::_decIndex
private

Definition at line 54 of file LabelledPrioritizedTimeNet.hh.

◆ _decompositions

vector<TimeDecomposedTransition> Diades::Petri::LabelledPrioritizedTimeNet::_decompositions
private

Definition at line 53 of file LabelledPrioritizedTimeNet.hh.

Referenced by decomposedTransitions().

◆ _staticInterval

Diades::Graph::ConstNodeMap<Interval> Diades::Petri::LabelledPrioritizedTimeNet::_staticInterval
private

Definition at line 51 of file LabelledPrioritizedTimeNet.hh.

◆ _toDecompose

list<Transition> Diades::Petri::LabelledPrioritizedTimeNet::_toDecompose
private

Definition at line 52 of file LabelledPrioritizedTimeNet.hh.

The documentation for this class was generated from the following file:
Generated on Tue May 12 2020 15:52:06 for DiaDes by   doxygen 1.8.13