src/ata.mli

   1 type t = {
   2     id : int;
   3     states : StateSet.t;
   4     init : StateSet.t;
   5     last : State.t;
   6     (* Transitions of the Alternating automaton *)
   7     trans : (State.t, (TagSet.t * Transition.t) list) Hashtbl.t;
   8     marking_states : StateSet.t;
   9     topdown_marking_states : StateSet.t;
  10     bottom_states : StateSet.t;
  11     true_states : StateSet.t;
  12 }
  13
  14
  15 val print : Format.formatter -> t -> unit
  16
  17 type jump_kind = NIL
  18             | NODE
  19             | STAR
  20             | JUMP_ONE of Ptset.Int.t
  21             | JUMP_MANY of Ptset.Int.t
  22             | CAPTURE_MANY of Ptset.Int.t
  23
  24
  25 val top_down_approx : t -> StateSet.t -> Tree.t -> jump_kind
  26
  27 val init : unit -> unit