type jump_kind = [ `CONTAINS of string | `NOTHING | `TAG of Tag.t ] module State : sig include Sigs.T with type t = int val make : unit -> t end module StateSet : sig include Ptset.S with type elt = int val print : Format.formatter -> t -> unit end module Formula : sig type 'a expr = False | True | Or of 'a * 'a | And of 'a * 'a | Atom of ([ `LLeft | `Left | `RRight | `Right ] * bool * State.t) type t val hash : t -> int val uid : t -> int val equal : t -> t -> bool val expr : t -> t expr val st : t -> (StateSet.t * StateSet.t * StateSet.t) * (StateSet.t * StateSet.t * StateSet.t) val size : t -> int val print : Format.formatter -> t -> unit val is_true : t -> bool val is_false : t -> bool val true_ : t val false_ : t val atom_ : [ `LLeft | `Left | `RRight | `Right ] -> bool -> StateSet.elt -> t val not_ : t -> t val or_ : t -> t -> t val and_ : t -> t -> t module Infix : sig val ( +| ) : t -> t -> t val ( *& ) : t -> t -> t val ( *+ ) : [ `LLeft | `Left | `RRight | `Right ] -> StateSet.elt -> t val ( *- ) : [ `LLeft | `Left | `RRight | `Right ] -> StateSet.elt -> t end end module Transition : sig type node = State.t * bool * Formula.t * bool type data = node type t val make : data -> t val node : t -> data val hash : t -> int val uid : t -> int val equal : t -> t -> bool module Infix : sig val ( ?< ) : State.t -> State.t val ( >< ) : State.t -> TagSet.t * bool -> State.t*(TagSet.t*bool*bool) val ( ><@ ) : State.t -> TagSet.t * bool -> State.t*(TagSet.t*bool*bool) val ( >=> ) : State.t * (TagSet.t*bool*bool) -> Formula.t -> (State.t*TagSet.t*t) end val print : Format.formatter -> t -> unit end module Formlist : Hlist.S with type elt = Transition.t type 'a t = { id : int; mutable states : StateSet.t; init : StateSet.t; starstate : StateSet.t option; trans : (State.t, (TagSet.t * Transition.t) list) Hashtbl.t; query_string : string; } val dump : Format.formatter -> 'a t -> unit module type ResultSet = sig type t type elt = [`Tree] Tree.node val empty : t val cons : elt -> t -> t val concat : t -> t -> t val iter : (elt -> unit) -> t -> unit val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a val map : (elt -> elt) -> t -> t val length : t -> int val merge : (bool*bool*bool*bool)-> elt -> t -> t -> t end module IdSet : ResultSet val top_down_count : 'a t -> Tree.t -> int val top_down : 'a t -> Tree.t -> IdSet.t val bottom_up_count : 'a t -> Tree.t -> [> `CONTAINS of 'b | `TAG of Tag.t ] -> int