Package jline.api.spn

Class Spn_reachgraph.SpnReachGraph

java.lang.Object

jline.api.spn.Spn_reachgraph.SpnReachGraph

Enclosing class:

Spn_reachgraph

public static class Spn_reachgraph.SpnReachGraph
extends Object

The reachability graph.

Field Summary

Fields

Modifier and Type	Field	Description
int[][]	E	E[r] = {from, to, event}, all 0-based.
long[][]	M	M[s][l]: tokens on level l in marking s (discovery order, 0 is m0).
long[]	m0
int[]	modes
int[]	places
String	status	"complete", "unbounded" or "cap".
boolean[]	tangible	True where no immediate event may fire.
int[]	transitions
boolean[]	unboundedlevels	Levels proven unbounded (status "unbounded" only).

Constructor Summary

Constructors

Constructor	Description
SpnReachGraph()

Method Summary

Methods inherited from class java.lang.Object

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

Field Details

places

public int[] places

transitions

public int[] transitions

modes

public int[] modes

M

public long[][] M

M[s][l]: tokens on level l in marking s (discovery order, 0 is m0).

E

public int[][] E

E[r] = {from, to, event}, all 0-based.

tangible

public boolean[] tangible

True where no immediate event may fire.

status

public String status

"complete", "unbounded" or "cap".

unboundedlevels

public boolean[] unboundedlevels

Levels proven unbounded (status "unbounded" only).

m0

public long[] m0

Constructor Details

SpnReachGraph

public SpnReachGraph()