Package jline.api.spn
Algorithms specific to the SPN formalism, as opposed to the
formalism-agnostic decision-diagram machinery in jline.api.mdd.
Spn_mdd turns a Petri net into the reachable set and
Kronecker rate descriptor that Mdd_mcd consumes.
Spn_sinvariants, Spn_conv,
Spn_rec_enabled and Spn_metrics
carry the product-form side: the invariant basis, the convolution over its
load vector, and the stationary measures read off the MDD-rec masses.
Property analysis: Spn_tinvariants,
Spn_siphons, Spn_traps and
Spn_structprops are structural (Farkas T-invariants,
minimal siphons and traps with Commoner's property, LP boundedness,
conservativeness, consistency, repetitiveness and net classes; they ignore
inhibitor arcs, priorities and immediate precedence, listed in
ignored); Spn_reachgraph and
Spn_reachprops are behavioural (boundedness,
deadlocks, L4 liveness, reversibility on the GSPN reachability graph);
Spn_properties aggregates them.
References:
- A.S. Miner, G. Ciardo, "Efficient Reachability Set Generation and Storage Using Decision Diagrams", ICATPN 1999, LNCS 1639, pp.6-25.
- S. Balsamo, A. Marin, I. Stojic, "Computation of the normalising constant for product-form models of distributed systems with synchronisation", Future Generation Computer Systems 111 (2020) 475-490.
- T. Murata, "Petri nets: properties, analysis and applications", Proc. IEEE 77(4) (1989) 541-580.
- J.L. Coleman, W. Henderson, P.G. Taylor, "Product form equilibrium distributions and a convolution algorithm for stochastic Petri nets", Performance Evaluation 26(3), 1996, 159-180.
MATLAB twin: matlab/src/api/spn/. Python twin:
python/line_solver/api/spn/.
-
ClassesClassDescriptionConvolution algorithm for the normalising constant of an S-invariant reachable product-form stochastic Petri net.Infinite-state stochastic Petri nets (iSPN) by the matrix-geometric method.Result of
Spn_ispn.spn_ispn(double[][], double[][], double[][], double[], boolean[], double[], double[], int); fields as in the MATLAB help.Linear-programming bounds on the mean marking and the throughputs of a stochastic timed Petri net.The brackets, each a 2 x n array with row 0 the minimum.One (transition, mode) pair over place-major levels.Options of the relaxation.Decision-diagram reachable set and Kronecker rate descriptor of a stochastic Petri net, so thatMdd_mcdcan analyse it.Everything the caller needs alongside the descriptor.One (transition, mode) pair of the net, in level coordinates.Options of the translation.Descriptor, diagram and metadata returned together.Stationary measures of a product-form stochastic Petri net from the MDD-rec masses.The stationary measures of Sec.Product form of a stochastic Petri net: decide whether one exists and derive the per-level factors g_l thatMdd_recandSpn_metricstake as input.Options of the product-form derivation.The product form, and the certificate that it is one.Structural and behavioural property analysis of a stochastic Petri net in one call: invariants, siphons and traps, the LP structural checks and net classes, the reachability-graph verdicts, and the liveness conclusions that the net class and Commoner's property license.All the properties.Untimed reachability graph of a generalised stochastic Petri net, over the markings of the place levels.The reachability graph.Behavioural properties of a generalised stochastic Petri net, read off its reachability graph (Spn_reachgraph, which honours inhibitor arcs, priorities and immediate precedence).The behavioural verdicts.Enabling-degree distribution of one mode of a product-form stochastic Petri net, by the masked MDD-rec recursion.Unnormalised enabling-degree masses of one mode.Minimal-support S-invariants (P-invariants) of a stochastic Petri net, and the load vector V = S m0.The invariant basis of a net, in place-level coordinates.All minimal siphons of a stochastic Petri net, and Commoner's check that each one contains an initially marked trap.The minimal siphons, in level coordinates.Structural properties of a stochastic Petri net decided from its incidence matrix C = Post - Pre by linear programming, and its net-class membership.The structural verdicts.Minimal-support semi-positive T-invariants of a stochastic Petri net.The T-invariant basis of a net, in event coordinates.All minimal traps of a stochastic Petri net, and which of them m0 marks.The minimal traps, in level coordinates.