Revision d75eb6f1 src/tools/seal/seal_verifier.ml
src/tools/seal/seal_verifier.ml | ||
---|---|---|
62 | 62 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@."); |
63 | 63 |
|
64 | 64 |
let consts = Corelang.(List.map const_of_top (get_consts prog)) in |
65 |
let sw_init, sw_sys = node_as_switched_sys consts mems sliced_nd in |
|
65 |
let sw_init, sw_sys, init_out, update_out = node_as_switched_sys consts mems sliced_nd in
|
|
66 | 66 |
let pp_res pp_expr = |
67 | 67 |
(Utils.fprintf_list ~sep:"@ " |
68 | 68 |
(fun fmt (g, up) -> |
... | ... | |
97 | 97 |
Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ " |
98 | 98 |
pp_res sw_sys |
99 | 99 |
); |
100 |
(* let new_node = Seal_export.to_lustre(m,sw_init, sw_sys) in
|
|
101 |
* Format.eprintf "%a@." Printer.pp_node new_node; *)
|
|
100 |
let new_node = Seal_export.to_lustre m sw_init sw_sys init_out update_out in
|
|
101 |
Format.eprintf "%a@." Printers.pp_node new_node;
|
|
102 | 102 |
() |
103 | 103 |
|
104 | 104 |
module Verifier = |
Also available in: Unified diff