public static enum ReplayAlgorithm.Debug extends java.lang.Enum<ReplayAlgorithm.Debug>
Modifier and Type | Method and Description |
---|---|
static java.io.PrintStream |
getOutputStream()
Returns the output stream currently set.
|
void |
print(ReplayAlgorithm.Debug db,
java.lang.String s) |
void |
println(ReplayAlgorithm.Debug db) |
void |
println(ReplayAlgorithm.Debug db,
java.lang.String s) |
static void |
setOutputStream(java.io.PrintStream out)
Sets the output stream.
|
static ReplayAlgorithm.Debug |
valueOf(java.lang.String name)
Returns the enum constant of this type with the specified name.
|
static ReplayAlgorithm.Debug[] |
values()
Returns an array containing the constants of this enum type, in
the order they are declared.
|
void |
writeEdgeTraversed(ReplayAlgorithm algorithm,
int fromMarking,
int transition,
int toMarking) |
void |
writeEdgeTraversed(ReplayAlgorithm algorithm,
int fromMarking,
int transition,
int toMarking,
java.lang.String extra)
Should be called when an edge is traversed in the search from marking with ID
fromMarking to marking with ID toMarking though firing transition.
|
void |
writeMarkingReached(ReplayAlgorithm algorithm,
int marking) |
void |
writeMarkingReached(ReplayAlgorithm algorithm,
int marking,
java.lang.String extra) |
public static final ReplayAlgorithm.Debug DOT
public static final ReplayAlgorithm.Debug NORMAL
public static final ReplayAlgorithm.Debug NONE
public static final ReplayAlgorithm.Debug STATS
public static ReplayAlgorithm.Debug[] values()
for (ReplayAlgorithm.Debug c : ReplayAlgorithm.Debug.values()) System.out.println(c);
public static ReplayAlgorithm.Debug valueOf(java.lang.String name)
name
- the name of the enum constant to be returned.java.lang.IllegalArgumentException
- if this enum type has no constant with the specified namejava.lang.NullPointerException
- if the argument is nullpublic void writeEdgeTraversed(ReplayAlgorithm algorithm, int fromMarking, int transition, int toMarking, java.lang.String extra)
algorithm
- fromMarking
- transition
- toMarking
- extra
- public void writeMarkingReached(ReplayAlgorithm algorithm, int marking, java.lang.String extra)
public void writeEdgeTraversed(ReplayAlgorithm algorithm, int fromMarking, int transition, int toMarking)
public void writeMarkingReached(ReplayAlgorithm algorithm, int marking)
public void println(ReplayAlgorithm.Debug db, java.lang.String s)
public void println(ReplayAlgorithm.Debug db)
public void print(ReplayAlgorithm.Debug db, java.lang.String s)
public static void setOutputStream(java.io.PrintStream out)
out
- public static java.io.PrintStream getOutputStream()