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 type options of the typed elements.

2. Check the types of the actions and guards.

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 e of smd.

   1. If e is an initial transition specifier, then set m(e) to None.

   2. Otherwise if e 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.

   3. Otherwise e is a junction j.

      1. Let m be the reverse transition graph of sma.

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

      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 convertible to o'.