Module InvarManager

module InvarManager: sig .. end
Invariant manager
Author(s): Christoph Sticksel

val main : bool ->
(int * Lib.kind_module) list Pervasives.ref ->
'a InputSystem.t -> Analysis.param -> TransSys.t -> unit
Entry point.

First boolean indicates whether the analysis should continue even when everything's been proved.

val on_exit : TransSys.t option -> unit
Cleanup before exit
val print_stats : TransSys.t option -> unit
Prints statistics and properties status.