Release coccinelle-0.1.9-rc1

[bpt/coccinelle.git] / ctl / ctl_engine.ml

diff --git a/ctl/ctl_engine.ml b/ctl/ctl_engine.ml
index 65c3338..e0f9a88 100644 (file)
--- a/ctl/ctl_engine.ml
+++ b/ctl/ctl_engine.ml
@@ -1097,7 +1097,8 @@ let satAX dir m s reqst = pre_forall dir m s s reqst
 
 (* E[phi1 U phi2] == phi2 \/ (phi1 /\ EXE[phi1 U phi2]) *)
 let satEU dir ((_,_,states) as m) s1 s2 reqst print_graph = 
-  let ctr = ref 0 in
+  (*Printf.printf "EU\n";
+  let ctr = ref 0 in*)
   inc satEU_calls;
   if s1 = []
   then s2
@@ -1110,21 +1111,23 @@ let satEU dir ((_,_,states) as m) s1 s2 reqst print_graph =
        match new_info with
          [] -> y
        | new_info ->
-           ctr := !ctr + 1;
-           print_graph y ctr;
+           (*ctr := !ctr + 1;
+           print_graph y ctr;*)
            let first = triples_conj s1 (pre_exist dir m new_info reqst) in
            let res = triples_union first y in
            let new_info = setdiff res y in
            (*Printf.printf "iter %d res %d new_info %d\n"
            !ctr (List.length res) (List.length new_info);
+           print_state "res" res;
+           print_state "new_info" new_info;
            flush stdout;*)
            f res new_info in
       f s2 s2
     else
       let f y =
        inc_step();
-       ctr := !ctr + 1;
-       print_graph y ctr;
+       (*ctr := !ctr + 1;
+       print_graph y ctr;*)
        let pre = pre_exist dir m y reqst in
        triples_union s2 (triples_conj s1 pre) in
       setfix f s2
@@ -1278,9 +1281,16 @@ let satAW dir ((grp,_,states) as m) s1 s2 reqst =
        print_state "y" y;
        flush stdout;*)
        let pre = pre_forall dir m y y reqst in
+       (*print_state "pre" pre;*)
        let conj = triples_conj s1 pre in (* or triples_conj_AW *)
        triples_union s2 conj in
-      setgfix f (triples_union s1 s2)
+      let drop_wits = List.map (function (s,e,_) -> (s,e,[])) in
+      (* drop wits on s1 represents that we don't want any witnesses from
+        the case that infinitely loops, only from the case that gets
+        out of the loop. s1 is like a guard. To see the problem, consider
+        an example where both s1 and s2 match some code after the loop.
+        we only want the witness from s2. *)
+      setgfix f (triples_union (drop_wits s1) s2)
 ;;
 
 let satAF dir m s reqst = 
@@ -1801,7 +1811,8 @@ let rec satloop unchecked required required_states
                       (* no graph, for the moment *)
                       (fun y str -> ()))
                    s1 in
-               strict_A2 strict satAW satEF dir m s1 s2 new_required_states)
+               strict_A2 strict satAW satEF dir m s1 s2 new_required_states
+               )
     | A.Implies(phi1,phi2) ->
        loop unchecked required required_states (A.Or(A.Not phi1,phi2))
     | A.Exists (keep,v,phi)     ->