Module Main

module Main: sig  end

module Predicate: sig  end

module Expression: sig  end

module C_System_Descr: sig  end

module C_Command: sig  end

module IntSet: sig  end

module Stats: sig  end

val inputCustomAbs : unit ->
       (string * (Ast.Expression.expression * bool) list) list *
       (Ast.Expression.expression * (Ast.Expression.expression * bool) list) list
       option * (Ast.Expression.expression * string) list

val constructInitialPredicates : string -> Predicate.predicate list

val constructInvariants : unit -> Predicate.predicate list

val constructEnvironmentAssumptions : unit -> (Expression.lval * Predicate.predicate) list

val constructKillPredicates : unit -> Predicate.predicate list

val modelCheck : C_System_Descr.location option -> unit

val interactive : unit -> unit

val testModelCheck : 'a -> unit

val main : unit -> unit