public interface SyncProduct
Modifier and Type | Field and Description |
---|---|
static byte |
LOG_MOVE |
static int |
MAXTRANS |
static byte |
MODEL_MOVE |
static int[] |
NOEVENT |
static int |
NORANK |
static byte |
SYNC_MOVE |
static byte |
TAU_MOVE |
Modifier and Type | Method and Description |
---|---|
int |
getCost(int transition)
returns the cost of firing t.
|
int[] |
getEventOf(int transition)
returns the sequence of event numbers associated with this transition.
|
byte[] |
getFinalMarking()
Return the final marking
|
byte[] |
getInitialMarking()
Return the initial marking as an array where each byte represents the marking
of that specific place in the interval 0..3
|
int[] |
getInput(int transition)
Returns a sorted array of places serving as input to transition t
|
java.lang.String |
getLabel()
Returns the label of the synchronous product
|
int[] |
getOutput(int transition)
Returns a sorted array of places serving as output to transition t
|
java.lang.String |
getPlaceLabel(int place)
Return the label of a place
|
int |
getRankOf(int transition)
returns the rank of the transition.
|
java.lang.String |
getTransitionLabel(int t)
Returns the label of transition t
|
int |
getTransitionPathLength(int transition)
Returns the path length of firing this transition in the graph.
|
byte |
getTypeOf(int transition)
returns the type of the transion as a byte equal to one of the constants
defined in this class: LOG_MOVE, SYNC_MOVE, MODEL_MOVE, TAU_MOVE
|
boolean |
isFinalMarking(byte[] marking)
Checks if a given marking is the (a) final marking
|
int |
numEventClasses()
returns the number of event classes known to this product
|
int |
numEvents()
The number of events in the trace
|
int |
numModelMoves()
returns the number of model moves in this product
|
int |
numPlaces()
The number of places is in principle bounded Integer.MAX_VALUE
|
int |
numTransitions()
Returns the number of transitions.
|
static final byte LOG_MOVE
static final byte MODEL_MOVE
static final byte SYNC_MOVE
static final byte TAU_MOVE
static final int MAXTRANS
static final int[] NOEVENT
static final int NORANK
int numTransitions()
int numPlaces()
int numEvents()
int[] getInput(int transition)
transition
- int[] getOutput(int transition)
transition
- byte[] getInitialMarking()
byte[] getFinalMarking()
int getCost(int transition)
t
- java.lang.String getTransitionLabel(int t)
t
- boolean isFinalMarking(byte[] marking)
marking
- java.lang.String getPlaceLabel(int place)
p
- java.lang.String getLabel()
int[] getEventOf(int transition)
transition
- int getRankOf(int transition)
transition
- byte getTypeOf(int transition)
transition
- int numEventClasses()
int numModelMoves()
int getTransitionPathLength(int transition)
predecessorTransition
-