sig
  type svar = {
    pos : Lib.position;
    num : int;
    name : string option;
    svar : StateVar.t;
    scope : (Lib.position * string) list;
  }
  val mk_svar :
    Lib.position ->
    int ->
    string option ->
    StateVar.t -> (Lib.position * string) list -> LustreContract.svar
  val prop_name_of_svar : LustreContract.svar -> string -> string -> string
  type mode = {
    name : LustreIdent.t;
    pos : Lib.position;
    path : string list;
    requires : LustreContract.svar list;
    ensures : LustreContract.svar list;
    candidate : bool;
  }
  val mk_mode :
    LustreIdent.t ->
    Lib.position ->
    string list ->
    LustreContract.svar list ->
    LustreContract.svar list -> bool -> LustreContract.mode
  type t = {
    assumes : LustreContract.svar list;
    guarantees : (LustreContract.svar * bool) list;
    modes : LustreContract.mode list;
  }
  val empty : unit -> LustreContract.t
  val mk :
    LustreContract.svar list ->
    (LustreContract.svar * bool) list ->
    LustreContract.mode list -> LustreContract.t
  val add_ass :
    LustreContract.t -> LustreContract.svar list -> LustreContract.t
  val add_gua :
    LustreContract.t -> (LustreContract.svar * bool) list -> LustreContract.t
  val add_modes :
    LustreContract.t -> LustreContract.mode list -> LustreContract.t
  val svars_of : LustreContract.t -> StateVar.StateVarSet.t
  val pp_print_svar : Format.formatter -> LustreContract.svar -> unit
  val pp_print_mode : bool -> Format.formatter -> LustreContract.mode -> unit
  val pp_print_contract :
    bool -> Format.formatter -> LustreContract.t -> unit
  module ModeTrace :
    sig
      type mode_tree
      val mode_paths_to_tree :
        LustreContract.mode list -> LustreContract.ModeTrace.mode_tree
      val mode_trace_to_tree :
        LustreContract.mode list list ->
        LustreContract.ModeTrace.mode_tree list
      val fmt_as_cex_step_xml :
        Format.formatter -> LustreContract.ModeTrace.mode_tree -> unit
      val fmt_as_cex_step_json :
        Format.formatter -> LustreContract.ModeTrace.mode_tree -> unit
    end
end