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

#include <RealTimeSystem.hh>

Public Member Functions

 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 Attributes

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 }
 
- 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)
 

Detailed Description

A RealTimeSystem is a system is modelled as as labelled time petri net (with priorities). The static time interval associated with a RealTimeSystem are bounded closed intervals and their bounds are integers. (Note that the restriction to integers is not a problem as the normal bounds are rationals that can be formally translated to integers (by normalisation). In a RealTimeSystem, transitions are labelled with events. An Event might be observable or not. By construction any RealTimeSystem contains the 'time point event' that is denoted 'lambda'. Event 'lambda' is set to be non observable.

Definition at line 33 of file RealTimeSystem.hh.

Constructor & Destructor Documentation

◆ RealTimeSystem()

Diades::Petri::RealTimeSystem::RealTimeSystem ( )
inline

Default constructor A RealTimeSystem is a LabelledPrioritizedTimeNet

Definition at line 44 of file RealTimeSystem.hh.

References Diades::Petri::LabelledNet::lambda(), and setNonObservable().

Member Function Documentation

◆ isObservable()

bool Diades::Petri::RealTimeSystem::isObservable ( Event  e) const
inline

Is the Event observable?

Parameters
ean Event
Returns
true if the Event is observable

Definition at line 71 of file RealTimeSystem.hh.

References timeDecompositionObservable().

◆ setNonObservable()

void Diades::Petri::RealTimeSystem::setNonObservable ( Event  e)
inline

Set the event to be non-observable

Parameters
ethe Event

Definition at line 61 of file RealTimeSystem.hh.

Referenced by RealTimeSystem().

◆ setObservable()

void Diades::Petri::RealTimeSystem::setObservable ( Event  e)
inline

Set the event to be observable

Parameters
ethe Event

Definition at line 52 of file RealTimeSystem.hh.

◆ timeDecompositionObservable()

void Diades::Petri::RealTimeSystem::timeDecompositionObservable ( )

Perform the time decomposition of a transition is associated with an observable event

Referenced by isObservable().

Member Data Documentation

◆ _observables

std::unordered_set<Event> Diades::Petri::RealTimeSystem::_observables
protected

Definition at line 36 of file RealTimeSystem.hh.

◆ _unobservables

std::unordered_set<Event> Diades::Petri::RealTimeSystem::_unobservables
protected

Definition at line 37 of file RealTimeSystem.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