diff options
| author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-11 14:50:18 +0200 |
|---|---|---|
| committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-11 14:50:18 +0200 |
| commit | fd027ca593bdfb2d2db811730521b4f5d52c8593 (patch) | |
| tree | 94982e74c74a480e9bafd235101d1934a330439e /abstract/abs_interp.ml | |
| parent | 9ca8bcb35eb0385c8f9852045bb282c445bd6901 (diff) | |
| download | scade-analyzer-fd027ca593bdfb2d2db811730521b4f5d52c8593.tar.gz scade-analyzer-fd027ca593bdfb2d2db811730521b4f5d52c8593.zip | |
Acceptable heuristic.
Diffstat (limited to 'abstract/abs_interp.ml')
| -rw-r--r-- | abstract/abs_interp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index 2597a63..b5fc684 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -171,7 +171,7 @@ end = struct (* program expressions *) cl : conslist; - guarantees : (id * bool_expr) list; + guarantees : (id * bool_expr * id) list; (* abstract interpretation *) cycle : (id * id * typ) list; (* s'(x) = s(y) *) @@ -283,7 +283,7 @@ end = struct let guarantees = Transform.guarantees_of_prog rp in Format.printf "Guarantees:@."; - List.iter (fun (id, f) -> + List.iter (fun (id, f, _) -> Format.printf " %s: %a@." id Formula_printer.print_expr f) guarantees; Format.printf "@."; @@ -433,7 +433,7 @@ end = struct Format.printf "Accessible: %a@." print_dd final; - let check_guarantee (id, f) = + let check_guarantee (id, f, _) = let cl = Formula.conslist_of_f f in Format.printf "@[<hv 4>%s:@ %a ⇒ ⊥ @ " id Formula_printer.print_conslist cl; |