---

SmvTypeDecl Class Reference

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

Public Methods
	SmvTypeDecl (SmvTrans smvTrans, TransSystem sys)
void	caseArray (Array type, Object o)
void	caseBool (Bool type, Object o)
void	caseCollection (Collection type, Object o)
void	caseEnumerated (Enumerated type, Object o)
void	caseField (Field type, Object o)
void	caseLock (Lock type, Object o)
void	caseRange (Range type, Object o)
void	caseRecord (Record type, Object o)
void	caseRef (Ref type, Object o)
void	defaultCase (Object obj)
int	getMaxCollectionSize ()
Private Methods
String	initValue (Type type, Object context)
String	varName (Object context)
Private Attributes
SmvTrans	smvTrans
TransSystem	system
StateVar	source
SmvVar	container
boolean	constrained
SmvVar	deadFlag
String	refIndexType
String	instNumType
int	maxSize

---

Detailed Description

BIR type switch for declaring SMV state variables.

An instance of this class is created by SmvTrans to help it declare all the components of a BIR variable (composite types have multiple components). Variables are declared by callbacks to the SmvTrans object on declareVar().

The SmvTypeDecl is applied to each variable by its type, with the variable itself being passed to the caseXXX() method as the second parameter (the Object context).

If the type is composite, then we recursively apply the type switch to the components of the composite type, but the context parameter is then a string denoting the prefix of the SMV variable name for the components of that variable.

Note that the varName() method must be called at the top of each caseXXX() method to record the variable source and other parameters for the subsequent recursive calls (which will not get the StateVar as a param).

Definition at line 63 of file SmvTypeDecl.java.

---

Member Function Documentation

void SmvTypeDecl::caseArray (  Array   type, Object   o )  [inline]

Declare array variable. An array variable is an aggregate with the following components: A length variable recording the length of the array One or more variables for each possible array slot (created via recursive calls). Definition at line 106 of file SmvTypeDecl.java.

void SmvTypeDecl::caseBool (  Bool   type, Object   o )  [inline]

Declare boolean variable. Definition at line 125 of file SmvTypeDecl.java.

void SmvTypeDecl::caseCollection (  Collection   type, Object   o )  [inline]

Declare collection variable. A collection variable is an aggregate with the following components: An inuse variable for each possible collection instance, which is true if that instance has been allocated. One or more variables for each possible collection instance (created via recursive calls). Definition at line 143 of file SmvTypeDecl.java.

void SmvTypeDecl::caseEnumerated (  Enumerated   type, Object   o )  [inline]

Declare enumerated variable. Since we used named integer constants for each enumerated value, this is really just a range type. Definition at line 168 of file SmvTypeDecl.java.

void SmvTypeDecl::caseField (  Field   type, Object   o )  [inline]

Declare field variable. Definition at line 181 of file SmvTypeDecl.java.

void SmvTypeDecl::caseLock (  Lock   type, Object   o )  [inline]

Declare lock variable. A lock variable is an aggregate with the following components: An owner variable indicating which thread holds the lock A count variable, recording the number of acquisitions of the lock (for relocking) A wait variable for each thread indicating whether that thread is blocked in the wait queue of this lock Definition at line 199 of file SmvTypeDecl.java.

void SmvTypeDecl::caseRange (  Range   type, Object   o )  [inline]

Declare range variable. Definition at line 218 of file SmvTypeDecl.java.

void SmvTypeDecl::caseRecord (  Record   type, Object   o )  [inline]

Declare record variable. An record variable is an aggregate with one or more variables for each field (created via recursive calls). Definition at line 234 of file SmvTypeDecl.java.

void SmvTypeDecl::caseRef (  Ref   type, Object   o )  [inline]

Declare reference variable. A reference is an aggregate with the following components: a refIndex variable, specifying the target pointed to (or 0 for null) an instance variable, specifying the instance number of the collection. Note that reference variables are unusual in that they may appear as final values in expressions even though they are implemented as two variables. We solve this problem by defining a "printForm" for an SMV variable that is used to display the variable in a formula. The printForm of a reference R is (R_refIndex * MAX_COLLECT_SIZE + R_instNum), thus the two components (R_refIndex and R_instNum) are combined into a single integer for the purposes of assignment and equality tests. Dereferencing (the most common operation) uses the components seperately. Definition at line 268 of file SmvTypeDecl.java.

String SmvTypeDecl::initValue (  Type   type, Object   context )  [inline, private]

Get initial value of variable. If the context is a String, the variable is a component, so just use the default value of the type. Otherwise (context is StateVar), get the initial value of that variable and translate it. Definition at line 296 of file SmvTypeDecl.java.

String SmvTypeDecl::varName (  Object   context )  [inline, private]

Return the name of the variable indicated by the context. The context is either a StateVar (for a top-level call) or a String denoting a prefix of a name (for a nested call to declare the components of a composite type). This must be called at the top of each caseXXX() method to set the source, container, and constrained fields. Definition at line 315 of file SmvTypeDecl.java.

---

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

• SmvTypeDecl.java

---