public class SyncProductImpl extends java.lang.Object implements SyncProduct
| Modifier and Type | Field and Description |
|---|---|
protected int[] |
cost |
protected int[][] |
eventNumbers |
protected byte[] |
finalMarking |
protected byte[] |
initMarking |
protected int[][] |
input |
protected java.lang.String |
label |
protected int[][] |
output |
protected java.lang.String[] |
places |
protected int[] |
ranks |
protected java.lang.String[] |
transitions |
DLOG_MOVE, LOG_MOVE, MAXTRANS, MODEL_MOVE, NOEVENT, NORANK, PSYNC_MOVE, PSYNC_MOVE_T2, SYNC_MOVE, SYNC_MOVE_T2, TAU_MOVE| Constructor and Description |
|---|
SyncProductImpl(java.lang.String label,
int numClasses,
java.lang.String[] transitions,
java.lang.String[] places,
int[][] eventNumbers,
int[] ranks,
int[] pathLengths,
byte[] types,
int[] cost) |
| Modifier and Type | Method and Description |
|---|---|
void |
addToFinalMarking(int... places) |
void |
addToInitialMarking(int... places) |
void |
addToInput(int t,
int... p) |
void |
addToOutput(int t,
int... p) |
int |
getCost(int t)
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 p)
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)
for full alignments: return Arrays.equals(marking, finalMarking);
for prefix alignments: check only if a specific place is marked.
|
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.
|
void |
setEventOf(int transition,
int[] event) |
void |
setFinalMarking(byte[] marking) |
void |
setFinalMarking(int... places) |
void |
setInitialMarking(byte[] marking) |
void |
setInitialMarking(int... places) |
void |
setInput(int t,
int... plist) |
void |
setOutput(int t,
int... plist) |
void |
setPlaceLabel(int p,
java.lang.String label) |
void |
setRankOf(int transition,
int rank) |
void |
setTransitionLabel(int t,
java.lang.String label) |
protected final java.lang.String[] transitions
protected final int[][] eventNumbers
protected final int[] ranks
protected final java.lang.String[] places
protected final int[] cost
protected final int[][] input
protected final int[][] output
protected byte[] initMarking
protected byte[] finalMarking
protected final java.lang.String label
public SyncProductImpl(java.lang.String label,
int numClasses,
java.lang.String[] transitions,
java.lang.String[] places,
int[][] eventNumbers,
int[] ranks,
int[] pathLengths,
byte[] types,
int[] cost)
public int numTransitions()
SyncProductnumTransitions in interface SyncProductpublic int numPlaces()
SyncProductnumPlaces in interface SyncProductpublic void setInput(int t,
int... plist)
public void setOutput(int t,
int... plist)
public void addToOutput(int t,
int... p)
public void addToInput(int t,
int... p)
public int[] getInput(int transition)
SyncProductgetInput in interface SyncProductpublic int[] getOutput(int transition)
SyncProductgetOutput in interface SyncProductpublic byte[] getInitialMarking()
SyncProductgetInitialMarking in interface SyncProductpublic byte[] getFinalMarking()
SyncProductgetFinalMarking in interface SyncProductpublic void setInitialMarking(byte[] marking)
public void setFinalMarking(byte[] marking)
public void setInitialMarking(int... places)
public void addToInitialMarking(int... places)
public void setFinalMarking(int... places)
public void addToFinalMarking(int... places)
public int getCost(int t)
SyncProductgetCost in interface SyncProductpublic java.lang.String getTransitionLabel(int t)
SyncProductgetTransitionLabel in interface SyncProductpublic java.lang.String getPlaceLabel(int p)
SyncProductgetPlaceLabel in interface SyncProductpublic void setTransitionLabel(int t,
java.lang.String label)
public void setPlaceLabel(int p,
java.lang.String label)
public boolean isFinalMarking(byte[] marking)
isFinalMarking in interface SyncProductpublic java.lang.String getLabel()
SyncProductgetLabel in interface SyncProductpublic int[] getEventOf(int transition)
SyncProductgetEventOf in interface SyncProductpublic void setEventOf(int transition,
int[] event)
public byte getTypeOf(int transition)
SyncProductgetTypeOf in interface SyncProductpublic int numEvents()
SyncProductnumEvents in interface SyncProductpublic int getRankOf(int transition)
SyncProductgetRankOf in interface SyncProductpublic void setRankOf(int transition,
int rank)
public int numEventClasses()
SyncProductnumEventClasses in interface SyncProductpublic int numModelMoves()
SyncProductnumModelMoves in interface SyncProductpublic int getTransitionPathLength(int transition)
SyncProductgetTransitionPathLength in interface SyncProduct