ata.mli

   1 type state = int
   2 val mk_state : unit -> state
   3
   4 type predicate = Ptset.t*Ptset.t -> Tree.Binary.t ->  [ `True | `False | `Maybe ]
   5 type formula_expr =
   6     False
   7   | True
   8   | Or of formula * formula
   9   | And of formula * formula
  10   | Atom of ([ `Left | `Right ] * bool * state * predicate option)
  11 and formula = { fid : int; pos : formula_expr; neg : formula; st : Ptset.t*Ptset.t;}
  12 val true_ : formula
  13 val false_ : formula
  14 val atom_ : ?pred:predicate option -> [`Left | `Right ] -> bool -> state -> formula
  15 val and_ : formula -> formula -> formula
  16 val or_ : formula -> formula -> formula
  17 val not_ : formula -> formula
  18 val equal_form : formula -> formula -> bool
  19 val pr_frm : Format.formatter -> formula -> unit
  20
  21
  22 type property = [ `None | `Existential  ]
  23
  24 type t = {
  25   id : int;
  26   states : Ptset.t;
  27   init : Ptset.t;
  28   final : Ptset.t;
  29   universal : Ptset.t;
  30   phi : (TagSet.t * state, bool * formula) Hashtbl.t;
  31   delta : (TagSet.t, Ptset.t * bool * Ptset.t * Ptset.t) Hashtbl.t;
  32   properties : (state,property) Hashtbl.t;
  33 }
  34 val dump : Format.formatter -> t -> unit
  35
  36 module Transitions : sig
  37 type t = state*TagSet.t*bool*formula
  38 (* Doing this avoid the parenthesis *)
  39 val ( ?< ) : state -> state
  40 val ( >< ) : state -> TagSet.t*bool -> state*(TagSet.t*bool)
  41 val ( >=> ) : state*(TagSet.t*bool) -> formula -> t
  42 val ( +| ) : formula -> formula -> formula
  43 val ( *& ) : formula -> formula -> formula
  44 val ( ** ) : [`Left | `Right ] -> state -> formula
  45
  46 end
  47 type transition = Transitions.t
  48 val equal_trans : transition -> transition -> bool
  49
  50
  51 module BottomUpNew :
  52 sig
  53   val miss : int ref
  54   val call : int ref
  55   val run : t -> Tree.Binary.t -> Tree.Binary.t list
  56 end