Preliminary work for multiple starters evaluation.

[tatoo.git] / src / ata.ml

diff --git a/src/ata.ml b/src/ata.ml
index 7310839..79d47a9 100644 (file)
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -142,6 +142,7 @@ end =
 type t = {
   id : Uid.t;
   mutable states : StateSet.t;
 type t = {
   id : Uid.t;
   mutable states : StateSet.t;

+  mutable starting_states : StateSet.t;

   mutable selecting_states: StateSet.t;
   transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t;
 }
   mutable selecting_states: StateSet.t;
   transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t;
 }


@@ -149,6 +150,7 @@ type t = {
 
 
 let get_states a = a.states
 
 
 let get_states a = a.states

+let get_starting_states a = a.starting_states

 let get_selecting_states a = a.selecting_states
 
 let get_trans a tag states =
 let get_selecting_states a = a.selecting_states
 
 let get_trans a tag states =


@@ -174,10 +176,12 @@ let print fmt a =
   fprintf fmt
     "Internal UID: %i@\n\
      States: %a@\n\
   fprintf fmt
     "Internal UID: %i@\n\
      States: %a@\n\

+     Starting states: %a@\n\

      Selection states: %a@\n\
      Alternating transitions:@\n"
     (a.id :> int)
     StateSet.print a.states
      Selection states: %a@\n\
      Alternating transitions:@\n"
     (a.id :> int)
     StateSet.print a.states

+    StateSet.print a.starting_states

     StateSet.print a.selecting_states;
   let trs =
     Hashtbl.fold
     StateSet.print a.selecting_states;
   let trs =
     Hashtbl.fold


@@ -219,19 +223,24 @@ let print fmt a =
 
 let complete_transitions a =
   StateSet.iter (fun q ->
 
 let complete_transitions a =
   StateSet.iter (fun q ->

-    let qtrans = Hashtbl.find a.transitions q in
-    let rem =
-      List.fold_left (fun rem (labels, _) ->
-        QNameSet.diff rem labels) QNameSet.any qtrans
-    in
-    let nqtrans =
-      if QNameSet.is_empty rem then qtrans
-      else
-        (rem, Formula.false_) :: qtrans
-    in
-    Hashtbl.replace a.transitions q nqtrans
+    if StateSet.mem q a.starting_states then ()
+    else
+      let qtrans = try Hashtbl.find a.transitions q with Not_found -> eprintf "Not found here 226\n%!"; raise Not_found in
+      let rem =
+        List.fold_left (fun rem (labels, _) ->
+          QNameSet.diff rem labels) QNameSet.any qtrans
+      in
+      let nqtrans =
+        if QNameSet.is_empty rem then qtrans
+        else
+          (rem, Formula.false_) :: qtrans
+      in
+      Hashtbl.replace a.transitions q nqtrans

   ) a.states
 
   ) a.states
 

+(* [cleanup_states] remove states that do not lead to a
+   selecting states *)
+

 let cleanup_states a =
   let memo = ref StateSet.empty in
   let rec loop q =
 let cleanup_states a =
   let memo = ref StateSet.empty in
   let rec loop q =


@@ -308,7 +317,7 @@ let normalize_negations auto =
           in
           Hashtbl.add memo_state key nq; nq
     in
           in
           Hashtbl.add memo_state key nq; nq
     in

-    let trans = Hashtbl.find auto.transitions q in
+    let trans = try Hashtbl.find auto.transitions q with Not_found -> eprintf "Not_found here 318\n%!"; [] in

     let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in
     Hashtbl.replace auto.transitions q' trans';
   done;
     let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in
     Hashtbl.replace auto.transitions q' trans';
   done;


@@ -326,6 +335,7 @@ module Builder =
         {
           id = next ();
           states = StateSet.empty;
         {
           id = next ();
           states = StateSet.empty;

+          starting_states = StateSet.empty;

           selecting_states = StateSet.empty;
           transitions = Hashtbl.create MED_H_SIZE;
         }
           selecting_states = StateSet.empty;
           transitions = Hashtbl.create MED_H_SIZE;
         }


@@ -350,8 +360,9 @@ module Builder =
       ); *)
       auto
 
       ); *)
       auto
 

-    let add_state a ?(selecting=false) q =
+    let add_state a ?(starting=false) ?(selecting=false) q =

       a.states <- StateSet.add q a.states;
       a.states <- StateSet.add q a.states;

+      if starting then a.starting_states <- StateSet.add q a.starting_states;

       if selecting then a.selecting_states <- StateSet.add q a.selecting_states
 
     let add_trans a q s f =
       if selecting then a.selecting_states <- StateSet.add q a.selecting_states
 
     let add_trans a q s f =