Package jline.api.spn

Class Spn_mdd

java.lang.Object

jline.api.spn.Spn_mdd

public class Spn_mdd
extends Object

Decision-diagram reachable set and Kronecker rate descriptor of a stochastic Petri net, so that Mdd_mcd can analyse it.

Levels are of two kinds. Place levels: one per (Place, class) pair, holding a token count. A multiclass net therefore has P*R of them, ordered place-major, so level p*R+k is class k in place p. Phase levels: one per mode whose firing time has more than one phase, holding the phase the running server occupies.

The rate structure factorises exactly under single-server firing semantics: a mode fires at a constant rate whenever every input level holds its enabling multiplicity and no inhibitor level has reached its threshold, so W_l^e[i, i + fire(l) - enab(l)] = 1 for enab(l) <= i < inhib(l) at every place level. A phase-type mode contributes two event families on its phase level, the internal phase changes D0 (marking unchanged) and the firings D1 (marking moved), each gated by the same per-level enabling indicators. Both are products of per-level terms, which is what Eq. 1 of the paper requires.

Phase-type firing and the memory policy. LINE discards a running server's phase when its mode becomes disabled, i.e. preemptive repeat. Resetting a mode's phase is then triggered by a JOINT condition on the place levels, which is not a product of per-level terms and has no Kronecker form. What this descriptor encodes is preemptive resume: a disabled mode's phase freezes and continues when the mode is re-enabled. The two policies coincide exactly when a mode is never disabled while running, so reachability records, for free, whether any phase-type mode was ever found disabled. phmemory "exact" (the default) errors when one was; "resume" proceeds deliberately with the resume semantics.

Other restrictions, each an error and never a silent approximation: no immediate transitions (they make vanishing states, which must be eliminated before a Kronecker rate descriptor exists) and no marking-dependent firing rates. A multi-server mode is accepted only when its enabling touches ONE level, because the enabling degree min_l floor(m(l)/enab(l)) is otherwise not a product of per-level terms.

MATLAB twin: spn_mdd.m. Python twin: api/spn/mdd.py.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	Spn_mdd.SpnInfo	Everything the caller needs alongside the descriptor.
static class	Spn_mdd.SpnMode	One (transition, mode) pair of the net, in level coordinates.
static class	Spn_mdd.SpnOptions	Options of the translation.
static class	Spn_mdd.SpnResult	Descriptor, diagram and metadata returned together.

Method Summary

Modifier and Type	Method	Description
static Spn_mdd.SpnResult	spn_mdd(Network model)	Translate the net with the default options.
static Spn_mdd.SpnResult	spn_mdd(Network model, Spn_mdd.SpnOptions options)	Build the reachable set and Kronecker descriptor of a stochastic Petri net.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Details

spn_mdd

public static Spn_mdd.SpnResult spn_mdd(Network model)

Translate the net with the default options.

spn_mdd

public static Spn_mdd.SpnResult spn_mdd(Network model,
 Spn_mdd.SpnOptions options)

Build the reachable set and Kronecker descriptor of a stochastic Petri net.

Parameters:

model - a Network holding Places and Transitions

options - translation options; null takes the defaults