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