Project

General

Profile

Revision 81229f63 src/tools/seal/seal_verifier.ml

View differences:

src/tools/seal/seal_verifier.ml
63 63

  
64 64
  let consts = Corelang.(List.map const_of_top (get_consts prog)) in
65 65
  let sw_init, sw_sys = node_as_switched_sys consts mems sliced_nd in
66
  let pp_res =
66
  let pp_res pp_expr =
67 67
    (Utils.fprintf_list ~sep:"@ "
68
       (fun fmt (gel, up) ->
69
         Format.fprintf fmt "@[<v 2>[%a]:@ %a@]"
70
           (Utils.fprintf_list ~sep:"; "
71
              (fun fmt (e,b) ->
72
                if b then Printers.pp_expr fmt e
73
                else Format.fprintf fmt "not(%a)"
74
                       Printers.pp_expr e)) gel
68
       (fun fmt (g, up) ->
69
         Format.fprintf fmt "@[<v 2>[%t]:@ %a@]"
70
           (fun fmt -> match g with None -> () | Some g -> pp_expr fmt g)
71
           
72
           (* (Utils.fprintf_list ~sep:"; "
73
            *    (fun fmt (e,b) ->
74
            *      if b then pp_expr fmt e
75
            *      else Format.fprintf fmt "not(%a)"
76
            *             pp_expr e)) gel *)
75 77
           (Utils.fprintf_list ~sep:";@ "
76 78
              (fun fmt (id, e) ->
77 79
                Format.fprintf fmt "%s = @[<hov 0>%a@]"
78 80
                  id
79
                  Printers.pp_expr e)) up
81
                  pp_expr e)) up
80 82
    ))
81 83
  in
82 84
  report ~level:1 (
......
88 90
               
89 91
    );
90 92
  report ~level:1 (fun fmt ->
93
      (*let pp_res = pp_res (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag)  in*)
94
       let pp_res = pp_res Printers.pp_expr in
91 95
      Format.fprintf fmt "@[<v 0>@[<v 3>Init:@ %a@]@ "
92
        pp_res sw_init;
96
        pp_res  sw_init;
93 97
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ "
94
        pp_res sw_sys
98
        pp_res  sw_sys
95 99
    );
96
  
97

  
100
  (* let new_node = Seal_export.to_lustre(m,sw_init, sw_sys) in  
101
   * Format.eprintf "%a@." Printer.pp_node new_node; *)
98 102
  ()
99 103
  
100 104
module Verifier =

Also available in: Unified diff