---

SpinTypeInit Class Reference

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

Public Methods
	SpinTypeInit (SpinTrans spinTrans, PrintWriter out)
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)
Private Methods
Expr	initValue (Type type, Object context)
void	simpleInit (Type type, Object o)
String	varName (Object context)
Private Attributes
SpinTrans	spinTrans
PrintWriter	out

---

Detailed Description

BIR TypeSwitch to initialize a variable of a BIR type in PROMELA.

The Object parameter to the type switch case methods is a context indicating whether the variable being initialized is top-level. If the context is a StateVar, the variable is top-level and the name and initial value for the variable should be retrieved from that StateVar object. If the context is a String, then the variable is a component of a collection, record, or array, and the String is the fully qualified variable name. In this case, the initial value comes from the type of the variable.

SPIN claims to initialize most types to 0 automatically, so we omit such initializations.

Definition at line 58 of file SpinTypeInit.java.

---

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

• SpinTypeInit.java

---