sig
  module type Var =
    sig
      type t
      val pp : Format.formatter -> Transition.Var.t -> unit
      val show : Transition.Var.t -> string
      val typ : Transition.Var.t -> [ `TyInt | `TyReal ]
      val compare : Transition.Var.t -> Transition.Var.t -> int
      val symbol_of : Transition.Var.t -> Syntax.symbol
      val of_symbol : Syntax.symbol -> Transition.Var.t option
    end
  module Make :
    functor
      (C : sig type t val context : Transition.Make.t Syntax.context end) (Var : Var) ->
      sig
        type t
        type var = Transition.Var.t
        val equal : Transition.Make.t -> Transition.Make.t -> bool
        val compare : Transition.Make.t -> Transition.Make.t -> int
        val pp : Format.formatter -> Transition.Make.t -> unit
        val show : Transition.Make.t -> string
        val construct :
          C.t Syntax.formula ->
          (Transition.Make.var * C.t Syntax.term) list -> Transition.Make.t
        val assume : C.t Syntax.formula -> Transition.Make.t
        val assign :
          Transition.Make.var -> C.t Syntax.term -> Transition.Make.t
        val parallel_assign :
          (Transition.Make.var * C.t Syntax.term) list -> Transition.Make.t
        val havoc : Transition.Make.var list -> Transition.Make.t
        val mul : Transition.Make.t -> Transition.Make.t -> Transition.Make.t
        val add : Transition.Make.t -> Transition.Make.t -> Transition.Make.t
        val zero : Transition.Make.t
        val one : Transition.Make.t
        val widen :
          Transition.Make.t -> Transition.Make.t -> Transition.Make.t
        val exists :
          (Transition.Make.var -> bool) ->
          Transition.Make.t -> Transition.Make.t
        val is_zero : Transition.Make.t -> bool
        val is_one : Transition.Make.t -> bool
        val mem_transform : Transition.Make.var -> Transition.Make.t -> bool
        val get_transform :
          Transition.Make.var -> Transition.Make.t -> C.t Syntax.term
        val transform :
          Transition.Make.t ->
          (Transition.Make.var * C.t Syntax.term) BatEnum.t
        val guard : Transition.Make.t -> C.t Syntax.formula
        val interpolate :
          Transition.Make.t list ->
          C.t Syntax.formula ->
          [ `Invalid | `Unknown | `Valid of C.t Syntax.formula list ]
        val valid_triple :
          C.t Syntax.formula ->
          Transition.Make.t list ->
          C.t Syntax.formula -> [ `Invalid | `Unknown | `Valid ]
        val defines : Transition.Make.t -> Transition.Make.var list
        val uses : Transition.Make.t -> Transition.Make.var list
        val abstract_post :
          (C.t, 'abs) SrkApron.property ->
          Transition.Make.t -> (C.t, 'abs) SrkApron.property
        module Iter :
          functor (I : Iteration.Domain) ->
            sig
              type iter = C.t I.t
              val alpha : Transition.Make.t -> Transition.Make.Iter.iter
              val closure : Transition.Make.Iter.iter -> Transition.Make.t
              val star : Transition.Make.t -> Transition.Make.t
              val equal :
                Transition.Make.Iter.iter ->
                Transition.Make.Iter.iter -> bool
              val widen :
                Transition.Make.Iter.iter ->
                Transition.Make.Iter.iter -> Transition.Make.Iter.iter
              val join :
                Transition.Make.Iter.iter ->
                Transition.Make.Iter.iter -> Transition.Make.Iter.iter
              val pp : Format.formatter -> Transition.Make.Iter.iter -> unit
              val show : Transition.Make.Iter.iter -> string
            end
      end
end