Module Strategy.A

module A: Analysis

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.