Module type InvGen.Out

module type Out = sig .. end
Signature of the module returned by the Make invariant generation functor when given a module with signature In.

val main : Numeral.t option ->
bool ->
bool ->
bool ->
'a InputSystem.t ->
Analysis.param ->
TransSys.t -> (TransSys.t * Term.TermSet.t * Term.TermSet.t) list
Runs the invariant generator.

main max_depth top_only modular two_state input_sys aparam sys:

* max_depth: length of the invariant generation run * top_only: run on top level only * modular: triggers modular MINING * two_state: generate two-state invariants * the rest should be obvious.

Clean exit for the invariant generator.

val exit : 'a -> unit