Module Analysis

module Analysis: sig .. end
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 Analysis.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 Analysis.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(s): 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
Merges two assumptions.
val assumptions_merge : assumptions -> assumptions -> assumptions
Assumptions of a transition system.
val assumptions_of_sys : TransSys.t -> assumptions
Fold over assumptions.
val assumptions_fold : ('a -> Scope.t -> Invs.t -> 'a) -> 'a -> assumptions -> 'a
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 = 
| 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.
type 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 -> Format.formatter -> param -> unit
Pretty printer for param.
val pp_print_result_quiet : Format.formatter -> result -> unit
Pretty printer for result, quiet version.
val pp_print_result : Format.formatter -> result -> unit
Pretty printer for result.