…Tools Simulator. Proc. of 30th International Conference on Applications and Theory of Petri Nets (Petri Nets 2009). Lecture Notes in Computer Science 5606, pp. 313-322, Springer-Verlag Berlin, 2009. K. Jensen,…
Timed Nets
…complex that modeling it by firing a sequence of simple transitions, rather than one complex transition, is most convenient. Leaving the clock unincremented during such a sequence lets us model…
Temporal logic for state spaces
…(e.g., the occurrence of certain transitions). Strongly connected components are used to make the model checking more efficient. Manual A manual describing how to use the temporal logic facilities is…
Performance output
…the data collector. The second column is a counter. The third column indicates the simulation steps at which the data values were collected. The fourth column indicates the model time…
Data collector functions
…data collector could be used in a predicate function for generic breakpoint monitor to stop a simulation when the Receive_Packet transition has occurred 5 times. let fun predBindElem (Top’Receive_Packet (1,…
Inhibitor arcs
…I add a new arc in the opposite direction, with the inscription ps Outgoing arcs Outgoing arcs are a bit more complicated than for queues or stacks, because I have…
Help entry in index
…Reenterable Model of Rectangular Communication Grid Reenterable Model of Rectangular Communication Grid with Cut-through Nodes Removing hierarchical constructs Reserved identifiers Resize, pan, and zoom Resource allocation example Resource allocation example…
Queue system example
…server timed; colset JobType = with A | B; colset Job = record jobType : JobType * AT : INT; colset Jobs = list Job; colset ServerxJob = product Server…
Queue system configuration example
…The net can also be downloaded here. Model Configurations It is often necessary to analyze and compare the behavior of different configurations of a model. It is always possible to…
Queue system queue delay
A number of monitors for the Queue System net illustrate different ways to measure the amount of time that jobs wait in the queue. Queue delay This is a generic…
