Module InvGen

module InvGen: sig .. end
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.