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:

• sim.cs

---