lurette 0.31 Tue, 12 Feb 2002 14:10:11 +0100 by jahier

Parent-Version:      0.30
Version-Log:

Various fixes so that lurette can be build from scratch.

Project-Description: Lurette

.lurette.prcs_aux

@@ -17,16 +17,18 @@
 (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)
 (test/passerelle.env 862 1012914629 b/17_passerelle 1.1)
+(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
 (source/parse_env.mli 939 1008328137 40_parse_env. 1.3)
 (ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
+(source/sim2chro.mli 1395 1013519411 b/23_sim2chro.m 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 32217 1013517738 24_generate_l 1.15)
+(source/gen_stubs.ml 32194 1013519411 24_generate_l 1.16)
 (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)
+(source/sim2chro.ml 2833 1013519411 b/24_sim2chro.m 1.1)
 (doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
 (doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
 (source/formula.mli 1870 1013445149 44_formula.ml 1.4)
@@ -35,7 +37,6 @@
 (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)
@@ -46,6 +47,7 @@
 (test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
 (interface/Makefile 197 1008255910 25_Makefile 1.6)
 (source/show_env.mli 929 1013445149 42_show_env.m 1.3)
+(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
 (Makefile 1703 1013445149 18_Makefile 1.17)
 (test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
 (source/print.mli 417 1013445149 46_print.mli 1.4)

interface/sut_idl_stub.ml

-(* 
-** This file was manually written for unit testing of get_ml_type
-** (through an assertion). 
-*)
-
-
-external sut_init : unit -> unit
-	= "camlidl_sut_idl_stub_sut_init"
-
-external sut_step : int -> bool -> bool * float
-	= "camlidl_sut_idl_stub_sut_step"
-
-external sut_try : int -> bool -> bool * float
-	= "camlidl_sut_idl_stub_sut_try"
-

lurette.prj

 ;; -*- Prcs -*-
 (Created-By-Prcs-Version 1 3 3)
 (Project-Description "Lurette")
-(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.
-
+(Project-Version lurette 0 31)
+(Parent-Version lurette 0 30)
+(Version-Log "
+Various fixes so that lurette can be build from scratch.
 ")
 (New-Version-Log "")
-(Checkin-Time "Tue, 12 Feb 2002 13:42:18 +0100")
+(Checkin-Time "Tue, 12 Feb 2002 14:10:11 +0100")
 (Checkin-Login jahier)
 (Populate-Ignore ())
 (Project-Keywords)
@@ -69,10 +53,13 @@ env.ml:
   (source/wtree.mli (lurette/b/0_wtree.mli 1.5 644))
   (source/wtree.ml (lurette/b/1_wtree.ml 1.7 644))
 
+  (source/sim2chro.mli (lurette/b/23_sim2chro.m 1.1 644))
+  (source/sim2chro.ml (lurette/b/24_sim2chro.m 1.1 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.15 644))
+  (source/gen_stubs.ml (lurette/24_generate_l 1.16 644))
 
 ;; Make files
   (OcamlMakefile (lurette/17_OcamlMakef 1.14 644))
@@ -100,8 +87,6 @@ env.ml:
 
 ;; Various files used for testing purposes
 
-  (interface/sut_idl_stub.ml (lurette/34_sut_idl_st 1.1 644))
-
   (test/usager.env (lurette/b/14_usager.env 1.2 644))
   (test/tram.env (lurette/b/15_tram.env 1.1 644))
   (test/porte.env (lurette/b/16_porte.env 1.1 644))
@@ -113,6 +98,7 @@ env.ml:
   (test/vrai_tram.lus (lurette/b/6_vrai_tram. 1.1 644))
   (test/vrai_tram.h (lurette/b/7_vrai_tram. 1.2 644))
   (test/vrai_tram.c (lurette/b/8_vrai_tram. 1.2 644))
+  (test/tram_simple.h (lurette/b/25_tram_simpl 1.1 644))
 
   (test/lurette.rif.exp (lurette/b/22_lurette.ri 1.2 644))
 

source/gen_stubs.ml

@@ -827,14 +827,13 @@ let (replace_bool_representation: alias list -> alias list) =
   
 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 
+    not ((Sys.file_exists old_stub)) ||
+    ((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
@@ -877,9 +876,14 @@ let main2 sut oracle =
     generate_stub_c oracle_m "oracle" oracle_vi_ord oracle_vo ; 
     generate_idl oracle_m "oracle" oracle_vi_ord oracle_vo ;
 
-     (*
-     ** We need to call camlidl now in order to get the ocaml types of the sut.
-     *)
+    (* 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" ;
+
+    (* We need to call camlidl now in order to get the ocaml types of the sut. *)
     if (not (Sys.file_exists "sut_idl_stub.ml"))
     then
       if ((Sys.command ("echo \"... camlidl -header sut_idl_stub.idl \" ;" 
@@ -889,16 +893,7 @@ let main2 sut oracle =
       else print_string "     ... ok\n";
     
     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"
+    update_stub "lurette_stub.ml.new" "lurette_stub.ml" 
 
  
 (****************************************************************************)

source/sim2chro.ml

+(*-----------------------------------------------------------------------
+** Copyright (C) 2001 - Verimag.
+** This file may only be copied under the terms of the GNU Library General
+** Public License 
+**-----------------------------------------------------------------------
+**
+** File: sim2chro.ml
+** Main author: jahier@imag.fr
+*)
+
+open Formula
+open List
+open Env_state
+    
+type ssl = (string * string) list
+
+let (put_var_decl: string -> ssl -> ssl -> out_channel -> bool -> unit) =
+  fun title sut_input_var_name_and_type_list sut_output_var_name_and_type_list 
+      rif display_local_var -> 
+    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 = Env_state.loc_env_unsorted () in
+    let local_var_name_and_type_list = 
+      Util.sort_list_string_pair local_var_name_and_type_list_unsorted 
+    in
+
+      put ("#program \" " ^ title ^ " \"\n"); 
+      
+      put "#@inputs\n";
+      List.iter put_vntl sut_input_var_name_and_type_list;
+
+      put "@#\n#@outputs\n";
+      List.iter put_vntl 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 -> env_out -> env_in -> env_loc 
+       -> bool -> unit) =
+  fun rif t input output local display_local_var -> 
+    let put s = output_string rif s in
+      put "#step ";
+      put (string_of_int t);
+      put "\n";
+      
+      List.iter 
+	(fun (_, e) -> (print_atomic_expr e rif; put " ")) 
+	(Util.sort_list_string_pair input);
+      put "#outs ";
+      List.iter 
+	(fun (_, e) -> (print_atomic_expr e rif; put " ")) 
+	(Util.sort_list_string_pair output);
+
+      if display_local_var then
+	List.iter 
+	  (fun (_, e) -> (print_atomic_expr e rif; put " ")) 
+	  (Util.sort_list_string_pair local);
+     
+      put "\n"
+
+
+let call_sim2chro _ =
+  let color_option = 
+    (* options for sim2chro to display local vars in green *) 
+    let loc_var_names = loc_env_unsorted () 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 cmd = (" sim2chro -ecran " ^ color_option ^ 
+	     " -in lurette.rif  > /dev/null &")
+  in
+  let _ = print_string cmd ; print_string "\n" in
+  let _ = Sys.command cmd in
+    ()
+

source/sim2chro.mli

+(*-----------------------------------------------------------------------
+** Copyright (C) 2001 - Verimag.
+** This file may only be copied under the terms of the GNU Library General
+** Public License 
+**-----------------------------------------------------------------------
+**
+** File: sim2chro.mli
+** Main author: jahier@imag.fr
+*)
+
+(** Defines functions to display variables history with sim2chro *)
+
+open Formula
+open Env_state
+    
+(** [put_var_decl title in_vn out_vn rif display_loca_var] puts the
+  variable names and type in (from [env_state]) in the file
+  associated to [rif]. [display_local_var] is a boolean telling
+  whether local vars should be displayed in the chronogram.  [in_vn]
+  and [out_vn] are the list of sut inputs and outputs variable names
+  and types. [title] is a string that is used to set a title to the
+  lurette window.
+*)
+val put_var_decl: string -> (string * string) list -> (string * string) list 
+  -> out_channel -> bool -> unit
+
+(**
+  [put_current_step_values rif t input output local display_local_var]
+  puts the values computed at times [t]. [input], [output], and [local] 
+  contain the value to be displayed. [display_local_var] tells whether 
+  to display local vars or not.
+*)
+val put_current_step_values: out_channel -> int -> env_out -> env_in -> env_loc 
+       -> bool -> unit
+
+(** 
+  Calls (fork) sim2chro.
+*)
+val call_sim2chro: unit -> unit
+
+

test/tram_simple.h

+/********
+* ec2c version 0.4-beta
+* c header file generated for node : tram_simple 
+* to be used with : tram_simple.c 
+********/
+/*-------- Predefined types ---------*/
+#ifndef _tram_simple_EC2C_PREDEF_TYPES
+#define _tram_simple_EC2C_PREDEF_TYPES
+typedef int _boolean;
+typedef int _integer;
+typedef char* _string;
+typedef double _real;
+typedef double _double;
+typedef float _float;
+#define _false 0
+#define _true 1
+#endif
+/*--------- Pragmas ----------------*/
+//MODULE: tram_simple 4 8
+//IN: _boolean demande_porte
+//IN: _boolean en_station
+//IN: _boolean porte_ouverte
+//IN: _boolean attention_depart
+//OUT: _boolean fermer_porte
+//OUT: _boolean ouvrir_porte
+//OUT: _boolean porte_ok
+//OUT: _boolean attention_depart_a_retentit
+//OUT: _boolean depart
+//OUT: _boolean accepter_demande
+//OUT: _boolean porte_demandee
+//OUT: _boolean depart_imminent
+#ifndef _tram_simple_EC2C_SRC_FILE
+/*--------Context type -------------*/
+struct tram_simple_ctx;
+/*--------Context allocation --------*/
+extern struct tram_simple_ctx* tram_simple_new_ctx(void* client_data);
+/*--------Context copy -------------*/
+extern void tram_simple_copy_ctx(struct tram_simple_ctx* dest, struct 
+tram_simple_ctx* src);
+/*-------- Reset procedure -----------*/
+extern void tram_simple_reset(struct tram_simple_ctx* ctx);
+/*-------- Step procedure -----------*/
+extern void tram_simple_step(struct tram_simple_ctx* ctx);
+/*-------- Input procedures -------------*/
+extern void tram_simple_I_demande_porte(struct tram_simple_ctx*, _boolean);
+extern void tram_simple_I_en_station(struct tram_simple_ctx*, _boolean);
+extern void tram_simple_I_porte_ouverte(struct tram_simple_ctx*, _boolean);
+extern void tram_simple_I_attention_depart(struct tram_simple_ctx*, _boolean);
+#endif