Project

General

Profile

Revision d75eb6f1 src/tools/seal/seal_verifier.ml

View differences:

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