sig
  type _ t
  exception UnsupportedFileFormat of string
  val read_input_lustre : string -> LustreNode.t InputSystem.t
  val translate_contracts_lustre : string -> string -> unit
  val read_input_native : string -> TransSys.t InputSystem.t
  val silent_contracts_of : 'InputSystem.t -> (Scope.t * string list) list
  val ordered_scopes_of : 'InputSystem.t -> Scope.t list
  val maximal_abstraction_for_testgen :
    'InputSystem.t ->
    Scope.t -> Analysis.assumptions -> Analysis.param option
  val next_analysis_of_strategy :
    'InputSystem.t -> Analysis.results -> Analysis.param option
  val trans_sys_of_analysis :
    ?preserve_sig:bool ->
    'InputSystem.t -> Analysis.param -> TransSys.t * 'InputSystem.t
  val pp_print_path_pt :
    'InputSystem.t ->
    TransSys.t ->
    TransSys.instance list -> bool -> Format.formatter -> Model.path -> unit
  val pp_print_path_xml :
    'InputSystem.t ->
    TransSys.t ->
    TransSys.instance list -> bool -> Format.formatter -> Model.path -> unit
  val pp_print_path_json :
    'InputSystem.t ->
    TransSys.t ->
    TransSys.instance list -> bool -> Format.formatter -> Model.path -> unit
  val pp_print_path_in_csv :
    'InputSystem.t ->
    TransSys.t ->
    TransSys.instance list -> bool -> Format.formatter -> Model.path -> unit
  val slice_to_abstraction_and_property :
    'InputSystem.t ->
    Analysis.param ->
    TransSys.t ->
    (StateVar.t * Model.value list) list ->
    Property.t ->
    TransSys.t * TransSys.instance list *
    (StateVar.t * Model.value list) list * Term.t * 'InputSystem.t
  val reconstruct_lustre_streams :
    'InputSystem.t ->
    StateVar.t list ->
    (StateVar.t * (LustreIdent.t * int * LustreNode.call_cond list) list)
    list StateVar.StateVarMap.t
  val is_lustre_input : 'InputSystem.t -> bool
  val compile_to_rust : 'InputSystem.t -> Scope.t -> string -> unit
  val compile_oracle_to_rust :
    'InputSystem.t ->
    Scope.t ->
    string ->
    string * (Lib.position * int) list * (string * Lib.position * int) list
  val contract_gen_param :
    'InputSystem.t -> Analysis.param * (Scope.t -> LustreNode.t)
  val unsliced_trans_sys_of :
    ?preserve_sig:bool ->
    'InputSystem.t -> Analysis.param -> TransSys.t * 'InputSystem.t
end