Module type ChaoticIteration.Data

Parameters of the analysis.

type t

Information stored at each vertex.

type edge

Edge of the graph.

val join : t -> t -> t

Operation to join data when several paths meet.

val equal : t -> t -> bool

Equality test for data.

val analyze : edge -> t -> t

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.

val widening : t -> t -> t

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.