Compares two process models (given in binary files created by cs2ccmb) and checks whether the first one is a consistent abstraction of the second. The mode of operation (similarity or bisimilarity) is determined by the field 'bisim'.
|
Static Public Member Functions |
Model | loadModel (string filename) |
| Load (deserialize) model from given binary file. On failure, the error is printed and null is returned.
|
int | Main (string[] args) |
| Main.
|
bool | searchImpl (Node a, Node i, Node asucc) |
| Search an i-successor that matches asucc.
|
bool | searchAbstr (Node a, Node i, Node isucc) |
| Search an a-successor that matches isucc.
|
bool | similar (Node anode, Node inode) |
| Check whether given nodes are similar wrt.
|
Static Private Attributes |
Model | abstr |
| Abstract model.
|
Model | impl |
| Implementation model.
|
StatePredicate | implPred |
| Predicate for implementation states (states not contained in this do not need to satisfy bisimulation requirements).
|
PairSet | vert = new PairSet() |
| Vertices of the bisimulation graph (contains (Node,Node) ).
|
PairSet | edges = new PairSet() |
| Edges of the bisimulation graph; contains predecessor pairs (Pair',Pair), where the pairs are vertices (Node,Node).
|
PairSet | unrelated = new PairSet() |
| Set of node pairs that are known to be unrelated.
|
bool | bisim = false |
Debugging.Logger | log = new Debugging.Logger() |
| Logger for debugging output.
|
bool | debug = false |
| Flag wheter checking is verbose (for debugging).
|
int | numNodes = 0 lastPrintedNodes = 0 |