spn_rec_enabled.h File Reference

Enabling-degree distribution of one mode of a product-form stochastic Petri net, by the masked MDD-rec recursion. More...

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

Include dependency graph for spn_rec_enabled.h:

Go to the source code of this file.

Classes
struct	line::spn::SpnEnabling< T >
	Unnormalised enabling-degree masses of one mode. More...

Namespaces
namespace	line
namespace	line::spn

Functions
template<class T>
SpnEnabling< T >	line::spn::spn_rec_enabled (const mdd::MddStruct &mdds, const std::vector< std::vector< T > > &g, const SpnMode< T > &mde, std::size_t nplacelevels)
	Enabling-degree masses of mode mde over the reachable set in mdds.

Detailed Description

Enabling-degree distribution of one mode of a product-form stochastic Petri net, by the masked MDD-rec recursion.

S. Balsamo, A. Marin, I. Stojic, FGCS 111 (2020) 475-490, Sec. 5.3.

The enabling degree of a mode in marking m is

e(m) = min_{l : I_l > 0} floor(m_l / I_l),

zero when any inhibitor threshold is met. P(e >= k) is therefore the mass of the marking subset in which EVERY input level holds at least k*I_l tokens and no inhibitor fires, which is a per-level restriction and so exactly what mdd::mdd_rec_masked computes: the paper's second modified recurrence is the same walk under a different mask, not a second algorithm.

The masses returned are UNNORMALISED, as in the paper; divide by G from mdd::mdd_rec for probabilities. spn_metrics does that and turns them into the transition measures.

Definition in file spn_rec_enabled.h.