Main Page | Namespace List | Class Hierarchy | Class List | File List | Class Members

CCM::SimChecker Class Reference

List of all members.

Detailed Description

(Bi)similarity checker.

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


Member Function Documentation

Model CCM::SimChecker::loadModel string  filename  )  [static]
 

Load (deserialize) model from given binary file. On failure, the error is printed and null is returned.

int CCM::SimChecker::Main string[]  args  )  [static]
 

Main.

bool CCM::SimChecker::searchAbstr Node  a,
Node  i,
Node  isucc
[static]
 

Search an a-successor that matches isucc.

If a match is found, a new edge is put into edges and true is returned; otherwise returns false.

Parameters:
a Node that abstracts node i
i Node that implements node a
isucc Successor node of i for which a corresponding a-successor is to be searched

bool CCM::SimChecker::searchImpl Node  a,
Node  i,
Node  asucc
[static]
 

Search an i-successor that matches asucc.

If a match is found, a new edge is put into edges and true is returned; otherwise returns false.

Parameters:
a Node that abstracts node i
asucc Successor node of a for which a corresponding i-successor is to be searched
i Node that implements node a

bool CCM::SimChecker::similar Node  anode,
Node  inode
[static]
 

Check whether given nodes are similar wrt.

to the given abstraction relations. If this.bisim==true, then it checks for bisimilarity.

Parameters:
anode Abstract node
inode Implementation node


Member Data Documentation

Model CCM::SimChecker::abstr [static, private]
 

Abstract model.

bool CCM::SimChecker::bisim = false [static, private]
 

bool CCM::SimChecker::debug = false [static, private]
 

Flag wheter checking is verbose (for debugging).

PairSet CCM::SimChecker::edges = new PairSet() [static, private]
 

Edges of the bisimulation graph; contains predecessor pairs (Pair',Pair), where the pairs are vertices (Node,Node).

Model CCM::SimChecker::impl [static, private]
 

Implementation model.

StatePredicate CCM::SimChecker::implPred [static, private]
 

Predicate for implementation states (states not contained in this do not need to satisfy bisimulation requirements).

Debugging.Logger CCM::SimChecker::log = new Debugging.Logger() [static, private]
 

Logger for debugging output.

int CCM::SimChecker::numNodes = 0 lastPrintedNodes = 0 [static, private]
 

PairSet CCM::SimChecker::unrelated = new PairSet() [static, private]
 

Set of node pairs that are known to be unrelated.

PairSet CCM::SimChecker::vert = new PairSet() [static, private]
 

Vertices of the bisimulation graph (contains (Node,Node) ).


The documentation for this class was generated from the following file:
Generated on Mon Jun 21 01:20:50 2004 for cs2ccmb by doxygen 1.3.7