Factor-control-flow-graph

Factor-control-flow-graph --- фактор-уграф.

Let [math]\displaystyle{ R }[/math] be a set of alts of a cf-graph [math]\displaystyle{ G }[/math] such that every node of [math]\displaystyle{ G }[/math] belongs to a single alt from [math]\displaystyle{ R }[/math], i.e. [math]\displaystyle{ R }[/math] forms a partition of [math]\displaystyle{ V(G) }[/math].

The cf-graph [math]\displaystyle{ G' }[/math] in which [math]\displaystyle{ V(G')=R }[/math] is said to be obtained by reduction of alts [math]\displaystyle{ R }[/math] into nodes (notation [math]\displaystyle{ G'=R(G) }[/math]) if the following properties hold:

(1) for any [math]\displaystyle{ C_1,C_2\in R }[/math], [math]\displaystyle{ (C_1,C_2)\in A(G') }[/math] if and only if there are [math]\displaystyle{ p_1\in C_1 }[/math] and [math]\displaystyle{ p_2\in C_2 }[/math] such that [math]\displaystyle{ (p_1,p_2)\in A(G) }[/math],

(2) [math]\displaystyle{ C\in R }[/math] is the initial node of [math]\displaystyle{ G' }[/math] if and only if [math]\displaystyle{ C }[/math] contains the initial node of [math]\displaystyle{ G }[/math],

(3) [math]\displaystyle{ C\in R }[/math] is the terminal node of [math]\displaystyle{ G' }[/math] if and only if [math]\displaystyle{ C }[/math] contains the terminal node of [math]\displaystyle{ G }[/math].

The cf-graph [math]\displaystyle{ G' }[/math] is called a factor-control-flow-graph (or factor-cf-graph) of the cf-graph [math]\displaystyle{ G }[/math] with respect to [math]\displaystyle{ R }[/math].

Let [math]\displaystyle{ R }[/math] be a set of mutually disjoint alts of a cf-graph [math]\displaystyle{ G }[/math] that form a partitation of some subset [math]\displaystyle{ Y\subset V(G) }[/math]. Then [math]\displaystyle{ R(G) }[/math] is defined as cf-graph [math]\displaystyle{ R'(G) }[/math], where [math]\displaystyle{ R'=R\bigcup \{ \{p\}: p\in V(G)\setminus Y\} }[/math].