Module ChaoticIteration

module ChaoticIteration: sig .. end
Fixpoint computation with widenings using weak topological orderings as defined by Fran├žois Bourdoncle and implemented in WeakTopological.

Fixpoint is another (simpler) fixpoint computation module, with general references.

The general idea of fixpoint computation is to iteratively compute the result of the analysis a vertex from the results of its predecessors, until stabilisation is achieved on every vertex. The way to determine, at each step, the next vertex to analyse is called a chaotic iteration strategy. A good strategy can make the analysis much faster. To enforce the termination of the analyse and speed it up when it terminates in too many steps, one can also use a widening, to ensure that there is no infinite (nor too big) sequence of intermediary results for a given vertex. However, it usually results in a loss of precision, which is why choosing a good widening set (the set of points on which the widening will be performed) is mandatory.

This module computes a fixpoint over a graph using weak topological ordering, which can be used to get both the iteration strategy and the widening set. The module WeakTopological aims to compute weak topological orderings which are known to be excellent decompositions w.r.t these two critical points.
Author(s): Thibault Suzanne
See also Efficient chaotic iteration strategies with widenings , Fran├žois Bourdoncle, Formal Methods in Programming and their Applications, Springer Berlin Heidelberg, 1993

type 'a widening_set = 
| FromWto
| Predicate of ('a -> bool)
How to determine which vertices are to be considered as widening points.

module type G = sig .. end
Minimal graph signature for the algorithm.
module type Data = sig .. end
Parameters of the analysis.
module Make: 
functor (G : G) ->
functor (D : Data with type edge = G.E.t) -> sig .. end