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.

author
Christoph Sticksel
val get_uid : unit -> int

Provides a different id every time.

type assumptions = Invs.t Scope.Map.t

Type of scope-wise assumptions.

Empty assumptions.

val assumptions_empty : assumptions

Empty assumptions.

Merges two assumptions.

val assumptions_merge : assumptions -> assumptions -> assumptions

Merges two assumptions.

Assumptions of a transition system.

val assumptions_of_sys : TransSys.t -> assumptions

Assumptions of a transition system.

Fold over assumptions.

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

Fold over assumptions.

type info = {
top : Scope.t;
uid : int;
abstraction_map : bool Scope.Map.t;
assumptions : assumptions;
}

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 =
| Interpreter of info

Analysis of the contract of a system.

| ContractCheck of info

First analysis of a system.

| First of info

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

| Refinement of info * result

Parameter of an analysis.

and result = {
param : param;
time : float;
sys : TransSys.t;
contract_valid : bool option;
requirements_valid : bool option;
}

Result of analysing a transistion system

val info_clone : info -> info
val param_clone : param -> param
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 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_some_falsified : result -> bool

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

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_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_clean : results -> results

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

val pp_print_param : bool -> Stdlib.Format.formatter -> param -> unit

Pretty printer for param.

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

Pretty printer for result, quiet version.

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

Pretty printer for result.