Module InvarManager

Invariant manager

author
Christoph Sticksel
val main : bool -> bool -> (int * Lib.kind_module) list Stdlib.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.