spn_mdd.h File Reference

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

#include <algorithm>
#include <cmath>
#include <cstddef>
#include <limits>
#include <set>
#include <string>
#include <vector>
#include "line/api/mdd/mdd.h"
#include "line/api/mdd/mdd_types.h"
#include "line/api/mam/map_moment.h"
#include "line/lang/distribution.h"
#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_mdd.h:

Go to the source code of this file.

Classes
struct	line::spn::SpnMode< T >
	One (transition, mode) pair of the net, in level coordinates. More...
struct	line::spn::SpnInfo< T >
	Everything the caller needs alongside the descriptor. More...
struct	line::spn::SpnResult< T >
	Descriptor, diagram and metadata returned together. More...
struct	line::spn::SpnOptions
	Options of the translation. More...

Namespaces
namespace	line
namespace	line::spn

Functions
template<class T>
SpnResult< T >	line::spn::spn_mdd (const qn::NetworkStruct< T > &sn, const SpnOptions &options=SpnOptions())
	Build the reachable set and Kronecker descriptor of a stochastic Petri net.

Detailed Description

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

Port of matlab/src/api/spn/spn_mdd.m, jline.api.spn.Spn_mdd and python/line_solver/api/spn/mdd.py.

Levels are of two kinds. PLACE LEVELS hold a token count, one per Place. PHASE LEVELS hold the phase the running server of a multi-phase mode occupies, one per such mode.

ONE LEVEL PER PLACE, NOT PER (PLACE, CLASS). The other three codebases carry (nnodes x nclasses) arc matrices and so give a multiclass net P*R place levels. This port reads NetworkStruct::transparam, whose enabling, firing and inhibiting arcs are per (mode, NODE) with no class dimension – which is also how state_events.h evaluates them, summing the marking over classes before every test. A multiclass net is therefore REJECTED here rather than silently collapsed onto class-aggregated levels: the aggregation would be a different model, not an approximation of this one. Single-class nets, which is what an SPN normally is, agree level for level with the other codebases.

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.

The initial marking comes from the reference station of each closed class (SpnOptions::init overrides it): unlike the object-graph codebases, a NetworkStruct carries no per-place state to read instead.

Definition in file spn_mdd.h.