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.