Project

General

Profile

« Previous | Next » 

Revision 720f159a

Added by Teme Kahsai over 8 years ago

mapping horn values to lustre values in xml format

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