…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
…3 simulations. Comparing confidence interval levels It can also be useful to run several different simulation replications for different numbers of simulations to investigate the effects on both the estimate…
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
…the model time at which the job was created. MONITOR DECLS globref longdelaytime = 200; globref fileid = (NONE : TextIO.outstream option); fun getfid () = (* this will raise…
Queue system configuration example
…for this example, and they are briefly explained below. colset ProcDist = with DISCRETE | EXP; globref num_of_servers = 4; globref avg_proc_time = 360; globref procdist = EXP; fun initServers()…
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…
