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