spn_metrics.h File Reference

Stationary measures of a product-form stochastic Petri net from the MDD-rec masses. More...

#include <cmath>
#include <cstddef>
#include <limits>
#include <vector>
#include "line/api/mdd/mdd.h"
#include "line/api/mdd/mdd_rec.h"
#include "line/api/spn/spn_mdd.h"
#include "line/api/spn/spn_rec_enabled.h"
#include "line/num/number.h"
#include "line/util/error.h"

Include dependency graph for spn_metrics.h:

Go to the source code of this file.

Classes
struct	line::spn::SpnMetrics< T >
	The stationary measures of Sec. More...

Namespaces
namespace	line
namespace	line::spn

Functions
template<class T>
SpnMetrics< T >	line::spn::spn_metrics (const mdd::MddStruct &mdds, const std::vector< std::vector< T > > &g, const SpnInfo< T > &info)
	Every measure of Sec.

Detailed Description

Stationary measures of a product-form stochastic Petri net from the MDD-rec masses.

S. Balsamo, A. Marin, I. Stojic, FGCS 111 (2020) 475-490, Sec. 3.1 for the definitions and Sec. 5.3 for the recursions they are read off.

n(P_j) = sum_k k P(m_j = k) mean tokens u(P_j) = 1 - P(m_j = 0) place utilization u(T_j) = P(e_j >= 1) transition utilization x(T_j) = sum_k min(k, c_j) W(T_j) P(e_j = k) throughput x(P_j) = sum_T I_j(T) x(T) tokens removed per unit time

ONE DEVIATION FROM THE PAPER'S x(T_j), AND IT IS A GENERALISATION. The paper writes x(T_j) = sum_k k W(T_j) P(e_j = k), which is INFINITE-SERVER firing semantics – every enabling set fires in parallel. LINE's own rate law is min(enabling degree, nmodeservers) * W(T), so c_j above is the mode's server count: c_j = 1 recovers single-server semantics, x = W(T) P(e >= 1), and c_j = infinity recovers the paper's formula exactly. Using the paper's form for a single-server mode would report a throughput that grows with the token population of a net whose transition can only fire one set at a time.

The measures come out of ONE reachable set and ONE set of g_l, so they are mutually consistent by construction: no per-measure fixed point, no iteration.

Definition in file spn_metrics.h.