Add a first runtime function. Positive fragment seems to work.

[tatoo.git] / src / auto / ata.ml

diff --git a/src/auto/ata.ml b/src/auto/ata.ml
index 576941d..f4f11db 100644 (file)
--- a/src/auto/ata.ml
+++ b/src/auto/ata.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-04 23:39:48 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-05 16:31:57 CET by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -29,6 +29,12 @@ type state_ctx = { mutable left : StateSet.t;
              mutable epsilon : StateSet.t}
 
 type pred_ = move * bool * State.t
+let make_ctx a b c d e =
+  { left = a; right = b; up1 = c; up2 = d; epsilon = e }
+
+let print_ctx fmt c = fprintf fmt "{ left : %a; right : %a; up1: %a ; up2 : %a; epsilon : %a }"
+  StateSet.print c.left StateSet.print c.right StateSet.print c.up1 StateSet.print c.up2
+  StateSet.print c.epsilon
 
 module Move : (Formula.PREDICATE with type data = pred_ and type ctx = state_ctx ) =
 struct
@@ -42,8 +48,6 @@ struct
 
   type ctx = state_ctx
 
-  let make_ctx a b c d e =
-    { left = a; right = b; up1 = c; up2 = d; epsilon = e }
 
   include Hcons.Make(Node)
   let _pr_buff = Buffer.create 10
@@ -76,7 +80,7 @@ struct
   exception NegativeAtom of (move*State.t)
   let eval ctx p =
     let l, b, s = p.node in
-    if b then raise (NegativeAtom(l,s));
+    if not b then raise (NegativeAtom(l,s));
     StateSet.mem s begin
       match l with
         `Left -> ctx.left
@@ -91,8 +95,8 @@ 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 top_states : StateSet.t;
+  mutable bottom_states: StateSet.t;
   mutable selection_states: StateSet.t;
   transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
 }
@@ -101,13 +105,22 @@ let next = Uid.make_maker ()
 
 let create () = { id = next ();
                   states = StateSet.empty;
-(*                  top_states = StateSet.empty;
-                  bottom_states = StateSet.empty; *)
+                  top_states = StateSet.empty;
+                  bottom_states = StateSet.empty;
                   selection_states = StateSet.empty;
                   transitions = Hashtbl.create 17;
  }
 
 
+let get_trans a states tag =
+  StateSet.fold (fun q acc0 ->
+    try
+      let trs = Hashtbl.find a.transitions q in
+      List.fold_left (fun acc1 (labs, phi) ->
+        if QNameSet.mem tag labs then (q,phi)::acc1 else acc1) acc0 trs
+    with Not_found -> acc0
+  ) states []
+
 (*
   [add_trans a q labels f] adds a transition [(q,labels) -> f] to the
   automaton [a] but ensures that transitions remains pairwise disjoint
@@ -146,10 +159,14 @@ let print fmt a =
   fprintf fmt
     "\nInternal UID: %i@\n\
      States: %a@\n\
+     Top states: %a@\n\
+     Bottom states: %a@\n\
      Selection states: %a@\n\
      Alternating transitions:@\n"
     (a.id :> int)
     StateSet.print a.states
+    StateSet.print a.top_states
+    StateSet.print a.bottom_states
     StateSet.print a.selection_states;
   let trs =
     Hashtbl.fold
@@ -207,7 +224,7 @@ let complete_transitions a =
    complementing the sub-automaton in the negative states.
    [TODO check the meaning of negative upward arrows]
 *)
-let normalize_negations a =
+let normalize_negations auto =
   let memo_state = Hashtbl.create 17 in
   let todo = Queue.create () in
   let rec flip b f =
@@ -226,7 +243,7 @@ let normalize_negations a =
            either we have a positive state deep below a negation
            or we have a negative state in a positive formula
            b' = sign of the state
-           b = sign of the containing formula
+           b = sign of the enclosing formula
         *)
         let not_q =
           try
@@ -236,6 +253,10 @@ let normalize_negations a =
             Not_found ->
               (* create a new state and add it to the todo queue *)
               let nq = State.make () in
+              if not (StateSet.mem q auto.bottom_states) then
+                auto.bottom_states <- StateSet.add nq auto.bottom_states;
+              if not (StateSet.mem q auto.top_states) then
+                auto.top_states <- StateSet.add nq auto.top_states;
               Hashtbl.add memo_state (q, false) nq;
               Queue.add (q, false) todo; nq
         in
@@ -243,7 +264,9 @@ let normalize_negations a =
       end
     end
   in
-  StateSet.iter (fun q -> Queue.add (q, true) todo) a.selection_states;
+  (* states that are not reachable from a selection stat are not interesting *)
+  StateSet.iter (fun q -> Queue.add (q, true) todo) auto.selection_states;
+
   while not (Queue.is_empty todo) do
     let (q, b) as key = Queue.pop todo in
     let q' =
@@ -251,10 +274,17 @@ let normalize_negations a =
         Hashtbl.find memo_state key
       with
         Not_found ->
-          let nq = if b then q else State.make () in
+          let nq = if b then q else
+              let nq = State.make () in
+              if not (StateSet.mem q auto.bottom_states) then
+                auto.bottom_states <- StateSet.add nq auto.bottom_states;
+              if not (StateSet.mem q auto.top_states) then
+                auto.top_states <- StateSet.add nq auto.top_states;
+              nq
+          in
           Hashtbl.add memo_state key nq; nq
     in
-    let trans = Hashtbl.find a.transitions q in
+    let trans = Hashtbl.find auto.transitions q in
     let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in
-    Hashtbl.replace a.transitions q' trans'
+    Hashtbl.replace auto.transitions q' trans'
   done