Project

General

Profile

Revision 720f159a

View differences:

src/backends/Horn/horn_backend.ml
539 539

  
540 540

  
541 541
let traces_file fmt basename prog machines =
542
  (* Format.fprintf fmt *)
543
  (*   "; Horn code traceability generated by %s@.; SVN version number %s@.@." *)
544
  (*   (Filename.basename Sys.executable_name) *)
545
  (*   Version.number; *)
546

  
542 547
  Format.fprintf fmt
543
    "; Horn code traceability generated by %s@.; SVN version number %s@.@."
544
    (Filename.basename Sys.executable_name)
545
    Version.number;
548
  "<?xml version=\"1.0\"?>\n<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">\n";
546 549

  
547 550
  (* We extract the annotation dealing with traceability *)
548 551
  let machines_traces = List.map (fun m ->
......
584 587
  in
585 588

  
586 589
  List.iter (fun m ->
587
    Format.fprintf fmt "; Node %s@." m.mname.node_id;
590
    (* Format.fprintf fmt "; Node %s@." m.mname.node_id; *)
591
    Format.fprintf fmt "    <Node name=\"%s\">@." m.mname.node_id;
588 592

  
589 593
    let memories_old =
590 594
      List.map (fun (p, v) ->
......
622 626
      Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
623 627
    in
624 628

  
625
    Format.fprintf fmt "; Init predicate@.";
626

  
627
    Format.fprintf fmt "; horn encoding@.";
628
    Format.fprintf fmt "(%a %a)@."
629
      pp_machine_init_name m.mname.node_id
630
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
631

  
632
    Format.fprintf fmt "; original expressions@.";
633
    Format.fprintf fmt "(%a %a%t%a)@."
634
      pp_machine_init_name m.mname.node_id
635
      (Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
636
      (fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt " ")
637
      (Utils.fprintf_list ~sep:" " (fun fmt (prefix, ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next;
638

  
639
    Format.pp_print_newline fmt ();
640
    Format.fprintf fmt "; Step predicate@.";
641

  
642
    Format.fprintf fmt "; horn encoding@.";
643
    Format.fprintf fmt "(%a %a)@."
644
      pp_machine_step_name m.mname.node_id
645
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
646
    Format.fprintf fmt "; original expressions@.";
647
    Format.fprintf fmt "(%a %a%t%a)@."
648
      pp_machine_step_name m.mname.node_id
649
      (Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
650
      (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ")
651
      (Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next);
652
    Format.pp_print_newline fmt ();
653
  ) (List.rev machines);
629
    Format.fprintf fmt "      <Init name=\"%a\">@."
630
                   pp_machine_init_name m.mname.node_id;
631

  
632
    Format.fprintf fmt "\t<input name=\"%a\" type=\"\">%a</input> @."
633
                   (Utils.fprintf_list ~sep:" | " pp_var) (rename_machine_list m.mname.node_id m.mstep.step_inputs)
634
                   (Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_inputs);
635

  
636
    Format.fprintf fmt "\t<output name=\"%a\" type=\"\">%a</output> @."
637
                   (Utils.fprintf_list ~sep:" | " pp_var) (rename_machine_list m.mname.node_id m.mstep.step_outputs)
638
                   (Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs);
639

  
640
    Format.fprintf fmt "\t<local name=\"%a\" type=\"\">%t%a</local> @."
641
                   (Utils.fprintf_list ~sep:" | " pp_var) (rename_next_list (full_memory_vars machines m))
642
   (fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt " ")
643
   (Utils.fprintf_list ~sep:" " (fun fmt (prefix, ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next;
644

  
645
    Format.fprintf fmt "      </Init>@.";
646

  
654 647

  
648
    Format.fprintf fmt "      <Step name=\"%a\">@."
649
                   pp_machine_step_name m.mname.node_id;
650

  
651
    Format.fprintf fmt "\t<input name=\"%a\" type=\"\">%a</input> @."
652
                   (Utils.fprintf_list ~sep:" | " pp_var) (rename_machine_list m.mname.node_id m.mstep.step_inputs)
653
                   (Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_inputs);
654

  
655
    Format.fprintf fmt "\t<output name=\"%a\" type=\"\">%a</output> @."
656
                   (Utils.fprintf_list ~sep:" | " pp_var) (rename_machine_list m.mname.node_id m.mstep.step_outputs)
657
                   (Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs);
658

  
659
    Format.fprintf fmt "\t<local name=\"%a\" type=\"\">%t%a</local> @."
660
                   (Utils.fprintf_list ~sep:" | " pp_var) ((rename_current_list (full_memory_vars machines m)) @
661
    (rename_next_list (full_memory_vars machines m)))
662
                   (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ")
663
                     (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next);
664

  
665
    Format.fprintf fmt "      </Step>@.";
666
     Format.fprintf fmt "    </Node>@.";
667

  
668
  ) (List.rev machines);
669
  Format.fprintf fmt "</Traces>@.";
655 670

  
656 671
(* Local Variables: *)
657 672
(* compile-command:"make -C ../.." *)
src/main_lustre_compiler.ml
268 268
	Horn_backend.translate fmt basename prog machine_code;
269 269
	(* Tracability file if option is activated *)
270 270
	if !Options.traces then (
271
	let traces_file = destname ^ ".traces" in (* Could be changed *)
271
	let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
272 272
	let traces_out = open_out traces_file in
273 273
	let fmt = formatter_of_out_channel traces_out in
274
	Horn_backend.traces_file fmt basename prog machine_code
274
	Horn_backend.traces_file fmt basename prog machine_code;
275

  
275 276
	)
276 277
      end
277 278
    | "lustre" ->

Also available in: Unified diff