Module MoxiInput

type error =
  1. | UnexpectedChar of Lib.position * char
  2. | SyntaxError of Lib.position
  3. | TypeError of MoxiTypeChecker.error
  4. | Unsupported of Lib.position * string
    (*

    A well-sorted construct that kmoxi does not translate

    *)
val pp_print_error : Stdlib.Format.formatter -> error -> unit

Print an error as file:line:column: error: message

type system_check = TransSys.t SubSystem.t
val check_file : string -> (unit, error) Stdlib.result

Parse and type check the script in a file, without translating it

val moxi_name_of_uf : UfSymbol.t -> string option

The MoXI name of a function defined with define-fun, given the symbol it is translated to, which has a fresh name

val call_name : TransSys.t -> TransSys.instance -> string

The name of a subsystem call, given the caller and the instance of the call. Raises Failure if the call has no name, which every call kmoxi builds has.

val of_file : string -> ((system_check * string list) list * string option, error) Stdlib.result

Parse, type check and translate the script in a file into one transition system per check-system command, in the order of the script, each with the names of its properties that are current-state formulas, and the logic set with set-logic, if any