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 definitions: Visit a state machine definition smd by visiting its state machine members.

  2. 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 enter expression.

    2. Junction definitions: If smm is a junction definition, then

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

      2. Visit each of the two enter expressions the definition.

    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.

  3. State definition members: Visit a state definition member sdm as follows:

    1. TODO

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

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

  6. Qualified identifiers: Visit a qualified identifier q in name group G

    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.

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

Clone this wiki locally