Module `InvGen`

Generic invariant generation.

Invariant generation is written as a functor and is instantiated to create boolean, integer and real invariant generation.

For more details, refer to the paper about invariant generation that I need to write but haven't yet.

val main_bool : bool -> 'a InputSystem.t -> Analysis.param -> TransSys.t -> unit: Temporary entry point for boolean invariant generation.

val main_int : bool -> 'a InputSystem.t -> Analysis.param -> TransSys.t -> unit: Temporary entry point for integer invariant generation.

val main_real : bool -> 'a InputSystem.t -> Analysis.param -> TransSys.t -> unit: Temporary entry point for real invariant generation.

val exit : 'a -> unit: Temporary exit point for boolean invariant generation.

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

module BoolInvGen : Out: Boolean invariant generation module.

module IntInvGen : Out: Int invariant generation module.

module RealInvGen : Out: Real invariant generation module.

module EqOnly : sig ... end: Graph modules for equivalence-only invgen.