---

SpinTypeName Class Reference

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

Public Methods
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)

---

Detailed Description

Type namer for SPIN translator.

Generates PROMELA types from BIR types.

Note: the Object parameter to the typeswitch case methods indicates the context. If null, the variable is top-level, so we want to generate the PROMELA type (e.g., bit, int, short, typedef {...} ). If non-null, the variable is nested inside of a record, array, or collection, so we want to simply return the defined name of the type (since PROMELA insists that struct field types be identifiers).

Definition at line 55 of file SpinTypeName.java.

---

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

• SpinTypeName.java

---