Package jline.api.spn

Class Spn_sinvariants

java.lang.Object
jline.api.spn.Spn_sinvariants
public class Spn_sinvariants extends Object
Minimal-support S-invariants (P-invariants) of a stochastic Petri net, and the load vector V = S m0.

An S-invariant is a non-negative left null vector of the incidence matrix, U' C = 0, so U' m is conserved by every firing. The minimal-support ones form a basis of all of them (S. Balsamo, A. Marin, I. Stojic, FGCS 111 (2020), Sec. 3.1) and are what the convolution algorithm Spn_conv decomposes the reachability set along; Spn_mdd uses a single positive invariant for a much weaker purpose, to bound each place a priori.

FARKAS' ALGORITHM, on [C | I]: for each transition column in turn, keep the rows that already annihilate it and add, for every pair of rows of opposite sign in it, the positive combination that cancels it; then drop every row whose support strictly contains another's, which is what leaves the minimal supports. Rows are kept in integer arithmetic and divided by their gcd, so a multiplicity is never lost to rounding and two invariants that differ only by a positive scale are the same row.

ARC MULTIPLICITIES MUST BE INTEGRAL. A fractional arc has no Petri-net meaning and would make the gcd normalisation and the ILP-free convolution both wrong, so it is refused rather than rounded.

Levels are the (place, class) pairs of Spn_mdd, place-major, so the invariants come out in the coordinates the decision diagram and Spn_conv both use.

MATLAB twin: spn_sinvariants.m. Python twin: api/spn/sinvariants.py.

  • Method Details

    • spn_sinvariants

      public static Spn_sinvariants.SpnInvariants spn_sinvariants(NetworkStruct sn)
      Minimal-support S-invariants with the marking taken from the model.

    • spn_sinvariants

      public static Spn_sinvariants.SpnInvariants spn_sinvariants(NetworkStruct sn, double[] init)
      Minimal-support S-invariants and the load vector of a net.
      Parameters:
      sn - a NetworkStruct holding Places and Transitions
      init - initial tokens per place level, place-major; null takes them from the reference station of each closed class, as Spn_mdd does
      Returns:
      the invariant basis and the load vector