public class MarkingGraph
extends java.lang.Object
| Modifier and Type | Field and Description |
|---|---|
java.util.ArrayList<java.lang.String> |
alphabet |
java.util.ArrayList<Edge> |
edges |
java.util.ArrayList<java.lang.Integer> |
final_markings |
int |
init_marking |
java.util.ArrayList<Marking> |
markings |
java.util.ArrayList<java.util.ArrayList<Edge>> |
next |
java.util.ArrayList<java.util.ArrayList<Edge>> |
prev |
| Constructor and Description |
|---|
MarkingGraph() |
| Modifier and Type | Method and Description |
|---|---|
void |
addEdge(int from,
int label,
int to) |
void |
addEdge(int from,
java.lang.String label,
int to) |
void |
addFinalMarking(int m) |
void |
addLabel(java.lang.String label) |
void |
calculatePrevPost() |
int |
findOrPut(Marking m) |
Marking |
getMarking(int m) |
void |
init() |
void |
setInitMarking(int m) |
public java.util.ArrayList<Marking> markings
public java.util.ArrayList<java.lang.String> alphabet
public java.util.ArrayList<Edge> edges
public int init_marking
public java.util.ArrayList<java.lang.Integer> final_markings
public java.util.ArrayList<java.util.ArrayList<Edge>> prev
public java.util.ArrayList<java.util.ArrayList<Edge>> next
public void init()
public void setInitMarking(int m)
public void addFinalMarking(int m)
public void addEdge(int from,
java.lang.String label,
int to)
public void addEdge(int from,
int label,
int to)
public void addLabel(java.lang.String label)
public Marking getMarking(int m)
public int findOrPut(Marking m)
public void calculatePrevPost()