Implement the multiple-starters feature:

[tatoo.git] / src / ata.mli

diff --git a/src/ata.mli b/src/ata.mli
index 6b4c02a..eada8d0 100644 (file)
--- a/src/ata.mli
+++ b/src/ata.mli
@@ -68,7 +68,10 @@ module Formula :
   end
 (** Modules representing the Boolean formulae used in transitions *)
 
-module Transition : Hcons.S with type data = State.t * QNameSet.t * Formula.t
+module Transition : sig
+  include Hcons.S with type data = State.t * QNameSet.t * Formula.t
+  val print : Format.formatter -> t -> unit
+end
 (** A [Transition.t] is a hashconsed triple of the state, the set of labels and the formula *)
 
 
@@ -82,6 +85,9 @@ end
 type t
 (** 2-way Selecting Alternating Tree Automata *)
 
+val uid : t -> Uid.t
+(** return the internal unique ID of the automaton *)
+
 val get_states : t -> StateSet.t
 (** return the set of states of the automaton *)
 
@@ -110,6 +116,11 @@ val concat : t -> t -> t
     nodes [N], [a'' N = a' (a N)].
 *)
 
+val merge : t -> t -> t
+(** [merge a a'] creates a new automaton [a''] that evaluates both [a] and [a'']
+    in parallel
+*)
+
 module Builder :
 sig
   type auto = t