Package jline.api.spn

package jline.api.spn
Stochastic Petri net analysis.

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.

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.
  • 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/.

  • Classes
    Class
    Description
    Spn_conv
    Convolution algorithm for the normalising constant of an S-invariant reachable product-form stochastic Petri net.
    Spn_lpbnd
    Linear-programming bounds on the mean marking and the throughputs of a stochastic timed Petri net.
    Spn_lpbnd.SpnLpBounds
    The brackets, each a 2 x n array with row 0 the minimum.
    Spn_lpbnd.SpnLpMode
    One (transition, mode) pair over place-major levels.
    Spn_lpbnd.SpnLpOptions
    Options of the relaxation.
    Spn_mdd
    Decision-diagram reachable set and Kronecker rate descriptor of a stochastic Petri net, so that Mdd_mcd can analyse it.
    Spn_mdd.SpnInfo
    Everything the caller needs alongside the descriptor.
    Spn_mdd.SpnMode
    One (transition, mode) pair of the net, in level coordinates.
    Spn_mdd.SpnOptions
    Options of the translation.
    Spn_mdd.SpnResult
    Descriptor, diagram and metadata returned together.
    Spn_metrics
    Stationary measures of a product-form stochastic Petri net from the MDD-rec masses.
    Spn_metrics.SpnMetricsResult
    The stationary measures of Sec.
    Spn_pf
    Product form of a stochastic Petri net: decide whether one exists and derive the per-level factors g_l that Mdd_rec and Spn_metrics take as input.
    Spn_pf.SpnPfOptions
    Options of the product-form derivation.
    Spn_pf.SpnPfResult
    The product form, and the certificate that it is one.
    Spn_rec_enabled
    Enabling-degree distribution of one mode of a product-form stochastic Petri net, by the masked MDD-rec recursion.
    Spn_rec_enabled.SpnEnabling
    Unnormalised enabling-degree masses of one mode.
    Spn_sinvariants
    Minimal-support S-invariants (P-invariants) of a stochastic Petri net, and the load vector V = S m0.
    Spn_sinvariants.SpnInvariants
    The invariant basis of a net, in place-level coordinates.