Revision 720f159a
Added by Teme Kahsai over 8 years ago
| 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 ../.." *) |
Also available in: Unified diff
mapping horn values to lustre values in xml format