Skip to content

Check State Machine Uses

Rob Bocchino edited this page Jul 17, 2024 · 17 revisions

This algorithm traverses a state machine source model and checks that each use refers to definition. It also constructs the use-def map.

Input

  1. A list tul of translation units.

  2. An analysis data structure a representing the results of analysis so far.

Output

  1. An analysis state machine data structure a with updated use-def map.

Procedure

  1. Translation unit lists: Visit each translation unit tu in tul in order.

  2. Translation units: Visit a translation unit tu by visiting its members tum.

  3. Translation unit members: Visit a translation unit member tum as follows:

    1. State machine definitions: Otherwise if tum is a state machine definition d then visit each translation unit member of d

    2. State definitions: Otherwise if tum 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 a. If no such mapping exists, then throw an internal error.

      3. Push s onto the nested scope of a.

      4. Visit each member of d.

      5. Pop s off the nested scope of a.

    3. Action definitions: If tum is a action definition, then visit the type name use appearing in tum.

    4. Guard definitions: If tum is a guard definition, then visit the type name use appearing in tum.

    5. Signal definitions: If tum is a signal definition, then visit the type name use appearing in tum.

    6. Initial transition specifications: If tum is a initial transition specification, then visit the action as a unqualified name using the action name group and visit the state as a qualified name using the state name group in tum.

    7. State transition specifications: If tum is a state transition specification, then visit the signal as a unqualified name using the signal name group and visit the guard as a unqualified name using the guard name group, and visit the action as a unqualified name using the action name group, and visit the state as a qualified name in the state name group in tum.

    8. Junction definitions: If tum is a junction definition, then visit the guard as a unqualified name using the guard name group, and visit the action as a unqualified name using the action name group, and visit the state as a qualified name using the state name group in tum.

  4. Expressions: Visit an expression e as follows:

    1. Unqualified names: If e is an unqualified name n, then

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

      2. Record the mapping from e to sym in the use-def map of a.

    2. Dot expressions: Otherwise if e is a dot expression e'.n, then

      1. Visit e'.

      2. Look up the mapping from e' to sym' in the use-def map of a. 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 a. 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 e to sym in the use-def map of a.

    3. Other expressions: Otherwise visit each expression and type appearing in e.

  5. Type names: Visit a type name tn as follows:

    1. Unqualified names: Use the same algorithm as for unqualified name expressions, but use the type name group instead of the value name group.

    2. Qualified names: Use the same algorithm as for dot expressions, but use the type name group instead of the value name group.

    3. Other types: Nothing to do.

Clone this wiki locally