Package jline.api.spn

Class Spn_reachgraph

java.lang.Object

jline.api.spn.Spn_reachgraph

public class Spn_reachgraph
extends Object

Untimed reachability graph of a generalised stochastic Petri net, over the markings of the place levels.

Built breadth-first from m0 under the GSPN firing rules of LINE's simulator: an event is enabled when every input level holds its pre multiplicity and no inhibitor threshold is reached; when an IMMEDIATE event is enabled only the enabled immediate events of the highest firing priority may fire (the marking is vanishing), otherwise every enabled timed event may. Markings are numbered in discovery order, successors in event order, so the numbering matches the other codebases.

status is "complete"; "unbounded" when a new marking strictly covers a BFS ancestor in a MONOTONE net (no inhibitor arc, immediate precedence or priority), which proves the levels where it grows (unboundedlevels) unbounded and stops the search; or "cap" when maxstates markings were stored and another was found. A queueing place is refused.

References: T. Murata, Proc. IEEE 77(4) (1989), Sec. V-A; B.R. Haverkort, Performance of Computer Communication Systems, Wiley, 1998, Ch. 14.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	Spn_reachgraph.SpnReachGraph	The reachability graph.

Field Summary

Fields

Modifier and Type	Field	Description
static final int	DEFAULT_MAXSTATES	Default cap on the stored markings.

Method Summary

Modifier and Type	Method	Description
static Spn_reachgraph.SpnReachGraph	spn_reachgraph(NetworkStruct sn)
static Spn_reachgraph.SpnReachGraph	spn_reachgraph(NetworkStruct sn, double[] init)
static Spn_reachgraph.SpnReachGraph	spn_reachgraph(NetworkStruct sn, double[] init, int maxstates)	The reachability graph.

Methods inherited from class java.lang.Object

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

Field Details

DEFAULT_MAXSTATES

public static final int DEFAULT_MAXSTATES

Default cap on the stored markings.

See Also:

• Constant Field Values

Method Details

spn_reachgraph

public static Spn_reachgraph.SpnReachGraph spn_reachgraph(NetworkStruct sn)

spn_reachgraph

public static Spn_reachgraph.SpnReachGraph spn_reachgraph(NetworkStruct sn,
 double[] init)

spn_reachgraph

public static Spn_reachgraph.SpnReachGraph spn_reachgraph(NetworkStruct sn,
 double[] init,
 int maxstates)

The reachability graph.

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 graph