solver_nc_spn.h File Reference

Stationary analysis of a PRODUCT-FORM stochastic Petri net by MDD-rec. More...

#include <cmath>
#include <cstddef>
#include <string>
#include <vector>
#include "line/api/spn/spn_metrics.h"
#include "line/api/spn/spn_pf.h"
#include "line/lang/qn/network_struct.h"
#include "line/solvers/nc/nc_types.h"
#include "line/util/matrix.h"

Include dependency graph for solver_nc_spn.h:

Go to the source code of this file.

Classes
struct	line::nc::NcSpnSolution< T >
	The product-form solve, with the certificate that produced it. More...

Namespaces
namespace	line
namespace	line::nc

Functions
template<class T>
NcSpnSolution< T >	line::nc::solver_nc_spn_analyzer (const qn::NetworkStruct< T > &sn, const NcSolverOptions &opt)
	Analyse a product-form stochastic Petri net.

Detailed Description

Stationary analysis of a PRODUCT-FORM stochastic Petri net by MDD-rec.

The normalising constant is obtained from one memoised walk of the decision diagram holding the reachable set, and every reported measure is a masked walk of the same diagram.

This is the rec method of SolverNC, and the first analytical route LINE offers for a Petri net – CTMC solves the explicit generator, SSA and LDES simulate, FLD fluidises. Three functions do the work and each is the subject of its own reference:

spn_pf decides the product form and derives the per-place factors g_l (Coleman-Henderson-Taylor complex balance) mdd_rec G = sum_S prod_l g_l(s_l) in O(sum_l nodes_l * |S_l|) rather than O(|S|) (Balsamo-Marin-Stojic) spn_metrics mean tokens, place and mode utilisation, and throughputs, all from masked walks of the same diagram

WHAT THIS REACHES THAT THE EXPLICIT GENERATOR DOES NOT. The diagram stores the reachable set, never the generator, so the cost is set by the number of diagram nodes and not by |S|. It also does not need the marking to be a conserved job population: a mode may consume two tokens and produce one, or consume one and produce two, which is the fork-join and batch case that the MDD-rec paper exists to serve.

UN FOLLOWS LINE, NOT THE PAPER. A Place is an INF station, and LINE reports U = Q at an infinite server, which is what SolverCTMC returns for the same net. The paper's place utilisation u(P_j) = 1 - P(m_j = 0) is a different quantity and rides on the returned metrics block instead.

ARITHMETIC. spn_pf needs a transcendental field and says so; everything downstream of it – mdd_rec, spn_metrics – is rational.

See also

spn_pf, mdd_rec, spn_metrics, spn_mdd

Definition in file solver_nc_spn.h.