public class Dijkstra
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
Dijkstra.Full
Special version of Dijkstra that builds the entire search space, i.e.
|
ReplayAlgorithm.CloseResult, ReplayAlgorithm.Debug
Modifier and Type | Field and Description |
---|---|
protected int |
alignmentCost |
protected int |
alignmentLength |
protected int |
alignmentResult |
protected int |
block
Stores the last block in use
|
protected int |
blockBit
Stores the number of trailing 0's in the blockSize.
|
protected int |
blockMask
equals blockSize-1
|
protected int |
blockSize
Stores the blockSize as a power of 2
|
protected int |
closedActions |
protected int |
costUpperLimit |
protected ReplayAlgorithm.Debug |
debug
Stores the selected debug level
|
protected int |
edgesTraversed |
protected boolean |
enabledBlockedByCost |
protected static int |
HEURISTICINFINITE |
protected int |
heuristicsComputed |
protected int |
heuristicsDerived |
protected int |
heuristicsEstimated |
protected int |
indexInBlock
Stores the first new index in current block
|
protected int |
iteration |
protected int |
markingsReached |
protected int |
maximumNumberOfStates |
protected boolean |
moveSorting
Indicate if moves should be considered totally ordered.
|
protected SyncProduct |
net
The synchronous product under investigation
|
protected static int |
NOPREDECESSOR |
protected int |
numPlaces |
protected int |
pollActions |
protected boolean |
preferExact
Flag indicating if exact solutions should be kept separate
|
protected Queue |
queue
Stores the open set as a priority queue
|
protected int |
queueActions |
protected gnu.trove.map.TObjectIntMap<Utils.Statistic> |
replayStatistics |
protected static int |
RESTART |
protected int |
runTime |
protected int |
setupTime |
protected long |
startConstructor |
protected long |
timeoutAtTimeInMillisecond |
protected VisitedSet |
visited
Stores the closed set
|
Constructor and Description |
---|
Dijkstra(SyncProduct product) |
Dijkstra(SyncProduct product,
boolean moveSorting,
boolean queueSorting,
ReplayAlgorithm.Debug debug) |
Modifier and Type | Method and Description |
---|---|
int |
addNewMarking(byte[] marking)
Adds a new marking to the internal storage.
|
protected void |
addToQueue(int marking) |
protected ReplayAlgorithm.CloseResult |
closeOrUpdateMarking(int m,
byte[] marking_m,
int bm,
int im) |
protected void |
deriveOrEstimateHValue(int from,
int fromBlock,
int fromIndex,
int transition,
int to,
int toBlock,
int toIndex) |
boolean |
equalMarking(int marking1,
byte[] marking2)
Checks equality of the stored marking1 to the given marking2.
|
protected int |
expandMarking(int m,
byte[] marking_m,
int bm,
int im) |
protected void |
fillMarking(byte[] markingArray,
int marking) |
protected void |
fillStatistics(int[] alignment) |
protected void |
fire(byte[] marking,
int transition) |
protected byte[] |
fire(byte[] fromMarking,
int transition,
int block,
int index) |
protected int[] |
getAlignmentWhenEmptyQueueReached(long startTime) |
long |
getEstimatedMemorySize()
Estimates the memory size of the internal data structures in bytes.
|
int |
getExactHeuristic(int marking,
byte[] markingArray,
int markingBlock,
int markingIndex)
Dijkstra always estimates 0
|
int |
getFScore(int marking)
Returns the f score for a stored marking
|
int |
getFScore(int block,
int index)
Returns the f score for a stored marking
|
int |
getGScore(int marking)
Returns the g score for a stored marking
|
int |
getGScore(int block,
int index)
Returns the g score for a stored marking
|
int |
getHScore(int marking)
Returns the h score for a stored marking
|
int |
getHScore(int block,
int index)
Returns the h score for a stored marking
|
int |
getIterationNumber()
Returns the current iteration number of the algorithm if there are multiple
iterations in which the same marking IDs will be present.
|
int |
getLastRankOf(int marking)
Returns the highest rank of an event explained by the path through which the
stored marking with ID markingId was reached.
|
byte[] |
getMarking(int marking)
Returns the explicit representation of the marking stored with ID markingId.
|
SyncProduct |
getNet()
Returns the synchronous product for which this ReplayAlgorithm was
instantiated
|
int |
getPathLength(int marking)
returns the length of the path from the initial marking to reach this marking
|
int |
getPredecessor(int marking)
Returns the predecessor for a stored marking
|
int |
getPredecessor(int block,
int index)
Returns the predecessor for a stored marking
|
int |
getPredecessorTransition(int marking)
Returns the predecessor transition for a stored marking
|
int |
getPredecessorTransition(int block,
int index)
Returns the predecessor transition for a stored marking
|
gnu.trove.map.TObjectIntMap<Utils.Statistic> |
getStatistics()
Obtain the statistics after computing an alignment.
|
protected void |
growArrays()
Grow the internal array structure.
|
protected int[] |
handleFinalMarkingReached(long startTime,
int marking) |
boolean |
hasExactHeuristic(int marking)
returns true if the heuristic stored for the given marking is exact or an
estimate.
|
boolean |
hasExactHeuristic(int block,
int index)
returns true if the heuristic stored for the given marking is exact or an
estimate.
|
int |
hashCode(byte[] marking)
Returns the hashCode of a stored marking which is provided as an array of
length 2*bm, where the first bm bytes provide the low bits and the second bm
bytes provide the high bits.
|
int |
hashCode(int marking)
Returns the hashCode of a stored marking
|
boolean |
hasPlaceBetween(int preTransition,
int transition)
returns true if there is a place common in the output set of transitionFrom
and the input set of transitionTo
|
protected void |
initializeIteration() |
protected void |
initializeIterationInternal() |
boolean |
isClosed(int marking)
Returns true if marking is in the closed set
|
boolean |
isClosed(int block,
int index)
Returns the g score for a stored marking
|
protected boolean |
isEnabled(byte[] marking,
int transition,
int block,
int index) |
protected boolean |
isFinal(int marking)
To allow for prefix versions of this algorithm, ask the net if the given
marking is final.
|
boolean |
isInfinite(int heur)
Checks if a value for the h-score is INFINITE.
|
protected void |
processedMarking(int marking,
int blockMarking,
int indexInBlock) |
void |
putStatistic(Utils.Statistic stat,
int value)
Adds a statistic to the set of statistics.
|
int[] |
run(Canceler canceller,
int timeoutMilliseconds,
int maximumNumberOfStates,
int costUpperLimit)
Run the replay algorithm.
|
protected int[] |
runReplayAlgorithm(Canceler canceller,
long startTime,
int timeoutMilliseconds) |
void |
setClosed(int marking)
Set the g score for a stored marking
|
void |
setClosed(int block,
int index)
Set the g score for a stored marking
|
void |
setGScore(int marking,
int score)
Set the g score for a stored marking
|
void |
setGScore(int block,
int index,
int score)
Set the g score for a stored marking
|
void |
setHScore(int marking,
int score,
boolean isExact)
Set the h score for a stored marking
|
void |
setHScore(int block,
int index,
int score,
boolean isExact)
set the h score for a stored marking
|
void |
setPredecessor(int marking,
int predecessorMarking)
Sets the predecessor for a stored marking
|
void |
setPredecessor(int block,
int index,
int predecessorMarking)
Sets the predecessor for a stored marking
|
void |
setPredecessorTransition(int marking,
int transition)
Sets the predecessor transition for a stored marking
|
void |
setPredecessorTransition(int block,
int index,
int transition)
Sets the predecessor transition for a stored marking
|
protected void |
terminateIteration(int[] alignment,
int markingsReachedInRun,
int closedActionsInRun) |
protected void |
writeEdgeTraversed(ReplayAlgorithm algorithm,
int fromMarking,
int transition,
int toMarking,
java.lang.String extra) |
protected void |
writeEndOfAlignmentDot(int[] alignment,
int markingsReachedInRun,
int closedActionsInRun) |
protected void |
writeEndOfAlignmentNormal(int[] alignment,
int markingsReachedInRun,
int closedActionsInRun) |
protected void |
writeEndOfAlignmentStats(int[] alignment,
int markingsReachedInRun,
int closedActionsInRun) |
protected void |
writeStatus() |
protected static final int RESTART
protected VisitedSet visited
protected final SyncProduct net
protected Queue queue
protected boolean moveSorting
protected final ReplayAlgorithm.Debug debug
protected final boolean preferExact
protected int pollActions
protected int closedActions
protected int queueActions
protected int edgesTraversed
protected boolean enabledBlockedByCost
protected int markingsReached
protected int heuristicsComputed
protected int heuristicsEstimated
protected int heuristicsDerived
protected int alignmentLength
protected int alignmentCost
protected int setupTime
protected int runTime
protected int iteration
protected long startConstructor
protected int numPlaces
protected long timeoutAtTimeInMillisecond
protected int maximumNumberOfStates
protected int costUpperLimit
protected gnu.trove.map.TObjectIntMap<Utils.Statistic> replayStatistics
protected static int HEURISTICINFINITE
protected static final int NOPREDECESSOR
protected int alignmentResult
protected final int blockSize
protected final int blockBit
protected final int blockMask
protected int block
protected int indexInBlock
public Dijkstra(SyncProduct product)
public Dijkstra(SyncProduct product, boolean moveSorting, boolean queueSorting, ReplayAlgorithm.Debug debug)
public int getExactHeuristic(int marking, byte[] markingArray, int markingBlock, int markingIndex)
protected boolean isFinal(int marking)
protected void deriveOrEstimateHValue(int from, int fromBlock, int fromIndex, int transition, int to, int toBlock, int toIndex)
public gnu.trove.map.TObjectIntMap<Utils.Statistic> getStatistics()
ReplayAlgorithm
protected void fillStatistics(int[] alignment)
public long getEstimatedMemorySize()
ReplayAlgorithm
getEstimatedMemorySize
in interface ReplayAlgorithm
public int[] run(Canceler canceller, int timeoutMilliseconds, int maximumNumberOfStates, int costUpperLimit) throws nl.tue.astar.util.ilp.LPMatrixException
ReplayAlgorithm
canceller
- Allows for canceling the computationtimeoutMilliseconds
- Timeout for the computationmaximumNumberOfStates
- Maximum number of states expandedcostUpperLimit
- Maximum cost of the alignment. Providing an upperbound of 0 will
answer the yes/no question if the trace is fitting (assuming
synchronous and tau-moves have cost 0)nl.tue.astar.util.ilp.LPMatrixException
- Exceptions is thrown if there is a problem with the LP
computations.protected int[] runReplayAlgorithm(Canceler canceller, long startTime, int timeoutMilliseconds) throws nl.tue.astar.util.ilp.LPMatrixException
nl.tue.astar.util.ilp.LPMatrixException
protected int[] getAlignmentWhenEmptyQueueReached(long startTime)
protected int expandMarking(int m, byte[] marking_m, int bm, int im)
protected void writeEdgeTraversed(ReplayAlgorithm algorithm, int fromMarking, int transition, int toMarking, java.lang.String extra)
protected ReplayAlgorithm.CloseResult closeOrUpdateMarking(int m, byte[] marking_m, int bm, int im)
protected void initializeIteration() throws nl.tue.astar.util.ilp.LPMatrixException
nl.tue.astar.util.ilp.LPMatrixException
- in subclasses using (I)LPprotected void initializeIterationInternal()
protected void addToQueue(int marking)
protected void processedMarking(int marking, int blockMarking, int indexInBlock)
protected int[] handleFinalMarkingReached(long startTime, int marking)
protected void writeEndOfAlignmentStats(int[] alignment, int markingsReachedInRun, int closedActionsInRun)
protected void writeEndOfAlignmentNormal(int[] alignment, int markingsReachedInRun, int closedActionsInRun)
protected void writeEndOfAlignmentDot(int[] alignment, int markingsReachedInRun, int closedActionsInRun)
protected void terminateIteration(int[] alignment, int markingsReachedInRun, int closedActionsInRun)
protected byte[] fire(byte[] fromMarking, int transition, int block, int index)
protected void fire(byte[] marking, int transition)
protected boolean isEnabled(byte[] marking, int transition, int block, int index)
public boolean hasPlaceBetween(int preTransition, int transition)
transitionFrom
- transitionTo
- public byte[] getMarking(int marking)
ReplayAlgorithm
marking
- an ID of a previously stored marking (ID obtained through
addNewMarking())protected void fillMarking(byte[] markingArray, int marking)
public int addNewMarking(byte[] marking)
ReplayAlgorithm
marking
- the byte[] indicating the number of tokens per placeprotected void writeStatus()
public boolean equalMarking(int marking1, byte[] marking2)
marking1
- marking2
- SyncProduct.getInitialMarking();
public int hashCode(int marking)
marking
- public int hashCode(byte[] marking)
marking
- SyncProduct.getInitialMarking();
public SyncProduct getNet()
ReplayAlgorithm
public int getLastRankOf(int marking)
ReplayAlgorithm
marking
- an ID of a previously stored marking (ID obtained through
addNewMarking()public void putStatistic(Utils.Statistic stat, int value)
ReplayAlgorithm
public int getIterationNumber()
ReplayAlgorithm
public int getPathLength(int marking)
ReplayAlgorithm
protected void growArrays()
public int getGScore(int block, int index)
block
- the memory block the marking is stored inindex
- the index at which the marking is stored in the memory blockpublic void setGScore(int block, int index, int score)
block
- the memory block the marking is stored inindex
- the index at which the marking is stored in the memory blockpublic void setGScore(int marking, int score)
marking
- public int getHScore(int marking)
getHScore
in interface ReplayAlgorithm
marking
- public int getHScore(int block, int index)
block
- the memory block the marking is stored inindex
- the index at which the marking is stored in the memory blockpublic void setHScore(int block, int index, int score, boolean isExact)
block
- the memory block the marking is stored inindex
- the index at which the marking is stored in the memory blockpublic void setHScore(int marking, int score, boolean isExact)
marking
- public int getPredecessor(int marking)
marking
- public int getPredecessor(int block, int index)
block
- the memory block the marking is stored inindex
- the index at which the marking is stored in the memory blockpublic void setPredecessor(int block, int index, int predecessorMarking)
block
- the memory block the marking is stored inindex
- the index at which the marking is stored in the memory blockpublic void setPredecessor(int marking, int predecessorMarking)
marking
- public int getPredecessorTransition(int marking)
marking
- public int getPredecessorTransition(int block, int index)
block
- the memory block the marking is stored inindex
- the index at which the marking is stored in the memory blockpublic void setPredecessorTransition(int block, int index, int transition)
block
- the memory block the marking is stored inindex
- the index at which the marking is stored in the memory blockpublic void setPredecessorTransition(int marking, int transition)
marking
- public boolean isClosed(int marking)
isClosed
in interface ReplayAlgorithm
marking
- public boolean isClosed(int block, int index)
block
- the memory block the marking is stored inindex
- the index at which the marking is stored in the memory blockpublic void setClosed(int block, int index)
block
- the memory block the marking is stored inindex
- the index at which the marking is stored in the memory blockpublic void setClosed(int marking)
marking
- public int getFScore(int marking)
getFScore
in interface ReplayAlgorithm
marking
- public int getFScore(int block, int index)
block
- the memory block the marking is stored inindex
- the index at which the marking is stored in the memory blockpublic int getGScore(int marking)
getGScore
in interface ReplayAlgorithm
marking
- public boolean hasExactHeuristic(int marking)
hasExactHeuristic
in interface ReplayAlgorithm
marking
- public boolean hasExactHeuristic(int block, int index)
marking
- block
- the memory block the marking is stored inindex
- the index at which the marking is stored in the memory blockpublic boolean isInfinite(int heur)
ReplayAlgorithm
isInfinite
in interface ReplayAlgorithm
heur
- a value for the h-score