lurette 0.19 Thu, 06 Dec 2001 15:17:25 +0100 by jahier

Parent-Version:      0.18
Version-Log:

Fix a bug where the variables were not given in the good order to
the oracle.

Give a diagnostic when the oracle is broken.

Put everything related to sim2chro in tis own module.

Project-Description: Lurette

Makefile

@@ -14,6 +14,7 @@ SOURCES = $(SUT) sut_stub.c  sut_idl_stub.idl \
           $(LURETTE_DIR)/source/formula.mli $(LURETTE_DIR)/source/formula.ml \
           $(LURETTE_DIR)/source/print.mli $(LURETTE_DIR)/source/print.ml \
           $(LURETTE_DIR)/source/env_state.mli $(LURETTE_DIR)/source/env_state.ml \
+          $(LURETTE_DIR)/source/sim2chro.mli $(LURETTE_DIR)/source/sim2chro.ml \
           $(LURETTE_DIR)/source/eval.mli $(LURETTE_DIR)/source/eval.ml \
           $(LURETTE_DIR)/source/solver.mli $(LURETTE_DIR)/source/solver.ml  \
           $(LURETTE_DIR)/source/wtree.mli $(LURETTE_DIR)/source/wtree.ml  \

OcamlMakefile

@@ -5,7 +5,7 @@
 #                            For updates see:
 #             http://miss.wu-wien.ac.at/~mottl/ocaml_sources
 #
-#        $Id: OcamlMakefile 1.5 Thu, 06 Dec 2001 12:40:09 +0100 jahier $
+#        $Id: OcamlMakefile 1.6 Thu, 06 Dec 2001 15:17:25 +0100 jahier $
 #
 ###########################################################################
 
@@ -491,7 +491,7 @@ dot:
 
 # 
 try:
-	$(LURETTE_DIR)/make_lurette tram_simple vrai_tram; \
+	$(LURETTE_DIR)/make_lurette tram_simple tram_oracle; \
 	./lurette 50 10 10 tram_env_porte.env x tram_env_usager.env tram_env_tramway.env
 
 

lurette.prj

 ;; -*- Prcs -*-
 (Created-By-Prcs-Version 1 3 3)
 (Project-Description "Lurette")
-(Project-Version lurette 0 18)
-(Parent-Version lurette 0 17)
-(Version-Log " Handle pre in formula and expressions. Also add (in
-green) the environment local vars in the sim2chro output.
+(Project-Version lurette 0 19)
+(Parent-Version lurette 0 18)
+(Version-Log "
+Fix a bug where the variables were not given in the good order to
+the oracle.
+
+Give a diagnostic when the oracle is broken.
+
+Put everything related to sim2chro in tis own module.
 ")
 (New-Version-Log "")
-(Checkin-Time "Thu, 06 Dec 2001 12:40:09 +0100")
+(Checkin-Time "Thu, 06 Dec 2001 15:17:25 +0100")
 (Checkin-Login jahier)
 (Populate-Ignore ())
 (Project-Keywords)
@@ -18,8 +23,8 @@ green) the environment local vars in the sim2chro output.
 
 
 ;; Sources files
-  (source/lurette.mli (lurette/11_lurette.ml 1.7 644))
-  (source/lurette.ml (lurette/12_lurette.ml 1.11 644))
+  (source/lurette.mli (lurette/11_lurette.ml 1.8 644))
+  (source/lurette.ml (lurette/12_lurette.ml 1.12 644))
 
   (source/graph.mli (lurette/13_graph.mli 1.2 644))
   (source/graph.ml (lurette/14_graph.ml 1.2 644))
@@ -27,7 +32,7 @@ green) the environment local vars in the sim2chro output.
   (source/env.mli (lurette/15_env.mli 1.5 644))
   (source/env.ml (lurette/16_env.ml 1.9 644))
 
-  (source/util.ml (lurette/35_util.ml 1.3 644))
+  (source/util.ml (lurette/35_util.ml 1.4 644))
 
   (source/solver.mli (lurette/38_solver.mli 1.1 644))
   (source/solver.ml (lurette/39_solver.ml 1.2 644))
@@ -48,16 +53,16 @@ green) the environment local vars in the sim2chro output.
   (source/eval.ml (lurette/49_eval.ml 1.2 644))
 
   (source/env_state.mli (lurette/50_env_state. 1.2 644))
-  (source/env_state.ml (lurette/51_env_state. 1.2 644))
+  (source/env_state.ml (lurette/51_env_state. 1.3 644))
 
   (source/wtree.mli (lurette/b/0_wtree.mli 1.1 644))
   (source/wtree.ml (lurette/b/1_wtree.ml 1.1 644))
 
-  (source/gen_stubs.ml (lurette/24_generate_l 1.11 644))
+  (source/gen_stubs.ml (lurette/24_generate_l 1.12 644))
 
 ;; Make files
-  (OcamlMakefile (lurette/17_OcamlMakef 1.5 644))
-  (Makefile (lurette/18_Makefile 1.10 644))
+  (OcamlMakefile (lurette/17_OcamlMakef 1.6 644))
+  (Makefile (lurette/18_Makefile 1.11 644))
   (test/Makefile (../Makefile) :symlink)
   (interface/Makefile (lurette/25_Makefile 1.5 644))
   (make_lurette (lurette/27_make_luret 1.5 744))

source/env_state.ml

@@ -22,8 +22,6 @@ open Wtree
 ** formula. 
 *)
 
-(* XXX Should they really be mutable ??? *)
-
 type env_stateT = {
   (* var names and types given file by file *)
   mutable var_names: (string * (vnt list * vnt list * vnt list)) list;
@@ -43,7 +41,6 @@ type env_stateT = {
 }
 
 
-
 (* XXX suis-je oblig d'initialiser des choses ici alors que je dois 
    le faire plus tard ??? 
 *)

source/gen_stubs.ml

@@ -875,7 +875,7 @@ let main2 sut oracle =
   let oracle_alias = replace_bool_representation oracle_alias0 in
   let oracle_vi = replace_ct_by_their_alias oracle_vi0 oracle_alias in
   let oracle_vo = replace_ct_by_their_alias oracle_vo0 oracle_alias in
-
+    
    (*
    ** Sorts variables lexicographically w.r.t. to their names.
    *)
@@ -885,13 +885,14 @@ let main2 sut oracle =
   in
   let sut_vi_ord = sort_vars sut_vi in
   let sut_vo_ord = sort_vars sut_vo in
-  let oracle_vi_ord = sort_vars oracle_vi in
+  let oracle_vi_ord = List.append sut_vi_ord sut_vo_ord in
+  let oracle_vi_ord_decl = sort_vars oracle_vi in
   let sut_vars_ord = sort_vars (List.append sut_vi sut_vo) in
     
      (* 
      ** Aborts if the variables are inconsistent in the sut and in the oracle.
      *)
-    (match check_var_type sut_vars_ord oracle_vi_ord oracle_vo with
+    (match check_var_type sut_vars_ord oracle_vi_ord_decl oracle_vo with
 	 Ok -> () | Error(err_msg) -> failwith err_msg );
     
     generate_stub_c sut_m "sut" sut_vi_ord sut_vo_ord ; 

source/lurette.ml

@@ -99,64 +99,6 @@ let (read_var_names: string -> vnt list * vnt list) =
       (i, o)
 
 
-(*------------------------------------------------------------------------*)
-
-(*
-** To put the values of sut inputs and outputs in a rif file to display
-** them using sim2cro.
-*)
-    
-let (put_var_decl: out_channel -> unit) =
-  fun rif -> 
-    let put s = output_string rif s in
-    let put_vt = function
-	"boolean" -> put "bool"
-      | any -> put any
-    in
-    let put_vntl = (fun (vn,vt) -> put vn; put ":"; put_vt vt; put "\n") in
-    
-    let local_var_name_and_type_list_unsorted = 
-      fold_left 
-	(fun acc (_, (_,_,x)) -> Util.merge acc x) 
-	[] 
-	env_state.var_names 
-    in
-    let local_var_name_and_type_list = 
-      Util.sort_list_string_pair local_var_name_and_type_list_unsorted 
-    in
-
-      put "#program \"lurette variables chronogram\"\n"; 
-      
-      put "#@inputs\n";
-      List.iter put_vntl Lurette_stub.sut_input_var_name_and_type_list;
-
-      put "@#\n#@outputs\n";
-      List.iter put_vntl Lurette_stub.sut_output_var_name_and_type_list;
-      
-      if display_local_var then
-	List.iter put_vntl local_var_name_and_type_list;
-
-      put "@#\n"
-
-let (put_current_step_values: out_channel -> int -> sut_in -> sut_out -> env_loc 
-       -> unit) =
-  fun rif t input output local -> 
-    let put s = output_string rif s in
-      put "#step ";
-      put (string_of_int t);
-      put "\n";
-      
-      Lurette_stub.print_sut_in input rif;
-      put "#outs ";
-      Lurette_stub.print_sut_out output rif;
-
-      if display_local_var then
-	List.iter (fun (_, e) -> (print_atomic_expr e rif; put " ")) 
-	  (Util.sort_list_string_pair local);
-     
-      put "\n"
-
-
 (*------------------------------------------------------------------------*)
 
  	
@@ -186,45 +128,11 @@ let rec (main : unit -> 'a) =
       let n = int_of_string Sys.argv.(2) in
       let p = int_of_string Sys.argv.(3) in
       let res = main2 s n p in
-      let color_option = 
-	(* options for sim2chro to display local vars in green *) 
-	let loc_var_names =
-	  fold_left 
-	    (fun acc (_, (_,_,x)) -> (Util.merge acc x )) 
-	    []
-	    env_state.var_names
-	in
-	let varcolor_str = 
-	  fold_left 
-	    (fun acc (vn, _) -> 
-	       (acc ^ " -varcolor " ^ vn ^ " LightGreen "))
-	    ""
-	    loc_var_names
-	in
-	let varnamecolor_str = 
-	  fold_left 
-	    (fun acc (vn, _) -> 
-	       (acc ^ " -varnamecolor " ^ vn ^ " LightGreen "))
-	    ""
-	    loc_var_names
-	in
-	let varnumcolor_str = 
-	  fold_left 
-	    (fun acc (vn, _) -> 
-	       (acc ^ " -varnumcolor " ^ vn ^ " LightGreen "))
-	    ""
-	    loc_var_names
-	in
-	  (varcolor_str ^ varnamecolor_str ^ varnumcolor_str)
-      in
       let _ = 
-	if not step_by_step then
-	  let cmd = (" sim2chro -ecran " ^ color_option ^ 
-		     " -in lurette.rif  > /dev/null &")
-	  in
-	  let _ = print_string cmd in
-	    Sys.command cmd
-	else 0
+	if not step_by_step then (
+	  Sim2chro.call_sim2chro ()
+	)
+	else ()
       in
 	res
 
@@ -284,18 +192,19 @@ and
       if step_by_step then (
 	generate_env_graph [] "environment" ;  
 	gv ("environment.ps");        
-	put_var_decl stdout ;   
+	Sim2chro.put_var_decl stdout display_local_var;   
       )
-      else put_var_decl rif ;
+      else Sim2chro.put_var_decl rif display_local_var;
       
       main_loop 1 s n p rif sut_out_init ;
 
+      flush stdout;
+      flush rif;
       close_out rif; 
 
 and
   main_loop t s n p rif output = 
 
-
 (* Generates `n*p' inputs from the environment *)
   let (arcs_inputs_loc: (node list list * sut_in * env_loc) list) 
     = env_try n p output
@@ -306,22 +215,61 @@ and
     = List.map (fun (_, input, _) -> input) arcs_inputs_loc 
   in
 
-(* Tries the sut `thickness'^nth times *)
-  let (outputs: env_in list)
-    = List.map sut_try inputs 
-  in
+(* Tries the sut `n*p'^nth times *)
+  let (outputs: env_in list) = List.map sut_try inputs in
 
-(* Tries the oracle `thickness'^nth times *)
+(* Tries the oracle `n*p'^nth times *)
   let (results: bool list) = 
     List.map2 (fun x y -> oracle_try (x, y)) inputs outputs 
   in
-  let _ = if (List.mem false results) then 
-    assert false
-  else
-    ()
+
+(* Aborts if at least one of the pairs (input, output) breaks the oracle *)
+  let _ = 
+    if (List.mem false results) 
+    then (
+      let print_vntl = 
+	(fun (vn,vt) ->  
+	   print_string "\n***      ";
+	   print_string vn; 
+	   print_string ":"; 
+	   print_string vt
+	) 
+      in
+	print_string ("*** An assertion of the oracle has been violated" ^ 
+		      " at time "  ^ (string_of_int t) ^
+		      " with the following values:\n  ");
+	
+	
+	print_string "\n***   sut inputs names and types:" ;
+	List.iter (print_vntl) Lurette_stub.sut_input_var_name_and_type_list;
+	print_string "\n***   sut outputs names and types: " ;
+	List.iter (print_vntl) Lurette_stub.sut_output_var_name_and_type_list;
+	print_string "\n***" ;
+
+	Util.list_iter3 
+	  (fun i o r -> 
+	     if (not r) then
+	       (
+		 print_string "\n***   sut inputs:" ;
+		 print_sut_in i stdout; 
+		 print_string "     sut outputs: " ;
+		 print_sut_out o stdout
+	       )
+	     else
+	       ()
+	  )
+	  inputs
+	  outputs
+	  results ;
+	flush stdout;
+	flush rif;
+	Sim2chro.call_sim2chro ();
+	failwith ""
+    )
+    else ()
   in
     
-(* Choose among the `n*p' possible pairs (input, ouput) *)
+(* Chooses among the `n*p' possible pairs (input, ouput) *)
   let ran = Random.int (n*p) in
   let new_output = List.nth outputs ran in
   let (arcs, input, loc) = List.nth arcs_inputs_loc ran in
@@ -335,13 +283,13 @@ and
     let str =  
       if (step_by_step) then (
 	generate_env_graph [] "environment" ;  
-	put_current_step_values stdout t input output env_state.local ;
+	Sim2chro.put_current_step_values stdout t input output env_state.local display_local_var;
 	print_string 
 	  "\nOne more loop ? [type any char to stop, `CR' to continue]\n"; 
 	read_line ()
       )
       else (
-	put_current_step_values rif t input output env_state.local ;
+	Sim2chro.put_current_step_values rif t input output env_state.local display_local_var;
 	""
       )
     in

source/lurette.mli

@@ -11,6 +11,5 @@
 
 open Env
 
-
 val main : unit -> unit
 

source/util.ml

@@ -46,6 +46,20 @@ let (readfile: string -> string) =
       str
 
 
+let rec (list_iter3: ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list 
+	   -> 'c list -> unit) =
+  fun f l1 l2 l3 -> 
+    match (l1, l2, l3) with
+	([], [], []) -> ()
+      | (e1::t1, e2::t2, e3::t3) -> 
+	  (
+	    (f e1 e2 e3);
+            (list_iter3 (f) t1 t2 t3);
+	  )
+      | _ -> failwith ("*** Error: list_map3 should be called with lists "  
+		       ^ "of the same size.\n")
+
+
 let rec (list_map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list 
 	   -> 'c list -> 'd list) =
   fun f l1 l2 l3 -> 
@@ -54,7 +68,7 @@ let rec (list_map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list
       | (e1::t1, e2::t2, e3::t3) -> 
 	  (f e1 e2 e3)::(list_map3 f t1 t2 t3)
       | _ -> failwith ("*** Error: list_map3 should be called with lists "  
-		       ^ "of the same size.")
+		       ^ "of the same size.\n")
 
 let rec (list_map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list 
 	   -> 'c list -> 'd list -> 'e list) =
@@ -64,7 +78,7 @@ let rec (list_map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list
       | (e1::t1, e2::t2, e3::t3, e4::t4) -> 
 	  (f e1 e2 e3 e4)::(list_map4 f t1 t2 t3 t4)
       | _ -> failwith ("*** Error: list_map3 should be called with lists "  
-		       ^ "of the same size.")
+		       ^ "of the same size.\n")
 	  
 (*
 ** Sorts variables lexicographically w.r.t. to their names.