diff options
Diffstat (limited to 'abstract/abs_interp.ml')
| -rw-r--r-- | abstract/abs_interp.ml | 37 |
1 files changed, 14 insertions, 23 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index 7950144..7a53134 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -52,6 +52,7 @@ end = struct guarantees; Format.printf "@."; + let env = E.set_disjunct env "/exit" DNever in let env = E.apply_f env init_f in let cl = Formula.conslist_of_f f in @@ -72,7 +73,7 @@ end = struct let tr_assigns = List.fold_left (fun q (_, id, _) -> if id.[0] = 'N' then - (String.sub id 1 (String.length id - 1), NIdent id)::q + (String.sub id 1 (String.length id - 1), id)::q else q) [] vars @@ -95,14 +96,10 @@ end = struct (* loop : st -> env -> env -> env *) - let loop st pnew stay = + let loop st acc0 = - Format.printf "Loop @[<hv>%a@]@.New @[<hv>%a@]@.Stay @[<hv>%a@]@." - Formula_printer.print_conslist st.cl - E.print_all pnew E.print_all stay; - - let add_stay = cycle st st.cl pnew in - let acc0 = E.join stay add_stay in + Format.printf "Loop @[<hv>%a@]@.@." + Formula_printer.print_conslist st.cl; let fsharp cl i = Format.printf "Acc @[<hv>%a@]@." E.print_all i; @@ -121,7 +118,7 @@ end = struct let x = iter 0 acc0 in let y = fix E.eq (fsharp st.cl_g) x in (* decreasing iteration *) - let z = E.apply_cl y st.cl in + let z = E.apply_cl y st.cl in (* no more guarantee *) y, z (* @@ -130,20 +127,14 @@ end = struct let do_prog widen_delay rp = let st = init_state widen_delay rp in - let pnew = st.env in - let pnew_c = E.apply_cl pnew st.cl in - - let stay, stay_c = loop st pnew (E.vbottom pnew) in - - Format.printf "@.@[<hov>New %a@]@.@." - E.print_all pnew_c; - Format.printf "@[<hov>Stay %a@]@.@." - E.print_all stay_c; - - let final = E.join pnew_c stay_c in + let final, final_c = loop st st.env in - Format.printf "@[<hov>Final %a@]@.@." + Format.printf "@[<hov>F %a@]@.@." E.print_all final; + (* + Format.printf "@[<hov>F' %a@]@.@." + E.print_all final_c; + *) let check_guarantee (id, f) = let cl = Formula.conslist_of_f f in @@ -162,9 +153,9 @@ end = struct end; if List.exists (fun (p, _, _) -> p) st.rp.all_vars then begin - Format.printf "Probes:@[<v>"; + Format.printf "Probes: @[<v 0>"; List.iter (fun (p, id, _) -> - if p then Format.printf " %a ∊ %a@ " + if p then Format.printf "%a ∊ %a@ " Formula_printer.print_id id E.print_itv (E.var_itv final id)) st.rp.all_vars; |