Checking State Machine Semantics

Input

1. A state machine definition d

Output

1. If the semantic check passes, a state machine analysis data structure sma representing the results of the analysis.

2. Otherwise an error and no output.

Procedure

1. Create an empty state machine analysis sma.

2. Enter state machine symbols for sma and d.

3. Check state machine uses for sma and d.

4. Check initial transitions for sma and d.

5. Check signal uses for sma and d.

6. Check the transition graph for sma and d.

7. Check typed elements for sma and d.

8. Compute the flattened state transition map for sma and d.

9. Compute the flattened choice transition map for sma and d.