1 files changed, 17 insertions, 9 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 1838591..0a330c2 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -88,7 +88,7 @@ end = struct
       let env = E.apply_f env init_f in
 
       Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
-      Format.printf "Cycle formula: %a@.@." Formula_printer.print_conslist cl;
+      Format.printf "Cycle formula: %a@.@." Formula_printer.print_expr f;
 
       { p; root_scope; f; cl; all_vars; env }
 
@@ -116,24 +116,32 @@ end = struct
                  not (List.exists (fun (_, id2, _) -> id2 = "N"^id) vars))
               vars) in
       let e = List.fold_left E.forgetvar e forget_vars in
-      Format.printf "Pass cycle: %a@.@." E.print_all e;
       e
 
 
+    (* cycle : st -> env -> env *)
+    let cycle st i =
+      let i' = E.apply_cl i st.cl in
+      i', pass_cycle st.all_vars i'
+
     (*
       do_prog : prog -> id -> st
     *)
     let do_prog p root =
       let st = init_state p root in
 
-      let rec step acc i n =
-        Format.printf "Step %d: %a@." n E.print_all acc;
+      let _, acc = cycle st st.env in
+
+      let rec step acc n =
         if n < 10 then begin
-          let i' = E.apply_cl (E.join i acc) st.cl in
-          let j = pass_cycle st.all_vars i' in
-          let acc' = (if n > 6 then E.widen else E.join) acc j in
-          step acc' i (n+1)
+          Format.printf "Step %d: %a@." n E.print_all acc;
+          let i', j = cycle st acc in
+          Format.printf " -> %a@." E.print_all i';
+          Format.printf "Pass cycle: %a@.@." E.print_all j;
+
+          let acc' = (if n >= 7 then E.widen else E.join) acc j in
+          step acc' (n+1)
         end
       in
-      step (E.vbottom st.env) st.env 0
+      step acc 0
 end