spn_sinvariants.h File Reference

Minimal-support S-invariants (P-invariants) of a stochastic Petri net, and the load vector V = S m0. More...

#include <algorithm>
#include <cmath>
#include <cstddef>
#include <map>
#include <string>
#include <vector>
#include "line/lang/lang_types.h"
#include "line/lang/qn/network_struct.h"
#include "line/num/number.h"
#include "line/util/error.h"
#include "line/util/matrix.h"

Include dependency graph for spn_sinvariants.h:

Go to the source code of this file.

Classes
struct	line::spn::SpnInvariants
	The invariant basis of a net, in place-level coordinates. More...

Namespaces
namespace	line
namespace	line::spn

Functions
template<class T>
SpnInvariants	line::spn::spn_sinvariants (const qn::NetworkStruct< T > &sn, const std::vector< double > &init=std::vector< double >())
	Minimal-support S-invariants and the load vector of a net.

Detailed Description

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.

Definition in file spn_sinvariants.h.