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 type merge_conf = NO | ONLY1 | ONLY2 | ONLY12 | MARK | MARK1 | MARK2 | MARK12 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 -> Uid.t 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 * TagSet.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 -> Uid.t 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 : merge_conf -> elt -> t -> t -> t val mk_quick_tag_loop : (elt -> elt -> 'a*t array) -> 'a -> int -> Tree.t -> Tag.t -> (elt -> elt -> 'a*t array) val mk_quick_star_loop : (elt -> elt -> 'a*t array) -> 'a -> int -> Tree.t -> (elt -> elt -> 'a*t array) end module IdSet : ResultSet module GResult (Doc : sig val doc : Tree.t end) : ResultSet val top_down_count : 'a t -> Tree.t -> int val top_down_count1 : 'a t -> Tree.t -> int val top_down : 'a t -> Tree.t -> IdSet.t val top_down1 : 'a t -> Tree.t -> IdSet.t val bottom_up_count : 'a t -> Tree.t -> [> `CONTAINS of 'b | `TAG of Tag.t ] -> int val bottom_up : 'a t -> Tree.t -> [> `CONTAINS of 'b | `TAG of Tag.t ] -> IdSet.t module Test (Doc : sig val doc : Tree.t end ) : sig module Results : ResultSet val top_down : 'a t -> Tree.t -> Results.t val top_down1 : 'a t -> Tree.t -> Results.t end