Module Analysis

Interface between strategy and low-level analysis

An analysis distinguishes exactly one system as the top system, and looks at its properties and its contract. Subsystems are view either as abstract with their contract or as concrete with their implementations.

The result of an analysis indicates which properties of the top system are invariant, whether the system conforms to its contract and whether it conforms to the preconditions of all its subsystems.

Values of type param are produced by a strategy and parameterize the input-specific transitions system generators, in particular the slicing ot the cone of influence.

Values of type result are produced by running an analysis of a generated transition system. The accumulated results are used by a strategey to decide the next steps.

NB: The uid stored in an info must be unique because it is used during transition system generation to avoid name clashes in UFs and svars.

val get_uid : unit -> int

Provides a different id every time.

type assumptions = Invs.t Scope.Map.t

Type of scope-wise assumptions.

val assumptions_empty : assumptions

Empty assumptions.

val assumptions_merge : assumptions -> assumptions -> assumptions

Merges two assumptions.

val assumptions_of_sys : TransSys.t -> assumptions

Assumptions of a transition system.

val assumptions_fold : ('a -> Scope.t -> Invs.t -> 'a) -> 'a -> assumptions -> 'a

Fold over assumptions.

type info = {
  1. top : Scope.t;
    (*

    The top system for the analysis run

    *)
  2. uid : int;
    (*

    UID for the analysis.

    *)
  3. abstraction_map : bool Scope.Map.t;
    (*

    Systems flagged true are to be represented abstractly, those flagged false are to be represented by their implementation.

    *)
  4. assumptions : assumptions;
    (*

    Properties that can be assumed invariant in subsystems

    *)
}

Information for the creation of a transition system

val shrink_info_to_sys : info -> TransSys.t -> info

Shrinks an abstraction map to the subsystems of a system.

type param =
  1. | Interpreter of info
    (*

    Simulation of a system

    *)
  2. | ContractCheck of info
    (*

    Analysis of the contract of a system.

    *)
  3. | First of info
    (*

    First analysis of a system.

    *)
  4. | Refinement of info * result
    (*

    Refinement of a system. Store the result of the previous analysis.

    *)
  5. | ContractMonitor of info

Parameter of an analysis.

and result = {
  1. param : param;
    (*

    Parameters of the analysis.

    *)
  2. time : float;
    (*

    Runtime of the analysis.

    *)
  3. sys : TransSys.t;
    (*

    System analyzed, contains property statuses and invariants.

    *)
  4. contract_valid : bool option;
    (*

    None if system analyzed has not contracts, Some true if it does and they have been proved correct, Some false if it does and some are unknown / falsified.

    *)
  5. requirements_valid : bool option;
    (*

    None if system analyzed has not sub-requirements, Some true if it does and they have been proved correct, Some false if it does and some are unknown / falsified.

    *)
}

Result of analysing a transistion system

val info_clone : info -> info

Clones an info, only changes its uid.

val param_clone : param -> param

Clones a param, only changes its uid.

val info_of_param : param -> info

The info or a param.

val shrink_param_to_sys : param -> TransSys.t -> param

Shrinks a param to a system.

val param_scope_is_abstract : param -> Scope.t -> bool

Return true if a scope is flagged as abstract in the abstraction_map of a param. Default to false if the node is not in the map.

val no_system_is_abstract : ?include_top:bool -> param -> bool

Return true if no system is flagged abstract in the abstraction_map of a param.

val param_assumptions_of_scope : param -> Scope.t -> Invs.t

Retrieve the assumptions of a scope from a param.

val mk_result : param -> TransSys.t -> float -> result

Returns a result from an analysis.

val result_is_all_proved : result -> bool

Returns true if all properties in the system in a result have been proved.

val result_is_all_inv_proved : result -> bool

Returns true if all invariant properties in the system in a result have been proved.

val result_is_some_falsified : result -> bool

Returns true if some properties in the system in a result have been falsified.

val result_is_some_inv_falsified : result -> bool

Returns true if some invariant properties in the system in a result have been falsified.

val result_is_some_reach_proved : result -> bool

Returns true if some reachability properties in the system in a result have been proven reachable.

type results

Map from Scope.t to result storing the results found this far.

val mk_results : unit -> results

Creates a new results.

val results_add : result -> results -> results

Adds a result to a results.

val results_find : Scope.t -> results -> result list

Returns the list of results for a top scope.

Raises Not_found if not found.

val results_last : Scope.t -> results -> result

Returns the last result corresponding to a scope.

val results_size : results -> int

Returns the total number of analyzed systems so far

val results_length : results -> int

Returns the total number of results stored in a results. Used to generate UIDs for params.

val results_is_safe : results -> bool option

Returns None if no properties were falsified but some could not be proved, Some true if all properties were proved, and Some false if some were falsified.

val results_is_empty : results -> bool
val results_clean : results -> results

Cleans the results by removing nodes that don't have any property or contract.

type pp_print_system_user_name = Stdlib.Format.formatter -> Scope.t -> unit
val pp_print_param : bool -> TransSys.t -> pp_print_system_user_name -> Stdlib.Format.formatter -> param -> unit

Pretty printer for param.

val pp_print_result_quiet : pp_print_system_user_name -> Stdlib.Format.formatter -> result -> unit

Pretty printer for result, quiet version.

val pp_print_result : pp_print_system_user_name -> Stdlib.Format.formatter -> result -> unit

Pretty printer for result.