Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit d35c3931 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.27 Tue, 12 Feb 2002 09:02:01 +0100 by jahier

Parent-Version:      0.26
Version-Log:

Add an option --sith-seed that lets one set the value of the seed
used to initialize the random engine.

Project-Description: Lurette
parent 8e54c847
......@@ -8,8 +8,8 @@
(source/util.ml 4367 1013445149 35_util.ml 1.7)
(source/wtree.ml 9842 1013445149 b/1_wtree.ml 1.6)
(source/solver.ml 11461 1013445149 39_solver.ml 1.7)
(source/command_line.ml 3650 1012999707 b/20_command_li 1.1)
(source/lurette.ml 9596 1013445149 12_lurette.ml 1.16)
(source/command_line.ml 3846 1013500921 b/20_command_li 1.2)
(source/lurette.ml 10158 1013500921 12_lurette.ml 1.17)
(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)
......@@ -29,7 +29,7 @@
(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)
(source/command_line.mli 1154 1012999707 b/21_command_li 1.1)
(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/env_state.mli 3228 1013445149 50_env_state. 1.6)
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 26)
(Parent-Version lurette 0 25)
(Project-Version lurette 0 27)
(Parent-Version lurette 0 26)
(Version-Log "
Re-arrange the code so that lurette_stub.ml is not called by all the
modules of lurette to avoid that everything is recompiled each time a
new sut is used. To do that, lurette nows only manipulates list of
substitutuions instead of tuples (as only lurette_stub knows the size
of the tuples).
Also fix two bugs along the way:
o wtree.ml: Random.int n draw between 0 inclusive and n *exclusive* !
o wtree.ml: in wtree_product, make sure that I do not unsort list of nodes
o solver.ml: in draw_in_bdd, I was tossing up the top var of the formula
instead of tossing up the one of the support
Plus a few cosmetic change:
show_env.ml:
lurette.ml:
prints the previous nodes in green environment.ps
lurette.ml:
rename arcs_inputs_loc into nll_inputs_loc.
Add an option --sith-seed that lets one set the value of the seed
used to initialize the random engine.
")
(New-Version-Log "")
(Checkin-Time "Mon, 11 Feb 2002 17:32:29 +0100")
(Checkin-Time "Tue, 12 Feb 2002 09:02:01 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -42,7 +20,7 @@ lurette.ml:
;; Sources files
(source/lurette.mli (lurette/11_lurette.ml 1.10 644))
(source/lurette.ml (lurette/12_lurette.ml 1.16 644))
(source/lurette.ml (lurette/12_lurette.ml 1.17 644))
(source/graph.mli (lurette/13_graph.mli 1.4 644))
(source/graph.ml (lurette/14_graph.ml 1.3 644))
......@@ -76,8 +54,8 @@ lurette.ml:
(source/wtree.mli (lurette/b/0_wtree.mli 1.4 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.6 644))
(source/command_line.ml (lurette/b/20_command_li 1.1 644))
(source/command_line.mli (lurette/b/21_command_li 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.14 644))
......
......@@ -13,14 +13,15 @@ type optionsT = {
mutable step_by_step : bool ;
mutable display_local_var : bool ;
mutable display_sim2chro : bool ;
mutable cudd_heap_init : int
mutable cudd_heap_init : int ;
mutable user_seed : int
}
type cmd_line_optionT =
Step | NoStep
| DisplayLocalVar | NoDisplayLocalVar
| Sim2chro | NoSim2chro
| CuddHeapInit
| CuddHeapInit | Seed
(* Names of the command line options to override the defaults. *)
let (string_to_option: (string * cmd_line_optionT) list) = [
......@@ -28,6 +29,9 @@ let (string_to_option: (string * cmd_line_optionT) list) = [
("--step", Step);
("-s", Step);
("--with-seed", Seed);
("-seed", Seed);
("--display-local-var", DisplayLocalVar);
("--do-not-display-local-var", NoDisplayLocalVar);
("-nlv", NoDisplayLocalVar);
......@@ -48,8 +52,9 @@ let (option_to_usage: cmd_line_optionT -> string) =
| NoDisplayLocalVar -> "Do not display environment local variables in sim2chro.\n"
| Sim2chro -> "Call sim2chro when lurette resumes (Default).\n"
| NoSim2chro -> "Do not call sim2chro when lurette resumes.\n"
| CuddHeapInit -> "Sets a magic number (related to the gc) that is used by mldd \n\t\t\tfor initializing Dd (Default is 20).\n"
| 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"
let (group_common_options: (string * cmd_line_optionT) list ->
(string * cmd_line_optionT) list) =
fun list ->
......
......@@ -17,7 +17,8 @@ type optionsT = {
mutable step_by_step : bool ;
mutable display_local_var : bool ;
mutable display_sim2chro : bool ;
mutable cudd_heap_init : int
mutable cudd_heap_init : int ;
mutable user_seed : int
}
val usage : string
......@@ -33,8 +34,9 @@ type cmd_line_optionT =
Step | NoStep
| DisplayLocalVar | NoDisplayLocalVar
| Sim2chro | NoSim2chro
| CuddHeapInit
| CuddHeapInit | Seed
val string_to_option: (string * cmd_line_optionT) list
(** XXX *)
(** Mapping from options string (e.g., "--no-step") to the cmd_line_optionT
type. *)
......@@ -22,7 +22,8 @@ let (options:Command_line.optionsT) = {
step_by_step = false ;
display_local_var = true ;
display_sim2chro = true ;
cudd_heap_init = 20
cudd_heap_init = 20 ;
user_seed = 0
}
......@@ -94,6 +95,8 @@ let (read_var_names: string -> vnt list * vnt list) =
let arg_nb = (Array.length Sys.argv)
external random_seed: unit -> int = "sys_random_seed";;
let rec (main : unit -> 'a) =
fun _ ->
try
......@@ -133,10 +136,18 @@ and
| CuddHeapInit ->
let str = (Sys.argv.(n+1)) in
cmd_line_string_to_int str
options.cudd_heap_init <- cmd_line_string_to_int str
("*** Error when calling lurette: an " ^
"integer is expected after the " ^
"option --init-cudd-heap\n") ;
n+2
| Seed ->
let str = (Sys.argv.(n+1)) in
options.user_seed <- cmd_line_string_to_int str
("*** Error when calling lurette: an " ^
"integer is expected after the " ^
"option --with-seed\n") ;
n+2
end
with Not_found -> n
and
......@@ -194,8 +205,16 @@ and
env_state.pre_form
in
(* Initialize the random engine *)
Random.self_init ();
let seed =
if (options.user_seed = 0)
then (random_seed ())
else options.user_seed
in
Random.init seed ;
print_string "The random engine was initialized with the seed ";
print_int seed;
print_string "\n ";
env_state.local <- local1 ;
(* Initialisation of the sut and the oracle *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment