Check Signal Uses

This algorithm traverses a state machine definition and checks that, within each state definition, each transition uses a unique signal.

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 if the check succeeds; otherwise an error.

Procedure

Visit each state definition d that is a transitive member of smd and do the following:

1. Initialize a set S of signal symbols to an empty map.

2. Visit each state transition specifier sts that is a member of d and do the following:

   1. Use the use-def map of sma to look up the symbol s referred to in the on clause of sts.

   2. If S contains a mapping from s to sts', then use sts' to report the error.

   3. Otherwise map s to sts in S.