Skip to content

Check State Machine Uses

Jump to bottom
Rob Bocchino edited this page Jul 17, 2024 · 17 revisions

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

  1. State machine definition members: Visit a state machine member smm as follows:

    1. 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.

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

    3. State transition specifiers: If smm is a state transition specifier, 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 smm.

    4. Junction definitions: If smm 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 smm.

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

  2. Enter expressions: Visit an enter expression e as follows:

    1. If the optional do clause is present in e, then visit its identifier in the action name group.

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

  3. Qualified identifiers: Visit a qualified identifier q in name group G as follows:

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

      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 e to sym in the use-def map of sma.

    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.

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

Clone this wiki locally