lurette 0.30 Tue, 12 Feb 2002 13:42:18 +0100 by jahier

Parent-Version:      0.29
Version-Log:

gen_stubs.ml:
    Updates the stubs files (lurette_stub.ml, sut_stub.c,
    sut_idl_stub.idl, oracle_stub.c, oracle_idl_stub.idl) iff they have
    changed to avoid unnecessary recompilations.

Makefile:
    Minor cosmetic changes.

wtree.ml,mli:
env.ml:

    Also remove a loop in the dependencies that was confusing
    ocamldot (but how could it work before with that loop ?). To do that,
    pass Solver.is_satisfiable as a argument of Wtree.choose_n_formula so
    that Wtree does not depend on Solver anymore.

Project-Description: Lurette

.lurette.prcs_aux

@@ -6,15 +6,15 @@
 (source/env_state.ml 2145 1013445149 51_env_state. 1.7)
 (source/graph.ml 2476 1012914629 14_graph.ml 1.3)
 (source/util.ml 4367 1013445149 35_util.ml 1.7)
-(source/wtree.ml 9842 1013445149 b/1_wtree.ml 1.6)
+(source/wtree.ml 9645 1013517738 b/1_wtree.ml 1.7)
 (source/solver.ml 11461 1013445149 39_solver.ml 1.7)
 (source/command_line.ml 3846 1013500921 b/20_command_li 1.2)
 (source/lurette.ml 10371 1013504295 12_lurette.ml 1.18)
 (source/solver.mli 972 1013445149 38_solver.mli 1.6)
 (source/env.mli 2506 1013445149 15_env.mli 1.8)
 (lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
-(source/env.ml 9000 1013445149 16_env.ml 1.13)
-(make_lurette 1054 1012914629 27_make_luret 1.6)
+(source/env.ml 9036 1013517738 16_env.ml 1.14)
+(make_lurette 812 1013517738 27_make_luret 1.7)
 (test/vrai_tram.lus 453 1007379917 b/6_vrai_tram. 1.1)
 (lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
 (doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
@@ -23,7 +23,7 @@
 (ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
 (doc/automata_format 0 1007379917 b/3_automata_f 1.1)
 (source/eval.ml 7903 1013445149 49_eval.ml 1.4)
-(source/gen_stubs.ml 31372 1013445149 24_generate_l 1.14)
+(source/gen_stubs.ml 32217 1013517738 24_generate_l 1.15)
 (source/parse_env.ml 9215 1012914629 41_parse_env. 1.4)
 (test/lurette.rif.exp 4746 1013504295 b/22_lurette.ri 1.2)
 (interface/TAGS 1956 1007380262 26_TAGS 1.3)
@@ -32,14 +32,14 @@
 (source/formula.mli 1870 1013445149 44_formula.ml 1.4)
 (source/command_line.mli 1266 1013500921 b/21_command_li 1.2)
 (TAGS 9825 1007379917 21_TAGS 1.6)
-(source/wtree.mli 2860 1013445149 b/0_wtree.mli 1.4)
+(source/wtree.mli 2964 1013517738 b/0_wtree.mli 1.5)
 (source/env_state.mli 3228 1013445149 50_env_state. 1.6)
 (test/porte.env 861 1012914629 b/16_porte.env 1.1)
 (interface/sut_idl_stub.ml 338 1006263457 34_sut_idl_st 1.1)
 (source/eval.mli 1668 1013445149 48_eval.mli 1.4)
 (README 74 1011881677 10_README 1.2)
 (test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
-(OcamlMakefile 17012 1013504295 17_OcamlMakef 1.13)
+(OcamlMakefile 17010 1013517738 17_OcamlMakef 1.14)
 (source/show_env.ml 3167 1013445149 43_show_env.m 1.2)
 (test/tram.env 806 1012914629 b/15_tram.env 1.1)
 (doc/synthese 2556 1007379917 b/2_synthese 1.1)

OcamlMakefile

@@ -5,7 +5,7 @@
 #                            For updates see:
 #             http://miss.wu-wien.ac.at/~mottl/ocaml_sources
 #
-#        $Id: OcamlMakefile 1.13 Tue, 12 Feb 2002 09:58:15 +0100 jahier $
+#        $Id: OcamlMakefile 1.14 Tue, 12 Feb 2002 13:42:18 +0100 jahier $
 #
 ###########################################################################
 
@@ -492,7 +492,6 @@ dot:
 	dot -Tps $(RESULT).dep.dot > $(RESULT).dep.ps ;  \
 	cp $(RESULT).dep.ps ../doc ; cp $(RESULT).depfull.ps ../doc ; popd
 
-#
 try:
 	$(LURETTE_DIR)/make_lurette ControleurPorte vrai_tram; \
 #	./lurette 10 2 2 tram.env usager.env porte.env passerelle.env | sim2chro -ecran

lurette.prj

 ;; -*- Prcs -*-
 (Created-By-Prcs-Version 1 3 3)
 (Project-Description "Lurette")
-(Project-Version lurette 0 29)
-(Parent-Version lurette 0 28)
-(Version-Log "
-Put the names of the environements in the sim2chro window title.
+(Project-Version lurette 0 30)
+(Parent-Version lurette 0 29)
+(Version-Log " 
+
+gen_stubs.ml: 
+    Updates the stubs files (lurette_stub.ml, sut_stub.c,
+    sut_idl_stub.idl, oracle_stub.c, oracle_idl_stub.idl) iff they have
+    changed to avoid unnecessary recompilations.
+
+Makefile:
+    Minor cosmetic changes.
+
+wtree.ml,mli:
+env.ml:
+
+    Also remove a loop in the dependencies that was confusing
+    ocamldot (but how could it work before with that loop ?). To do that,
+    pass Solver.is_satisfiable as a argument of Wtree.choose_n_formula so
+    that Wtree does not depend on Solver anymore.
+
 ")
 (New-Version-Log "")
-(Checkin-Time "Tue, 12 Feb 2002 09:58:15 +0100")
+(Checkin-Time "Tue, 12 Feb 2002 13:42:18 +0100")
 (Checkin-Login jahier)
 (Populate-Ignore ())
 (Project-Keywords)
@@ -25,7 +41,7 @@ Put the names of the environements in the sim2chro window title.
   (source/graph.ml (lurette/14_graph.ml 1.3 644))
 
   (source/env.mli (lurette/15_env.mli 1.8 644))
-  (source/env.ml (lurette/16_env.ml 1.13 644))
+  (source/env.ml (lurette/16_env.ml 1.14 644))
 
   (source/util.ml (lurette/35_util.ml 1.7 644))
 
@@ -50,20 +66,20 @@ Put the names of the environements in the sim2chro window title.
   (source/env_state.mli (lurette/50_env_state. 1.6 644))
   (source/env_state.ml (lurette/51_env_state. 1.7 644))
 
-  (source/wtree.mli (lurette/b/0_wtree.mli 1.4 644))
-  (source/wtree.ml (lurette/b/1_wtree.ml 1.6 644))
+  (source/wtree.mli (lurette/b/0_wtree.mli 1.5 644))
+  (source/wtree.ml (lurette/b/1_wtree.ml 1.7 644))
 
   (source/command_line.ml (lurette/b/20_command_li 1.2 644))
   (source/command_line.mli (lurette/b/21_command_li 1.2 644))
 
-  (source/gen_stubs.ml (lurette/24_generate_l 1.14 644))
+  (source/gen_stubs.ml (lurette/24_generate_l 1.15 644))
 
 ;; Make files
-  (OcamlMakefile (lurette/17_OcamlMakef 1.13 644))
+  (OcamlMakefile (lurette/17_OcamlMakef 1.14 644))
   (Makefile (lurette/18_Makefile 1.17 644))
   (test/Makefile (../Makefile) :symlink)
   (interface/Makefile (lurette/25_Makefile 1.6 644))
-  (make_lurette (lurette/27_make_luret 1.6 744))
+  (make_lurette (lurette/27_make_luret 1.7 744))
 
 
 ;; Documentation

make_lurette

 #! /bin/sh
 # 
 
-Help="usage: make_lurette <sut> <oracle>
+Help="usage: make_lurette <sut> <oracle> <make options>
 
 The first and second args of this scripts should respectively be the
 name of the sut and the name of the oracle modules (without any
 extension). 
 
-1) It call gen_stubs script to generate the stub files to interface
-the C (poc) files implementing the sut and the oracle with the rest of
-the lurette system (which is emplemented in ocaml).
+1) It calls the gen_stubs script to generate stub files to interface
+the C (poc) files implementing the sut and the oracle with lurette.
 
 2) It generates a file named lurette.in which is included in the
-Makefile (which defines the name of the sut and the oracle).
+lurette Makefile.
 
 3) Then it calls make.
 
 "
 
 case $# in
-    2)
-############################
-
-	echo "... Generating the stub files: gen_stubs $1 $2"
+    [01])
+	echo "$Help"
+	exit 0
+	;;
+    *)
+	echo "... Generates the stub files (gen_stubs $1 $2)"
 	/home/jahier/lurette/interface/gen_stubs $1 $2
 
-############################
-	echo "... generates the lurette.in file (which is included in the Makefile) "
+
+	echo "... generates lurette.in file "
 	rm -f lurette.in
 	cat << EOF >> lurette.in
 
@@ -38,13 +39,8 @@ export ORACLE
 
 EOF
 
-############################
-	echo "... Making lurette: make"
-	
-	make dc # XXX pas satisfaisant !!!
-	;;
-    *)
-	echo "$Help"
-	exit 0
+	echo "... make"
+	shift 2
+	make $@
 	;;
 esac

source/env.ml

@@ -252,7 +252,9 @@ let (env_try: int -> int -> env_in ->
     let fte = Eval.eval_wtree_list input wtl cn_ll in
 
       (* Drawing n formula *)
-    let nl_fl_ll  = map2 (Wtree.choose_n_formula n fte) cn_ll wtl in
+    let nl_fl_ll  = 
+      map2 (Wtree.choose_n_formula (Solver.is_satisfiable) n fte) cn_ll wtl 
+    in
     let nll_fll_l = merge_lll nl_fl_ll in
 
       (* Drawing p solutions for each of the n formula *)

source/gen_stubs.ml

@@ -261,7 +261,7 @@ let (generate_stub_c: module_name -> string -> vn_ct list -> vn_ct list -> unit)
 ** that interfaces the sut and the oracle with Lurette.
 *)
   fun mod_name str vi vo ->  
-    let oc = open_out (str ^ "_stub.c") in
+    let oc = open_out (str ^ "_stub.c.new") in
     let put s = output_string oc s in
     let ov = List.rev vo in
     let (lo_v, lo_t) = List.hd ov in
@@ -363,7 +363,7 @@ let (generate_idl : module_name -> sut_or_oracle -> vn_ct list -> vn_ct list
 ** will interface C poc files with lurette. 
 *)
   fun mod_name str vi vo ->  
-    let oc = open_out (str ^ "_idl_stub.idl") in
+    let oc = open_out (str ^ "_idl_stub.idl.new") in
     let put s = output_string oc s in
     let ov = List.rev vo in
     let (lo_v, lo_t) = List.hd ov in
@@ -553,7 +553,7 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
 *)
   fun (sut_in, sut_out) -> 
 
-    let oc = open_out "lurette_stub.ml" in
+    let oc = open_out "lurette_stub.ml.new" in
     let put s = output_string oc s in
     let rec (format_string_list: string -> string list -> string) =
        (* 
@@ -824,7 +824,18 @@ let (replace_bool_representation: alias list -> alias list) =
   fun ta -> 
     ("_boolean", "boolean")::(List.remove_assoc "_boolean" ta)
   
-
+  
+let update_stub new_stub old_stub = 
+  (* Replace old_stub by new_stub iff they are different *)
+  if (Sys.file_exists old_stub) 
+  then
+    if ((Util.readfile old_stub) <> (Util.readfile new_stub))
+    then 
+      if ((Sys.command ("cp " ^ new_stub ^ " " ^ old_stub)) <> 0) 
+      then assert false
+      else print_string ("... " ^ old_stub ^ " successfully created.\n")
+    
+	
 let main2 sut oracle =
   let sut_h = (sut ^ ".h") in
   let oracle_h = (oracle ^ ".h") in
@@ -869,15 +880,27 @@ let main2 sut oracle =
      (*
      ** We need to call camlidl now in order to get the ocaml types of the sut.
      *)
-    if ((Sys.command ("echo \"camlidl -header sut_idl_stub.idl ...\" ;" ^
-		      " camlidl -header sut_idl_stub.idl ")) <> 0)  
-    then print_string (" Can't call camlidl on sut_idl_stub.idl; " ^
-		       "is camlidl in your path? Does sut_idl_stub.idl exist?\n\n") 
-    else print_string "     ... ok\n";
+    if (not (Sys.file_exists "sut_idl_stub.ml"))
+    then
+      if ((Sys.command ("echo \"... camlidl -header sut_idl_stub.idl \" ;" 
+			^         " camlidl -header sut_idl_stub.idl ")) <> 0)  
+      then print_string ("*** Can't call camlidl on sut_idl_stub.idl; " ^
+			 "is camlidl in your path? Does sut_idl_stub.idl exist?\n\n") 
+      else print_string "     ... ok\n";
+    
+    generate_lurette_stub_file (get_ml_type sut_vi_ord sut_vo_ord) ;
+    
 
-    generate_lurette_stub_file (get_ml_type sut_vi_ord sut_vo_ord)
+    (* Update the stubs iff they have changed to avoid unnecessary re-compilations *)
+    update_stub "sut_idl_stub.idl.new" "sut_idl_stub.idl" ;
+    update_stub "sut_stub.c.new" "sut_stub.c" ;
 
-	
+    update_stub "oracle_idl_stub.idl.new" "oracle_idl_stub.idl" ;
+    update_stub "oracle_stub.c.new" "oracle_stub.c" ;
+
+    update_stub "lurette_stub.ml.new" "lurette_stub.ml"
+
+ 
 (****************************************************************************)
 (****************************************************************************)
 

source/wtree.ml

@@ -12,7 +12,6 @@
 (****************************************************************************)
 
 open Formula 
-open Solver
 
 type wtree = wnode list
 and  wnode = | L of int * node list 
@@ -200,9 +199,9 @@ let rec (choose_a_formula: formula_table -> wtree -> node list
 
 type acc = ((node list * formula list) list * wtree)
 
-let rec (choose_n_formula_acc: int -> formula_table -> node list -> 
-	   acc -> acc) =
-  fun n ft nfl (ntl_fl_l0, wt0) -> 
+let rec (choose_n_formula_acc: (formula list -> bool) -> int -> 
+	   formula_table -> node list -> acc -> acc) =
+  fun is_satisfiable n ft nfl (ntl_fl_l0, wt0) -> 
     let _ = assert ((List.sort (-) nfl) = nfl) in
     if (wt0 = []) then 
       failwith "*** No more formula can be tried.\n"
@@ -212,23 +211,18 @@ let rec (choose_n_formula_acc: int -> formula_table -> node list ->
       else 
 	let (ntl, fl) = choose_a_formula ft wt0 nfl in
 	  if (is_satisfiable fl) then
-	    choose_n_formula_acc (n-1) ft nfl ((ntl, fl)::ntl_fl_l0, wt0)
+	    choose_n_formula_acc (is_satisfiable) (n-1) ft nfl ((ntl, fl)::ntl_fl_l0, wt0)
 	  else
 	    let wt = rm_elt ntl wt0 in
-	      choose_n_formula_acc n ft nfl (ntl_fl_l0, wt)
-
-let (choose_n_formula: int -> formula_table -> node list -> wtree -> 
-    (node list * formula list) list) =
-  fun n ft nfl wt -> 
-   (*
-    ** [choose_n_formula n ft nft wt] draws a list of formula (and the list of
-    ** their corresponding target nodes) in [wt] according to node weigths. 
-    ** [nfl] is the node list [wt] was build from; and [ft] is used to make 
-    ** the correspondance between the pair of nodes appearing in [wt] and 
-    ** formula.
-    *)
+	      choose_n_formula_acc (is_satisfiable) n ft nfl (ntl_fl_l0, wt)
+
+
+(* Exported *)
+let (choose_n_formula: (formula list -> bool) -> int -> formula_table -> 
+       node list -> wtree -> (node list * formula list) list) =
+  fun is_satisfiable n ft nfl wt -> 
     let _ = assert ((List.sort (-) nfl) = nfl) in
-    let (nl_fl_l, _) = choose_n_formula_acc n ft nfl ([], wt) in
+    let (nl_fl_l, _) = choose_n_formula_acc (is_satisfiable) n ft nfl ([], wt) in
       nl_fl_l
 
 (****************************************************************************)

source/wtree.mli

@@ -62,15 +62,15 @@ val build_wtree_table: wgraph -> wtree_table
 
 
 
-val choose_n_formula: int -> formula_table -> node list -> wtree -> 
-(** 
- [choose_n_formula n ft nft wt] draws a list of formula (and the
- list of their corresponding target nodes) in `wt' according to node
- weights.  `nfl' is the node list `wt' was build from; and `ft' is
- used to make the correspondence between the pair of nodes appearing
- in `wt' and formula.
+val choose_n_formula: (formula list -> bool) -> int -> formula_table -> 
+		 node list -> wtree -> (node list * formula list) list
+(** [choose_n_formula is_satisfiable n ft nft wt] draws a list of
+ formula (and the list of their corresponding target nodes) in `wt'
+ according to node weights.  `nfl' is the node list `wt' was build
+ from; and `ft' is used to make the correspondence between the pair
+ of nodes appearing in `wt' and formula. [is_satisfiable] states
+ whether a formula is satisfiable or not.
 *)
-    (node list * formula list) list
 
 
 val rm_elt: node list -> wtree -> wtree