Module Strategy

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

module A = Analysis
type info = {
  1. opacity : Opacity.t;
    (*

    Whether the node should be always abstracted by its contract, never, or sometimes

    *)
  2. has_contract : bool;
    (*

    Does the system have a contract?

    *)
  3. has_impl : bool;
    (*

    Does the system have an implementation?

    *)
  4. has_modes : bool;
    (*

    Does the system have modes?

    *)
}

Information used by the strategy module.

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

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

  • a list of the scopes of the main systems and their strategy info;
  • a list of all the scopes of all the systems and their strategy info.
val next_modular_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 modular 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 is_candidate_for_analysis : info -> bool

Takes information about a (sub)system, and returns whether the subsystem is candidate for analysis