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

2. Check the types of the actions and guards.

Computing the Type Option Map

Algorithm:

1. Let m be the type option map of sma.

2. Visit each typed element e of smd.

Visiting typed elements: To visit a typed element e, do the following:

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

2. Otherwise if e is an initial transition specifier, a state entry specifier, or a state exit specifier, then then set m(e) 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 choice c.

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

   2. If r.arcMap(j) is empty, then set m(j) to None. This happens when c is the initial node of the transition graph.

   3. Otherwise

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

      2. Visit each typed element in E.

      3. Let O be the set of type options m(e) such that e is an element of E.

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

      5. 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, a state entry specifier, or a state exit 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 choice definition, then check that all guards and actions specified in e have type options o' such that o is convertible to o'.