Module `Strategy`

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.

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