Check Typed Elements

This algorithm assigns a type option to each typed element. It checks the type options for consistency with the semantic rules.

Input

1. A state machine definition smd.

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

Output

1. sma with the type map updated if the check passes; otherwise an error.

Procedure

1. Compute the reverse junction map.

2. Compute the type options of all the typed elements.

3. Check the types of the actions and guards.

Computing the Reverse Junction Map

1. Let m be the reverse junction map of sma.

2. Visit each typed element of smd.

   1. Let n be the node being visited.

   2. If n is an initial transition specifier or a state transition specifier whose destination is a junction j, then add n to m(j).

   3. Otherwise n is a junction definition j. For each enter expression e in j, if the destination is a junction j', then add n to m(j').

Computing Type Options

1. Let m be the type map of sma.

2. Set the visited symbol set of sma to the empty set.

3. Visit each typed element of smd.

   1. Let n be the node being visited.

   2. If n is an initial transition specifier, then set m(n) to None.

   3. Otherwise if n is a state definition sd, then for each state transition specifier sts in sd

      1. Let o be the type option specified in the signal of sts.

      2. Set m(sts) to o.

   4. Otherwise n is a junction j.

      1. Let m be the reverse junction map of sma.

      2. Let E be the set of typed elements m(n).

      3. Visit each typed element in E.

      4. Let O be the set of type options of elements of E.

      5. Let o be the common type option of O. If there is no common type, then return an error.

Checking the Types of Actions and Guards

1. Visit each typed element e of smd.

   1. Let o be the type option associated with e in the type map.

   2. If e is a initial transition specifier, then check that o is convertible to the type option of each of the actions specified in e.

   3. Otherwise if e is a state transition specifier or junction definition, then check that all guards and actions specified in e have type options o' such that o is covertible to o'.