diff options
| -rw-r--r-- | abstract/abs_interp_edd.ml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index f08be44..510bf93 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -200,6 +200,8 @@ end = struct let fmt = Format.formatter_of_out_channel o in Format.fprintf fmt "digraph G {@[<v 4>@,"; + let nov = Hashtbl.create 12 in + let f f_rec = function | DChoice(n, v, x) -> let aux fmt = function @@ -208,12 +210,21 @@ end = struct | DVal(i, _) -> Format.fprintf fmt "v%d" i | DChoice(n, _, _) -> Format.fprintf fmt "n%d" n in + let p = try Hashtbl.find nov v with _ -> [] in + Hashtbl.replace nov v (n::p); Format.fprintf fmt "n%d [label=\"%s\"];@ " n v; List.iter (fun (i, c) -> if c <> DBot then Format.fprintf fmt "n%d -> %a [label=\"%s\"];@ " n aux c i; f_rec c) x | _ -> () in memo f v.root; + + Hashtbl.iter (fun var nodes -> + Format.fprintf fmt "{ rank = same; "; + List.iter (Format.fprintf fmt "n%d; ") nodes; + Format.fprintf fmt "}@ ") + nov; + Format.fprintf fmt "@]}@."; close_out o |