Project

General

Profile

Revision df647a81

View differences:

src/basic_library.ml
146 146
	["+";"-";"*";"/";"mod";"&&";"||";"xor";"impl";"<";">";"<=";">=";"!=";"="])
147 147
     @(List.map unary_fun ["uminus";"not"]))
148 148
*)  
149
let pp_c i pp_val fmt vl =
149
let pp_c i get_val_type pp_val fmt vl =
150 150
  match i, vl with
151
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
151
    | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3
152 152
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
153 153
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 
154 154
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 
155
    | "=", [v1; v2] when get_val_type v1 == Types.Tbool-> Format.fprintf fmt "((!!%a) == (!!%a))" pp_val v1 pp_val v2
155 156
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 
156 157
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 
157 158
    | "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2
......
190 191
  match i, vl with
191 192
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 
192 193
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
193
  | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 
194
  | "impl", [v1; v2] -> Format.fprintf fmt "(%a ==> %a)" pp_val v1 pp_val v2 
195
  | "=", [v1; v2] -> ( 
196
    try 
197
      match (get_val_type v1), (get_val_type v2) with
198
      | Types.Tbool, _ | _, Types.Tbool -> Format.fprintf fmt "(%a <==> %a)" pp_val v1 pp_val v2 
199
      | _ -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 
200
    with Not_found -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 
201
  )
194
  | "not", [v] -> Format.fprintf fmt "((%a == 0)?1:0)" pp_val v 
195
  | "impl", [v1; v2] -> Format.fprintf fmt "(%a?(%a?1:0):1)" pp_val v1 pp_val v2 
196
  | "=", [v1; v2] when get_val_type v1 == Types.Tbool-> Format.fprintf fmt "(((!!%a) == (!!%a))?1:0)" pp_val v1 pp_val v2
197
  | "=", [v1; v2] -> Format.fprintf fmt "((%a == %a)?1:0)" pp_val v1 pp_val v2
202 198
  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 
203 199
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2
204 200
  | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
src/c_backend.ml
208 208
  let rec aux t pp_suffix =
209 209
  match (Types.repr t).Types.tdesc with
210 210
  | Types.Tclock t'       -> aux t' pp_suffix
211
  | Types.Tbool           -> fprintf fmt "int %s%a" var pp_suffix ()
212
  | Types.Treal           -> fprintf fmt "real %s%a" var pp_suffix ()
211
  | Types.Tbool           -> fprintf fmt "_Bool %s%a" var pp_suffix ()
212
  | Types.Treal           -> fprintf fmt "double %s%a" var pp_suffix ()
213 213
  | Types.Tint            -> fprintf fmt "int %s%a" var pp_suffix ()
214 214
  | Types.Tarray (d, t')  ->
215 215
    let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
......
225 225

  
226 226

  
227 227
let pp_c_decl_instance_var fmt (name, (node, static)) = 
228
  fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name
228
  fprintf fmt "%a %s" pp_machine_memtype_name (node_name node) name
229 229

  
230 230
let pp_c_tag fmt t =
231 231
 pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
......
256 256
      if Types.is_array_type v.var_type
257 257
      then fprintf fmt "*%a" pp_var v
258 258
      else fprintf fmt "%s->_reg.%a" self pp_var v
259
    | Fun (n, vl)   -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl
259
    | Fun (n, vl)   -> Basic_library.pp_c n Machine_code.get_val_type (pp_c_val self pp_var) fmt vl
260 260

  
261 261
let pp_c_checks self outputs fmt checks =
262 262
  Utils.fprintf_list ~sep:"" 
......
326 326
 | _           :: q, Power (v, n) ->
327 327
   pp_value_suffix self loop_vars pp_value fmt v
328 328
 | _               , Fun (n, vl)  ->
329
   Basic_library.pp_c n (pp_value_suffix self loop_vars pp_value) fmt vl
329
   Basic_library.pp_c n Machine_code.get_val_type (pp_value_suffix self loop_vars pp_value) fmt vl
330 330
 | _               , _            ->
331 331
   let pp_var_suffix fmt v = fprintf fmt "%a%a" pp_value v pp_suffix loop_vars in
332 332
   pp_c_val self pp_var_suffix fmt value
......
344 344
  let reordered_loop_vars = reorder_loop_variables loop_vars in
345 345
  let rec aux fmt vars =
346 346
    match vars with
347
    | [] ->
348
      fprintf fmt "%a = %a;" 
349
	(pp_value_suffix self loop_vars pp_var) var_name
350
	(pp_value_suffix self loop_vars pp_var) value
347
    | [] -> fprintf fmt "%a = %a;" (pp_value_suffix self loop_vars pp_var) var_name
348
      (pp_value_suffix self loop_vars pp_var) value
351 349
    | (d, LVar i) :: q ->
352 350
(*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
353 351
      fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
......
388 386
 try (* stateful node instance *)
389 387
   let (n,_) = List.assoc i instances in
390 388
  (* Format.eprintf "pp_instance_call: %s , outputs are %a@.@?" (node_name n) (Utils.fprintf_list ~sep:", " Printers.pp_var) outputs; *)
391
 fprintf fmt "%s_step (%a%t%a%t%s->%s);"
389
 fprintf fmt "%s_step (%a%t%a%t&(%s->%s));"
392 390
     (node_name n)
393 391
     (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read machine_outputs))) inputs
394 392
     (Utils.pp_final_char_if_non_empty ", " inputs) 
......
419 417
 )
420 418
let pp_machine_reset instances self fmt inst =
421 419
  let (node, static) = List.assoc inst instances in
422
  fprintf fmt "%a(%a%t%s->%s);"
420
  fprintf fmt "%a(%a%t&(%s->%s));"
423 421
    pp_machine_reset_name (node_name node)
424 422
    (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
425 423
    (Utils.pp_final_char_if_non_empty ", " static)
......
468 466

  
469 467
(**************************************************************************)
470 468
(*     Printing spec for c *)
471

  
472 469
(**************************************************************************)
473 470

  
474 471
let pp_ident is_output fmt id =
......
555 552
    | Array _      
556 553
    | Access _       -> assert false (* no arrays *)
557 554
    | Power (v, n)  -> assert false
558
    | LocalVar v    -> pp_var fmt v
555
    | LocalVar v    -> pp_var "" fmt v
559 556
    | StateVar v    ->     
560 557
      if Types.is_array_type v.var_type
561 558
      then assert false
562
      else fprintf fmt "%s->_reg.%a" self pp_var v
559
      else fprintf fmt "%a" (pp_var (self^"._reg.")) v
563 560
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_acsl n Machine_code.get_val_type (pp_acsl_val self pp_var)) vl
564 561

  
562
(* Access to the value of a variable:
563
   - if it's not a scalar output, then its name is enough
564
   - otherwise, dereference it (it has been declared as a pointer,
565
     despite its scalar Lustre type)
566
   - moreover, cast arrays variables into their original array type.
567
*)
568
let pp_acsl_var_read outputs pre fmt id =
569
  if Types.is_array_type id.var_type
570
  then
571
    assert false (* no array *)
572
  else ( (* Hack to cast boolean variables as int for ACSL predicates *)
573
    (* This hack doesn't work because of int equality != bool equality and _Bool
574
        is supported now*)
575
    (*if (Types.repr id.var_type).Types.tdesc = Types.Tbool then
576
      fprintf fmt "(int)" 
577
    ;*)
578
    if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *)
579
    then fprintf fmt "%s*%s" pre id.var_id
580
    else fprintf fmt "%s%s" pre id.var_id
581
  )
565 582

  
566 583
let rec pp_eexpr_logic_instr 
567 584
    ((node_id, inputs, outputs, locals, memory) as m) self fmt instr =
......
570 587
  | MLocalAssign (i,v) -> (
571 588
    match outputs with 
572 589
    | [o] -> if i = o then
573
	fprintf fmt "%a;" (pp_acsl_val self (pp_c_var_read outputs)) v
590
	fprintf fmt "%a;" (pp_acsl_val self (pp_acsl_var_read outputs)) v
574 591
      else
575 592
	fprintf fmt "\\let %a = %a;" 
576 593
	  (pp_c_var_read outputs (* TODO no variable shold be treated as output *)) i
577
	  (pp_acsl_val self (pp_c_var_read outputs)) v
594
	  (pp_acsl_val self (pp_acsl_var_read outputs)) v
578 595

  
579 596
    | _ -> assert false (* should not happen: only a single output *)
580 597
)
......
601 618
  let self = mk_self m in
602 619
  let pp_expr_def fmt ee =
603 620
    match ee.mmstep_logic.step_instrs with
604
    | [MStep([o], i, vl)] -> () (* We do nothing, the expression is simple and 
605
				   was introduced directly in the contract *)
621
    (*| [MStep([o], i, vl)] -> () (* We do nothing, the expression is simple and 
622
				   was introduced directly in the contract *) *)
606 623
    | _ -> ((* We define a new ACSL predicate *)
607
      fprintf fmt "/*@@ @[<v 3>predicate spec_%i(%a%t%a *%s) =@;%a@]@;*/@." 
624
      fprintf fmt "/*@@ @[<v 3>predicate spec_%i(%a%t%a %s) =@;%a@]@;*/@." 
608 625
	ee.muid   
609 626
	(Utils.fprintf_list ~sep:", " pp_acsl_var_decl) ee.mmstep_logic.step_inputs
610 627
	(Utils.pp_final_char_if_non_empty ", " ee.mmstep_logic.step_inputs)
......
622 639
	  [] spec.m_behaviors)
623 640
    )
624 641

  
625
(* Access to the value of a variable:
626
   - if it's not a scalar output, then its name is enough
627
   - otherwise, dereference it (it has been declared as a pointer,
628
     despite its scalar Lustre type)
629
   - moreover, cast arrays variables into their original array type.
630
*)
631
let pp_acsl_var_read outputs fmt id =
632
  if Types.is_array_type id.var_type
633
  then
634
    assert false (* no array *)
635
  else ( (* Hack to cast boolean variables as int for ACSL predicates *)
636
    if (Types.repr id.var_type).Types.tdesc = Types.Tbool then
637
      fprintf fmt "(int)" 
638
    ;
639
    if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *)
640
    then fprintf fmt "*%s" id.var_id
641
    else fprintf fmt "%s" id.var_id
642
  )
643

  
644
    
645 642
let pp_requires_mem machines fmt m =
646 643
  let self = mk_self m in
647 644
  List.iter (fun v -> fprintf fmt "requires \\valid(%s);@;" v.var_id) m.mstep.step_outputs;
648 645
  fprintf fmt "requires \\valid(%s);@;" self;
649 646
  let mems = Machine_code.get_mems m machines in
650
  List.iter (fun prefix -> fprintf fmt "requires \\valid(%s%a);@;" self
647
  (*List.iter (fun prefix -> fprintf fmt "requires \\valid(%s%a);@;" self
651 648
    (Utils.fprintf_list ~sep:"" (fun fmt s -> fprintf fmt "->%s" s)) prefix
652 649
  )
653
    (Machine_code.get_instances m machines);
650
    (Machine_code.get_instances m machines);*)
654 651
  if List.length mems + List.length m.mstep.step_outputs > 1 then
655
    fprintf fmt "requires \\separated(@[<hov>%a%t%a@]);@;" 
652
    fprintf fmt "requires \\separated(@[<hov>%a%t%s@]);@;" 
656 653
      (Utils.fprintf_list ~sep:",@ " 
657 654
	 (fun fmt v -> pp_print_string fmt v.var_id))
658 655
      m.mstep.step_outputs 
659
      (Utils.pp_final_char_if_non_empty ",@ " mems)
660
      (Utils.fprintf_list ~sep:",@ " 
656
      (Utils.pp_final_char_if_non_empty ",@ " m.mstep.step_outputs)
657
      self
658

  
659
      (*(Utils.fprintf_list ~sep:",@ " 
661 660
	 (fun fmt (prefix, var) -> fprintf fmt "&%s%a->_reg.%s"
662 661
	   self 
663 662
	   (Utils.fprintf_list ~sep:"" (fun fmt s -> fprintf fmt "->%s" s)) prefix
664 663
	   var.var_id	 
665 664
	 ))
666
      mems
665
      mems*)
667 666

  
668 667
let pp_assigns machines fmt m =
669 668
  let self = mk_self m in
670 669
  let mems = Machine_code.get_mems m machines in
671
  fprintf fmt "assigns @[<hov>%a%t%a@];@;" 
670
  fprintf fmt "assigns @[<hov>%a%t*%s@];@;" 
672 671
    (Utils.fprintf_list ~sep:",@ " 
673 672
       (fun fmt v -> fprintf fmt "*%s" v.var_id))
674 673
    m.mstep.step_outputs 
675
    (Utils.pp_final_char_if_non_empty ",@ " mems)
674
    (Utils.pp_final_char_if_non_empty ",@ " m.mstep.step_outputs)
675
    self
676
(*
676 677
    (Utils.fprintf_list ~sep:",@ " 
677 678
       (fun fmt (prefix, var) -> fprintf fmt "%s%a->_reg.%s"
678 679
	 self 
......
680 681
	    (fun fmt s -> fprintf fmt "->%s" s)) prefix
681 682
	 var.var_id	 
682 683
       ))
683
    mems
684
    mems*)
685

  
686
(*TODO: BEGIN*)
687

  
688
(* concat two lists and remove duplicates *)
689
let rec concat_uniq l1 l2 =
690
  match l1 with
691
    | [] -> l2
692
    | t::q -> let l = concat_uniq q l2 in
693
      if List.mem t l2 then l else t::l
694

  
695
(* A type for dependance, it can be a node or a variable *)
696
type dep_t = Dep_Var of string | Dep_Node of string
697

  
698
(* Take a machine and output the list of all dependance *)
699
let gen_dep instrs =
700
  let rec gen_dep_val = function
701
    | Cst c         -> []
702
    | Array vl      -> assert false
703
    | Access (t, i) -> assert false
704
    | Power (v, n)  -> assert false
705
    | LocalVar v    -> []
706
    | StateVar v    -> [Dep_Var v.var_id]
707
    | Fun (n, vl)   -> List.fold_left (fun l x-> concat_uniq (gen_dep_val x) l) [] vl
708
  and gen_dep_instr = function
709
    | MReset i -> assert false
710
    | MLocalAssign (i,v) -> gen_dep_val v
711
    | MStateAssign (i,v) -> concat_uniq (gen_dep_val (StateVar i)) (gen_dep_val v)
712
    | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  -> gen_dep_instr (MLocalAssign (i0, Fun (i, vl)))
713
    | MStep (il, i, vl) -> List.fold_left (fun l x-> concat_uniq (gen_dep_val x) l) [Dep_Node i] vl
714
    | MBranch (g,hl) -> List.fold_left (fun l (x, y)-> concat_uniq (gen_dep_instrs y) l) (gen_dep_val g) hl
715
  and gen_dep_instrs instrs =
716
    List.fold_left (fun l x-> concat_uniq (gen_dep_instr x) l) [] instrs
717
  in
718
  gen_dep_instrs instrs
719

  
720
(* Print a function call/declaration in acsl *) 
721
let pp_acsl_fun name fmt args =
722
    fprintf fmt "%s(@[<v>%a@])"
723
      name
724
      (Utils.fprintf_list ~sep:",@ " (fun fmt f-> f fmt)) args
725

  
726
(* Print an invariant call/decl in acsl *)
727
let pp_acsl_fun_init name self inst fmt mem =
728
  let arg = fun fmt-> (match inst, mem with
729
    | x,  None    -> fprintf fmt "%a %s" pp_machine_memtype_name name self
730
    | "", Some "" -> fprintf fmt "%s" self
731
    | "", Some m  -> fprintf fmt "\\at(*%s, %s)" self m
732
    | x,  Some "" -> fprintf fmt "%s.%s" self inst
733
    | x,  Some m  -> fprintf fmt "\\at(%s->%s, %s)" self inst m)
734
  in
735
  pp_acsl_fun ("init_"^name) fmt [arg]
684 736

  
685 737

  
738
(* Print a machine instruction in acsl for transition lemma *) 
739
let preprocess_acsl_instr instances outputs instr =
740
  match instr with 
741
    | MStep ([i0], i, vl) when Basic_library.is_internal_fun i && (not (List.mem i0 outputs)) ->
742
      Some (i0, Fun (i, vl))
743
    | MStep ([i0], i, vl) when (not (Basic_library.is_internal_fun i)) && node_name (fst (List.assoc i instances)) = "_arrow" ->
744
      assert (List.length vl == 2);
745
      Some (i0, Fun ("arrow_"^i, vl))
746
    | MLocalAssign (i,v) when not (List.mem i outputs) ->
747
      Some (i, v)
748
    | _ -> None
749

  
750

  
751
let pp_cast fmt = function
752
  | Types.Tbool           -> fprintf fmt "(_Bool)"
753
  | Types.Treal           -> fprintf fmt "(double)"
754
  | Types.Tint            -> fprintf fmt "(int)"
755
  | _ -> assert false
756

  
757
let getFunType i args =
758
  match i, args with
759
  | "ite", [v1; v2; v3] -> v2
760
  | "uminus", [v] -> v
761
  | "not", [v] -> v
762
  | "impl", [v1; v2] -> v1
763
  | "=", [v1; v2] -> Types.Tbool
764
  | "mod", [v1; v2] -> v1
765
  | "xor", [v1; v2] -> v1
766
  | _, [v1; v2] -> v1
767
  | _ -> assert false
768

  
769
let rec get_val_type v =
770
match v with 
771
| Cst _
772
| LocalVar _ 
773
| StateVar _-> Machine_code.get_val_type v
774
| Fun (n, vl) -> getFunType n (List.map get_val_type vl)
775
| Array _
776
| Access _
777
| Power _ -> assert false
778

  
779
let get_var_type t = (Types.repr t.var_type).Types.tdesc
780

  
781
(* Print a machine instruction in acsl for transition lemma *) 
782
let rec pp_acsl_instr vars instances self pointer fmt instr =
783
  match instr with 
784
    | MReset i ->
785
      let (node, static) = List.assoc i instances in
786
      assert (List.length static == 0);
787
      if node_name node = "_arrow" then
788
        fprintf fmt "%s.%s._reg._first==1" self i
789
      else
790
        pp_acsl_fun_init (node_name node) self i fmt (Some "")
791
    | MLocalAssign (i,v) -> fprintf fmt "%a == %a"
792
      (pp_acsl_var_read pointer "") i
793
      (pp_acsl_val (self^"1") (pp_acsl_var_read pointer)) v
794
    | MStateAssign (i,v) -> fprintf fmt "%a == %a"
795
      (pp_acsl_val (self^"2") (pp_acsl_var_read pointer)) (StateVar i)
796
      (pp_acsl_val (self^"1") (pp_acsl_var_read pointer)) v
797
    | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
798
      pp_acsl_instr vars instances self pointer fmt (MLocalAssign (i0, Fun (i, vl)))
799
    | MStep (il, i, vl) ->
800
      let pp_val fmt x = (match get_val_type x with Types.Tbool -> fprintf fmt "((%a)?1:0)" | _ -> fprintf fmt "%a") (pp_acsl_val (self^"1") (pp_acsl_var_read [])) x in
801
      pp_acsl_fun ("Ctrans_"^(node_name (fst (List.assoc i instances)))) fmt
802
      ((List.map (fun x fmt-> fprintf fmt "%a %a" pp_cast (get_val_type x) pp_val x) vl)@
803
      (List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_var_type x)*) (pp_acsl_var_read [] "") x) il)@
804
        [(fun fmt->fprintf fmt "%s1.%s" self i);(fun fmt->fprintf fmt "%s2.%s" self i)])
805
    | MBranch (g,hl) ->
806
      let t = fst (List.hd hl) in
807
      if hl <> [] && (t = tag_true || t = tag_false) then
808
        let tl = try List.assoc tag_true  hl with Not_found -> [] in
809
        let el = try List.assoc tag_false hl with Not_found -> [] in
810
        fprintf fmt "(%a)?(%a):(%a)"
811
          (pp_acsl_val self (pp_acsl_var_read pointer)) g
812
          (Utils.fprintf_list ~sep:"&& " (pp_acsl_instr vars instances self pointer)) tl
813
          (Utils.fprintf_list ~sep:"&& " (pp_acsl_instr vars instances self pointer)) el
814
      else assert false
815

  
816
(* Print all machine instructions in acsl for transition lemma *) 
817
let pp_acsl_instrs outputs self pointer instances vars fmt instrs =
818
  if List.length instrs == 0 then fprintf fmt "\\true" else
819
  let handle (locals, instrs) i =
820
    match preprocess_acsl_instr instances outputs i with
821
      | None    -> (locals, i::instrs)
822
      | Some l  -> (l::locals, instrs)
823
  in
824
  let pp_let fmt (i, v) =
825
    match v with
826
      | Fun (s, [x;y]) when String.length s >= 6 && String.sub s 0 6 = "arrow_" ->
827
        let var = String.sub s 6 (String.length s - 6) in
828
        fprintf fmt "\\let %a = %s1.%s._reg._first?%a:%a; (%s2.%s._reg._first==0) &&"
829
          (pp_acsl_var_read pointer "") i
830
          self var
831
          (pp_acsl_val (self^"1") (pp_acsl_var_read [])) x
832
          (pp_acsl_val (self^"1") (pp_acsl_var_read [])) y
833
          self var
834
      | _ ->
835
        fprintf fmt "\\let %a = %a;"
836
          (pp_acsl_var_read pointer "") i
837
          (pp_acsl_val (self^"1") (pp_acsl_var_read pointer)) v
838
  in
839
  let (locals, instrs) = List.fold_left handle ([], []) instrs in
840
  fprintf fmt "%a@,%a"
841
    (Utils.fprintf_list ~sep:"@," pp_let)
842
    (List.rev locals)
843
    (Utils.fprintf_list ~sep:" &&@," (pp_acsl_instr vars instances self pointer))
844
    instrs
845

  
846
(* Take a dependance and print it for invariant predicate *)
847
(*
848
let pp_acsl_dep self instances fmt = function
849
  | Dep_Var s -> fprintf fmt "%s2._reg.%s == %s1._reg.%s" self s self s
850
  | Dep_Node s ->
851
    pp_acsl_fun ("inv_"^(node_name (fst (List.assoc s instances)))) fmt [fun fmt->fprintf fmt "%s1.%s" self i];
852
    fprintf fmt "&&@, %t == %t" (pp_acsl_at self s)
853
      (pp_acsl_at self s)
854
*)
855

  
856
(* Print a transition call/decl in acsl *)
857
let pp_acsl_fun_trans infos pre name inputs outputs suffix flag_output self flag_mem locals fmt existential =
858
  let (locals, existential) = (*([], match existential with None -> None | Some x -> Some []) in*)
859
  match infos with
860
    | None -> (locals, existential)
861
    | Some (instrs, instances) ->
862
      let nonlocals = List.fold_left (fun l x-> match preprocess_acsl_instr instances outputs x with | Some (i, _) -> i::l | None -> l) [] instrs in
863
      (
864
        List.filter (fun x-> not (List.mem x nonlocals)) locals,
865
        match existential with None -> None | Some existential -> Some (List.filter (fun x-> not (List.mem x nonlocals)) existential)
866
      )
867
  in
868
  let mems = function 1 -> "Pre" | 2 -> "Here" | _ -> assert false in
869
  let pp_self_read =
870
    if flag_mem then fun i fmt-> fprintf fmt "\\at(*%s, %s)" self (mems i)
871
    else fun i fmt-> fprintf fmt "%s%i" self (match suffix with None -> i | Some s -> s+i-1)
872
  in
873
  let (pp_var, pp_self) =
874
    match existential with
875
      | None    -> (pp_acsl_var_decl, (fun i fmt-> fprintf fmt "%a %s%i" pp_machine_memtype_name name self i))
876
      | Some ex -> (if List.length ex != 0 then fprintf fmt "\\exists %a;@," (Utils.fprintf_list ~sep:";@,\\exists " pp_acsl_var_decl) ex);
877
                   (pp_acsl_var_read (if flag_output then outputs else []) "", pp_self_read)
878
  in
879
  let pp_vars = List.map (fun x fmt-> match suffix with None-> pp_var fmt x | Some i -> fprintf fmt "%a%i" pp_var x (i+1)) in
880
    (pp_acsl_fun (pre^"trans_"^name)) fmt
881
    ((pp_vars (inputs@outputs))@[pp_self 1;pp_self 2]@(pp_vars locals))
882

  
883
let depth = 1
884

  
885
(* Print an invariant call/decl in acsl *)
886
let pp_acsl_fun_inv name self fmt mem =
887
  let arg = fun fmt-> (match mem with
888
    | None -> fprintf fmt "%a %s%i" pp_machine_memtype_name name self depth
889
    | Some "" -> fprintf fmt "%s" self
890
    | Some "Here" -> fprintf fmt "*%s" self
891
    | Some m -> fprintf fmt "\\at(*%s, %s)" self m)
892
  in
893
  pp_acsl_fun ("inv_"^name) fmt [arg]
894

  
895
(* Print an invariant call/decl in acsl *)
896
let pp_acsl_inv name inputs outputs self fmt spec =
897
  let rec iter base x = function
898
    | i when i = base-1 -> []
899
    | i -> (i, x)::(iter base x (i-1))
900
  in
901
  let rec iterList base = function
902
    | []   -> []
903
    | t::q -> (iter base t depth)@(iterList base q)
904
  in
905
  let trans_pred fmt i =
906
    fprintf fmt "%a" (pp_acsl_fun_trans  None "C" name inputs outputs (Some i) false self false []) (Some [])
907
  in
908
  let spec_pred fmt i =
909
    let pp_eexpr_expr self j fmt ee = 
910
      fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (fun fmt x-> fprintf fmt "%a%i" (pp_acsl_var_read [] "") x i)) ee.mmstep_logic.step_inputs self j
911
    in
912
    fprintf fmt "%a%t%a"
913
    (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self (i))) spec.m_requires
914
    (Utils.pp_final_char_if_non_empty "&&@," spec.m_requires)
915
    (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self (i))) spec.m_ensures
916
  in
917
  let aux fmt base =
918
    let selfs = iter base self (depth-1) in
919
    let ios = iterList (if base == 0 then 0 else base + 1) (inputs@outputs) in
920
    (if List.length selfs == 0 && List.length ios == 0 then 
921
      fprintf fmt "(%a%t%t)"
922
     else
923
      fprintf fmt "(\\exists %a%t%a;@,%a%t%t)"
924
        (Utils.fprintf_list ~sep:", "   (fun fmt (i, x)-> fprintf fmt "%a %s%i" pp_machine_memtype_name name self i)) selfs
925
        (Utils.pp_final_char_if_non_empty ", " (iter base self (depth-1)))
926
        (Utils.fprintf_list ~sep:", "   (fun fmt (i, x)-> fprintf fmt "%a%i" pp_acsl_var_decl x i)) ios
927
    )
928
      (Utils.fprintf_list ~sep:"&&@," (fun fmt (i, f)-> fprintf fmt "%a" f i)) (iter base trans_pred (depth-1))
929
      (Utils.pp_final_char_if_non_empty "&&@," (iter base trans_pred (depth-1))) 
930
      (fun fmt->
931
        if base == 0 then
932
          Utils.fprintf_list ~sep:"&&@," (fun fmt (i, f)-> fprintf fmt "%a" f i) fmt (iter base spec_pred depth)
933
        else
934
          pp_acsl_fun_init name (self^(string_of_int base)) "" fmt (Some "")
935
      )
936
  in
937
  Utils.fprintf_list ~sep:"||@," (fun fmt (i, f)-> fprintf fmt "%a" f i) fmt (iter 0 aux depth)
938

  
939
(* Print an invariant call/decl in acsl *)
940
let pp_acsl_lem_inv name inputs outputs fmt self =
941
  fprintf fmt "\\forall %a %s1, %s2, %a;@,%a==>@,%a==>@,%a"
942
    pp_machine_memtype_name name self self
943
    (Utils.fprintf_list ~sep:", " pp_acsl_var_decl) (inputs@outputs)
944
    (pp_acsl_fun_inv name (self^"1")) (Some "")
945
    (pp_acsl_fun_trans None "C" name inputs outputs None false self false []) (Some [])
946
    (pp_acsl_fun_inv name (self^"2")) (Some "")
947

  
948
(* Print an invariant call/decl in acsl *)
949
let pp_acsl_lem_spec name inputs outputs self fmt spec =
950
  let pp_eexpr_expr self j fmt ee =
951
    fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [] "")) ee.mmstep_logic.step_inputs self j
952
  in
953
  fprintf fmt "\\forall %a %s1, %s2, %a;@,%a==>@,%a==>@,%a%t%a"
954
    pp_machine_memtype_name name self self
955
    (Utils.fprintf_list ~sep:", " pp_acsl_var_decl) (inputs@outputs)
956
    (pp_acsl_fun_inv name (self^"1")) (Some "")
957
    (pp_acsl_fun_trans None "C" name inputs outputs None false self false []) (Some [])
958
    (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self 1)) spec.m_requires
959
    (Utils.pp_final_char_if_non_empty "&&@," spec.m_requires)
960
    (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self 2)) spec.m_ensures
961

  
962
(* Print the definition of the transition in acsl *)
963
let pp_acsl_def_trans fmt m =
964
  let name = m.mname.node_id in
965
  let inputs = m.mstep.step_inputs in
966
  let outputs = m.mstep.step_outputs in
967
  let locals = m.mstep.step_locals in
968
  let memory = m.mmemory in
969
  let vars = inputs@outputs@locals@memory in
970
  if m.mname.node_id <> arrow_id then (
971
    let self = mk_self m in
972
    fprintf fmt "/*@@ @[<v 3>predicate %a =@;%a;@]@;*/@."
973
      (pp_acsl_fun_trans (Some (m.mstep.step_instrs, m.minstances)) "" name inputs outputs None false self false locals) None
974
	    (pp_acsl_instrs outputs self [] m.minstances vars) m.mstep.step_instrs;
975
    fprintf fmt "/*@@ @[<v 3>predicate %a =@;%a;@]@;*/@."
976
      (pp_acsl_fun_init name self "") None
977
	    (pp_acsl_instrs [] self [] m.minstances vars) m.minit;
978
    fprintf fmt "/*@@ @[<v 3>predicate %a =@;%a;@]@;*/@."
979
      (pp_acsl_fun_trans None "C" name inputs outputs None false self false []) None
980
	    (pp_acsl_fun_trans (Some (m.mstep.step_instrs, m.minstances)) "" name inputs outputs None false self false locals) (Some locals);
981
    match m.mspec with None -> () | Some spec -> fprintf fmt "/*@@ @[<v 3>predicate %a =@;%a;@]@;*/@."
982
      (pp_acsl_fun_inv name self) None (pp_acsl_inv name inputs outputs self) spec;
983
    fprintf fmt "/*@@ @[<v 3>lemma inv_spec_%s : @;%a;@]@;*/@." name (pp_acsl_lem_spec name inputs outputs self) spec;
984
    fprintf fmt "/*@@ @[<v 3>lemma inv_inv_%s : @;%a;@]@;*/@." name (pp_acsl_lem_inv name inputs outputs) self
985
  )
986

  
987
(*;
988
  fprintf fmt "/*@@ @[<v 3>predicate inv_%s{L1, L2}(@[<v>@[%a *%s@]@]) =@;%a;@]@;*/@."
989
    m.mname.node_id
990
	  pp_machine_memtype_name m.mname.node_id
991
	  self
992
    (Utils.fprintf_list ~sep:" &&@," (printDep self "L1" "L2" m.minstances)) (gen_dep m.mstep.step_instrs);
993
  fprintf fmt "/*@@ @[<v 3>lemma transitivity_%s{L1, L2, L3, L4} :@, \forall @[<v>@[%a%t@]@,@[%a@]%t@[%a *%s@]@];@, %t;@]@;*/@."
994
    m.mname.node_id
995
    (Utils.fprintf_list ~sep:",@ " pp_acsl_var_decl) m.mstep.step_inputs
996
    (Utils.pp_final_char_if_non_empty ",@ " m.mstep.step_inputs) 
997
    (Utils.fprintf_list ~sep:",@ " pp_acsl_var_decl) m.mstep.step_outputs
998
    (Utils.pp_final_char_if_non_empty ",@," m.mstep.step_outputs)
999
	pp_machine_memtype_name m.mname.node_id
1000
	self
1001
  (fun fmt->
1002
    fprintf fmt "inv_%s{L1, L2}(%s) ==>@," m.mname.node_id self;
1003
    fprintf fmt "inv_%s{L3, L4}(%s) ==>@," m.mname.node_id self;
1004
    fprintf fmt "trans_%s{L2, L3}(%a%t%a%t\\at(%s, L2)) ==>@,"
1005
      m.mname.node_id
1006
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [] "")) m.mstep.step_inputs
1007
      (Utils.pp_final_char_if_non_empty ", " m.mstep.step_inputs) 
1008
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [] "")) m.mstep.step_outputs
1009
      (Utils.pp_final_char_if_non_empty ", " m.mstep.step_outputs)
1010
      self;
1011
    fprintf fmt "trans_%s{L1, L4}(%a%t%a%t\\at(%s, L1)@]@])"
1012
      m.mname.node_id
1013
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [] "")) m.mstep.step_inputs
1014
      (Utils.pp_final_char_if_non_empty ", " m.mstep.step_inputs) 
1015
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [] "")) m.mstep.step_outputs
1016
      (Utils.pp_final_char_if_non_empty ", " m.mstep.step_outputs)
1017
      self)
1018
*)
1019

  
1020
(*
1021
    (print_reset_prototype self) (m.mname.node_id, m.mstatic)
1022
    (Utils.fprintf_list ~sep:"@," 
1023
       (pp_machine_instr 
1024
	  (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs, m.mstep.step_locals, m.mmemory, m.minstances, m.mcalls) self)) 
1025
    m.minit
1026
    (Utils.pp_newline_if_non_empty m.minit)
1027
    (* Print specification if any: insert side effect at the end of the function body  *)
1028
    (fun fmt -> match m.mspec with
1029
    | None -> ()
1030
    | Some spec -> pp_acsl_spec_init_side_effects m m.mstep.step_outputs fmt spec
1031
    )*)
1032

  
1033
(*TODO: END*)
1034

  
686 1035
let pp_acsl_mem_valid machines fmt m =
1036
  let self = mk_self m in
687 1037
  fprintf fmt "@[<v 2>/*@@ ";
688 1038
  pp_requires_mem machines fmt m;
1039
	fprintf fmt "ensures %a;@," (pp_acsl_fun_trans None "C" m.mname.node_id m.mstep.step_inputs m.mstep.step_outputs None true self true []) (Some []);
689 1040
  pp_assigns machines fmt m;
690 1041
  fprintf fmt "@]*/@.";
691 1042
  ()
......
697 1048
      (* If the eexpr contains a single definition we use it directly. Otherwise,
698 1049
	 we rely on an external predicate *)
699 1050
    match ee.mmstep_logic.step_instrs with
700
    | [MStep([o], i, vl)] -> 
1051
    (*| [MStep([o], i, vl)] -> 
701 1052
      fprintf fmt "%a %t"
702 1053
	(Utils.fprintf_list ~sep:" " pp_quantifiers) ee.mquantifiers
703 1054
	(fun fmt ->
......
706 1057
	    ee.mmstep_logic.step_inputs@ee.mmstep_logic.step_outputs@ee.mmstep_logic.step_locals@ee.mmmemory 
707 1058
	  in 
708 1059
	  pp_expr_rhs vars self (pp_c_var_read outputs) fmt o.var_type value 
709
	)
710
    | _ -> fprintf fmt "spec_%i(%a, %s);" 
1060
	)*)
1061
    | _ -> fprintf fmt "spec_%i(%a, *%s);" 
711 1062
      ee.muid   
712
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read outputs)) ee.mmstep_logic.step_inputs
1063
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read outputs "")) ee.mmstep_logic.step_inputs
713 1064
      self
714 1065
  in
715 1066
  fprintf fmt "@[<v 2>/*@@ ";
716 1067
  (* Valid pointers *)
717 1068
  pp_requires_mem machines fmt m;
718
  
719 1069
  (* Spec requires *)
720 1070
  Utils.fprintf_list ~sep:"" 
721 1071
    (fun fmt r -> fprintf fmt "requires %a@ " pp_eexpr_expr r) 
722 1072
    fmt 
723 1073
    spec.m_requires;
1074
  fprintf fmt "requires %a;@," (pp_acsl_fun_inv m.mname.node_id self) (Some "Here");
724 1075
  Utils.fprintf_list ~sep:"" 
725 1076
    (fun fmt r -> fprintf fmt "ensures %a@ " pp_eexpr_expr r) 
726 1077
    fmt 
727 1078
    spec.m_ensures;
1079
  fprintf fmt "ensures %a;@," (pp_acsl_fun_inv m.mname.node_id self) (Some "Here");
1080
	fprintf fmt "ensures %a;@," (pp_acsl_fun_trans None "C" m.mname.node_id m.mstep.step_inputs m.mstep.step_outputs None true self true []) (Some []);
728 1081
  fprintf fmt "@ ";
729 1082
    (* TODO assigns + separated *)
730 1083
    (* fprintf fmt "assigns *self%t%a;@ "  *)
......
997 1350
    (Utils.pp_final_char_if_non_empty ", " m.mstatic)
998 1351
    pp_machine_static_link_name m.mname.node_id
999 1352

  
1000
let print_machine_decl machines fmt m =
1353
let print_machine_spec machines fmt m =
1001 1354
  if m.mname.node_id <> arrow_id then 
1002 1355
    (
1003 1356
      (* We don't print arrow function *)
1004
      
1357

  
1005 1358
      (* Print specification if any: insert logic definition before the function  *)
1006
      (match m.mspec with
1359
      match m.mspec with
1007 1360
      | None -> ()
1008 1361
      | Some spec -> 
1009 1362
	pp_acsl_spec_logics m m.mstep.step_outputs fmt spec
1010
      );
1011
      
1363
    )
1364

  
1365
let print_machine_decl machines fmt m =
1366
  if m.mname.node_id <> arrow_id then 
1367
    (
1368
   (*   (* We don't print arrow function *)
1369

  
1012 1370
      (* Static allocation *)
1013 1371
      if !Options.static_mem
1014 1372
      then (
......
1021 1379
      (* Dynamic allocation *)
1022 1380
	fprintf fmt "extern %a;@.@."
1023 1381
	  print_alloc_prototype (m.mname.node_id, m.mstatic)
1024
      );
1382
      );*)
1025 1383
      let self = mk_self m in
1384
	    fprintf fmt "/*@@ensures %a;@." (pp_acsl_fun_init m.mname.node_id self "") (Some "Here");
1385
	    fprintf fmt "assigns *%s;*/@." self;
1026 1386
      fprintf fmt "extern %a;@.@."
1027 1387
	(print_reset_prototype self) (m.mname.node_id, m.mstatic);
1028 1388
    (* Print specification contracts if any *)
1029 1389
      (match m.mspec with
1030 1390
      | None -> pp_acsl_mem_valid machines fmt m
1031
      | Some spec -> 
1032
	pp_acsl_spec_contracts machines m m.mstep.step_outputs fmt spec
1391
      | Some spec -> pp_acsl_spec_contracts machines m m.mstep.step_outputs fmt spec
1033 1392
      );
1034 1393
      fprintf fmt "extern %a;@.@."
1035 1394
	(print_step_prototype self)
......
1064 1423
    (pp_c_type "") base_type
1065 1424
    vdecl.var_id
1066 1425

  
1426
let rec list_to_partial l = match l with
1427
  | []   -> [[]]
1428
  | _::q -> l::(list_to_partial q)
1429

  
1067 1430
let print_alloc_code fmt m =
1068 1431
  let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
1069 1432
  fprintf fmt "%a *_alloc;@,_alloc = (%a *) malloc(sizeof(%a));@,assert(_alloc);@,%a%areturn _alloc;"
......
1079 1442
  then
1080 1443
    (* C99 code *)
1081 1444
    let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
1082
    fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%t%t@]@,}@.@."
1445
    fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%t%a%t%t%t@]@,}@.@."
1083 1446
      (print_step_prototype self) (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
1084 1447
      (* locals *)
1085 1448
      (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) m.mstep.step_locals
......
1097 1460
      | None -> ()
1098 1461
      | Some spec -> pp_acsl_spec_side_effects m m.mstep.step_outputs fmt spec
1099 1462
      )
1463
      (let f = fun fmt x-> fprintf fmt "/*@@assert (%a);*/@," (pp_acsl_fun_trans (Some (m.mstep.step_instrs, m.minstances)) "" m.mname.node_id m.mstep.step_inputs m.mstep.step_outputs None true self true m.mstep.step_locals) (Some x) in
1464
      (Utils.fprintf_list ~sep:"@," f)) (List.rev (list_to_partial m.mstep.step_locals))
1465
      (fun fmt-> fprintf fmt "/*@@assert (%a);*/@," (pp_acsl_fun_trans None "C" m.mname.node_id m.mstep.step_inputs m.mstep.step_outputs None true self true []) (Some []))
1466
      (let pp_eexpr_expr fmt ee = 
1467
        fprintf fmt "spec_%i(%a, *%s)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read m.mstep.step_outputs "")) ee.mmstep_logic.step_inputs self
1468
       in
1469
       fun fmt -> match m.mspec with
1470
        | Some spec when 0 < List.length spec.m_ensures-> fprintf fmt "/*@@assert (%a);*/@," (Utils.fprintf_list ~sep:"&&@," pp_eexpr_expr) spec.m_ensures
1471
        | None ->fprintf fmt ""
1472
      )
1100 1473
      (fun fmt -> fprintf fmt "return;")
1101 1474
  else
1102 1475
    (* C90 code *)
......
1193 1566
    ) m.mstep.step_outputs;
1194 1567
  fprintf fmt "@ /* Main memory allocation */@ ";
1195 1568
  if (!Options.static_mem && !Options.main_node <> "")
1196
  then (fprintf fmt "%a(static,main_mem);@ " pp_machine_static_alloc_name mname)
1569
  then (*(fprintf fmt "%a(static,main_mem);@ " pp_machine_static_alloc_name mname)*) (fprintf fmt "%a main_mem;@ " pp_machine_memtype_name mname)
1197 1570
  else (fprintf fmt "%a *main_mem = %a();@ " pp_machine_memtype_name mname pp_machine_alloc_name mname);
1198 1571
  fprintf fmt "@ /* Initialize the main memory */@ ";
1199 1572
  fprintf fmt "%a(%s);@ " pp_machine_reset_name mname main_mem;
1200 1573
  fprintf fmt "@ ISATTY = isatty(0);@ ";
1201 1574
  fprintf fmt "@ /* Infinite loop */@ ";
1575
  (match m.mspec with
1576
      | None -> ()
1577
      | Some spec -> fprintf fmt "/*@@ loop invariant %a;*/@," (pp_acsl_fun_inv m.mname.node_id "main_mem") (Some "")
1578
  );
1202 1579
  fprintf fmt "@[<v 2>while(1){@ ";
1203
  fprintf fmt  "fflush(stdout);@ ";
1580
  (*fprintf fmt  "fflush(stdout);@ ";*)
1204 1581
  List.iter 
1205 1582
    (fun v -> fprintf fmt "%s = %a;@ "
1206 1583
      v.var_id
......
1373 1750
  fprintf header_fmt "/* Global constant (declarations, definitions are in C file) */@.";
1374 1751
  List.iter (fun c -> print_const_decl header_fmt c) (get_consts prog);
1375 1752
  pp_print_newline header_fmt ();
1753

  
1376 1754
  (* Print the struct declarations of all machines. *)
1377 1755
  fprintf header_fmt "/* Struct declarations */@.";
1378
  List.iter (print_machine_struct header_fmt) machines;
1756
  List.iter (print_machine_struct header_fmt) (List.rev machines);
1757
  pp_print_newline header_fmt ();
1758

  
1759
  (* Print the spec of all machines *)
1760
  fprintf header_fmt "/* Spec declarations */@.";
1761
  List.iter (print_machine_spec machines header_fmt) machines;
1379 1762
  pp_print_newline header_fmt ();
1763

  
1764
  (* Print the transition of all machines *)
1765
  fprintf header_fmt "/* Transitions declarations */@.";
1766
  List.iter (pp_acsl_def_trans header_fmt) (List.rev machines);
1767
  pp_print_newline header_fmt ();
1768

  
1380 1769
  (* Print the prototypes of all machines *)
1381 1770
  fprintf header_fmt "/* Nodes declarations */@.";
1382 1771
  List.iter (print_machine_decl machines header_fmt) machines;
src/dot_backend.ml
1
open Format
2
open Corelang
3
open Machine_code
4

  
5
let pp_fun i = 
6
  match i with
7
  | "ite" -> "ite"
8
  | "uminus" -> "uminus"
9
  | "not" -> "not"
10
  | "=" -> "equal"
11
  | "&&" -> "and"
12
  | "||" -> "or"
13
  | "impl" -> "impl"
14
  | "xor" -> "xor"
15
  | "!=" -> "different"
16
  | "mod" -> "mod"
17
  | ">" -> "gt"
18
  | "<" -> "lt"
19
  | ">=" -> "gte"
20
  | "<=" -> "lte"
21
  | _ -> Printf.printf "%s\n" i;assert false
22

  
23
let rec print_instr_dep instances name fmt instr =
24
  match instr with 
25
  | MReset i -> ()
26
  | MLocalAssign (i,v) -> ()
27
  | MStateAssign (i,v) -> ()
28
  | MStep (il, i, vl) ->
29
      let name' = try node_name (fst (List.assoc i instances)) with Not_found -> pp_fun i in
30
      Format.fprintf fmt "  %s -> %s;" name name'
31
  | MBranch (g,hl) -> ()
32

  
33
let print_machine_dep fmt m =
34
  Format.fprintf fmt "%s [color=red];@.%a"
35
    m.mname.node_id
36
    (Utils.fprintf_list ~sep:"@." (print_instr_dep m.minstances m.mname.node_id)) m.mstep.step_instrs
37

  
38
(*
39
let rec print_instr_struct instances name fmt instr =
40
  match instr with 
41
  | MReset i -> ()
42
  | MLocalAssign (i,v) -> ()
43
  | MStateAssign (i,v) -> ()
44
  | MStep (il, i, vl) ->
45
      let name' = try node_name (fst (List.assoc i instances)) with Not_found -> pp_fun i in
46
      Format.fprintf fmt "  %s -> %s;@." name name'
47
  | MBranch (g,hl) -> ()
48

  
49
let rec translate_expr vars ((m, si, j, d, s) as args) expr =
50
 match expr.expr_desc with
51
 | Expr_const v                     -> Cst v
52
 | Expr_ident x                     -> translate_ident vars args x
53
 | Expr_array el                    -> Array (List.map (translate_expr vars args) el)
54
 | Expr_access (t, i)               -> Access (translate_expr vars args t, translate_expr vars args (expr_of_dimension i))
55
 | Expr_power  (e, n)               -> Power  (translate_expr vars args e, translate_expr vars args (expr_of_dimension n))
56
 | Expr_tuple _
57
 | Expr_arrow _ 
58
 | Expr_fby _
59
 | Expr_pre _                       -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
60
 | Expr_when    (e1, _, _)          -> translate_expr vars args e1
61
 | Expr_merge   (x, _)              -> raise NormalizationError
62
 | Expr_appl (id, e, _) when Basic_library.is_internal_fun id ->
63
   let nd = node_from_name id in
64
   (match e.expr_desc with
65
   | Expr_tuple el -> Fun (node_name nd, List.map (translate_expr vars args) el)
66
   | _             -> Fun (node_name nd, [translate_expr vars args e]))
67
 | Expr_ite (g,t,e) -> (
68
   (* special treatment depending on the active backend. For horn backend or
69
      acsl spec, ite are preserved in expression. While they are removed for C
70
      or Java backends. *)
71
     Fun ("ite", [translate_expr vars args g; translate_expr vars args t; translate_expr vars args e])
72
 )
73
 | _                   -> raise NormalizationError
74

  
75

  
76
  let nd = match top.top_decl_desc with Node nd -> nd | _ -> assert false in
77

  
78
List.map (fun d -> d.Dimension.dim_loc, translate_expr (node_vars nd) init_args (expr_of_dimension d)) nd.node_checks;
79
*)
80

  
81
let print_machine_struct orig dest fmt m =
82
  Format.fprintf fmt "subgraph cluster_%s {@.label = \"%s\"@.}@." m.mname.node_id m.mname.node_id
83

  
84
(*
85
digraph G {
86
	subgraph cluster_0 {
87
		style=filled;
88
		color=lightgrey;
89
		node [style=filled,color=white];
90
		a0 -> a1 -> a2 -> a3;
91
		label = "process #1";
92
	}
93

  
94
	subgraph cluster_1 {
95
		node [style=filled];
96
		b0 -> b1 -> b2 -> b3;
97
		label = "process #2";
98
		color=blue
99
	}
100
	start -> a0;
101
	start -> b0;
102
	a1 -> b3;
103
	b2 -> a3;
104
	a3 -> a0;
105
	a3 -> end;
106
	b3 -> end;
107

  
108
	start [shape=Mdiamond];
109
	end [shape=Msquare];
110
}
111
*)
112
let translate_to_dep destname basename prog machines =
113
	  let source_file = destname ^ "_dep.dot" in
114
	  let source_out = open_out source_file in
115
	  let fmt = formatter_of_out_channel source_out in
116
    Format.fprintf fmt "digraph %s {@.%a}@." basename (Utils.fprintf_list ~sep:"@." print_machine_dep) machines
117

  
118
let translate_to_struct destname basename prog machines = () (*
119
	  let source_file = destname ^ "_struct.dot" in
120
	  let source_out = open_out source_file in
121
	  let fmt = formatter_of_out_channel source_out in
122
    Format.fprintf fmt "digraph %s {@.%a}@." basename (Utils.fprintf_list ~sep:"" (print_machine_struct "input" "output")) (get_nodes prog)*)
123

  
124
let translate destname basename prog machines =
125
    translate_to_dep destname basename prog machines;
126
    translate_to_struct destname basename prog machines
127

  
128

  
129
(* Local Variables: *)
130
(* compile-command:"make -C .." *)
131
(* End: *)
src/machine_code.ml
591 591
	   common branches are not merged while they are in C or Java
592 592
	   backends. *)
593 593
	match !Options.output with
594
	| "horn" -> s_logic
595
	| "C" | "java" | _ -> join_guards_list s_logic
594
	| "C" | "horn" -> s_logic
595
	| "java" | _ -> join_guards_list s_logic
596 596
      )
597 597
    };
598 598
    mmstep_effects = {
......
605 605
	   common branches are not merged while they are in C or Java
606 606
	   backends. *)
607 607
	match !Options.output with
608
	| "horn" -> s_side_effects
609
	| "C" | "java" | _ -> join_guards_list s_side_effects
608
	| "C" | "horn" -> s_side_effects
609
	| "java" | _ -> join_guards_list s_side_effects
610 610
      )
611 611
    }
612 612
  }    
......
664 664
  ;
665 665

  
666 666
  let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> ISet.add l) nd.node_locals ISet.empty, [] in
667
  let keep_ite = (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false) in
667
  let keep_ite = (match !Options.output with | "horn" | "C" -> true | "java" | _ -> false) in
668 668
  let m, init, j, locals, s = translate_eqs nd keep_ite [] init_args (List.rev sorted_eqs_rev) in
669 669
  let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in
670 670
  {
......
684 684
	   common branches are not merged while they are in C or Java
685 685
	   backends. *)
686 686
	match !Options.output with
687
	| "horn" -> s
688
	| "C" | "java" | _ -> join_guards_list s
687
	| "C" | "horn" -> s
688
	| "java" | _ -> join_guards_list s
689 689
      );
690 690
    };
691 691
    mspec = Utils.option_map (translate_spec nd) nd.node_spec;
src/main_lustre_compiler.ml
277 277
	let fmt = formatter_of_out_channel source_out in
278 278
	Horn_backend.translate fmt basename normalized_prog machine_code
279 279
      end
280
    | "dot" ->
281
      begin
282
	Dot_backend.translate destname basename normalized_prog machine_code
283
      end
280 284
    | _ -> assert false
281 285
  in
282 286
  report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
src/options.ml
48 48
    "-c-spec", Arg.Set c_spec, 
49 49
    "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
50 50
    "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";
51
    "-dot", Arg.Unit (fun () -> output := "dot"), "generates dot graph";
51 52
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
52 53
    "-inline", Arg.Set global_inline, "inline all node calls (require a main node)";
53 54
    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";
test/tests_ok.list
1
./src/kind_fmcad08/misc/ex8_e8_376.lus,top
2
./src/kind_fmcad08/misc/_6counters_e8_371_e2_80.lus,top
3
./src/kind_fmcad08/misc/_6counters_e8_371_e1_448.lus,top
4
./src/kind_fmcad08/misc/_6counters.lus,top
5
./src/kind_fmcad08/misc/ex8_e7_74_e7_740.lus,top
6
./src/kind_fmcad08/misc/durationThm_1_e3_389_e5_5.lus,top
7
./src/kind_fmcad08/misc/two_counters_e2_3.lus,top
8
./src/kind_fmcad08/misc/stalmark.lus,top
9
./src/kind_fmcad08/misc/durationThm_3_e3_442.lus,top
10
./src/kind_fmcad08/misc/durationThm_1_e3_389.lus,top
11
./src/kind_fmcad08/misc/stalmark_e8_64_e7_80.lus,top
12
./src/kind_fmcad08/misc/durationThm_1.lus,top
13
./src/kind_fmcad08/misc/durationThm_3_e7_334_e2_62.lus,top
14
./src/kind_fmcad08/misc/switch2.lus,top
15
./src/kind_fmcad08/misc/durationThm_3_e1_71.lus,top
16
./src/kind_fmcad08/misc/_6counters_e8_371_e3_224.lus,top
17
./src/kind_fmcad08/misc/ticket3i_all_e8_505_e7_2450.lus,top
18
./src/kind_fmcad08/misc/durationThm_2_e7_145_e8_73.lus,top
19
./src/kind_fmcad08/misc/ex8_e7_74.lus,top
20
./src/kind_fmcad08/misc/ticket3i_3.lus,top
21
./src/kind_fmcad08/misc/_6counter.lus,top
22
./src/kind_fmcad08/misc/durationThm_2_e2_63.lus,top
23
./src/kind_fmcad08/misc/durationThm_3_e3_442_e4_165.lus,top
24
./src/kind_fmcad08/misc/ex8_e7_74_e8_302.lus,top
25
./src/kind_fmcad08/misc/durationThm_1_e7_217_e1_89.lus,top
26
./src/kind_fmcad08/misc/ticket3i_6_e7_1096_e7_2688.lus,top
27
./src/kind_fmcad08/misc/ticket3i_7_e1_2192_e1_1852.lus,top
28
./src/kind_fmcad08/misc/ticket3i_5_e7_3307.lus,top
29
./src/kind_fmcad08/misc/durationThm_1_e7_217_e3_132.lus,top
30
./src/kind_fmcad08/misc/ex3_e8_381_e8_477.lus,top
31
./src/kind_fmcad08/misc/ticket3i_3_e7_1312_e8_1916.lus,top
32
./src/kind_fmcad08/misc/durationThm_1_e1_350.lus,top
33
./src/kind_fmcad08/misc/ticket3i_all_e2_1117_e7_553.lus,top
34
./src/kind_fmcad08/misc/ticket3i_4_e7_1775_e7_3320.lus,top
35
./src/kind_fmcad08/misc/ticket3i_2.lus,top
36
./src/kind_fmcad08/misc/durationThm_2_e3_329_e5_124.lus,top
37
./src/kind_fmcad08/misc/durationThm_3_e2_148.lus,top
38
./src/kind_fmcad08/misc/durationThm_3_e2_63.lus,top
39
./src/kind_fmcad08/misc/twisted_counters.lus,top
40
./src/kind_fmcad08/misc/stalmark_e7_27_e7_31.lus,top
41
./src/kind_fmcad08/misc/durationThm_2_e7_149.lus,top
42
./src/kind_fmcad08/misc/ticket3i_5.lus,top
43
./src/kind_fmcad08/misc/two_counters.lus,top
44
./src/kind_fmcad08/misc/ticket3i_all_e7_591.lus,top
45
./src/kind_fmcad08/misc/ticket3i_7_e2_2724_e7_524.lus,top
46
./src/kind_fmcad08/misc/durationThm_2_e1_301.lus,top
47
./src/kind_fmcad08/misc/ticket3i_3_e8_1788.lus,top
48
./src/kind_fmcad08/misc/switch.lus,top
49
./src/kind_fmcad08/misc/durationThm_2_e7_145_e2_169.lus,top
50
./src/kind_fmcad08/misc/ticket3i_7_e7_3176.lus,top
51
./src/kind_fmcad08/misc/durationThm_2_e3_329_e4_1.lus,top
52
./src/kind_fmcad08/misc/ticket3i_3_e8_1703_e8_2560.lus,top
53
./src/kind_fmcad08/misc/ex3_e8_381_e7_224.lus,top
54
./src/kind_fmcad08/misc/durationThm_1_e2_3.lus,top
55
./src/kind_fmcad08/misc/ex8_e8_220_e7_249.lus,top
56
./src/kind_fmcad08/misc/ticket3i_3_e7_1312_e7_1495.lus,top
57
./src/kind_fmcad08/misc/ex3_e7_590_e7_590.lus,top
58
./src/kind_fmcad08/misc/_6countern.lus,top
59
./src/kind_fmcad08/misc/ticket3i_3_e7_1312.lus,top
60
./src/kind_fmcad08/misc/stalmark_e8_64.lus,top
61
./src/kind_fmcad08/misc/ticket3i_1_e7_1669.lus,top
62
./src/kind_fmcad08/misc/ticket3i_1.lus,top
63
./src/kind_fmcad08/misc/ticket3i_3_e8_1703.lus,top
64
./src/kind_fmcad08/misc/ticket3i_7.lus,top
65
./src/kind_fmcad08/misc/durationThm_3_e3_442_e5_260.lus,top
66
./src/kind_fmcad08/misc/durationThm_1_e7_217_e2_352.lus,top
67
./src/kind_fmcad08/misc/ex3_e7_655.lus,top
68
./src/kind_fmcad08/misc/_6counters_e8_371_e7_304.lus,top
69
./src/kind_fmcad08/misc/ex8.lus,top
70
./src/kind_fmcad08/misc/ticket3i_4.lus,top
71
./src/kind_fmcad08/misc/ticket3i_7_e8_2126_e7_78.lus,top
72
./src/kind_fmcad08/misc/ticket3i_all_e7_1837.lus,top
73
./src/kind_fmcad08/misc/durationThm_3.lus,top
74
./src/kind_fmcad08/misc/traffic_e7_46_e7_171.lus,top
75
./src/kind_fmcad08/misc/ticket3i_3_e8_1703_e7_3491.lus,top
76
./src/kind_fmcad08/misc/ticket3i_all.lus,top
77
./src/kind_fmcad08/misc/durationThm_2_e7_145_e3_222.lus,top
78
./src/kind_fmcad08/misc/two_counters_e3_325.lus,top
79
./src/kind_fmcad08/misc/durationThm_2_e7_145_e1_343.lus,top
80
./src/kind_fmcad08/misc/ticket3i_all_e3_557_e7_3464.lus,top
81
./src/kind_fmcad08/misc/durationThm_3_e7_334.lus,top
82
./src/kind_fmcad08/misc/durationThm_3_e7_334_e1_431.lus,top
83
./src/kind_fmcad08/misc/two_counters_e7_222.lus,top
84
./src/kind_fmcad08/misc/two_counters_e1_268.lus,top
85
./src/kind_fmcad08/misc/traffic_e7_46.lus,top
86
./src/kind_fmcad08/misc/ex8_e8_220.lus,top
87
./src/kind_fmcad08/misc/ex3.lus,top
88
./src/kind_fmcad08/misc/ticket3i_6.lus,top
89
./src/kind_fmcad08/misc/ex3_e8_381.lus,top
90
./src/kind_fmcad08/misc/durationThm_3_e7_334_e7_118.lus,top
91
./src/kind_fmcad08/misc/durationThm_1_e3_389_e4_294.lus,top
92
./src/kind_fmcad08/misc/ticket3i_3_e7_99.lus,top
93
./src/kind_fmcad08/misc/durationThm_2_e3_99.lus,top
94
./src/kind_fmcad08/misc/stalmark_e7_76.lus,top
95
./src/kind_fmcad08/misc/durationThm_3_e7_334_e3_42.lus,top
96
./src/kind_fmcad08/misc/durationThm_3_e3_207.lus,top
97
./src/kind_fmcad08/misc/ticket3i_7_e3_59_e7_2122.lus,top
98
./src/kind_fmcad08/misc/stalmark_e7_27.lus,top
99
./src/kind_fmcad08/misc/_6counters_e3_140_e8_149.lus,top
100
./src/kind_fmcad08/misc/durationThm_2.lus,top
101
./src/kind_fmcad08/misc/_6counter2.lus,top
102
./src/kind_fmcad08/misc/stalmark_e8_48.lus,top
103
./src/kind_fmcad08/misc/durationThm_1_e7_217_e7_31.lus,top
104
./src/kind_fmcad08/misc/ticket3i_7_e7_3176_e1_2924.lus,top
105
./src/kind_fmcad08/misc/traffic.lus,top
106
./src/kind_fmcad08/misc/durationThm_2_e7_145_e7_154.lus,top
107
./src/kind_fmcad08/misc/durationThm_3_e1_36.lus,top
108
./src/kind_fmcad08/misc/stalmark_e8_64_e8_207.lus,top
109
./src/kind_fmcad08/misc/durationThm_1_e7_217.lus,top
110
./src/kind_fmcad08/misc/ticket3i_all_e1_2706_e7_1776.lus,top
111
./src/kind_fmcad08/memory1/DRAGON_2_e2_4481.lus,top
112
./src/kind_fmcad08/memory1/DRAGON_5.lus,top
113
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e3_671_e7_1882.lus,top
114
./src/kind_fmcad08/memory1/DRAGON_6.lus,top
115
./src/kind_fmcad08/memory1/FIREFLY_luke_rt_e2_3460.lus,top
116
./src/kind_fmcad08/memory1/DRAGON_all_e2_6104_e2_3308.lus,top
117
./src/kind_fmcad08/memory1/DRAGON_2_e7_25_e1_154.lus,top
118
./src/kind_fmcad08/memory1/DRAGON_2_e1_2316.lus,top
119
./src/kind_fmcad08/memory1/FIREFLY_4_e3_3511_e2_1923.lus,top
120
./src/kind_fmcad08/memory1/DRAGON_3_e1_4783.lus,top
121
./src/kind_fmcad08/memory1/FIREFLY_luke_1a_e2_284_e7_998.lus,top
122
./src/kind_fmcad08/memory1/DRAGON_4_e7_2329_e7_3856.lus,top
123
./src/kind_fmcad08/memory1/DRAGON_10.lus,top
124
./src/kind_fmcad08/memory1/DRAGON_6_e7_5046_e7_3623.lus,top
125
./src/kind_fmcad08/memory1/FIREFLY_luke_rt_e1_913_e7_1403.lus,top
126
./src/kind_fmcad08/memory1/FIREFLY_6.lus,top
127
./src/kind_fmcad08/memory1/DRAGON_11_e1_2450_e3_2330.lus,top
128
./src/kind_fmcad08/memory1/DRAGON_all_e3_5957.lus,top
129
./src/kind_fmcad08/memory1/FIREFLY_a3_e2_2086_e1_3235.lus,top
130
./src/kind_fmcad08/memory1/DRAGON_13_e7_2336.lus,top
131
./src/kind_fmcad08/memory1/DRAGON_4_e7_2329_e3_4574.lus,top
132
./src/kind_fmcad08/memory1/FIREFLY_luke_1a_e2_284_e1_2924.lus,top
133
./src/kind_fmcad08/memory1/DRAGON_14_e2_3606.lus,top
134
./src/kind_fmcad08/memory1/DRAGON_8_e3_786.lus,top
135
./src/kind_fmcad08/memory1/DRAGON_2_e7_25.lus,top
136
./src/kind_fmcad08/memory1/FIREFLY_luke_rt_e2_3460_e2_2670.lus,top
137
./src/kind_fmcad08/memory1/FIREFLY_all_e3_3496.lus,top
138
./src/kind_fmcad08/memory1/FIREFLY_all_e2_2924_e2_1767.lus,top
139
./src/kind_fmcad08/memory1/DRAGON_3_e1_4783_e7_4070.lus,top
140
./src/kind_fmcad08/memory1/DRAGON_all_e1_4022_e7_2886.lus,top
141
./src/kind_fmcad08/memory1/DRAGON_7_e7_3157_e2_2082.lus,top
142
./src/kind_fmcad08/memory1/DRAGON_10_e1_3587_e7_872.lus,top
143
./src/kind_fmcad08/memory1/DRAGON_all2_e7_5406_e1_6690.lus,top
144
./src/kind_fmcad08/memory1/DRAGON_13_e3_1418_e3_2761.lus,top
145
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e7_3191_e8_2830.lus,top
146
./src/kind_fmcad08/memory1/FIREFLY_all_e1_1207_e1_1201.lus,top
147
./src/kind_fmcad08/memory1/DRAGON_2_e7_25_e7_4469.lus,top
148
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e3_671.lus,top
149
./src/kind_fmcad08/memory1/FIREFLY_a3_e1_3233_e1_3123.lus,top
150
./src/kind_fmcad08/memory1/DRAGON_9_e7_1843_e7_2225.lus,top
151
./src/kind_fmcad08/memory1/DRAGON_1_e1_3184_e7_1888.lus,top
152
./src/kind_fmcad08/memory1/DRAGON_4_e2_2799_e7_2499.lus,top
153
./src/kind_fmcad08/memory1/FIREFLY_a3_e3_314_e1_1979.lus,top
154
./src/kind_fmcad08/memory1/DRAGON_4_e1_4312.lus,top
155
./src/kind_fmcad08/memory1/FIREFLY_5_e1_2552_e7_1169.lus,top
156
./src/kind_fmcad08/memory1/FIREFLY_luke_rt.lus,top
157
./src/kind_fmcad08/memory1/DRAGON_all.lus,top
158
./src/kind_fmcad08/memory1/FIREFLY_luke_4_e2_325.lus,top
159
./src/kind_fmcad08/memory1/DRAGON_3_e7_4884.lus,top
160
./src/kind_fmcad08/memory1/FIREFLY_all_e2_2924_e1_768.lus,top
161
./src/kind_fmcad08/memory1/FIREFLY_1_e1_1092_e7_1119.lus,top
162
./src/kind_fmcad08/memory1/FIREFLY_11_e1_3457.lus,top
163
./src/kind_fmcad08/memory1/DRAGON_10_e3_144_e7_523.lus,top
164
./src/kind_fmcad08/memory1/FIREFLY_luke_rt_e2_3460_e3_1333.lus,top
165
./src/kind_fmcad08/memory1/DRAGON_all2_e7_5406_e7_6697.lus,top
166
./src/kind_fmcad08/memory1/FIREFLY_11.lus,top
167
./src/kind_fmcad08/memory1/DRAGON_5_e7_2017_e2_664.lus,top
168
./src/kind_fmcad08/memory1/FIREFLY_7.lus,top
169
./src/kind_fmcad08/memory1/DRAGON_12_e1_4640_e7_128.lus,top
170
./src/kind_fmcad08/memory1/DRAGON_all_e3_4821_e4_1791.lus,top
171
./src/kind_fmcad08/memory1/DRAGON_4_e3_1540_e1_5048.lus,top
172
./src/kind_fmcad08/memory1/FIREFLY_4_e3_3511_e4_1464.lus,top
173
./src/kind_fmcad08/memory1/FIREFLY_4_e3_3511_e1_2375.lus,top
174
./src/kind_fmcad08/memory1/DRAGON_2_e7_25_e2_5340.lus,top
175
./src/kind_fmcad08/memory1/FIREFLY_u1_e7_3318.lus,top
176
./src/kind_fmcad08/memory1/DRAGON_all_e1_4022_e3_3628.lus,top
177
./src/kind_fmcad08/memory1/DRAGON_1_e2_1997_e7_3613_e2_3409.lus,top
178
./src/kind_fmcad08/memory1/DRAGON_11_e1_2450_e2_1483.lus,top
179
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e7_3191.lus,top
180
./src/kind_fmcad08/memory1/FIREFLY_u1_e2_3403_e2_957.lus,top
181
./src/kind_fmcad08/memory1/DRAGON_all2_e3_4612_e1_6463.lus,top
182
./src/kind_fmcad08/memory1/DRAGON_12_e2_1618_e7_4732.lus,top
183
./src/kind_fmcad08/memory1/DRAGON_12_e2_1618_e3_2012.lus,top
184
./src/kind_fmcad08/memory1/DRAGON_all2_e8_4626.lus,top
185
./src/kind_fmcad08/memory1/FIREFLY_8_e2_1711_e7_1962.lus,top
186
./src/kind_fmcad08/memory1/DRAGON_8_e3_786_e7_4541.lus,top
187
./src/kind_fmcad08/memory1/DRAGON_14_e3_5120.lus,top
188
./src/kind_fmcad08/memory1/DRAGON_all2_e3_4612_e4_3719.lus,top
189
./src/kind_fmcad08/memory1/FIREFLY_11_e3_2076_e1_1270.lus,top
190
./src/kind_fmcad08/memory1/DRAGON_11_e1_2450_e1_5887.lus,top
191
./src/kind_fmcad08/memory1/DRAGON_11_e2_1678_e1_3565.lus,top
192
./src/kind_fmcad08/memory1/DRAGON_all2_e8_5504.lus,top
193
./src/kind_fmcad08/memory1/DRAGON_5_e1_1835.lus,top
194
./src/kind_fmcad08/memory1/DRAGON_10_e7_3861_e2_1020.lus,top
195
./src/kind_fmcad08/memory1/DRAGON_all2_e3_4612_e8_5861.lus,top
196
./src/kind_fmcad08/memory1/FIREFLY_luke_4.lus,top
197
./src/kind_fmcad08/memory1/FIREFLY_a3_e3_314_e2_2812.lus,top
198
./src/kind_fmcad08/memory1/FIREFLY_4.lus,top
199
./src/kind_fmcad08/memory1/FIREFLY_luke_1a_e2_284_e3_3091.lus,top
200
./src/kind_fmcad08/memory1/DRAGON_all_e3_4821_e5_1536.lus,top
201
./src/kind_fmcad08/memory1/DRAGON_10_e2_402.lus,top
202
./src/kind_fmcad08/memory1/DRAGON_5_e7_2017.lus,top
203
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e1_1691.lus,top
204
./src/kind_fmcad08/memory1/FIREFLY_5_e2_2884_e2_1492.lus,top
205
./src/kind_fmcad08/memory1/DRAGON_3_e3_5422_e1_2288.lus,top
206
./src/kind_fmcad08/memory1/FIREFLY_luke_rt_e1_913.lus,top
207
./src/kind_fmcad08/memory1/FIREFLY_6_e2_3302.lus,top
208
./src/kind_fmcad08/memory1/DRAGON_3_e1_4783_e3_511.lus,top
209
./src/kind_fmcad08/memory1/DRAGON_all2.lus,top
210
./src/kind_fmcad08/memory1/FIREFLY_all.lus,top
211
./src/kind_fmcad08/memory1/FIREFLY_a3_e1_3233_e3_2970.lus,top
212
./src/kind_fmcad08/memory1/DRAGON_5_e7_2017_e3_1763.lus,top
213
./src/kind_fmcad08/memory1/DRAGON_2_e2_3183_e3_5972.lus,top
214
./src/kind_fmcad08/memory1/FIREFLY_8_e2_1711.lus,top
215
./src/kind_fmcad08/memory1/FIREFLY_all_e2_2924_e3_3946.lus,top
216
./src/kind_fmcad08/memory1/FIREFLY_luke_3_e1_2217_e3_1200.lus,top
217
./src/kind_fmcad08/memory1/FIREFLY_luke_rt_e1_913_e2_3353.lus,top
218
./src/kind_fmcad08/memory1/DRAGON_all_e1_4037.lus,top
219
./src/kind_fmcad08/memory1/DRAGON_all2_e8_5504_e2_1598.lus,top
220
./src/kind_fmcad08/memory1/DRAGON_10_e3_3429.lus,top
221
./src/kind_fmcad08/memory1/FIREFLY_4_e3_3511_e7_3568.lus,top
222
./src/kind_fmcad08/memory1/FIREFLY_1.lus,top
223
./src/kind_fmcad08/memory1/DRAGON_3.lus,top
224
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e3_671_e3_941.lus,top
225
./src/kind_fmcad08/memory1/DRAGON_all_e7_1941_e2_6086.lus,top
226
./src/kind_fmcad08/memory1/FIREFLY_all_e1_1207_e3_1928.lus,top
227
./src/kind_fmcad08/memory1/FIREFLY_5.lus,top
228
./src/kind_fmcad08/memory1/DRAGON_10_e7_3861_e7_2180.lus,top
229
./src/kind_fmcad08/memory1/FIREFLY_luke_rt_e2_3460_e7_471.lus,top
230
./src/kind_fmcad08/memory1/DRAGON_all2_e2_2073_e8_3691.lus,top
231
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e2_3049_e2_698.lus,top
232
./src/kind_fmcad08/memory1/DRAGON_1_e1_5070.lus,top
233
./src/kind_fmcad08/memory1/FIREFLY_5_e2_2884_e1_2678.lus,top
234
./src/kind_fmcad08/memory1/DRAGON_2_e2_3183_e2_3580.lus,top
235
./src/kind_fmcad08/memory1/FIREFLY_9.lus,top
236
./src/kind_fmcad08/memory1/FIREFLY_rt.lus,top
237
./src/kind_fmcad08/memory1/FIREFLY_3_e2_2236_e1_2305.lus,top
238
./src/kind_fmcad08/memory1/FIREFLY_u1.lus,top
239
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e1_1139_e1_1565.lus,top
240
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e3_671_e1_725.lus,top
241
./src/kind_fmcad08/memory1/FIREFLY_luke_2.lus,top
242
./src/kind_fmcad08/memory1/DRAGON_14_e7_3162_e2_753.lus,top
243
./src/kind_fmcad08/memory1/DRAGON_all2_e7_5406.lus,top
244
./src/kind_fmcad08/memory1/DRAGON_11_e3_382_e1_505.lus,top
245
./src/kind_fmcad08/memory1/FIREFLY_8_e2_1711_e3_1753.lus,top
246
./src/kind_fmcad08/memory1/DRAGON_all_e3_4821_e1_1318.lus,top
247
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e2_3049_e3_2697.lus,top
248
./src/kind_fmcad08/memory1/DRAGON_all_e2_6104_e3_2607.lus,top
249
./src/kind_fmcad08/memory1/DRAGON_9_e7_1843_e1_5434.lus,top
250
./src/kind_fmcad08/memory1/DRAGON_1_e2_1997.lus,top
251
./src/kind_fmcad08/memory1/DRAGON_12.lus,top
252
./src/kind_fmcad08/memory1/DRAGON_5_e7_2017_e1_5832.lus,top
253
./src/kind_fmcad08/memory1/DRAGON_all_e2_6104_e1_6205.lus,top
254
./src/kind_fmcad08/memory1/FIREFLY_1_e1_1092_e3_389.lus,top
255
./src/kind_fmcad08/memory1/DRAGON_11.lus,top
256
./src/kind_fmcad08/memory1/DRAGON_10_e1_998.lus,top
257
./src/kind_fmcad08/memory1/FIREFLY_a3_e1_3233_e7_906.lus,top
258
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e3_671_e2_2131.lus,top
259
./src/kind_fmcad08/memory1/FIREFLY_all_e1_1207_e2_3220.lus,top
260
./src/kind_fmcad08/memory1/FIREFLY_all_e2_3678.lus,top
261
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e2_3049_e1_946.lus,top
262
./src/kind_fmcad08/memory1/DRAGON_1_e1_14612_e2_2653_e7_4370.lus,top
263
./src/kind_fmcad08/memory1/DRAGON_8_e7_3752.lus,top
264
./src/kind_fmcad08/memory1/FIREFLY_4_e3_3511_e5_3248.lus,top
265
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e7_3191_e3_1250.lus,top
266
./src/kind_fmcad08/memory1/FIREFLY_a3_e2_2086_e3_2542.lus,top
267
./src/kind_fmcad08/memory1/DRAGON_all2_e7_5406_e2_3084.lus,top
268
./src/kind_fmcad08/memory1/FIREFLY_all_e3_1600_e5_84.lus,top
269
./src/kind_fmcad08/memory1/FIREFLY_8_e2_1711_e2_2673.lus,top
270
./src/kind_fmcad08/memory1/DRAGON_3_e1_4783_e2_158.lus,top
271
./src/kind_fmcad08/memory1/FIREFLY_all_e3_1600_e3_2055.lus,top
272
./src/kind_fmcad08/memory1/FIREFLY_all_e3_1600_e7_1607.lus,top
273
./src/kind_fmcad08/memory1/DRAGON_2_e7_25_e8_3171.lus,top
274
./src/kind_fmcad08/memory1/DRAGON_all2_e8_5504_e7_579.lus,top
275
./src/kind_fmcad08/memory1/DRAGON_3_e2_5343_e1_988.lus,top
276
./src/kind_fmcad08/memory1/FIREFLY_2_e3_151_e3_1540.lus,top
277
./src/kind_fmcad08/memory1/FIREFLY_luke_1a_e7_3042_e3_1213.lus,top
278
./src/kind_fmcad08/memory1/DRAGON_all2_e7_5406_e3_506.lus,top
279
./src/kind_fmcad08/memory1/FIREFLY_8.lus,top
280
./src/kind_fmcad08/memory1/FIREFLY_all_e1_1207_e7_156.lus,top
281
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e7_3191_e7_2146.lus,top
282
./src/kind_fmcad08/memory1/DRAGON_4_e2_2799_e1_1303.lus,top
283
./src/kind_fmcad08/memory1/FIREFLY_5_e2_2884_e3_1882.lus,top
284
./src/kind_fmcad08/memory1/DRAGON_14_e7_3162.lus,top
285
./src/kind_fmcad08/memory1/DRAGON_all_e2_6104.lus,top
286
./src/kind_fmcad08/memory1/FIREFLY_rt_e3_1770_e2_637.lus,top
287
./src/kind_fmcad08/memory1/DRAGON_12_e2_1618_e1_6030.lus,top
288
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e7_2574.lus,top
289
./src/kind_fmcad08/memory1/FIREFLY_8_e2_1711_e1_1489.lus,top
290
./src/kind_fmcad08/memory1/DRAGON_4_e2_2799_e3_1915.lus,top
291
./src/kind_fmcad08/memory1/DRAGON_3_e1_4783_e1_3755.lus,top
292
./src/kind_fmcad08/memory1/DRAGON_3_e3_5422_e2_3135.lus,top
293
./src/kind_fmcad08/memory1/DRAGON_3_e3_3846.lus,top
294
./src/kind_fmcad08/memory1/FIREFLY_3_e2_2236_e2_1058.lus,top
295
./src/kind_fmcad08/memory1/FIREFLY_3_e2_2236_e3_2657.lus,top
296
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e1_1139_e2_2893.lus,top
297
./src/kind_fmcad08/memory1/FIREFLY_1_e1_1092_e2_1853.lus,top
298
./src/kind_fmcad08/memory1/DRAGON_13_e7_2336_e3_3117.lus,top
299
./src/kind_fmcad08/memory1/DRAGON_2.lus,top
300
./src/kind_fmcad08/memory1/DRAGON_2_e7_25_e3_829.lus,top
301
./src/kind_fmcad08/memory1/FIREFLY_luke_1a_e2_284_e2_2755.lus,top
302
./src/kind_fmcad08/memory1/FIREFLY_all_e7_1909.lus,top
303
./src/kind_fmcad08/memory1/FIREFLY_5_e2_2884.lus,top
304
./src/kind_fmcad08/memory1/FIREFLY_a3_e3_314_e4_897.lus,top
305
./src/kind_fmcad08/memory1/DRAGON_4_e2_2799.lus,top
306
./src/kind_fmcad08/memory1/FIREFLY_4_e3_3511_e3_422.lus,top
307
./src/kind_fmcad08/memory1/FIREFLY_luke_1b.lus,top
308
./src/kind_fmcad08/memory1/FIREFLY_3.lus,top
309
./src/kind_fmcad08/memory1/FIREFLY_all_e1_3406.lus,top
310
./src/kind_fmcad08/memory1/FIREFLY_luke_1a.lus,top
311
./src/kind_fmcad08/memory1/DRAGON_1_e3_11891_e7_4569_e4_4881.lus,top
312
./src/kind_fmcad08/memory1/DRAGON_4_e2_2799_e2_2251.lus,top
313
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e1_1139_e3_1839.lus,top
314
./src/kind_fmcad08/memory1/DRAGON_13_e7_2336_e2_1255.lus,top
315
./src/kind_fmcad08/memory1/FIREFLY_3_e2_2236.lus,top
316
./src/kind_fmcad08/memory1/DRAGON_12_e2_1618.lus,top
317
./src/kind_fmcad08/memory1/DRAGON_10_e2_2785_e3_1744.lus,top
318
./src/kind_fmcad08/memory1/DRAGON_9_e7_1843_e3_5316.lus,top
319
./src/kind_fmcad08/memory1/DRAGON_2_e2_3183_e1_2644.lus,top
320
./src/kind_fmcad08/memory1/DRAGON_14_e7_3162_e3_4298.lus,top
321
./src/kind_fmcad08/memory1/FIREFLY_5_e2_2884_e7_3594.lus,top
322
./src/kind_fmcad08/memory1/DRAGON_14_e7_3162_e1_3998.lus,top
323
./src/kind_fmcad08/memory1/FIREFLY_luke_rt_e1_913_e1_1993.lus,top
324
./src/kind_fmcad08/memory1/FIREFLY_all_e3_1600_e2_676.lus,top
325
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e3_671_e5_1637.lus,top
326
./src/kind_fmcad08/memory1/DRAGON_all2_e3_4612_e2_5774.lus,top
327
./src/kind_fmcad08/memory1/DRAGON_11_e1_2450.lus,top
328
./src/kind_fmcad08/memory1/DRAGON_9_e7_1843.lus,top
329
./src/kind_fmcad08/memory1/DRAGON_11_e1_2450_e7_5791.lus,top
330
./src/kind_fmcad08/memory1/FIREFLY_2.lus,top
331
./src/kind_fmcad08/memory1/DRAGON_14_e1_5710.lus,top
332
./src/kind_fmcad08/memory1/DRAGON_8.lus,top
333
./src/kind_fmcad08/memory1/DRAGON_4.lus,top
334
./src/kind_fmcad08/memory1/DRAGON_4_e3_4133.lus,top
335
./src/kind_fmcad08/memory1/DRAGON_9.lus,top
336
./src/kind_fmcad08/memory1/DRAGON_all_e1_4022_e2_267.lus,top
337
./src/kind_fmcad08/memory1/FIREFLY_a3_e2_2086_e2_2689.lus,top
338
./src/kind_fmcad08/memory1/FIREFLY_luke_2_e2_1375_e1_418.lus,top
339
./src/kind_fmcad08/memory1/FIREFLY_luke_rt_e3_1549.lus,top
340
./src/kind_fmcad08/memory1/FIREFLY_a3_e1_3233.lus,top
341
./src/kind_fmcad08/memory1/FIREFLY_4_e3_3511.lus,top
342
./src/kind_fmcad08/memory1/DRAGON_13.lus,top
343
./src/kind_fmcad08/memory1/DRAGON_11_e3_382_e4_4421.lus,top
344
./src/kind_fmcad08/memory1/DRAGON_all2_e3_4612_e3_1543.lus,top
345
./src/kind_fmcad08/memory1/DRAGON_13_e7_2336_e7_685.lus,top
346
./src/kind_fmcad08/memory1/DRAGON_1.lus,top
347
./src/kind_fmcad08/memory1/FIREFLY_1_e1_1092.lus,top
348
./src/kind_fmcad08/memory1/DRAGON_10_e1_3587_e3_2749.lus,top
349
./src/kind_fmcad08/memory1/FIREFLY_5_e2_2229.lus,top
350
./src/kind_fmcad08/memory1/DRAGON_9_e7_1843_e2_1145.lus,top
351
./src/kind_fmcad08/memory1/DRAGON_14_e3_1259_e1_5798.lus,top
352
./src/kind_fmcad08/memory1/DRAGON_7_e2_2872_e3_2640.lus,top
353
./src/kind_fmcad08/memory1/DRAGON_12_e2_1618_e2_138.lus,top
354
./src/kind_fmcad08/memory1/DRAGON_all2_e3_4612_e5_3642.lus,top
355
./src/kind_fmcad08/memory1/FIREFLY_all_e2_2924_e7_3371.lus,top
356
./src/kind_fmcad08/memory1/FIREFLY_luke_3.lus,top
357
./src/kind_fmcad08/memory1/FIREFLY_a3_e1_3233_e2_2392.lus,top
358
./src/kind_fmcad08/memory1/DRAGON_1_e1_14612_e1_268_e7_501.lus,top
359
./src/kind_fmcad08/memory1/DRAGON_all2_e8_5504_e1_4719.lus,top
360
./src/kind_fmcad08/memory1/DRAGON_13_e7_2336_e1_541.lus,top
361
./src/kind_fmcad08/memory1/FIREFLY_luke_rt_e2_3460_e1_1455.lus,top
362
./src/kind_fmcad08/memory1/DRAGON_7.lus,top
363
./src/kind_fmcad08/memory1/DRAGON_all_e7_4065.lus,top
364
./src/kind_fmcad08/memory1/DRAGON_11_e2_5396_e3_282.lus,top
365
./src/kind_fmcad08/memory1/FIREFLY_9_e7_170_e3_3647.lus,top
366
./src/kind_fmcad08/memory1/FIREFLY_a3_e2_2086_e7_2614.lus,top
367
./src/kind_fmcad08/memory1/DRAGON_8_e2_3896_e3_3125.lus,top
368
./src/kind_fmcad08/memory1/FIREFLY_luke_2_e7_1826_e8_126.lus,top
369
./src/kind_fmcad08/memory1/FIREFLY_1_e1_1092_e1_1486.lus,top
370
./src/kind_fmcad08/memory1/FIREFLY_luke_5.lus,top
371
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e3_671_e4_147.lus,top
372
./src/kind_fmcad08/memory1/DRAGON_all_e1_4022_e1_1759.lus,top
373
./src/kind_fmcad08/memory1/DRAGON_14.lus,top
374
./src/kind_fmcad08/memory1/DRAGON_5_e7_2017_e7_2326.lus,top
375
./src/kind_fmcad08/memory1/DRAGON_all_e3_4821_e2_1089.lus,top
376
./src/kind_fmcad08/memory1/DRAGON_7_e2_2872_e2_5844.lus,top
377
./src/kind_fmcad08/memory1/FIREFLY_10.lus,top
378
./src/kind_fmcad08/memory1/FIREFLY_all_e3_1600_e4_2415.lus,top
379
./src/kind_fmcad08/memory1/FIREFLY_all_e3_1600_e1_667.lus,top
380
./src/kind_fmcad08/memory1/DRAGON_5_e2_3018_e2_936.lus,top
381
./src/kind_fmcad08/memory1/DRAGON_14_e7_3162_e7_3528.lus,top
382
./src/kind_fmcad08/memory1/DRAGON_10_e3_144_e5_2046.lus,top
383
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e3_671_e6_1974.lus,top
384
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e2_3049.lus,top
385
./src/kind_fmcad08/memory1/FIREFLY_10_e7_919_e2_3192.lus,top
386
./src/kind_fmcad08/memory1/FIREFLY_luke_rt_e1_913_e3_2128.lus,top
387
./src/kind_fmcad08/memory1/FIREFLY_a3_e2_2952.lus,top
388
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e7_3191_e2_1864.lus,top
389
./src/kind_fmcad08/memory1/DRAGON_4_e7_2329.lus,top
390
./src/kind_fmcad08/memory1/FIREFLY_luke_1b_e7_3191_e1_1303.lus,top
391
./src/kind_fmcad08/memory1/FIREFLY_a3.lus,top
392
./src/kind_fmcad08/memory1/FIREFLY_3_e2_2236_e7_3681.lus,top
393
./src/kind_fmcad08/simulation/PRODUCER_CONSUMER_vt_e3_507.lus,top
394
./src/kind_fmcad08/simulation/metros_2_e1_1116.lus,top
395
./src/kind_fmcad08/simulation/car_6_e3_294_e3_47.lus,top
396
./src/kind_fmcad08/simulation/speed_e7_207_e7_538.lus,top
397
./src/kind_fmcad08/simulation/car_6_e1_152_e1_391.lus,top
398
./src/kind_fmcad08/simulation/car_3_e8_33_e2_1010.lus,top
399
./src/kind_fmcad08/simulation/metros_1_e7_1255_e7_12.lus,top
400
./src/kind_fmcad08/simulation/metros_4_e3_1091_e2_1317.lus,top
401
./src/kind_fmcad08/simulation/metros_2_e1_190.lus,top
402
./src/kind_fmcad08/simulation/metros_1_e1_846_e3_1060.lus,top
403
./src/kind_fmcad08/simulation/fast_1_e8_751.lus,top
404
./src/kind_fmcad08/simulation/metros_4_e3_1091.lus,top
405
./src/kind_fmcad08/simulation/ums_e8_1032.lus,top
406
./src/kind_fmcad08/simulation/fast_1_e7_2044_e7_1287.lus,top
407
./src/kind_fmcad08/simulation/metros_4_e3_1091_e4_232.lus,top
408
./src/kind_fmcad08/simulation/metros_3_e4_987.lus,top
409
./src/kind_fmcad08/simulation/metros_4_e2_968_e2_1166.lus,top
410
./src/kind_fmcad08/simulation/car_3_e8_33.lus,top
411
./src/kind_fmcad08/simulation/Gas.lus,top
412
./src/kind_fmcad08/simulation/metros_4_e2_968_e3_931.lus,top
413
./src/kind_fmcad08/simulation/production_cell.lus,top
414
./src/kind_fmcad08/simulation/production_cell_e8_792.lus,top
415
./src/kind_fmcad08/simulation/car_5_e7_244_e3_1071.lus,top
416
./src/kind_fmcad08/simulation/speed_e7_207.lus,top
417
./src/kind_fmcad08/simulation/car_1_e7_184_e3_299.lus,top
418
./src/kind_fmcad08/simulation/metros_3_e3_1275.lus,top
419
./src/kind_fmcad08/simulation/hysteresis_1.lus,top
420
./src/kind_fmcad08/simulation/car_6_e2_589_e3_349.lus,top
421
./src/kind_fmcad08/simulation/car_3_e1_586.lus,top
422
./src/kind_fmcad08/simulation/metros_3_e3_1275_e4_164.lus,top
423
./src/kind_fmcad08/simulation/metros_4_e2_968_e4_801.lus,top
424
./src/kind_fmcad08/simulation/PRODUCER_CONSUMER_vt_e2_1352.lus,top
425
./src/kind_fmcad08/simulation/car_2.lus,top
426
./src/kind_fmcad08/simulation/car_4_e3_57_e4_1047.lus,top
427
./src/kind_fmcad08/simulation/metros_2_e1_1116_e2_617.lus,top
428
./src/kind_fmcad08/simulation/metros_3_e3_1275_e7_529.lus,top
429
./src/kind_fmcad08/simulation/metros_2_e2_968.lus,top
430
./src/kind_fmcad08/simulation/fast_1_e8_747_e7_692.lus,top
431
./src/kind_fmcad08/simulation/car_4_e3_556.lus,top
432
./src/kind_fmcad08/simulation/car_all.lus,top
433
./src/kind_fmcad08/simulation/PRODUCER_CONSUMMER_luke_2.lus,top
434
./src/kind_fmcad08/simulation/production_cell_e8_6_e8_427.lus,top
435
./src/kind_fmcad08/simulation/car_2_e8_491_e7_826.lus,top
436
./src/kind_fmcad08/simulation/car_all_e8_856_e1_217.lus,top
437
./src/kind_fmcad08/simulation/fast_1_e7_2044.lus,top
438
./src/kind_fmcad08/simulation/car_all_e8_856_e3_180.lus,top
439
./src/kind_fmcad08/simulation/car_all_e3_1068_e1_178.lus,top
440
./src/kind_fmcad08/simulation/car_all_e3_1068.lus,top
441
./src/kind_fmcad08/simulation/metros_3_e4_987_e3_291.lus,top
442
./src/kind_fmcad08/simulation/metros_2_e1_1116_e7_1440.lus,top
443
./src/kind_fmcad08/simulation/cd.lus,top
444
./src/kind_fmcad08/simulation/metros_4.lus,top
445
./src/kind_fmcad08/simulation/speed_e7_207_e8_507.lus,top
446
./src/kind_fmcad08/simulation/PRODUCER_CONSUMER_vt_e7_1059_e8_1111.lus,top
447
./src/kind_fmcad08/simulation/production_cell_e7_207_e8_241.lus,top
448
./src/kind_fmcad08/simulation/metros_1_e1_846_e1_1317.lus,top
449
./src/kind_fmcad08/simulation/metros_1_e2_1102_e7_1163.lus,top
450
./src/kind_fmcad08/simulation/metros_2_e1_1116_e3_287.lus,top
451
./src/kind_fmcad08/simulation/production_cell_e8_6_e7_651.lus,top
452
./src/kind_fmcad08/simulation/metros_1_e8_725_e1_919.lus,top
453
./src/kind_fmcad08/simulation/metros_3_e3_1275_e5_846.lus,top
454
./src/kind_fmcad08/simulation/car_4_e3_57_e5_999.lus,top
455
./src/kind_fmcad08/simulation/production_cell_e7_21.lus,top
456
./src/kind_fmcad08/simulation/car_5_e3_11_e1_429.lus,top
457
./src/kind_fmcad08/simulation/cd_e7_621_e7_669.lus,top
458
./src/kind_fmcad08/simulation/ums.lus,top
459
./src/kind_fmcad08/simulation/metros_4_e2_968.lus,top
460
./src/kind_fmcad08/simulation/car_5.lus,top
461
./src/kind_fmcad08/simulation/metros_2_e1_1116_e1_556.lus,top
462
./src/kind_fmcad08/simulation/car_4_e8_118_e7_178.lus,top
463
./src/kind_fmcad08/simulation/fast_2_e7_2526_e7_2736.lus,top
464
./src/kind_fmcad08/simulation/car_all_e3_1068_e5_882.lus,top
465
./src/kind_fmcad08/simulation/fast_2_e7_2526.lus,top
466
./src/kind_fmcad08/simulation/tramway_e7_1834_e7_2363.lus,top
467
./src/kind_fmcad08/simulation/car_all_e2_142.lus,top
468
./src/kind_fmcad08/simulation/car_5_e2_405_e2_1083.lus,top
469
./src/kind_fmcad08/simulation/speed2_e8_449.lus,top
470
./src/kind_fmcad08/simulation/car_2_e7_1027_e7_359.lus,top
471
./src/kind_fmcad08/simulation/car_3_e7_626.lus,top
472
./src/kind_fmcad08/simulation/metros_2_e2_704_e3_76.lus,top
473
./src/kind_fmcad08/simulation/car_all_e8_856.lus,top
474
./src/kind_fmcad08/simulation/metros_1_e7_606.lus,top
475
./src/kind_fmcad08/simulation/cd_e7_8.lus,top
476
./src/kind_fmcad08/simulation/metros_1_e2_1102_e1_317.lus,top
477
./src/kind_fmcad08/simulation/PRODUCER_CONSUMMER_luke_2_e7_1068_e8_1019.lus,top
478
./src/kind_fmcad08/simulation/hysteresis_3.lus,top
479
./src/kind_fmcad08/simulation/metros_3_e3_1275_e1_1350.lus,top
480
./src/kind_fmcad08/simulation/car_5_e2_405_e8_1055.lus,top
481
./src/kind_fmcad08/simulation/car_all_e3_1068_e4_275.lus,top
482
./src/kind_fmcad08/simulation/metros_4_e3_1091_e3_522.lus,top
483
./src/kind_fmcad08/simulation/PRODUCER_CONSUMER_1.lus,top
484
./src/kind_fmcad08/simulation/metros_1_e2_1102_e3_961.lus,top
485
./src/kind_fmcad08/simulation/fast_2_e8_460_e7_43.lus,top
486
./src/kind_fmcad08/simulation/car_6.lus,top
487
./src/kind_fmcad08/simulation/fast_1.lus,top
488
./src/kind_fmcad08/simulation/car_3_e7_626_e1_305.lus,top
489
./src/kind_fmcad08/simulation/metros_3_e4_987_e2_80.lus,top
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff