---

CaseNode Class Reference

Inheritance diagram for CaseNode:[legend]Collaboration diagram for CaseNode:[legend]List of all members.

Public Methods
	CaseNode ()
	CaseNode (int capacity)
	CaseNode (Case x)
void	addCase (String cond, TreeNode node)
void	addCase (String cond, String expr)
void	addElement (Case x)
void	addTrapCase (String cond, String desc, boolean fatal)
Object	clone ()
TreeNode	compose (TreeNode tree, Case context)
Case	elementAt (int pos)
Case	firstElement ()
TreeNode	getCase (String cond)
Vector	getLeafCases (Vector leafCases)
Vector	getLeaves (Vector leaves)
int	indexOf (Case x)
void	insertElementAt (Case x, int pos)
void	print (int level)
int	size ()
TreeNode	specialize (ExprNode leaf, Case context)
Private Methods
boolean	conditionInconsistent (String cond, Case context)
boolean	conditionRedundant (String cond, Case context)
void	expand ()
void	indent (int level)
Private Attributes
int	size = 0
Case[]	data

---

Detailed Description

Case node of case tree.

A case node represents a conditional expression. Each case has a condition and a value (another case tree node). The cases must be mutually exclusive and the last case must be the default (i.e., is the value of the expression if all the previous conditions are false).

Definition at line 50 of file CaseNode.java.

---

Member Function Documentation

Object CaseNode::clone (    )  [inline]

Make a copy of this CaseNode (and its Cases). Definition at line 83 of file CaseNode.java.

TreeNode CaseNode::compose (  TreeNode   tree, Case   context )  [inline]

Compose this case node with another case tree. Basically this just clones the original case tree all the way down to the leaves so that when we append the other tree to the leaf, we don't change the original case tree. The context argument is used to allow nodes to update their parent pointers. Reimplemented from TreeNode. Definition at line 100 of file CaseNode.java.

boolean CaseNode::conditionInconsistent (  String   cond, Case   context )  [inline, private]

Check if case is inconsistent (conflicts with some parent case's condition). We do a simple text-based match on the expressions looking for certain common patterns. This is not a general constraint consistency check (which is OK, since if we fail to detect an inconsistency, it just results in more PROMELA code, not an incorrect model). In particular, we look for conditions of the form "x == S" and "x == R" where S does not equal R. Definition at line 123 of file CaseNode.java.

boolean CaseNode::conditionRedundant (  String   cond, Case   context )  [inline, private]

Check if condition is redundant (appears as condition of some parent case). Definition at line 145 of file CaseNode.java.

Vector CaseNode::getLeafCases (  Vector   leafCases )  [inline]

Collect all leaf cases (Case nodes with ExprNode values) into the vector. Reimplemented from TreeNode. Definition at line 177 of file CaseNode.java. Referenced by SpinTrans::caseAssignAction(), and SpinTrans::caseNewArrayExpr().

Vector CaseNode::getLeaves (  Vector   leaves )  [inline]

Collect all leaves (ExprNodes) into the vector. Reimplemented from TreeNode. Definition at line 190 of file CaseNode.java. Referenced by SpinTrans::caseAssertAction(), and SpinTrans::caseLockAction().

TreeNode CaseNode::specialize (  ExprNode   leaf, Case   context )  [inline]

Specialize a case tree to a given context. Like compose() above, this clones the case tree as it walks over it (the second case tree being composed), and it specializes as it constructs the new cases. In particular: If some case's condition appeared in a parent case, then we specialize the CaseExpr to the value of that case's condition. If the first N-1 case conditions are inconsistent with the conditions in the parent cases, then we specialize the CaseExpr to the value of the last case. Reimplemented from TreeNode. Definition at line 245 of file CaseNode.java.

---

The documentation for this class was generated from the following file:

• CaseNode.java

---