Module Strategy

module Strategy: sig .. end
A strategy returns an Analysis.param option which is None if done. It takes

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


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.