lurette 0.53 Fri, 29 Mar 2002 11:04:44 +0100 by jahier

Parent-Version:      0.52
Version-Log:

Add a --verbose and a --help options to the command line.

Also clean up a little bit comments in various places.

Project-Description: Lurette

OcamlMakefile

@@ -5,7 +5,7 @@
 #                            For updates see:
 #             http://miss.wu-wien.ac.at/~mottl/ocaml_sources
 #
-#        $Id: OcamlMakefile 1.24 Thu, 28 Mar 2002 18:10:42 +0100 jahier $
+#        $Id: OcamlMakefile 1.25 Fri, 29 Mar 2002 11:04:44 +0100 jahier $
 #
 ###########################################################################
 
@@ -500,7 +500,7 @@ runbug:
 try:
 	../make_lurette ControleurPorte vrai_tram; \
 #	./lurette 10 2 2 tram.env usager.env porte.env passerelle.env | sim2chro -ecran
-	./lurette 10 2 2 tram.env usager.env porte.env passerelle.env 
+	./lurette 10 2 2 tram.env usager.env porte.env passerelle.env
 
 yvan:
 	$(LURETTE_DIR)/make_lurette heater Heater_vrai; \

lurette.prj

 ;; -*- Prcs -*-
 (Created-By-Prcs-Version 1 3 3)
 (Project-Description "Lurette")
-(Project-Version lurette 0 52)
-(Parent-Version lurette 0 51)
+(Project-Version lurette 0 53)
+(Parent-Version lurette 0 52)
 (Version-Log "
-Remove the necessity to provide an oracle when the user does 
-not have any assertion to check. To do that, I parse the sut 
-file and automatically generates a fake oracle that answers always 
-true.
+Add a --verbose and a --help options to the command line.
+
+Also clean up a little bit comments in various places.
 ")
 (New-Version-Log "")
-(Checkin-Time "Thu, 28 Mar 2002 18:10:42 +0100")
+(Checkin-Time "Fri, 29 Mar 2002 11:04:44 +0100")
 (Checkin-Login jahier)
 (Populate-Ignore ())
 (Project-Keywords)
@@ -29,17 +28,17 @@ true.
 
 ;; Sources files for lurette only
   (source/lurette.mli (lurette/11_lurette.ml 1.12 644))
-  (source/lurette.ml (lurette/12_lurette.ml 1.30 644))
+  (source/lurette.ml (lurette/12_lurette.ml 1.31 644))
 
-  (source/command_line.ml (lurette/b/20_command_li 1.4 644))
-  (source/command_line.mli (lurette/b/21_command_li 1.4 644))
+  (source/command_line.ml (lurette/b/20_command_li 1.5 644))
+  (source/command_line.mli (lurette/b/21_command_li 1.5 644))
 
 ;; Sources files common to lurette and ima_exe
   (source/graph.mli (lurette/13_graph.mli 1.6 644))
   (source/graph.ml (lurette/14_graph.ml 1.5 644))
 
-  (source/env.mli (lurette/15_env.mli 1.10 644))
-  (source/env.ml (lurette/16_env.ml 1.21 644))
+  (source/env.mli (lurette/15_env.mli 1.11 644))
+  (source/env.ml (lurette/16_env.ml 1.22 644))
 
   (source/util.ml (lurette/35_util.ml 1.16 644))
 
@@ -64,7 +63,7 @@ true.
   (source/eval.mli (lurette/48_eval.mli 1.9 644))
   (source/eval.ml (lurette/49_eval.ml 1.12 644))
 
-  (source/env_state.mli (lurette/50_env_state. 1.13 644))
+  (source/env_state.mli (lurette/50_env_state. 1.14 644))
   (source/env_state.ml (lurette/51_env_state. 1.15 644))
 
   (source/wtree.mli (lurette/b/0_wtree.mli 1.7 644))
@@ -76,7 +75,7 @@ true.
   (source/gen_stubs.ml (lurette/24_generate_l 1.21 644))
 
 ;; Make files
-  (OcamlMakefile (lurette/17_OcamlMakef 1.24 644))
+  (OcamlMakefile (lurette/17_OcamlMakef 1.25 644))
   (Makefile (lurette/18_Makefile 1.25 644))
   (interface/Makefile (lurette/25_Makefile 1.6 644))
   (test/Makefile_ima_exe (lurette/b/35_Makefile_i 1.2 644))

source/command_line.ml

@@ -15,15 +15,17 @@ type optionsT = {
   mutable display_sim2chro : bool ;
 (*   mutable cudd_heap_init : int ; *)
   mutable user_seed : int ;
+  mutable verbose : bool ;
+  mutable help : bool ;
   mutable oracle : bool
 }
 
 type cmd_line_optionT = 
-    Step | NoStep 
+    Step | NoStep | Help
   | DisplayLocalVar | NoDisplayLocalVar 
   | Sim2chro | NoSim2chro 
 (*   | CuddHeapInit  *)
-  | Seed | NoOracle
+  | Seed | NoOracle | Verbose
 
 (* Names of the command line options to override the defaults. *)
 let (string_to_option: (string * cmd_line_optionT) list) = [
@@ -34,6 +36,12 @@ let (string_to_option: (string * cmd_line_optionT) list) = [
   ("--with-seed", Seed);
   ("-seed", Seed);
 
+  ("-v", Verbose);
+  ("--verbose", Verbose);
+
+  ("-h", Help);
+  ("--help", Help);
+
   ("--no-oracle", NoOracle);
 
   ("--display-local-var", DisplayLocalVar);
@@ -59,6 +67,8 @@ let (option_to_usage: cmd_line_optionT -> string) =
 (*       | CuddHeapInit -> "Set a magic number (related to the gc) that is used by mldd \n\t\t\tfor initializing Dd (Default is 20).\n" *)
       | Seed ->  "Set the value of the seed the random engine is initialized with (0 lets the system draw a seed).\n"
       | NoOracle -> "Do not need to specify an oracle.\n "
+      | Verbose -> "Set on a wordier mode.\n"
+      | Help -> "Print this message.\n"
 
 let (group_common_options: (string * cmd_line_optionT) list -> 
        (string * cmd_line_optionT) list) =

source/command_line.mli

@@ -19,6 +19,8 @@ type optionsT = {
   mutable display_sim2chro : bool ;
 (*   mutable cudd_heap_init : int ; *)
   mutable user_seed : int ;
+  mutable verbose : bool ;
+  mutable help : bool ;
   mutable oracle : bool
 }
 
@@ -32,11 +34,11 @@ val cmd_line_string_to_int : string -> string -> int
 *)
 
 type cmd_line_optionT = 
-    Step | NoStep 
+    Step | NoStep | Help
   | DisplayLocalVar | NoDisplayLocalVar 
   | Sim2chro | NoSim2chro 
 (*   | CuddHeapInit  *)
-  | Seed | NoOracle
+  | Seed | NoOracle | Verbose
 
 
 val string_to_option: (string * cmd_line_optionT) list

source/env.ml

@@ -45,11 +45,11 @@ let _ = assert ( (add_missing_pre ["_pre3toto"; "_pre2titi"; "_pre2toto"])
   =  ["_pre2titi"; "_pre1titi"; "_pre3toto"; "_pre2toto"; "_pre1toto"] )
 
 
+(** Returns the initial node of the automata defined in
+  [file]. Also updates the various fields of [env_state] with the
+  content of [file].  *)
 let (read_env_state_one_file : string -> node) =
   fun file -> 
-    (** Returns the initial node of the automata defined in
-      [file]. Also updates the various fields of [env_state] with the
-      content of [file].  *)
     let 
       (* Parses the content of [file]. *)
       Parse_env.Automata(init_node, list_in, list_out, list_loc, 

source/env.mli

@@ -62,7 +62,9 @@ val env_step : node list list -> env_out -> env_loc -> unit
   
 
 val update_pre: env_in -> env_out -> env_loc -> unit 
-  (** Updates the values of pre variables (updating [env_state.pre]).  *)
+  (** [update_pre input output local] Updates the values of pre
+    variables (updating [env_state.pre]) with [input], [output], and
+    [local].  *)
 
 
 

source/env_state.mli

@@ -23,33 +23,34 @@ type env_stateT = {
     given module by module. *)
 
   mutable pre_var_names: var_name list;
+  (** internal names of pre variables. *)
 
   mutable output_var_names: vnt list;
   (** Output var names and types. *)
 
   mutable node_to_file_name: (int, string) Hashtbl.t;
-  (** Associates each node with its origin file name (i.e., the
-    [.aut] it comes from).
+  (** Associates each node in the environment automata with its 
+    origin file name (i.e., the [.env] file it comes from).
 
     We need that information to be able to retrieve the list of
     variables that ougth to be generated from a list of nodes (the
-    current node in the virtual automata product). Indeed, some
+    current nodes in the (virtual) automata product). Indeed, some
     variables that should be drawn do no necessarily appear in
     formula; and once the whole bdd has been traversed for the draw,
     we need to be able to know what variables are still to be drawn.
   *)
 
   mutable atomic_formula_to_index: ((atomic_formula, int) Hashtbl.t); 
-  (** This indexing of (output and local) variable names is needed
+  (** This indexing of (output and local) variable names is used
     for constructing bdds in the boolean solver (for which variables
-    are [int], not [string]s.  *)
+    are [int], not [string]s).  *)
   mutable index_to_atomic_formula: ((int, atomic_formula) Hashtbl.t); 
   (** Ditto in the other way. *)
   mutable index_cpt: int;
-  (** Counter used to create the index *)
+  (** Counter used to create the index above. *)
 
   mutable bdd_manager: Manager.t;
-  (** bdd state *)
+  (** bdd engine internal state. *)
 
   mutable bdd_tbl_global: (formula, Bdd.t) Hashtbl.t;
   mutable bdd_tbl: (formula, Bdd.t) Hashtbl.t;
@@ -66,8 +67,8 @@ type env_stateT = {
     relative to which bdd points to it. *)
   
   mutable current_nodes : node list list;
-  (** List of the automata node. Nodes belonging to automata that
-    should be run in parallel are grouped in the same list. *)
+  (** List of the automata current nodes (there are as many nodes as 
+    there are environment run in parallel). *)
   
   mutable graph : (node, arc_info) Graph.t ;
   (** The automata is stored in a Graph.t *)
@@ -76,9 +77,9 @@ type env_stateT = {
   (** Mapping from nodes to [wtree] (see the doc of the [Wtree] module). *)
 
   mutable pre: subst list;
-  (** Used to store the values of variables ``under a pre''. *)
+  (** Stores the values of pre variables. *)
   mutable input : env_in ;  
-  (** Used to store the values of input vars. *)
+  (** Ditto for input vars. *)
   mutable output: env_out ; 
   (** Ditto for output vars. *)
   mutable local : env_loc   

source/lurette.ml

@@ -18,24 +18,23 @@ open Command_line
 
 (*------------------------------------------------------------------------*)
 
-
-
 let (options:Command_line.optionsT) = {
   step_by_step = false ;
   display_local_var = true ;
   display_sim2chro = true ;
-(*   cudd_heap_init = 21 ; *)
   user_seed = 0 ;
+  verbose = false ;
+  help = false ;
   oracle = true
 }
 
 
+(** [check_var_decl_consistency out_env in_sut out_sut] checks the
+  consistency of variable declarations made in the environment and the
+  SUT. It raises an exception if the declarations are inconsistent.
+*)
 let (check_var_decl_consistency : (vn * string) list -> (vn * string) list -> unit) =
   fun in_sut out_sut ->
-    (** [check_var_decl_consistency out_env in_sut out_sut] checks the
-       consistency of variable declarations made in the environment and the
-       SUT. It raises an exception if the declarations are inconsistent.
-    *)
     let in_env_unsorted = Env_state.in_env_unsorted () in
     let out_env_unsorted = Env_state.out_env_unsorted () in
     let in_env = Util.sort_list_string_pair in_env_unsorted in
@@ -119,6 +118,8 @@ and
 	    | NoSim2chro  -> options.display_sim2chro <- false ; (n+1)
 
 	    | NoOracle  -> options.oracle <- false ; (n+1)
+	    | Verbose  -> options.verbose <- true ; (n+1)
+	    | Help  -> options.help <- true ; (n+1)
 		
 (* 	    | CuddHeapInit -> *)
 (* 		let str = (Sys.argv.(n+1)) in *)
@@ -137,15 +138,15 @@ and
       end
     with Not_found -> n
 and
-  (get_env_from_args: int -> string list list -> string list list) =
-  fun n file_ll -> 
-    (** Returns the environment file names given at top-level into a
-      list of list.  E.g., if the call [lurette 10 2 3 env1 x env2 x
-      env3 env4] is done, then [get_env_from_args 10 []] (where 10 is
-      the arg nb) returns [[["env1"; "env2"; "env3"]; ["env4"]]].
+  (** Returns the environment file names given at top-level into a
+    list of list.  E.g., if the call [lurette 10 2 3 env1 x env2 x
+    env3 env4] is done, then [get_env_from_args 10 []] (where 10 is
+    the arg nb) returns [[["env1"; "env2"; "env3"]; ["env4"]]].
 
-      Also set the lurette command line options if any.  
+    Also set the lurette command line options if any.  
     *)
+  (get_env_from_args: int -> string list list -> string list list) =
+  fun n file_ll -> 
     if (n = arg_nb) then file_ll
     else
       let m = get_lurette_options n in
@@ -237,7 +238,8 @@ and
       Hashtbl.add env_state.snt 
 	(Bdd.dfalse env_state.bdd_manager) (Util.zero_sol, Util.one_sol);
 
-      main_loop 1 s n p rif (Hashtbl.create 0) ;
+      if not (options.help) 
+      then main_loop 1 s n p rif (Hashtbl.create 0) ;
 
       flush stdout;
       flush rif;
@@ -246,7 +248,10 @@ and
 and
   main_loop t s n p rif sut_output = 
 
-(*   let _ = print_string ("\n--- step " ^ (string_of_int t) ^ ":\n"); flush stdout in  *)
+  let _ = 
+    if options.verbose
+    then print_string ("\n--- step " ^ (string_of_int t) ^ ":\n"); flush stdout 
+  in  
 
 (* Generates `n*p' inputs from the environment *)
   let (nll_inputs_loc: (node list list * env_out * env_loc) list)