Check Transition Graph

This algorithm constructs and checks the transition graph for a state machine definition.

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 transition graph updated if the check passes; otherwise an error.

Procedure

1. Visit all the enter expressions that are transitively part of smd and construct the transition graph.

2. Check that the transition graph is connected.

3. Check for illegal cycles in the transition graph.

4. Update the transition graph in sma.

Checking That the Graph is Connected

1. Visit the nodes in the transition graph and compute a map that records, for each state definition and junction definition d in the graph, the number of graph edges that have d as their terminal nodes.

2. Check that each number stored in the map is at least 1.

Checking for Illegal Cycles

1. Create the following data structures, initially empty:

   1. path: A list of graph edges representing the current path being traversed. A graph edge stores an initial node and a terminal node.

   2. path node set: The set of nodes in the current path.

   3. visited node set: The set of nodes visited so far.

2. For each junction definition node n in the transition graph

   1. Check whether n appears in the path node set. If so, then the path node list represents an illegal cycle. Throw a semantic error. Use the path node list to construct the cycle for the error message.

   2. Otherwise if n is not in the visited node set, then

      1. Add n to the path node set.

      2. For each edge e = (n,n') such that n' is a junction definition

         1. Add e to the path.

         2. Visit n'.

      3. Add n to the visited node set.

   3. Otherwise we have already visited n; do nothing.