Package jline.api.spn

Class Spn_reachprops

java.lang.Object

jline.api.spn.Spn_reachprops

public class Spn_reachprops
extends Object

Behavioural properties of a generalised stochastic Petri net, read off its reachability graph (Spn_reachgraph, which honours inhibitor arcs, priorities and immediate precedence).

Verdicts are tri-state: 1 holds, 0 fails, -1 undetermined (graph not complete). bounded with the per-level bound (infinite where proven unbounded, NaN where undetermined); deadlockfree with the dead markings; live, per event, L4 liveness (the event labels an edge in every bottom strongly connected component); dead, per event, never fires; reversible, a single bottom component holding m0. A truncated graph still settles some verdicts: a dead marking makes deadlockfree and every live entry 0, and reversible 0 unless it is m0; an event seen firing is not dead.

Reference: T. Murata, Proc. IEEE 77(4) (1989), Secs. IV and V-A.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	Spn_reachprops.SpnReachProps	The behavioural verdicts.

Method Summary

Modifier and Type	Method	Description
static Spn_reachprops.SpnReachProps	spn_reachprops(NetworkStruct sn)
static Spn_reachprops.SpnReachProps	spn_reachprops(NetworkStruct sn, double[] init)
static Spn_reachprops.SpnReachProps	spn_reachprops(NetworkStruct sn, double[] init, int maxstates)	Behavioural properties of a net.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Details

spn_reachprops

public static Spn_reachprops.SpnReachProps spn_reachprops(NetworkStruct sn)

spn_reachprops

public static Spn_reachprops.SpnReachProps spn_reachprops(NetworkStruct sn,
 double[] init)

spn_reachprops

public static Spn_reachprops.SpnReachProps spn_reachprops(NetworkStruct sn,
 double[] init,
 int maxstates)

Behavioural properties of a net.

Parameters:

sn - a NetworkStruct of a closed model holding Places and Transitions

init - initial tokens per place level, as in Spn_siphons

maxstates - maximum number of stored markings

Returns:

the verdicts