Module Strategy

module Strategy: sig .. end

A strategy returns an Analysis.param option which is None if done. It takes

the results so far, and
a list of scope / bool pairs with the scopes sorted in topological order, starting from the top-most one. Booleans indicate whether the corresponding system can be abstracted.

module A: Analysis

type info = {

`can_refine : bool;`	`(*`	Does the system have a contract?	`*)`
`has_contract : bool;`	`(*`	Does the system have modes?	`*)`
`has_modes : bool;`

}

Information used by the strategy module.

val next_analysis : A.results ->
       (Scope.t -> (Scope.t * info) list) ->
       (Scope.t * info) list -> A.param option

Takes some results and some information about (sub)systems, and returns the next analysis to perform, if any. The information it takes is

a function which, given the scope of a system, returns the scope of its direct subsystems and its strategy info;
a list of all the scopes of all the systems and their strategy info.

val monolithic : (Scope.t * info) list -> A.param option

Works almost the same as next_analysis, but returns a single analysis parameter for a monolithic analysis. Only used for contract generation.