Commit b3c5c602 authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.11 Wed, 26 Nov 2003 08:52:30 +0100 by jahier

Parent-Version:      1.10
Version-Log:

No more side effects are done via the Env_state module.

Project-Description: Lurette
parent 540ee1f9
This diff is collapsed.
......@@ -17,6 +17,9 @@ par les poids sont un peu contre-intuitives.
****** Documentation
* le retour au source lutin est sans doute cassé (à voir quand le nouveau compilo
lutin sera la)
* il faut rajouter dans lurette une option --step-inside --step-edges
--step-vertices (et renommer --draw-inside par --try-inside ??)
......
This diff is collapsed.
This diff is collapsed.
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 1 10)
(Parent-Version lurette 1 9)
(Project-Version lurette 1 11)
(Parent-Version lurette 1 10)
(Version-Log "
removing of Env_state module -- part 1
No more side effects are done via the Env_state module.
Now env_step and env_try are fully functionnal (no side-effects).
")
(New-Version-Log ""
)
(Checkin-Time "Thu, 20 Nov 2003 10:09:54 +0100")
(Checkin-Time "Wed, 26 Nov 2003 08:52:30 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -23,46 +23,46 @@ Now env_step and env_try are fully functionnal (no side-effects).
;; Sources files for luc_exe
(source/luc_exe.mli (lurette/b/31_ima_exe.ml 1.3 644))
(source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.40 644))
(source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.41 644))
(source/command_line_luc_exe.ml (lurette/b/33_command_li 1.20 644))
(source/command_line_luc_exe.mli (lurette/b/34_command_li 1.13 644))
(source/command_line_luc_exe.ml (lurette/b/33_command_li 1.21 644))
(source/command_line_luc_exe.mli (lurette/b/34_command_li 1.14 644))
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.14 644))
(source/lurette.ml (lurette/12_lurette.ml 1.78 644))
(source/lurette.ml (lurette/12_lurette.ml 1.79 644))
(source/command_line.ml (lurette/b/20_command_li 1.16 644))
(source/command_line.mli (lurette/b/21_command_li 1.13 644))
(source/command_line.ml (lurette/b/20_command_li 1.17 644))
(source/command_line.mli (lurette/b/21_command_li 1.14 644))
;; Sources files common to lurette and luc_exe
(source/graph.mli (lurette/13_graph.mli 1.12 644))
(source/graph.ml (lurette/14_graph.ml 1.10 644))
(source/lucky.mli (lurette/15_env.mli 1.21 644))
(source/lucky.ml (lurette/16_env.ml 1.35 644))
(source/lucky.mli (lurette/15_env.mli 1.22 644))
(source/lucky.ml (lurette/16_env.ml 1.36 644))
(source/util.ml (lurette/35_util.ml 1.58 644))
(source/util.ml (lurette/35_util.ml 1.59 644))
(source/formula_to_bdd.ml (lurette/g/34_formula_to 1.3 644))
(source/formula_to_bdd.mli (lurette/g/35_formula_to 1.4 644))
(source/formula_to_bdd.ml (lurette/g/34_formula_to 1.4 644))
(source/formula_to_bdd.mli (lurette/g/35_formula_to 1.5 644))
(source/fair_bddd.ml (lurette/g/38_fair_bddd. 1.4 644))
(source/fair_bddd.mli (lurette/g/39_fair_bddd. 1.4 644))
(source/bddd.ml (lurette/g/36_bddd.ml 1.5 644))
(source/bddd.mli (lurette/g/37_bddd.mli 1.5 644))
(source/fair_bddd.ml (lurette/g/38_fair_bddd. 1.5 644))
(source/fair_bddd.mli (lurette/g/39_fair_bddd. 1.5 644))
(source/bddd.ml (lurette/g/36_bddd.ml 1.6 644))
(source/bddd.mli (lurette/g/37_bddd.mli 1.6 644))
(source/solver.mli (lurette/38_solver.mli 1.20 644))
(source/solver.ml (lurette/39_solver.ml 1.58 644))
(source/solver.mli (lurette/38_solver.mli 1.21 644))
(source/solver.ml (lurette/39_solver.ml 1.59 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.11 644))
(source/polyhedron.mli (lurette/d/26_polyhedron 1.6 644))
(source/store.mli (lurette/b/26_rnumsolver 1.22 644))
(source/store.ml (lurette/b/27_rnumsolver 1.30 644))
(source/store.mli (lurette/b/26_rnumsolver 1.23 644))
(source/store.ml (lurette/b/27_rnumsolver 1.31 644))
(source/parse_luc.mli (lurette/40_parse_env. 1.17 644))
(source/parse_luc.ml (lurette/41_parse_env. 1.49 644))
(source/parse_luc.mli (lurette/40_parse_env. 1.18 644))
(source/parse_luc.ml (lurette/41_parse_env. 1.50 644))
(source/show_env.mli (lurette/42_show_env.m 1.11 644))
(source/show_env.ml (lurette/43_show_env.m 1.20 644))
......@@ -70,14 +70,14 @@ Now env_step and env_try are fully functionnal (no side-effects).
(source/print.mli (lurette/46_print.mli 1.14 644))
(source/print.ml (lurette/47_print.ml 1.25 644))
(source/env_state.mli (lurette/50_env_state. 1.36 644))
(source/env_state.ml (lurette/51_env_state. 1.51 644))
(source/env_state.mli (lurette/50_env_state. 1.37 644))
(source/env_state.ml (lurette/51_env_state. 1.52 644))
(source/run_aut.mli (lurette/b/46_automata.m 1.7 644))
(source/run_aut.ml (lurette/b/47_automata.m 1.17 644))
(source/run_aut.mli (lurette/b/46_automata.m 1.8 644))
(source/run_aut.ml (lurette/b/47_automata.m 1.18 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.9 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.22 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.10 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.23 644))
(source/gne.mli (lurette/b/36_gne.mli 1.6 644))
(source/gne.ml (lurette/b/37_gne.ml 1.6 644))
......@@ -147,16 +147,16 @@ Now env_step and env_try are fully functionnal (no side-effects).
(Makefile.common.source (lurette/e/33_Makefile.c 1.7 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.51 644))
(share/Makefile.lurette.in (lurette/b/38_Makefile.l 1.27 644))
(user-rules (lurette/c/14_myrules 1.48 644))
(user-rules (lurette/c/14_myrules 1.49 644))
(share/Makefile.test.in (lurette/c/25_user-rules 1.10 644))
(Makefile (lurette/d/13_Makefile 1.4 644))
(source/Makefile.lurettetop (lurette/d/14_Makefile.l 1.5 644))
(source/Makefile.gen_fake_lutin (lurette/d/17_Makefile.g 1.4 644))
(source/Makefile.show_luc (lurette/b/40_Makefile.s 1.12 644))
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.27 644))
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.28 644))
(source/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.8 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.25 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.26 644))
(source/Makefile (lurette/c/20_Makefile 1.26 644))
;; Documentation
......@@ -172,7 +172,7 @@ Now env_step and env_try are fully functionnal (no side-effects).
(ID_EN_VRAC (lurette/0_ID_EN_VRAC 1.1 644))
(INSTALL (lurette/f/26_INSTALL 1.2 744))
(TAGS (lurette/21_TAGS 1.6 644))
(TODO (lurette/d/22_TODO 1.29 644))
(TODO (lurette/d/22_TODO 1.30 644))
(share/lucky_init.csh.in (lurette/e/23_lucky_init 1.8 644))
(share/lucky_init.sh.in (lurette/e/24_lucky_init 1.11 644))
......@@ -180,11 +180,11 @@ Now env_step and env_try are fully functionnal (no side-effects).
(share/plot (lurette/e/35_plot 1.5 744))
(test/time-ossau.exp (lurette/b/48_time.exp 1.53 644))
(test/time-ossau.res (lurette/b/49_time.res 1.56 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.32 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.31 644))
(test/time-ossau.res (lurette/b/49_time.res 1.57 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.33 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.32 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.11 644))
(test/time-moucherotte.res (lurette/e/38_time-mouch 1.11 644))
(test/time-moucherotte.res (lurette/e/38_time-mouch 1.12 644))
;; Various files used for testing purposes
(test/cudd_gc_problem.luc (lurette/e/29_cudd_gc_pr 1.2 644))
......@@ -212,7 +212,7 @@ Now env_step and env_try are fully functionnal (no side-effects).
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.16 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.19 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.20 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.18 644))
(test/heater_int.lus (lurette/b/43_heater_int 1.1 644))
(test/heater_float.lus (lurette/b/44_heater_flo 1.2 644))
......@@ -284,8 +284,8 @@ Now env_step and env_try are fully functionnal (no side-effects).
;; xlurette
(ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.29 644))
(ihm/xlurette/xlurette.glade (lurette/c/13_xlurette.g 1.24 644))
(ihm/xlurette/xlurette_glade_interface.ml (lurette/c/15_xlurette_g 1.22 644))
(ihm/xlurette/xlurette.glade (lurette/c/13_xlurette.g 1.25 644))
(ihm/xlurette/xlurette_glade_interface.ml (lurette/c/15_xlurette_g 1.23 644))
(ihm/xlurette/makefile (lurette/c/16_makefile 1.17 644))
......@@ -471,12 +471,17 @@ Now env_step and env_try are fully functionnal (no side-effects).
;; Files added by populate at Fri, 14 Nov 2003 14:32:53 +0100,
;; to version 1.8(w), by jahier:
(source/var.ml (lurette/g/49_var.ml 1.1 644))
(source/var.ml (lurette/g/49_var.ml 1.2 644))
;; Files added by populate at Fri, 14 Nov 2003 14:32:55 +0100,
;; to version 1.8(w), by jahier:
(source/var.mli (lurette/g/50_var.mli 1.1 644))
(source/var.mli (lurette/g/50_var.mli 1.2 644))
;; Files added by populate at Wed, 26 Nov 2003 08:47:27 +0100,
;; to version 1.10(w), by jahier:
(source/thickness.ml (lurette/g/51_thickness. 1.1 644))
)
(Merge-Parents)
(New-Merge-Parents)
......@@ -66,6 +66,7 @@ SOURCES_OCAML = \
ifndef MLONLY
SOURCES_OCAML := \
$(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/thickness.ml \
$(LURETTE_PATH)/source/genlex.mli \
$(LURETTE_PATH)/source/genlex.ml \
$(LURETTE_PATH)/source/lexeme.mli \
......@@ -76,8 +77,6 @@ SOURCES_OCAML := \
$(LURETTE_PATH)/source/poly_draw.ml \
$(LURETTE_PATH)/source/prevar.mli \
$(LURETTE_PATH)/source/prevar.ml \
$(LURETTE_PATH)/source/command_line_luc_exe.mli \
$(LURETTE_PATH)/source/command_line_luc_exe.ml \
$(LURETTE_PATH)/source/value.mli \
$(LURETTE_PATH)/source/value.ml \
$(LURETTE_PATH)/source/var.mli \
......@@ -120,6 +119,8 @@ SOURCES_OCAML := \
$(LURETTE_PATH)/source/sim2chro.ml \
$(LURETTE_PATH)/source/lucky.mli \
$(LURETTE_PATH)/source/lucky.ml \
$(LURETTE_PATH)/source/command_line_luc_exe.mli \
$(LURETTE_PATH)/source/command_line_luc_exe.ml \
$(LURETTE_PATH)/source/luc_exe.mli \
$(LURETTE_PATH)/source/luc_exe.ml
endif
......
......@@ -34,6 +34,7 @@ SOURCES_C = ocaml2c.idl call_lurette_main.c
SOURCES = $(SOURCES_C) \
$(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/thickness.ml \
$(LURETTE_PATH)/source/genlex.mli \
$(LURETTE_PATH)/source/genlex.ml \
$(LURETTE_PATH)/source/lexeme.mli \
......
(*-----------------------------------------------------------------------
** Copyright (C) 2003 - Verimag.
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
......@@ -44,7 +44,7 @@ let string_of_sol_nb = string_of_float
type snt = (Bdd.t, sol_nb * sol_nb) Hashtbl.t
let snt_ref = ref (Hashtbl.create 1)
let snt_build = ref false
let (sol_number_snt : snt -> Bdd.t -> sol_nb * sol_nb) =
......@@ -78,6 +78,7 @@ let (clear_snt: unit -> unit) =
if Util.hashtbl_size Env_state.snt > 1000
then *)
Hashtbl.clear !snt_ref;
snt_build := false;
init_snt ()
let (sol_number_exists : Bdd.t -> snt -> bool) =
......@@ -173,9 +174,18 @@ and
(** [build_sol_nb_table bdd comb] build an internal table that
associates to each [bdd] its solution number. [comb] is a bdd made
of the the conjunctions of variables of [bdd] union the Boolean
variable to be generated (which migth not appear in [bdd]) ; it is
necessary because not all the variable to be generated appears
in the [bdd].
*)
let (build_sol_nb_table: var list -> Bdd.t -> Bdd.t -> unit) =
fun _ bdd comb ->
snt_build := true;
if
(sol_number_exists bdd !snt_ref)
then
......@@ -207,7 +217,8 @@ let (toss_up_one_var: Var.name -> Var.subst) =
if (ran < 0.5) then (var, B(true)) else (var, B(false))
let (toss_up_one_var_index: Var.env_in -> Env_state.lucky_state -> var_idx -> Var.subst option) =
let (toss_up_one_var_index: Var.env_in -> Env_state.t -> var_idx ->
Var.subst option) =
fun input state var_idx ->
(* if [var_idx] is a index that corresponds to a boolean variable,
this fonction performs a toss and returns a substitution for
......@@ -242,7 +253,7 @@ let (toss_up_one_var_index: Var.env_in -> Env_state.lucky_state -> var_idx -> Va
| _ -> None
let rec (draw_in_bdd_rec: Var.env_in -> Env_state.lucky_state -> Var.subst list * Store.t -> Bdd.t ->
let rec (draw_in_bdd_rec: Var.env_in -> Env_state.t -> Var.subst list * Store.t -> Bdd.t ->
Bdd.t -> Var.subst list * Store.t' * Store.p) =
fun input state (sl, store) bdd comb ->
(** Returns [sl] appended to a draw of all the boolean variables
......@@ -287,7 +298,7 @@ let rec (draw_in_bdd_rec: Var.env_in -> Env_state.lucky_state -> Var.subst list
draw_in_bdd_rec_ineq input state ineq (sl, store) bdd comb snt
and (draw_in_bdd_rec_bool: Var.env_in -> Env_state.lucky_state -> var -> Var.subst list * Store.t ->
and (draw_in_bdd_rec_bool: Var.env_in -> Env_state.t -> var -> Var.subst list * Store.t ->
Bdd.t -> Bdd.t -> snt -> Var.subst list * Store.t' * Store.p) =
fun input state var (sl, store) bdd comb snt ->
let bddvar = Bdd.topvar bdd in
......@@ -350,7 +361,7 @@ and (draw_in_bdd_rec_bool: Var.env_in -> Env_state.lucky_state -> var -> Var.sub
draw_in_bdd_rec input state (sl1, store) bdd1 new_comb
with
No_numeric_solution ->
if state.verbose then
if state.d.verbose then
print_string "\n..................BACKTRACK!\n";
if not (eq_sol_nb sol_nb2 zero_sol)
then draw_in_bdd_rec input state (sl2, store) bdd2 new_comb
......@@ -365,7 +376,7 @@ and (draw_in_bdd_rec_bool: Var.env_in -> Env_state.lucky_state -> var -> Var.sub
flush stdout;
assert false
and (draw_in_bdd_rec_ineq: Var.env_in -> Env_state.lucky_state -> Constraint.ineq ->
and (draw_in_bdd_rec_ineq: Var.env_in -> Env_state.t -> Constraint.ineq ->
Var.subst list * Store.t -> Bdd.t ->
Bdd.t -> snt -> Var.subst list * Store.t' * Store.p) =
fun input state cstr (sl, store) bdd comb snt ->
......@@ -424,7 +435,7 @@ and (draw_in_bdd_rec_ineq: Var.env_in -> Env_state.lucky_state -> Constraint.ine
flush stdout;
assert false
and (draw_in_bdd_rec_eq: Var.env_in -> Env_state.lucky_state -> Ne.t -> Var.subst list * Store.t ->
and (draw_in_bdd_rec_eq: Var.env_in -> Env_state.t -> Ne.t -> Var.subst list * Store.t ->
Bdd.t -> Bdd.t -> snt -> Var.subst list * Store.t' * Store.p) =
fun input state ne (sl, store) bdd comb snt ->
(*
......@@ -534,7 +545,8 @@ and (draw_in_bdd_rec_eq: Var.env_in -> Env_state.lucky_state -> Ne.t -> Var.subs
(* exported *)
let rec (draw_in_bdd: Var.env_in -> Env_state.lucky_state -> var list -> Bdd.t -> Bdd.t ->
let rec (draw_in_bdd: Var.env_in -> Env_state.t -> var list -> Bdd.t -> Bdd.t ->
Var.subst list * Store.t' * Store.p) =
fun input state store bdd comb ->
draw_in_bdd_rec input state ([], Store.create store) bdd comb
fun input state num_vars_to_gen bdd comb ->
build_sol_nb_table num_vars_to_gen bdd comb;
draw_in_bdd_rec input state ([], Store.create num_vars_to_gen) bdd comb
(*-----------------------------------------------------------------------
** Copyright (C) 2003 - Verimag.
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
......@@ -8,27 +8,19 @@
** Main author: jahier@imag.fr
*)
(** Bdd Drawer. *)
(** Machinery to perform a draw in a bdd (hence the third d ...) *)
type sol_nb = float
val build_sol_nb_table : Exp.var list -> Bdd.t -> Bdd.t -> unit
(**
[build_sol_nb_table bdd comb] build a table that associate each to
a [bdd] its solution number in its 2 branches. [comb] is a bdd made
of the the conjunctions of variables of [bdd] union the Boolean
variable to be generated (which migth not appear in [bdd]).
*)
val draw_in_bdd : Var.env_in -> Env_state.lucky_state -> Exp.var list -> Bdd.t ->
Bdd.t -> Var.subst list * Store.t' * Store.p
(**
[draw_in_bdd varl bdd comb] returns a draw of the Boolean variables
as well as a range base and a polyhedron based representation of
numeric constraints.
ZZZ [build_sol_nb_table bdd comb] ougth to be called before.
val draw_in_bdd : Var.env_in -> Env_state.t -> Exp.var list -> Bdd.t ->
Bdd.t -> Var.subst list * Store.t' * Store.p
(** [draw_in_bdd inputs state vars bdd comb] returns a draw of the
Boolean variables as well as a range based and a polyhedron based
representation of numeric constraints.
*)
val sol_number : Bdd.t -> sol_nb * sol_nb
......
......@@ -15,7 +15,7 @@ type optionsT = {
mutable display_sim2chro : bool ;
(* mutable cudd_heap_init : int ; *)
mutable user_seed : int ;
mutable verbose : bool ;
mutable verb : bool ;
mutable show_step : bool ;
mutable help : bool ;
mutable output : string ;
......
......@@ -19,7 +19,7 @@ type optionsT = {
mutable display_sim2chro : bool ;
(* mutable cudd_heap_init : int ; *)
mutable user_seed : int ;
mutable verbose : bool ;
mutable verb : bool ;
mutable show_step : bool ;
mutable help : bool ;
mutable output : string ;
......
(*-----------------------------------------------------------------------
** Copyright (C) 2002 - Verimag.
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
......@@ -18,7 +18,7 @@ type optionsT = {
mutable draw_mode : Lucky.step_mode ;
mutable compute_volume : bool;
mutable user_seed : int ;
mutable verbose : bool
mutable verb : bool
}
type cmd_line_optionT =
......
(*-----------------------------------------------------------------------
** Copyright (C) 2002 - Verimag.
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
......@@ -20,7 +20,7 @@ type optionsT = {
mutable draw_mode : Lucky.step_mode ;
mutable compute_volume : bool;
mutable user_seed : int ;
mutable verbose : bool
mutable verb : bool
}
val usage : string
......
This diff is collapsed.
......@@ -8,102 +8,59 @@
** Author: jahier@imag.fr
*)
(** Defines the environment state data type. All side effects occur
through that state.
(** Defines the environment state data type.
Such state contains two parts :
- a static part, that is set after the lucky files parsing,
and which never changes after
- a dynamic part, which changes after each step.
*)
open Parse_luc
(** The state of a lucky automaton is made of its current nodes
and its memories. *)
type lucky_state = {
memory : Var.subst list;
current_nodes : Parse_luc.node list list ;
verbose : bool
type node_info = {
file_name : string;
node_type : node_type;
source : source_info
}
val read_env_state : Parse_luc.automata list -> Parse_luc.node list list
(** [read_env_state files_l] updates the global variable
[env_state] using the automata defined in the list [files_l].
*)
(** Returns the names and types of input, output, and local vars of
an environment automata.
*)
val vars : string -> Exp.var list * Exp.var list * Exp.var list
(** Sets the var names and types of an env automata. *)
val set_vars : string -> Exp.var list * Exp.var list * Exp.var list -> unit
(** Returns all the input variables, unsorted. *)
val in_env_unsorted : unit -> Exp.var list
(** Returns all the output variables, unsorted. *)
val out_env_unsorted : unit -> Exp.var list
(** Returns all the local variables, unsorted. *)
val loc_env_unsorted : unit -> Exp.var list
(** Pre variables values. *)
val pre_var_names: unit -> Var.name list
(** Sets (internal) names of pre variables. *)
val set_pre_var_names : Var.name list -> unit
val add_pre_var_names : Var.name -> unit
(** Returns the output var names and types. *)
val output_vars : unit -> Exp.var list
(** Sets the output var names and types. *)
val set_output_vars : Exp.var list -> unit
(** Returns the file name where a node is defined.
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 nodes in the (virtual) automata product). Indeed, some
variables that should be drawn do not 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.
(**
There are some redundancies, but it is on purpose. The goal is to
precompute here and once for all what will be needed at runtime.
*)
val file_name : Parse_luc.node -> string
(** Sets the file name where a node is defined *)
val set_file_name : Parse_luc.node -> string -> unit
(** Returns nodes information related to the source lutin file: file
name, line and col numberfile name where a node is defined. *)
val source_info : Parse_luc.node -> Parse_luc.source_info
(** Sets the source information. *)
val set_source_info : Parse_luc.node -> Parse_luc.source_info -> unit
type static_state_fields = {
bool_vars_to_gen : Exp.var list list ;
num_vars_to_gen : Exp.var list list ;
in_vars : Exp.var list;
out_vars : Exp.var list;
loc_vars : Exp.var list;
memories_names : string list ;
output_var_names : Var.name list list ;
node : (node, node_info) Hashtbl.t;
graph : (node, arc_info) Graph.t
}
(** Returns the graph containing the automata nodes and arcs. *)
val graph : unit -> (Parse_luc.node, Parse_luc.arc_info) Graph.t
type dynamic_state_fields = {
memory : Var.subst list;
current_nodes : node list list ;
verbose : bool
}
(** Sets the current environment graph. *)
val set_graph : (Parse_luc.node, Parse_luc.arc_info) Graph.t -> unit
type t = {
d : dynamic_state_fields ;
s : static_state_fields
}
val read_env_state : Parse_luc.automata list -> t
(** Build the initial state from the list of parsed automata *)
(**/**)
val is_node_transient : Parse_luc.node -> t -> bool
(** outputs various statistic about the size of env_state tables *)
val dump_env_state_stat : out_channel -> unit
(* val set_verbose : bool -> unit *)
(* val verbose : unit -> bool *)
val set_transient_nodes : Parse_luc.node list -> unit
val add_transient_nodes : Parse_luc.node -> unit
val is_node_transient : Parse_luc.node -> bool
val clear_all : unit -> unit
(* val dump_env_state_stat : out_channel -> unit *)
(*-----------------------------------------------------------------------
** Copyright (C) 2003 - Verimag.
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
......@@ -41,6 +41,7 @@ let string_of_sol_nb = string_of_float
relative to which bdd points to it.
*)
type snt = (Bdd.t * Store.t, float * float) Hashtbl.t
let snt_build = ref false
(* let print_snt snt = *)
(* Hashtbl.iter *)
......@@ -102,6 +103,7 @@ let (init_snt : unit -> unit) =
let (clear_snt: unit -> unit) =
fun _ ->
Hashtbl.clear !snt_ref;
snt_build := false;
init_snt ()
let (sol_number_exists : Bdd.t -> Store.t -> snt -> bool) =
......@@ -298,9 +300,15 @@ and
(mult_sol_nb n0 factor)
(* exported *)
(**
[build_sol_nb_table bdd comb] build a table that associate each to
a [bdd] its solution number in its 2 branches. [comb] is a bdd made
of the the conjunctions of variables of [bdd] union the Boolean
variable to be generated (which migth not appear in [bdd]).
*)
let (build_sol_nb_table: var list -> Bdd.t -> Bdd.t -> unit) =
fun num_vars bdd comb ->
snt_build := true;
let store0 = Store.create num_vars in
if
(sol_number_exists bdd store0 !snt_ref)
......@@ -337,7 +345,7 @@ let (toss_up_one_var: Var.name -> Var.subst) =
if (ran < 0.5) then (var, B(true)) else (var, B(false))
let (toss_up_one_var_index: Var.env_in -> Env_state.lucky_state -> var_idx ->
let (toss_up_one_var_index: Var.env_in -> Env_state.t -> var_idx ->
Var.subst option) =
fun input state var_idx ->
(* if [var_idx] is a index that corresponds to a boolean variable,
......@@ -373,7 +381,7 @@ let (toss_up_one_var_index: Var.env_in -> Env_state.lucky_state -> var_idx ->
| _ -> None
let rec (draw_in_bdd_rec: Var.env_in -> Env_state.lucky_state ->
let rec (draw_in_bdd_rec: Var.env_in -> Env_state.t ->
Var.subst list * Store.t -> Bdd.t -> Bdd.t ->
Var.subst list * Store.t' * Store.p) =
fun input state (sl, store) bdd comb ->
......@@ -419,7 +427,7 @@ let rec (draw_in_bdd_rec: Var.env_in -> Env_state.lucky_state ->
draw_in_bdd_rec_ineq input state ineq (sl, store) bdd comb snt
and (draw_in_bdd_rec_bool: Var.env_in -> Env_state.lucky_state -> var ->
and (draw_in_bdd_rec_bool: Var.env_in -> Env_state.t -> var ->
Var.subst list * Store.t -> Bdd.t -> Bdd.t -> snt ->
Var.subst list * Store.t' * Store.p) =
fun input state var (sl, store) bdd comb snt ->
......@@ -483,7 +491,7 @@ and (draw_in_bdd_rec_bool: Var.env_in -> Env_state.lucky_state -> var ->
draw_in_bdd_rec input state (sl1, store) bdd1 new_comb
with
No_numeric_solution ->
if state.verbose then
if state.d<