spn_reachprops.h File Reference

Behavioural properties of a stochastic Petri net from its reachability graph (Murata 1989, sec. More...

#include <algorithm>
#include <cstddef>
#include <limits>
#include <string>
#include <vector>
#include "line/api/spn/spn_reachgraph.h"

Include dependency graph for spn_reachprops.h:

Go to the source code of this file.

Classes
struct	line::spn::SpnReachProps

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

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

Detailed Description

Behavioural properties of a stochastic Petri net from its reachability graph (Murata 1989, sec.

IV; Haverkort 1998, sec. 14.2), under the GSPN firing rule of spn_reachgraph, so inhibitor arcs, priorities and immediate events are honoured. Verdicts are tri-state: 1 true, 0 false, -1 unknown. On a complete graph: bounded = 1 and bound(l) is the largest token count of level l; deadlocks are the markings where nothing may fire; live(e) = 1 (L4-live) iff e labels an edge leaving a marking of every bottom strongly connected component; dead(e) = 1 iff e never fires; reversible = 1 iff there is one bottom SCC and it holds m0. On an unbounded or capped graph, bounded is 0 or -1, bound is NaN (Inf on the proven unbounded levels), a found deadlock makes deadlockfree, every live(e) and (when it is not m0) reversible 0, and the other verdicts are -1. MATLAB twin: matlab/src/api/spn/spn_reachprops.m.

Definition in file spn_reachprops.h.