Implement formulae parametrized by atomic predicates.

[tatoo.git] / src / ata.ml

diff --git a/src/ata.ml b/src/ata.ml
index cad28e1..6ec859c 100644 (file)
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -14,20 +14,84 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-01-30 19:09:27 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-02-06 14:24:24 CET by Kim Nguyen>
 *)
 
 open Format
+type move = [ `Left | `Right | `Up1 | `Up2 | `Epsilon ]
+type state_ctx = { left : StateSet.t;
+                   right : StateSet.t;
+                   up1 : StateSet.t;
+                   up2 : StateSet.t;
+                   epsilon : StateSet.t}
+type ctx_ = { mutable positive : state_ctx;
+             mutable negative : state_ctx }
+type pred_ = move * bool * State.t
 
+module Move : (Formula.PREDICATE with type data = pred_ and type ctx = ctx_ ) =
+struct
+
+  module Node =
+  struct
+    type t = move * bool * State.t
+    let equal n1 n2 = n1 = n2
+    let hash n = Hashtbl.hash n
+  end
+
+  type ctx = ctx_
+  let make_ctx a b c d e =
+    { left = a; right = b; up1 = c; up2 = d; epsilon = e }
+
+  include Hcons.Make(Node)
+
+  let print ppf a =
+    let _ = flush_str_formatter() in
+    let fmt = str_formatter in
+
+    let m, b, s = a.node in
+    let dir,num =
+      match  m with
+      | `Left ->  Pretty.down_arrow, Pretty.subscript 1
+      | `Right -> Pretty.down_arrow, Pretty.subscript 2
+      | `Epsilon -> Pretty.epsilon, ""
+      | `Up1 -> Pretty.up_arrow, Pretty.subscript 1
+      | `Up2 -> Pretty.up_arrow, Pretty.subscript 2
+    in
+    fprintf fmt "%s%s" dir num;
+    State.print fmt s;
+    let str = flush_str_formatter() in
+    if b then fprintf ppf "%s" str
+    else Pretty.pp_overline ppf str
+
+  let neg p =
+    let l, b, s = p.node in
+    make (l, not b, s)
+
+  let eval ctx p =
+    let l, b, s = p.node in
+    let nctx = if b then ctx.positive else ctx.negative in
+    StateSet.mem s begin
+      match l with
+        `Left -> nctx.left
+      | `Right -> nctx.right
+      | `Up1 -> nctx.up1
+      | `Up2 -> nctx.up2
+      | `Epsilon -> nctx.epsilon
+    end
+end
+
+module SFormula = Formula.Make(Move)
 type t = {
   id : Uid.t;
   mutable states : StateSet.t;
   mutable top_states : StateSet.t;
   mutable bottom_states: StateSet.t;
   mutable selection_states: StateSet.t;
-  transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t;
+  transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
 }
 
+
+
 let next = Uid.make_maker ()
 
 let create () = { id = next ();
@@ -47,7 +111,7 @@ let add_trans a q s f =
         (rem, tr :: atrs)
       else
         let nrem = QNameSet.diff rem labs in
-        nrem, (nlabs, Formula.or_ phi f)::atrs
+        nrem, (nlabs, SFormula.or_ phi f)::atrs
     ) (s, []) trs
   in
   let ntrs = if QNameSet.is_empty rem then ntrs
@@ -84,7 +148,7 @@ let print fmt a =
   let strs_strings, maxs = List.fold_left (fun (accl, accm) (q, s, f) ->
     let s1 = State.print sfmt q; flush_str_formatter () in
     let s2 = QNameSet.print sfmt s; flush_str_formatter () in
-    let s3 = Formula.print sfmt f; flush_str_formatter () in
+    let s3 = SFormula.print sfmt f; flush_str_formatter () in
     ( (s1, s2, s3) :: accl,
       max
         accm (2 + String.length s1 + String.length s2))