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 option 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 option map of sma.

2. Visit each typed element e of smd.

   1. If the mapping m(e) exists, then do nothing.

   2. Otherwise if e is an initial transition specifier its, then set m(its) to None.

   3. Otherwise if e is a state transition specifier sts, then

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

      2. Set m(sts) to o.

   4. Otherwise e is a junction j.

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

      2. Let E be the set of typed elements implied by the arc set r(j).

      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.

      6. Set m(j) to o.

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 option 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'.