sig
  val init_base : Numeral.t
  val trans_base : Numeral.t
  val prop_base : Numeral.t
  type t
  module Hashtbl :
    sig
      type key = t
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> '-> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> '-> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> '-> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> '-> 'a option) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
    end
  type pred_def = UfSymbol.t * (Var.t list * Term.t)
  type instance = {
    pos : Lib.position;
    map_down : StateVar.t StateVar.StateVarMap.t;
    map_up : StateVar.t StateVar.StateVarMap.t;
    guard_clock : Numeral.t -> Term.t -> Term.t;
  }
  val equal_scope : TransSys.t -> TransSys.t -> bool
  val compare_scope : TransSys.t -> TransSys.t -> int
  val pp_print_trans_sys : Format.formatter -> TransSys.t -> unit
  val pp_print_trans_sys_name : Format.formatter -> TransSys.t -> unit
  val init_of_bound :
    (UfSymbol.t -> unit) option -> TransSys.t -> Numeral.t -> Term.t
  val trans_of_bound :
    (UfSymbol.t -> unit) option -> TransSys.t -> Numeral.t -> Term.t
  val init_uf_symbol : TransSys.t -> UfSymbol.t
  val trans_uf_symbol : TransSys.t -> UfSymbol.t
  val init_formals : TransSys.t -> Var.t list
  val trans_formals : TransSys.t -> Var.t list
  val init_fun_of : TransSys.t -> Numeral.t -> Term.t
  val trans_fun_of : TransSys.t -> Numeral.t -> Numeral.t -> Term.t
  val init_flag_state_var : TransSys.t -> StateVar.t
  val init_flag_of_bound : TransSys.t -> Numeral.t -> Term.t
  val init_trans_open : TransSys.t -> StateVar.t list * Term.t * Term.t
  val get_logic : TransSys.t -> TermLib.logic
  val scope_of_trans_sys : TransSys.t -> Scope.t
  val get_properties : TransSys.t -> Property.t list
  val get_real_properties : TransSys.t -> Property.t list
  val is_candidate : TransSys.t -> string -> bool
  val get_candidates : TransSys.t -> Term.t list
  val get_candidate_properties : TransSys.t -> Property.t list
  val get_unknown_candidates : TransSys.t -> Term.t list
  val get_mode_requires :
    TransSys.t -> Term.t option * (Scope.t * Term.t) list
  val get_split_properties :
    TransSys.t -> Property.t list * Property.t list * Property.t list
  val mk_trans_sys :
    ?instance_var_id_start:int ->
    Scope.t ->
    StateVar.t option ->
    StateVar.t ->
    (StateVar.t * Term.t list) list ->
    StateVar.t list ->
    LustreExpr.expr LustreExpr.bound_or_fixed list StateVar.StateVarHashtbl.t ->
    Var.t list ->
    UfSymbol.t list ->
    UfSymbol.t ->
    Var.t list ->
    Term.t ->
    UfSymbol.t ->
    Var.t list ->
    Term.t ->
    (TransSys.t * TransSys.instance list) list ->
    Property.t list ->
    Term.t option * (Scope.t * Term.t) list -> Invs.t -> TransSys.t * int
  val iter_subsystems :
    ?include_top:bool -> (TransSys.t -> unit) -> TransSys.t -> unit
  val fold_subsystems :
    ?include_top:bool -> ('-> TransSys.t -> 'a) -> '-> TransSys.t -> 'a
  val fold_subsystem_instances :
    (TransSys.t -> (TransSys.t * TransSys.instance) list -> 'a list -> 'a) ->
    TransSys.t -> 'a
  val get_subsystems : TransSys.t -> TransSys.t list
  val get_subsystem_instances :
    TransSys.t -> (TransSys.t * TransSys.instance list) list
  val find_subsystem_of_scope : TransSys.t -> Scope.t -> TransSys.t
  val get_max_depth : TransSys.t -> int
  val map_cex_prop_to_subsystem :
    (Scope.t ->
     TransSys.instance ->
     (StateVar.t * Model.value list) list ->
     Model.value list -> Model.value list) ->
    TransSys.t ->
    (StateVar.t * Model.value list) list ->
    Property.t ->
    TransSys.t * TransSys.instance list *
    (StateVar.t * Model.value list) list * Property.t
  val state_vars : TransSys.t -> StateVar.t list
  val vars_of_bounds :
    ?with_init_flag:bool ->
    TransSys.t -> Numeral.t -> Numeral.t -> Var.t list
  val declare_vars_of_bounds :
    ?declare_init_flag:bool ->
    TransSys.t -> (UfSymbol.t -> unit) -> Numeral.t -> Numeral.t -> unit
  val declare_const_vars : TransSys.t -> (UfSymbol.t -> unit) -> unit
  val declare_init_flag_of_bounds :
    TransSys.t -> (UfSymbol.t -> unit) -> Numeral.t -> Numeral.t -> unit
  val define_and_declare_of_bounds :
    ?declare_sub_vars:bool ->
    TransSys.t ->
    (UfSymbol.t -> Var.t list -> Term.t -> unit) ->
    (UfSymbol.t -> unit) ->
    (Type.t -> unit) -> Numeral.t -> Numeral.t -> unit
  val uf_defs : TransSys.t -> TransSys.pred_def list
  val property_of_name : TransSys.t -> string -> Property.t
  val get_prop_term : TransSys.t -> string -> Term.t
  val get_prop_status : TransSys.t -> string -> Property.prop_status
  val is_inv : TransSys.t -> Term.t -> bool
  val is_proved : TransSys.t -> string -> bool
  val is_disproved : TransSys.t -> string -> bool
  val get_prop_status_all_nocands :
    TransSys.t -> (string * Property.prop_status) list
  val get_prop_status_all_unknown :
    TransSys.t -> (string * Property.prop_status) list
  val props_list_of_bound : TransSys.t -> Numeral.t -> (string * Term.t) list
  val set_prop_status : TransSys.t -> string -> Property.prop_status -> unit
  val set_prop_invariant : TransSys.t -> string -> Certificate.t -> unit
  val set_prop_false :
    TransSys.t -> string -> (StateVar.t * Model.value list) list -> unit
  val set_prop_ktrue : TransSys.t -> int -> string -> unit
  val has_properties : TransSys.t -> bool
  val all_props_proved : TransSys.t -> bool
  val add_properties : TransSys.t -> Property.t list -> TransSys.t
  val add_invariant : TransSys.t -> Term.t -> Certificate.t -> bool -> Term.t
  val add_scoped_invariant :
    TransSys.t -> string list -> Term.t -> Certificate.t -> bool -> Term.t
  val invars_of_bound :
    ?one_state_only:bool -> TransSys.t -> Numeral.t -> Term.t list
  val get_invariants : TransSys.t -> Invs.t
  val get_all_invariants : TransSys.t -> Invs.t Scope.Map.t
  val instantiate_term_all_levels :
    TransSys.t ->
    Numeral.t ->
    Scope.t ->
    Term.t ->
    bool -> (TransSys.t * Term.t list) * (TransSys.t * Term.t list) list
  val get_state_var_bounds :
    TransSys.t ->
    LustreExpr.expr LustreExpr.bound_or_fixed list StateVar.StateVarHashtbl.t
  val instantiate_term_cert_all_levels :
    TransSys.t ->
    Numeral.t ->
    Scope.t ->
    Term.t * Certificate.t ->
    bool ->
    (TransSys.t * (Term.t * Certificate.t) list) *
    (TransSys.t * (Term.t * Certificate.t) list) list
end