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 da43be79 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.70 Fri, 19 Jul 2002 17:31:37 +0200 by jahier

Parent-Version:      0.69
Version-Log:

ima_exe.ml:
lurette.ml:
env_state.ml:
  Factoring out code into  two new functions, clear_step and clear_all.

env_state.ml:
   Do not use to 2 ranges of indexes (one for atomic formula that depends on
pre,
   one if it is not) but maintain a list a unused indexes instead.

Project-Description: Lurette
parent 135fe2d5
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.30 Fri, 19 Jul 2002 10:19:59 +0200 jahier $
# $Id: OcamlMakefile 1.31 Fri, 19 Jul 2002 17:31:37 +0200 jahier $
#
###########################################################################
# Set these variables to the names of the sources to be processed and
......@@ -630,6 +630,7 @@ release:
cp $(LURETTE_PATH)/source/util.ml $(LURETTE_PATH)/source/gen_stubs.ml \
$(LURETTE_PATH)/source/show_ima.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/control.mli $(LURETTE_PATH)/source/control.ml \
$(LURETTE_PATH)/source/ima_exe.mli $(LURETTE_PATH)/source/ima_exe.ml \
$(LURETTE_PATH)/source/command_line_ima_exe.mli $(LURETTE_PATH)/source/command_line_ima_exe.ml \
$(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 69)
(Parent-Version lurette 0 68)
(Version-Log "
wtree.ml,mli: (deleted)
automa.ml,mli: (new files)
control.ml,mli: (new files)
Replace the [wtree] module by an [automata] module, that basically
does the same job, but in a different way. Namely, it no more uses
the [wtree] DS to use [graph]s instead. Indeed, the product of
wtrees introduces some problems, in particular to ensure its
correctness wrt to the automata run concurrently. Now, everything a
dead-simple wrt product: we simply perform a quasi-classical automata
product (well, at least, much closer from a classical product, cf
paper).
The way loop counters are handled has also changed. Now, counters are
handled via expressions of a simple arithmetic language that
basically lets one initialise a variable to an exact or a random
value (uniform or normal draw) and decrement it. Arcs are now
labelled by a formula plus 2 expressions of that mini-language (no
more weigth nor cpt_init stuff). The 1st expression is evaluated
during the draw, basically performs any operations on counters, and
returns a positive int that is used as the formula weigth. The second
expression (a kind of post-condition) is evaluated if its arc is the
one that has been elected to perform the step.
At several locations long lines (< 80) are reindented.
parse_env.ml:
In the ima format, IfThenElseExpr becomes IfThenElseNum.
Also, parse list more cleanly.
graph.ml,mli:
Add a function that test whether a transition is in the graph.
Do not sort list of transitions anymore (what was the point?).
Also do not sort nodes in any way.
show_env_env.ml,mli:
Abstract away nodes and arcs data types (so that I can display
Automata graphs). rename generate_env_graph into ima_to_dot.
lurette.ml:
(Project-Version lurette 0 70)
(Parent-Version lurette 0 69)
(Version-Log "
ima_exe.ml:
Fix a bug where bbd table were filled by asserted non regression expr.
lurette.ml:
Fix a bug where incorrect data was sent to sim2chro (ie, the output of the
previous step instead of the ones of the current step.
env_state.ml:
Factoring out code into two new functions, clear_step and clear_all.
env_state.ml:
solver.ml:
gne.ml:
Fix a performance bug where I was storing formula indexes even if
they were depending on inputs or pre, which is stupid as they generally
won't be used again. In order to fix that, I introduced new
atomic_formula <-> indexes table to stote the ones that do not depend
on inputs apart. It was also necassery to propogate the <<depend on pre>>
flag inside Gne.gn_expr (which i renamed Gne.t BTW).
Do not use to 2 ranges of indexes (one for atomic formula that depends on pre,
one if it is not) but maintain a list a unused indexes instead.
")
(New-Version-Log "")
(Checkin-Time "Fri, 19 Jul 2002 10:19:59 +0200")
(Checkin-Time "Fri, 19 Jul 2002 17:31:37 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -82,14 +29,14 @@ gne.ml:
;; Sources files for ima_exe
(source/ima_exe.mli (lurette/b/31_ima_exe.ml 1.1 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.13 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.14 644))
(source/command_line_ima_exe.ml (lurette/b/33_command_li 1.4 644))
(source/command_line_ima_exe.mli (lurette/b/34_command_li 1.3 644))
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.12 644))
(source/lurette.ml (lurette/12_lurette.ml 1.40 644))
(source/lurette.ml (lurette/12_lurette.ml 1.41 644))
(source/command_line.ml (lurette/b/20_command_li 1.7 644))
(source/command_line.mli (lurette/b/21_command_li 1.6 644))
......@@ -103,8 +50,8 @@ gne.ml:
(source/util.ml (lurette/35_util.ml 1.21 644))
(source/solver.mli (lurette/38_solver.mli 1.12 644))
(source/solver.ml (lurette/39_solver.ml 1.23 644))
(source/solver.mli (lurette/38_solver.mli 1.13 644))
(source/solver.ml (lurette/39_solver.ml 1.24 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.3 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.6 644))
......@@ -124,8 +71,8 @@ gne.ml:
(source/eval.mli (lurette/48_eval.mli 1.10 644))
(source/eval.ml (lurette/49_eval.ml 1.13 644))
(source/env_state.mli (lurette/50_env_state. 1.20 644))
(source/env_state.ml (lurette/51_env_state. 1.23 644))
(source/env_state.mli (lurette/50_env_state. 1.21 644))
(source/env_state.ml (lurette/51_env_state. 1.24 644))
(source/automata.mli (lurette/b/46_automata.m 1.1 644))
(source/automata.ml (lurette/b/47_automata.m 1.1 644))
......@@ -142,7 +89,7 @@ gne.ml:
(make_lurette (lurette/27_make_luret 1.13 744))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.30 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.31 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.4 644))
(bin/Makefile.show_ima (lurette/b/40_Makefile.s 1.4 644))
......@@ -165,7 +112,7 @@ gne.ml:
(TAGS (lurette/21_TAGS 1.6 644))
(test/time.exp (lurette/b/48_time.exp 1.1 644))
(test/time.res (lurette/b/49_time.res 1.1 644))
(test/time.res (lurette/b/49_time.res 1.2 644))
;; Various files used for testing purposes
(test/usager.env (lurette/b/14_usager.env 1.8 644))
......
......@@ -59,10 +59,12 @@ type env_stateT = {
latter, the former needs to be cleared at each step. *)
mutable index_cpt: int;
mutable global_index_cpt: int;
(** Counters used to manage the indexes above. *)
bdd_manager: Manager.t;
(** List of currently unused bdd var indexes *)
mutable free_index_list: int list;
mutable bdd_manager: Manager.t;
(** bdd engine internal state. *)
bdd_tbl_global: (formula, Bdd.t) Hashtbl.t;
......@@ -104,12 +106,6 @@ type env_stateT = {
(** Ditto for local vars. *)
}
(** Cudd var index are represented by C int; we use the first half to
store atomic_formula that depends on pre or input, and the second
half for the one that do not depend on them. *)
let half_max_c_int = 1000
(* 32768 *)
let (env_state:env_stateT) = {
var_names = Hashtbl.create 0;
......@@ -135,7 +131,7 @@ let (env_state:env_stateT) = {
global_atomic_formula_to_index = Hashtbl.create 0;
index_to_global_atomic_formula = Hashtbl.create 0;
index_cpt = 0 ;
global_index_cpt = half_max_c_int
free_index_list = []
}
......@@ -316,19 +312,21 @@ let (clear_bdd_global: unit -> unit) =
Hashtbl.clear env_state.bdd_tbl_global
(****************************************************************************)
let (index_cpt: unit -> int) =
fun _ ->
env_state.index_cpt
let (set_index_cpt: int -> unit) =
fun i ->
env_state.index_cpt <- i
let (global_index_cpt: unit -> int) =
fun _ ->
env_state.global_index_cpt
let (set_global_index_cpt: int -> unit) =
fun i ->
env_state.global_index_cpt <- i
let (get_an_index : unit -> int) =
fun _ ->
match env_state.free_index_list with
[] ->
env_state.index_cpt <- env_state.index_cpt + 1;
env_state.index_cpt
| i::tail ->
env_state.free_index_list <- tail;
i
let (free_indexes : int list -> unit) =
fun il ->
env_state.free_index_list <- append il env_state.free_index_list
(* exported *)
......@@ -340,23 +338,24 @@ let (atomic_formula_to_index : atomic_formula -> bool -> int) =
(
try Hashtbl.find env_state.atomic_formula_to_index f
with Not_found ->
set_index_cpt (env_state.index_cpt + 1);
Hashtbl.add env_state.atomic_formula_to_index f env_state.index_cpt;
Hashtbl.add env_state.index_to_atomic_formula env_state.index_cpt f;
assert (env_state.index_cpt < half_max_c_int);
env_state.index_cpt
let index = get_an_index () in
Hashtbl.add env_state.atomic_formula_to_index f index;
Hashtbl.add env_state.index_to_atomic_formula index f;
(* output_string stderr ( *)
(* (atomic_formula_to_string f) ^ "\t<-> " ^ *)
(* (string_of_int index) ^ "\n" ) ; *)
(* flush stderr; *)
index
)
else
(
try Hashtbl.find env_state.global_atomic_formula_to_index f
with Not_found ->
set_global_index_cpt (env_state.global_index_cpt + 1);
Hashtbl.add env_state.global_atomic_formula_to_index
f env_state.global_index_cpt;
Hashtbl.add env_state.index_to_global_atomic_formula
env_state.global_index_cpt f;
env_state.global_index_cpt
with Not_found ->
let index = get_an_index () in
Hashtbl.add env_state.global_atomic_formula_to_index f index;
Hashtbl.add env_state.index_to_global_atomic_formula index f;
index
)
......@@ -364,23 +363,32 @@ let (atomic_formula_to_index : atomic_formula -> bool -> int) =
let (index_to_atomic_formula : int -> atomic_formula) =
fun i ->
try Hashtbl.find env_state.index_to_global_atomic_formula i
with Not_found ->
with Not_found ->
Hashtbl.find env_state.index_to_atomic_formula i
(* exported *)
let (clear_atomic_formula_index : unit -> unit) =
fun _ ->
Hashtbl.clear env_state.index_to_atomic_formula ;
Hashtbl.clear env_state.atomic_formula_to_index ;
set_index_cpt 0
let index_to_free =
Hashtbl.fold
(fun index _ acc -> index::acc)
env_state.index_to_atomic_formula
[];
in
Hashtbl.clear env_state.index_to_atomic_formula ;
Hashtbl.clear env_state.atomic_formula_to_index ;
free_indexes index_to_free
(* exported *)
let (clear_global_atomic_formula_index : unit -> unit) =
fun _ ->
Hashtbl.clear env_state.index_to_global_atomic_formula ;
Hashtbl.clear env_state.global_atomic_formula_to_index ;
set_global_index_cpt half_max_c_int
env_state.index_cpt <- 0;
env_state.free_index_list <- []
(****************************************************************************)
let (output_var_names: unit -> vnt list) =
......@@ -499,7 +507,6 @@ let (read_env_state_one_file : string -> node) =
(init_node + node_nb)
(****************************************************************************)
(****************************************************************************)
(* Exported *)
let (read_env_state : string list list -> unit) =
......@@ -510,6 +517,33 @@ let (read_env_state : string list list -> unit) =
set_current_nodes nodes
(****************************************************************************)
(* Exported *)
let (clear_step : unit -> unit) =
fun _ ->
clear_bdd () ;
clear_atomic_formula_index () ;
(* if (t mod 100) = 0
then
if Util.hashtbl_size Env_state.snt > 1000
then *)
clear_sol_numbers () ;
set_sol_number
(Bdd.dtrue (bdd_manager ())) (Util.one_sol, Util.zero_sol);
set_sol_number
(Bdd.dfalse (bdd_manager ())) (Util.zero_sol, Util.one_sol)
(* Exported *)
let (clear_all : unit -> unit) =
fun _ ->
clear_bdd_global () ;
clear_global_atomic_formula_index () ;
clear_ima ();
clear_step ();
Manager.free env_state.bdd_manager ;
env_state.bdd_manager <- Manager.make 10 10 0 0 0
(****************************************************************************)
(* Exported *)
......@@ -549,6 +583,16 @@ let (dump_env_state_stat : unit -> unit) =
(string_of_int (hashtbl_size env_state.index_to_global_atomic_formula)));
dump "\n";
dump ("*** cpt_index:" ^
(string_of_int env_state.index_cpt));
dump "\n";
dump ("*** free_index_list: " ^
(fold_left (fun acc i -> acc ^ ", " ^ (string_of_int i)) "" env_state.free_index_list));
dump "\n";
dump ("*** bdd_tbl_global size:" ^
(string_of_int (hashtbl_size env_state.bdd_tbl_global)));
dump "\n";
......
......@@ -27,7 +27,6 @@ val read_env_state : string list list -> unit
should not share any variables with ["foo1"] and ["foo2"] then.
*)
(** Returns the names and types of input, output, and local vars of
an environment automata.
*)
......@@ -36,9 +35,6 @@ val var_names : string -> vnt list * vnt list * vnt list
(** Sets the var names and types of an env automata. *)
val set_var_names : string -> vnt list * vnt list * vnt list -> unit
(** Clear the current ima in order to dynamically load another one *)
val clear_ima : unit -> unit
(** Returns all the input variables, unsorted. *)
val in_env_unsorted : unit -> vnt list
......@@ -133,15 +129,13 @@ val set_sol_number : Bdd.t -> Util.sol_nb * Util.sol_nb -> unit
(** Tests whether sol numbers of a given bdd is available. *)
val sol_number_exists : Bdd.t -> bool
(** Clean up the sol number table. *)
val clear_sol_numbers: unit -> unit
(** Transforming a formula into a bdd is expensive; this is why we
store the result of this transformation a (internal)
table. Formula that does not depend on pre nor input vars are
stored in a different table that is not cleared at each new step
(cf [bdd_global] and [set_bdd_global] versus [bdd] and [set_bdd]).
Ditto for the atomic_formula <-> bdd index tables.
*)
(** Returns the bdd of a formula if it is available in [env_state],
......@@ -152,10 +146,6 @@ val bdd : formula -> Bdd.t
internal table. *)
val set_bdd : formula -> Bdd.t -> unit
(** Clean up the formula to bdd table. *)
val clear_bdd: unit -> unit
val clear_bdd_global: unit -> unit
(** Cf [bdd], but for formula that do not depend on pre nor
input vars. *)
val bdd_global : formula -> Bdd.t
......@@ -171,10 +161,18 @@ val atomic_formula_to_index : atomic_formula -> bool -> int
(** Returns the atomic formula of an index. *)
val index_to_atomic_formula : int -> atomic_formula
(** Clean up index_to_atomic_formula and atomic_formula_to_index tables. *)
val clear_atomic_formula_index : unit -> unit
val clear_global_atomic_formula_index : unit -> unit
(** Clean-up all the [env_state] fields that migth have been filled
by (non-regressios) asssertions.
*)
val clear_all : unit -> unit
(** Clean-up the [env_state] fields that contain information that
depends on input or pre. Indeed, this information is very likely
to change (especially wrt floats!) at each step, therefore we do
not keep that information to avoid memory problems.
*)
val clear_step : unit -> unit
(** Returns the control expression associated to a label *)
val ctrl_expr : string -> Control.expr
......
......@@ -53,7 +53,7 @@ let rec (parse_ima_files : rif_stream -> string list list -> string list list) =
let (replace_env_dynamically: rif_stream -> unit) =
fun stream ->
let ima_files = parse_ima_files stream [] in
Env_state.clear_ima ();
Env_state.clear_all ();
output_string stderr "loading ";
List.iter (fun x -> output_string stderr (x ^ " ")) (List.flatten ima_files);
output_string stderr " ...\n ";
......@@ -291,13 +291,7 @@ and
fun _ ->
(* Clean up tables as non-reg assert stuff migth have filled them *)
let _ =
Env_state.clear_bdd () ;
Env_state.clear_bdd_global () ;
Env_state.clear_atomic_formula_index () ;
Env_state.clear_global_atomic_formula_index () ;
Env_state.clear_ima ()
in
let _ = Env_state.clear_all () in
(* Initialisation of `Env_state.env_state' *)
let env_llist = (get_env_from_args 1 []) in
......@@ -351,7 +345,9 @@ and
in
Env.env_step nll call out loc ;
Env.update_pre
(Env_state.input ()) (Env_state.output ()) (Env_state.local ()) ;
(Env_state.input ())
(Env_state.output ())
(Env_state.local ()) ;
write_rif_output (Env_state.out_env_unsorted ()) out ;
else ();
......@@ -368,7 +364,8 @@ and
if options.verbose then
(
List.iter
(fun n -> output_string stderr ("current nodes:" ^ (string_of_int n) ^ "\n "))
(fun n ->
output_string stderr ("current nodes:" ^ (string_of_int n) ^ "\n "))
nl;
Control.print_state (Env_state.ctrl_state ());
flush stderr
......@@ -402,19 +399,22 @@ and
in
Env.env_step nll call out loc ;
Env.update_pre (Env_state.input ()) (Env_state.output ()) (Env_state.local ()) ;
(* Inputs and pre vars may change at ech new step,
therefore we need to clear those tables. *)
Env_state.clear_bdd () ;
Env_state.clear_atomic_formula_index () ;
Env.update_pre
(Env_state.input ())
(Env_state.output ())
(Env_state.local ()) ;
write_rif_output (Env_state.out_env_unsorted ()) out ;
if options.show_automata then (
Show_env.ima_to_dot (flatten (Env_state.current_nodes ()))
[] ("automata" ^ (string_of_int (Hashtbl.hash Sys.argv)))
(Env_state.graph ())
);
(* Clean-up cached info that depend on pre or inputs *)
Env_state.clear_step () ;
main_loop (t+1)
;;
......
......@@ -122,15 +122,6 @@ and
| 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 *)
(* 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 *)
| Output ->
let str = (Sys.argv.(n+1)) in
options.output <- str ;
......@@ -179,11 +170,8 @@ and
(main2 : int -> int -> int -> 'a) =
fun s n p ->
(* Clean up tables as non-reg assert stuff migth have filled them *)
let _ =
Env_state.clear_bdd () ;
Env_state.clear_bdd_global () ;
Env_state.clear_ima ()
in
let _ = Env_state.clear_all () in
(* Initialisation of `Env_state.env_state' *)
let env_llist = (get_env_from_args 4 []) in
let () = Env_state.read_env_state env_llist in
......@@ -377,25 +365,10 @@ and
(* Updates pre vars *)
Env.update_pre new_sut_output input loc ;
(* Inputs and pre vars may change at ech new step,
therefore we need to clear those tables. *)
Env_state.clear_bdd () ;
Env_state.clear_atomic_formula_index () ;
(* Migth be needed if reordering occurs in bdds. *)
(* XXX What should be the trade-off ?? *)
(* if (t mod 100) = 0 *)
(* then *)
(* if Util.hashtbl_size Env_state.snt > 1000 *)
(* then *)
Env_state.clear_sol_numbers () ;
Env_state.set_sol_number
(Bdd.dtrue (Env_state.bdd_manager ())) (Util.one_sol, Util.zero_sol);
Env_state.set_sol_number
(Bdd.dfalse (Env_state.bdd_manager ())) (Util.zero_sol, Util.one_sol);
(* Clean-up cached info that depend on pre or inputs *)
Env_state.clear_step ();
(* Decides whether to loop once more *)
(* Decides whether to loop once more *)
if ((str = "") && (s > t))
then main_loop (t+1) s n p rif new_sut_output
else
......
......@@ -17,18 +17,6 @@ open Rnumsolver
(****************************************************************************)
let (formula_list_to_conj: formula list -> formula) =
fun fl ->
(** Transform a (non-empty) list of formula to the conjunction
made of those formula.
*)
match fl with
[] -> assert false
| f::[] -> f
| f1::f2::tail ->
List.fold_left (fun x y -> And(x, y)) (And(f1, f2)) tail
let (lookup: env_in -> subst list -> var_name -> var_value option) =
fun input pre vn ->
try Some(Hashtbl.find input vn)
......@@ -40,8 +28,6 @@ let (lookup: env_in -> subst list -> var_name -> var_value option) =
type comp = SupZero | SupEqZero | EqZero | NeqZero
let rec (formula_to_bdd : env_in -> formula -> Bdd.t * bool) =
fun input f ->
(** Returns the bdd of [f] where input and pre variables
......
......@@ -27,8 +27,5 @@ val solve_formula : env_in -> int -> formula -> formula -> vnt list ->
*)
(** Raised during the draw. *)
(* exception No_numeric_solution *)
Command being timed: "./lurette 10000 1 1 tram.env usager.env porte.env passerelle.env -seed 1015403953 -ns2c --no-oracle"
User time (seconds): 10.54
System time (seconds): 0.14
Percent of CPU this job got: 80%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:13.21
User time (seconds): 9.51
System time (seconds): 0.12
Percent of CPU this job got: 78%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:12.33
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
......@@ -10,7 +10,7 @@
Maximum resident set size (kbytes): 0
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 556
Minor (reclaiming a frame) page faults: 1677
Minor (reclaiming a frame) page faults: 2560
Voluntary context switches: 0
Involuntary context switches: 0
Swaps: 0
......@@ -23,10 +23,10 @@
Exit status: 0
Command being timed: "./lurette 10 100 100 tram.env usager.env porte.env passerelle.env -seed 1015403953 -ns2c --no-oracle"
User time (seconds): 15.28
System time (seconds): 0.04
Percent of CPU this job got: 84%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:18.20
User time (seconds): 15.80
System time (seconds): 0.10
Percent of CPU this job got: 83%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:19.15
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
......@@ -34,7 +34,7 @@
Maximum resident set size (kbytes): 0
Average resident set size (kbytes): 0