Make.2-D
type edge = G.E.t
Edge of the graph.
How to analyze one edge: given an edge and the data stored at its origin, it must compute the resulting data to be stored at its destination.
The widening operator. fun _ x -> x
is correct and is equivalent to not doing widening. Note that to enforce termination, the following property should hold: for all sequence x_0, x_1, ...
of data, the sequence defined by y_0 =
x_0; y_{i+1} = widening y_i x_i
stabilizes in finite time.