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. Construct the transition graph.

2. Check the transition graph for reachability.

3. Check for choice cycles in the transition graph.

4. Construct the reverse transition graph.

Constructing the Transition Graph

1. Let n be the target of the initial transition specifier of the state machine.

2. Let G be the transition graph whose initial node is n and whose node map is empty.

3. For each transition graph node n in the state machine, set G.arcMap(n) to the empty map.

4. For each transition expression e in smd, except for the transition expression in the initial transition of the state machine, do the following:

   1. Let n be the start node corresponding to e. This is the state where e appears, if e appears in an initial transition or state transition, or the choice where e appears.

   2. Let n' be the end node corresponding to e. This is the state or choice referred to by e.

   3. Construct the arc a corresponding to the transition from n to n'.

   4. Add a to the set G.arcMap(n).

5. Set the transition graph of sma to G.

Checking for Reachability

Algorithm:

1. Let R be an empty set of transition graph nodes.

2. Visit the initial node of the transition graph and update R.

3. Check that R contains all the nodes of the transition graph.

Visiting nodes: To visit a node n of the transition graph T, do the following:

1. If R contains n, then do nothing.

2. Otherwise

   1. Add n to R.

   2. Visit all the nodes n' such that there is an arc from n to n' in T.

Checking for Choice Cycles

Algorithm:

1. Let visited be an empty set of choice definitions.

2. For each choice definition c that is a node in the transition graph

   1. Let L be an empty list of transition graph arcs.

   2. Let S be an empty set of choice definitions.

   3. Visit c with L and S.

Visiting choice definitions: To visit a choice definition c with list L and set S, do the following:

1. Check whether c appears in S. If so, then L represents a choice cycle. Throw a semantic error. Use L to construct the error message.

2. Otherwise if c is not in visited, then

   1. Add c to S.

   2. For each arc a from c to a choice definition c'

      1. Add a to L.

      2. Visit c'.

   3. Add c to visited.

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

Constructing the Reverse Transition Graph

1. Let m be the reverse transition graph of sma. To begin it has the initial node n, and it maps n to the empty set of arcs.

2. Visit each node n in the transition graph. For each arc a from n to n', add a to the set m.arcMap(n').