module Strategy:sig
..end
Analysis.param option
which is None
if done.
It takesbool
pairs with the scopes sorted in topological
order, starting from the top-most one. Booleans indicate whether the
corresponding system can be abstracted.module A: Analysis
type
info = {
|
can_refine : |
(* |
Does the system have a contract?
| *) |
|
has_contract : |
(* |
Does the system have modes?
| *) |
|
has_modes : |
val next_analysis : A.results ->
(Scope.t -> (Scope.t * info) list) ->
(Scope.t * info) list -> A.param option
val monolithic : (Scope.t * info) list -> A.param option
next_analysis
, but returns a single analysis
parameter for a monolithic analysis. Only used for contract generation.