CFG Extraction¶

Given a set of clocked guarded actions (CGAs), it is required to compose them into control flow graphs (CFGs). At greater length, but still informally, it is needed to determine which of the action variables encode control information and to link actions connected through those variables.

Examples¶

A1: ...   => { ..., x = 1 }
A2: x = 1 => { ... }

Here is a link between A1 and A2.

A1: ...   => { ..., x = 1 }
A2: x = 1 => { ... }
A3: x = 1 => { ... }

Here are links between A1 and A2 and between A1 and A3 (fork).

Links¶

Links between actions can be divided into two main groups:

1. Hard links
2. Soft links

The examples above illustrate hard links. There is a hard link Ai -> Aj iff Ai's actions contain x = v and Aj's guard is exactly x == v, where x is some variable (vector of variables) and v is a concrete value (vector of values).