Check State Machine Uses

This algorithm traverses a state machine definition and checks that each use of a state machine symbol refers to a definition. It also constructs the use-def map in the state machine analysis.

Input

1. A state machine definition smd.

2. A state machine analysis data structure sma representing the results of analysis so far.

Output

1. A state machine analysis data structure sma with updated use-def map.

Procedure

Visit each of the state machine members smm of smd as specified below.

Visiting State Machine Members

Visit a state machine member smm as follows:

1. Initial transition specifiers: If smm is an initial transition specifier, then visit its transition expression.

2. Choice definitions: If smm is a choice definition, then

   1. Visit the identifier following the keyword if in the guard name group.

   2. Visit each of the two transition expressions.

3. State definitions: If smm is a state definition d with name n, then

   1. Construct the unique state symbol sym corresponding to d.

   2. Look up the mapping from sym to s in the symbol-scope map of sma. If no such mapping exists, then throw an internal error.

   3. Push s onto the nested scope of sma.

   4. Visit each member of d.

   5. Pop s off the nested scope of sma.

4. Other members: For other state machine members, do nothing.

Visiting State Definition Members

Visit a state definition member sdm as follows:

1. Initial transition specifiers, choice definitions, and state definitions: If sdm is an initial transition specifier, choice definition, or state definition, then visit it as specified for the corresponding state machine member.

2. State transition specifiers: If smm is a state transition specifier, then do the following:

   1. Let n be the identifier following the keyword on. Visit n in the signal name group.

   2. If an if clause is present, then visit its identifier in the guard name group.

   3. Visit each of the identifiers in the action list of smm in the action name group.

   4. If a transition expression is present, then visit it.

Visiting Transition Expressions

Visit a transition expression e as follows:

1. Visit the each identifier in the action list of e in the action name group.

2. Let q be the qualified identifier appearing after the keyword enter in e. Visit q in the state name group.

Visiting Identifiers

Visit an identifier n in name group G as follows:

1. Look up the mapping from n to sym in the innermost nested scope of sma in name group G. If no such mapping exists, then throw a semantic error.

2. Record the mapping from n to sym in the use-def map of sma.

Visiting Qualified Identifiers

Visit a qualified identifier q in name group G as follows:

1. Unqualified names: If q is an unqualified name n, then visit the identifier n in name group G.

2. Qualified names: Otherwise if q is a qualified name q'.n, then

   1. Visit q'.

   2. Look up the mapping from q' to sym' in the use-def map of sma. If no such mapping exists, then throw an internal error.

   3. Look up the mapping from sym' to s in the symbol-scope map of sma. If no such mapping exists, then throw a semantic error.

   4. Look up the mapping from n to sym in s. If no such mapping exists, then throw a semantic error.

   5. Record the mapping from q to sym in the use-def map of sma.