spn_reachgraph.h File Reference

Reachability graph of a stochastic Petri net under the GSPN firing rule (Haverkort 1998, sec. More...

#include <cstddef>
#include <map>
#include <string>
#include <vector>
#include "line/api/spn/spn_net.h"

Include dependency graph for spn_reachgraph.h:

Go to the source code of this file.

Classes
struct	line::spn::SpnReachGraph

Namespaces
namespace	line
	Conservation laws of a layered queueing network, enumerated from its structure.
namespace	line::spn

Functions
template<class T>
SpnReachGraph	line::spn::spn_reachgraph (const qn::NetworkStruct< T > &sn, const std::vector< double > &init=std::vector< double >(), std::size_t maxstates=0)

Variables
constexpr std::size_t	line::spn::SPN_REACH_MAXSTATES = 100000
	Default cap on the number of explored markings.

Detailed Description

Reachability graph of a stochastic Petri net under the GSPN firing rule (Haverkort 1998, sec.

14.2; Ajmone Marsan et al.). An event is enabled in m when m covers its enabling arcs and no inhibitor threshold is reached; when any immediate event is enabled only the enabled immediate events of the highest priority may fire, otherwise every enabled event may. The markings are found breadth first from m0 and numbered in discovery order; E lists the edges (from, to, event), 0-based.

status is "complete" when the graph is finite and fully explored, "cap" when maxstates markings were found and another one appeared, and "unbounded" when a new marking strictly covers one of its ancestors (Karp-Miller), which proves unboundedness only for a monotone net: the covering test runs only without inhibitor arcs, priorities and mixed timed/immediate events. unboundedlevels marks the strictly larger levels. tangible(i) is false when an immediate event may fire in marking i. QUEUEING places carry state the marking does not hold and are refused. MATLAB twin: matlab/src/api/spn/spn_reachgraph.m.

Definition in file spn_reachgraph.h.