---

SmvVar Class Reference

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

Public Methods
	SmvVar (String name)
	SmvVar (String name, String type, StateVar source, SmvLit initVal, boolean constrained, SmvVar deadFlag)
void	addComponent (SmvVar var)
void	addUpdate (SmvExpr cond, SmvExpr assign)
SmvVar	getComponent (int i)
Vector	getComponents ()
SmvVar	getDeadFlag ()
SmvLit	getInitValue ()
String	getName ()
StateVar	getSource ()
String	getType ()
SmvExpr	getUpdateExpr ()
boolean	isBig ()
boolean	isConstrained ()
void	print (SmvTrans out)
void	setAggregate (SmvVar var)
void	setPrintForm (String printForm)
String	toString ()
Private Attributes
String	name
String	type
StateVar	source
SmvLit	initValue
SmvVar	aggregate
Vector	components
boolean	constrained
SmvVar	deadFlag
String	printForm
SmvExpr	updateExpr
SmvNaryExpr	updates
SmvNaryExpr	negUpdateConds

---

Detailed Description

An SMV variable.

Definition at line 43 of file SmvVar.java.

---

Constructor & Destructor Documentation

SmvVar::SmvVar (  String   name )  [inline]

Create a temp SmvVar used only to hold a prefix of a name (not declared). Definition at line 63 of file SmvVar.java.

---

Member Function Documentation

void SmvVar::addUpdate (  SmvExpr   cond, SmvExpr   assign )  [inline]

Add conditional update to variable. The expression "cond -> assign" is added to the conjunction of updates, and the negated condition is recorded in negUpdateConds (which forms the condition of the "variable unchanged" update). Definition at line 87 of file SmvVar.java. Referenced by SmvTrans::caseDerefExpr(), SmvTrans::caseNewArrayExpr(), SmvTrans::caseNewExpr(), SmvTrans::checkAssign(), SmvTrans::initAllComponents(), SmvTrans::recordGlobalVarAssignments(), SmvTrans::recordLockStatusUpdates(), and SmvTrans::recordThreadStatusUpdates().

SmvExpr SmvVar::getUpdateExpr (    )  [inline]

Build the update expression (TRANS formula) for the variable This must be called after all conditional updates have been added. To form the update expression, we use the conjunction of all the negated conditions to build one last update, specifying the variable is unchanged if none of the update conditions is true. We then add this last update to the update conjunction, which becomes the update expression. Finally, if there is a dead flag, then we allow the formula to be true if that variable is false OR the update expression is true. Definition at line 115 of file SmvVar.java. Referenced by SmvTrans::translateGlobal().

---

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

• SmvVar.java

---