# 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.

• `FromWto` indicates to use as widening points the heads of the weak topological ordering given as a parameter of the analysis function. This will always be a safe choice, and in most cases it will also be a good one with respect to the precision of the analysis.
• `Predicate f` indicates to use `f` as the characteristic function of the widening set. `Predicate (fun _ -> false)` can be used if a widening is not needed. This variant can be used when there is a special knowledge of the graph to achieve a better precision of the analysis. For instance, if the graph happens to be the flow graph of a program, the predicate should be true for control structures heads. In any case, a condition for a safe widening predicate is that every cycle of the graph should go through at least one widening point. Otherwise, the analysis may not terminate. Note that even with a safe predicate, ensuring the termination does still require a correct widening definition.

`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``