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

lurette 0.61 Fri, 03 May 2002 12:08:34 +0200 by jahier

Parent-Version:      0.60
Version-Log:

Add support for handling loops. This is based on the use of dynamic
weigths. The idea is to compute the dynamic weigths before the trees
are constructed.

Add a --show-aut option for ima_exe.

Also, Add the command lise args hashed to the end of the name of the dot file
that is used to visualize the ima file.

Project-Description: Lurette
parent b425173e
......@@ -2,56 +2,56 @@
;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3)
(test/usager.env 523 1019479246 b/14_usager.env 1.7)
(source/command_line_ima_exe.mli 989 1016127950 b/34_command_li 1.1)
(source/command_line_ima_exe.mli 1045 1020420514 b/34_command_li 1.2)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 12846 1020068208 51_env_state. 1.17)
(source/env_state.ml 13132 1020420514 51_env_state. 1.18)
(source/graph.ml 1819 1016011748 14_graph.ml 1.5)
(bin/Makefile.ima_exe 1926 1020068208 b/41_Makefile.i 1.1)
(source/util.ml 11635 1017837703 35_util.ml 1.17)
(source/wtree.ml 8580 1020068208 b/1_wtree.ml 1.10)
(bin/Makefile.ima_exe 1926 1020420514 b/41_Makefile.i 1.2)
(source/util.ml 12274 1020420514 35_util.ml 1.18)
(source/wtree.ml 11388 1020420514 b/1_wtree.ml 1.11)
(source/solver.ml 24560 1017837703 39_solver.ml 1.21)
(test/test_gen_stubs.h 1818 1020068208 b/45_test_gen_s 1.1)
(source/command_line.ml 4388 1019207707 b/20_command_li 1.7)
(source/lurette.ml 11553 1020068208 12_lurette.ml 1.35)
(source/lurette.ml 11711 1020420514 12_lurette.ml 1.36)
(source/solver.mli 1135 1016803757 38_solver.mli 1.10)
(source/env.mli 1893 1020068208 15_env.mli 1.12)
(source/env.mli 2077 1020420514 15_env.mli 1.13)
(test/heater_float.rif.exp 1461 1015514807 b/30_heater_flo 1.2)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(source/env.ml 7408 1020068208 16_env.ml 1.24)
(make_lurette 1239 1020068208 27_make_luret 1.11)
(source/env.ml 8072 1020420514 16_env.ml 1.25)
(make_lurette 1242 1020420514 27_make_luret 1.12)
(test/vrai_tram.lus 453 1007379917 b/6_vrai_tram. 1.1)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(test/passerelle.env 1105 1019479246 b/17_passerelle 1.6)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/rnumsolver.ml 10783 1017837703 b/27_rnumsolver 1.6)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/parse_env.mli 907 1016127950 40_parse_env. 1.6)
(source/parse_env.mli 908 1020420514 40_parse_env. 1.7)
(source/sim2chro.mli 1429 1017929190 b/23_sim2chro.m 1.4)
(source/ima_exe.ml 7212 1020068208 b/32_ima_exe.ml 1.5)
(source/ima_exe.ml 7748 1020420514 b/32_ima_exe.ml 1.6)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 7749 1016803757 49_eval.ml 1.12)
(source/gen_stubs.ml 36911 1020068208 24_generate_l 1.23)
(source/parse_env.ml 18408 1020068208 41_parse_env. 1.17)
(source/gen_stubs.ml 36501 1020420514 24_generate_l 1.24)
(source/parse_env.ml 18485 1020420514 41_parse_env. 1.18)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/sim2chro.ml 2680 1017929190 b/24_sim2chro.m 1.7)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/formula.mli 3498 1020068208 44_formula.ml 1.11)
(source/formula.mli 3646 1020420514 44_formula.ml 1.12)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/command_line.mli 1421 1017929190 b/21_command_li 1.6)
(source/wtree.mli 2321 1020068208 b/0_wtree.mli 1.8)
(source/wtree.mli 3417 1020420514 b/0_wtree.mli 1.9)
(test/porte.env 1130 1019479246 b/16_porte.env 1.6)
(source/env_state.mli 5868 1020068208 50_env_state. 1.16)
(source/env_state.mli 5850 1020420514 50_env_state. 1.17)
(source/rnumsolver.mli 1764 1017335442 b/26_rnumsolver 1.3)
(source/ima_exe.mli 447 1016127950 b/31_ima_exe.ml 1.1)
(source/eval.mli 1389 1016803757 48_eval.mli 1.9)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 22160 1020068208 17_OcamlMakef 1.27)
(source/command_line_ima_exe.ml 2400 1016803757 b/33_command_li 1.2)
(source/command_line_ima_exe.ml 2665 1020420514 b/33_command_li 1.3)
(test/ControleurPorte.rif.exp 4746 1016803757 b/29_Controleur 1.4)
(test/tram.env 1149 1019479246 b/15_tram.env 1.6)
(Makefile.lurette 1848 1020068208 b/38_Makefile.l 1.2)
(source/show_env.ml 2970 1020068208 43_show_env.m 1.5)
(Makefile.lurette 1866 1020420514 b/38_Makefile.l 1.3)
(source/show_env.ml 3271 1020420514 43_show_env.m 1.6)
(source/gne.mli 1107 1016803757 b/36_gne.mli 1.1)
(bin/Makefile.gen_stubs 467 1020068208 b/42_Makefile.g 1.1)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
......@@ -65,8 +65,8 @@
(test/heater_int.lus 170 1020068208 b/43_heater_int 1.1)
(source/graph.mli 1493 1015250295 13_graph.mli 1.6)
(test/heater_int.rif.exp 858 1017837703 b/28_heater_int 1.2)
(source/formula.ml 6982 1020068208 45_formula.ml 1.12)
(source/formula.ml 7330 1020420514 45_formula.ml 1.13)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/print.ml 6368 1020068208 47_print.ml 1.14)
(source/print.ml 6587 1020420514 47_print.ml 1.15)
(test/vrai_tram.h 2468 1012914629 b/7_vrai_tram. 1.2)
(bin/Makefile.show_ima 1321 1020068208 b/40_Makefile.s 1.1)
(bin/Makefile.show_ima 1243 1020420514 b/40_Makefile.s 1.2)
......@@ -4,7 +4,7 @@
OCAMLMAKEFILE = $(LURETTE_PATH)/OcamlMakefile
OCAMLNCFLAGS = -inline 10
OCAMLNCFLAGS = -inline 10 -noassert -unsafe
ifndef OCAMLFLAGS
OCAMLFLAGS := -noassert -unsafe
......@@ -30,11 +30,11 @@ SOURCES_OCAML = \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/gne.mli $(LURETTE_PATH)/source/gne.ml \
$(LURETTE_PATH)/source/parse_env.mli $(LURETTE_PATH)/source/parse_env.ml \
$(LURETTE_PATH)/source/wtree.mli $(LURETTE_PATH)/source/wtree.ml \
$(LURETTE_PATH)/source/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/rnumsolver.mli $(LURETTE_PATH)/source/rnumsolver.ml \
$(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/wtree.mli $(LURETTE_PATH)/source/wtree.ml \
$(LURETTE_PATH)/source/print.mli $(LURETTE_PATH)/source/print.ml \
$(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/sim2chro.mli $(LURETTE_PATH)/source/sim2chro.ml \
$(LURETTE_PATH)/source/env.mli $(LURETTE_PATH)/source/env.ml \
......
......@@ -32,11 +32,11 @@ SOURCES_OCAML = \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/gne.mli $(LURETTE_PATH)/source/gne.ml \
$(LURETTE_PATH)/source/parse_env.mli $(LURETTE_PATH)/source/parse_env.ml \
$(LURETTE_PATH)/source/wtree.mli $(LURETTE_PATH)/source/wtree.ml \
$(LURETTE_PATH)/source/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/rnumsolver.mli $(LURETTE_PATH)/source/rnumsolver.ml \
$(LURETTE_PATH)/source/print.mli $(LURETTE_PATH)/source/print.ml \
$(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/wtree.mli $(LURETTE_PATH)/source/wtree.ml \
$(LURETTE_PATH)/source/print.mli $(LURETTE_PATH)/source/print.ml \
$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/sim2chro.mli $(LURETTE_PATH)/source/sim2chro.ml \
$(LURETTE_PATH)/source/env.mli $(LURETTE_PATH)/source/env.ml \
......
......@@ -28,7 +28,6 @@ SOURCES_OCAML = \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/parse_env.mli $(LURETTE_PATH)/source/parse_env.ml \
$(LURETTE_PATH)/source/wtree.mli $(LURETTE_PATH)/source/wtree.ml \
$(LURETTE_PATH)/source/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/show_ima.ml
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 60)
(Parent-Version lurette 0 59)
(Version-Log "
Add an make release rule to package a lurette.tgz ready to distribute.
(Project-Version lurette 0 61)
(Parent-Version lurette 0 60)
(Version-Log "
Create a bin dir where all the biniries (except lurette) will live.
Add support for handling loops. This is based on the use of dynamic
weigths. The idea is to compute the dynamic weigths before the trees
are constructed.
Create a show_ima executable that lets one (Yvan actually) display
.env (or .ima) files off-line.
Move read_env_state from env.ml to env_state.ml.
Add support for lutin loops in the parser (not yet handled tough).
In gen_stubs.ml, try to automatically call lustre whenever no C poc
file exists for the invoked program.
Add a --show-aut option for ima_exe.
Also, Add the command lise args hashed to the end of the name of the dot file
that is used to visualize the ima file.
")
(New-Version-Log "")
(Checkin-Time "Mon, 29 Apr 2002 10:16:48 +0200")
(Checkin-Time "Fri, 03 May 2002 12:08:34 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -32,14 +27,14 @@ file exists for the invoked program.
;; 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.5 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.6 644))
(source/command_line_ima_exe.ml (lurette/b/33_command_li 1.2 644))
(source/command_line_ima_exe.mli (lurette/b/34_command_li 1.1 644))
(source/command_line_ima_exe.ml (lurette/b/33_command_li 1.3 644))
(source/command_line_ima_exe.mli (lurette/b/34_command_li 1.2 644))
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.12 644))
(source/lurette.ml (lurette/12_lurette.ml 1.35 644))
(source/lurette.ml (lurette/12_lurette.ml 1.36 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))
......@@ -48,10 +43,10 @@ file exists for the invoked program.
(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.12 644))
(source/env.ml (lurette/16_env.ml 1.24 644))
(source/env.mli (lurette/15_env.mli 1.13 644))
(source/env.ml (lurette/16_env.ml 1.25 644))
(source/util.ml (lurette/35_util.ml 1.17 644))
(source/util.ml (lurette/35_util.ml 1.18 644))
(source/solver.mli (lurette/38_solver.mli 1.10 644))
(source/solver.ml (lurette/39_solver.ml 1.21 644))
......@@ -59,26 +54,26 @@ file exists for the invoked program.
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.3 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.6 644))
(source/parse_env.mli (lurette/40_parse_env. 1.6 644))
(source/parse_env.ml (lurette/41_parse_env. 1.17 644))
(source/parse_env.mli (lurette/40_parse_env. 1.7 644))
(source/parse_env.ml (lurette/41_parse_env. 1.18 644))
(source/show_env.mli (lurette/42_show_env.m 1.5 644))
(source/show_env.ml (lurette/43_show_env.m 1.5 644))
(source/show_env.ml (lurette/43_show_env.m 1.6 644))
(source/formula.mli (lurette/44_formula.ml 1.11 644))
(source/formula.ml (lurette/45_formula.ml 1.12 644))
(source/formula.mli (lurette/44_formula.ml 1.12 644))
(source/formula.ml (lurette/45_formula.ml 1.13 644))
(source/print.mli (lurette/46_print.mli 1.8 644))
(source/print.ml (lurette/47_print.ml 1.14 644))
(source/print.ml (lurette/47_print.ml 1.15 644))
(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.16 644))
(source/env_state.ml (lurette/51_env_state. 1.17 644))
(source/env_state.mli (lurette/50_env_state. 1.17 644))
(source/env_state.ml (lurette/51_env_state. 1.18 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.8 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.10 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.9 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.11 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.4 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.7 644))
......@@ -86,17 +81,17 @@ file exists for the invoked program.
(source/gne.mli (lurette/b/36_gne.mli 1.1 644))
(source/gne.ml (lurette/b/37_gne.ml 1.1 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.23 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.24 644))
; little script that sets env vars and starts the lurette build
(make_lurette (lurette/27_make_luret 1.11 744))
(make_lurette (lurette/27_make_luret 1.12 744))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.27 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.2 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.3 644))
(bin/Makefile.show_ima (lurette/b/40_Makefile.s 1.1 644))
(bin/Makefile.ima_exe (lurette/b/41_Makefile.i 1.1 644))
(bin/Makefile.show_ima (lurette/b/40_Makefile.s 1.2 644))
(bin/Makefile.ima_exe (lurette/b/41_Makefile.i 1.2 644))
(bin/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.1 644))
;; Documentation
......
......@@ -39,7 +39,7 @@ case $# in
echo "... make"
shift 1
make $@
make $@ dc
;;
##############################################################
*)
......
......@@ -10,28 +10,36 @@
type optionsT = {
mutable show_automata : bool ;
mutable boot : bool ;
mutable user_seed : int
}
type cmd_line_optionT =
Seed | Boot
Seed | Boot | ShowAut | NoShowAut
(* Names of the command line options to override the defaults. *)
let (string_to_option: (string * cmd_line_optionT) list) = [
("-b", Boot);
("-boot", Boot);
("--boot", Boot);
("-boot", Boot);
("-b", Boot);
("--with-seed", Seed);
("-seed", Seed)
("-seed", Seed);
("--show-aut", ShowAut);
("-s", ShowAut);
("--no-show-aut", NoShowAut)
]
let (option_to_usage: cmd_line_optionT -> string) =
fun opt ->
match opt with
Boot -> "The automata starts generating values.\n"
| Seed -> "Set the value of the seed the random engine is initialized with (0 lets the system draw a seed).\n"
Boot -> "The automata starts generating values.\n"
| ShowAut -> "Run ima_exe showing the ima automata step.\n"
| NoShowAut -> "Do not show the ima automata (Default).\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 ->
......@@ -58,16 +66,16 @@ let usage_options =
(List.rev (group_common_options string_to_option))
let usage =
("\n\nusage: ./ima_exe [options]* <file>.env ([x] <file>.env)* \n" ^
("\n\nusage: ./ima_exe [options]* <file>.ima ([x] <file>.ima)* \n" ^
" where: " ^
"\n\t o `<file>.env' contains an environment automata. Environments " ^
"\n\t o `<file>.ima contains an environment automata. Environments " ^
"\n\t separated by `x' will executed as if their automata where " ^
"\n\t multiplied (necessary if they have common output variables).\n " ^
"\n\t o `options' is a list of options. The available options are: " ^
usage_options ^ "\n\n" ^
"Example: ./ima_exe env1.env x env2.env x env3.env env4\n\t" ^
"Example: ./ima_exe env1.ima x env2.ima x env3.ima env4\n\t" ^
"will run the environment `env1', `env2', and `env3' as a product, \n\t" ^
"and `env4' in parallel.\n\n ")
......
......@@ -13,6 +13,7 @@
type optionsT = {
mutable show_automata : bool ;
mutable boot : bool ;
mutable user_seed : int
}
......@@ -27,7 +28,7 @@ val cmd_line_string_to_int : string -> string -> int
*)
type cmd_line_optionT =
Seed | Boot
Seed | Boot | ShowAut | NoShowAut
val string_to_option: (string * cmd_line_optionT) list
......
......@@ -14,6 +14,7 @@
open List
open Solver
open Formula
open Wtree
(****************************************************************************)
......@@ -23,39 +24,43 @@ open Formula
type nl = node list
type nll = node list list
type sl = subst list
let (solve_formula_list: env_in -> int -> node list list ->
(node list list * sl * sl) list -> formula list -> var_name list ->
vnt list -> (node list list * sl * sl) list) =
fun input p nll acc fl bool_vars_to_gen num_vnt_to_gen ->
(*
** Returns [p] solutions for the conjunction of formula contained
** in [fl]; a solution is a triple containing (1) the node list [nll],
** which are the target nodes corresponding to the formula in [fl]
** (2) a list of substitutions for output vars, and (3) a list of
** substitutions for local vars.
*)
type cal = Wtree.cpt_action list
type call = Wtree.cpt_action list list
let (solve_formula_list: env_in -> int -> nll -> call
-> (nll * call * sl * sl) list -> formula list -> var_name list
-> vnt list -> (nll * call * sl * sl) list) =
fun input p nll call acc fl bool_vars_to_gen num_vnt_to_gen ->
(**
Returns [p] solutions for the conjunction of formula
contained in [fl]; a solution is a triple containing (1) the
node list [nll], which are the target nodes corresponding to
the formula in [fl] (2) the operations on loop counters
associated to a formula (3) a list of substitutions for output
vars, and (4) a list of substitutions for local vars.
*)
let sl_sl_l = Solver.solve_formula input p fl bool_vars_to_gen num_vnt_to_gen in
(* Adds the target nodes to the drawn substitutions *)
if acc = [] then
(* first formula *)
(List.map
(fun (sl1, sl2) ->
(nll, sl1, sl2))
(nll, call, sl1, sl2))
sl_sl_l
)
else
(List.map2
(fun (sl1, sl2) (nll, sl1_acc, sl2_acc) ->
(nll, (append sl1 sl1_acc), (append sl2 sl2_acc)))
(fun (sl1, sl2) (nll, call, sl1_acc, sl2_acc) ->
(nll, call, (append sl1 sl1_acc), (append sl2 sl2_acc)))
sl_sl_l
acc
)
let (solve_formula_list_list: env_in -> int -> node list list * formula list list
-> (node list list * sl * sl) list) =
fun input p (nll, fll) ->
let (solve_formula_list_list: env_in -> int
-> node list list * formula list list * call
-> (nll * call * sl * sl) list) =
fun input p (nll, fll, call) ->
let (get_vars_from_node: (vn list * vnt list) -> node -> (vn list * vnt list)) =
fun (bool_acc, num_acc) node ->
(* Gets the list of (output and local) boolean and numeric
......@@ -84,108 +89,118 @@ let (solve_formula_list_list: env_in -> int -> node list list * formula list lis
([], [])
bvnl_nvntl_l
in
let nll_sl_sl_l =
let nll_call_sl_sl_l =
Util.list_fold_left3
(solve_formula_list input p nll) [] fll bool_vars_to_gen_ll num_vnt_to_gen_ll
(solve_formula_list input p nll call) [] fll bool_vars_to_gen_ll num_vnt_to_gen_ll
in
nll_sl_sl_l
let (get_wtrees: node list list -> Wtree.wtree_table -> Wtree.wtree list) =
fun nll wtt ->
(** Get the wtrees corresponding to the list of list of nodes
[nll], and then multiply the wtrees in the inner
lists. E.g., the list [[[n1; n2]; [n3]]] leads to the list
of list of wtrees [[[t1; t2]; [t3]]] which is transformed
into [[t1 x t2; t3]], where [x] is the wtree product. *)
let wtll = map (map (Hashtbl.find wtt)) nll in
map (fun nl -> fold_left (Wtree.wtree_product) (hd nl) (tl nl)) wtll
nll_call_sl_sl_l
let (compute_wtrees: node list list -> Wtree.wtree list) =
fun nll ->
(** Computes the wtrees corresponding to the list of list of
nodes [nll], and then multiply the wtrees in the inner
lists. E.g., the list [[[n1; n2]; [n3]]] leads to the list of
list of wtrees [[[t1; t2]; [t3]]] which is transformed into
[[t1 x t2; t3]], where [x] is the wtree product. *)
let wtll = map (map (Wtree.build_wtree (Env_state.graph ()))) nll in
map (fun wtl -> fold_left (Wtree.wtree_product) (hd wtl) (tl wtl)) wtll
let (merge_lll: ('a list * 'f list) list list ->
('a list list * 'f list list) list) =
fun nl_fl_ll ->
(* Distributes the last ``[l]'' of [nl_fl_ll] over [nl] and [fl]. *)
match nl_fl_ll with
let (merge_lll: ('a list * 'f list * 'c list) list list ->
('a list list * 'f list list * 'c list list) list) =
fun nl_fl_cal_ll ->
(* Distributes the last ``[l]'' of [nl_fl_cal_ll] over [nl], [fl],
and [cal]. *)
match nl_fl_cal_ll with
[] -> assert false
| nl_fl_l0::nl_fl_ll_tail ->
let nll_fll_l0 =
map (fun (nl0, fl0) -> ([nl0], [fl0])) nl_fl_l0
| nl_fl_cal_l0::nl_fl_cal_ll_tail ->
let nll_fll_call_l0 =
map (fun (nl0, fl0, cal0) -> ([nl0], [fl0], [cal0])) nl_fl_cal_l0
in
(fold_left
(fun nll_fll_l nl_fl_l ->
(fun nll_fll_call_l nl_fl_cal_l ->
(map2
(fun (nl, fl) (nll, fll) -> (nl::nll, fl::fll))
nl_fl_l
nll_fll_l
(fun (nl, fl, cal) (nll, fll, call) -> (nl::nll, fl::fll, cal::call))
nl_fl_cal_l
nll_fll_call_l
)
)
nll_fll_l0
nl_fl_ll_tail)
nll_fll_call_l0
nl_fl_cal_ll_tail)
let _ = assert (
(* n = 2, env1 x env2 env3 *)
(merge_lll
[[([1;2], [Bvar("a");Bvar("b")]);
([4;5], [Bvar("d");Bvar("e")])];
[([3], [Bvar("c")]);
([6], [Bvar("f")])]])
=
[[[3]; [1; 2]], [[Bvar "c"]; [Bvar "a"; Bvar "b"]];
[[6]; [4; 5]], [[Bvar "f"]; [Bvar "d"; Bvar "e"]]]
)
let _ = assert (
(* n = 2, env1 x env2 env3 *)
(merge_lll
[[([1;2], [Bvar("a");Bvar("b")], []);
([4;5], [Bvar("d");Bvar("e")], [])];
[([3], [Bvar("c")], []);
([6], [Bvar("f")], [])]])
=
[[[3]; [1; 2]], [[Bvar "c"]; [Bvar "a"; Bvar "b"]], [[];[]];
[[6]; [4; 5]], [[Bvar "f"]; [Bvar "d"; Bvar "e"]], [[];[]]
]
)
let rec draw_n_p_values input n p cn_ll wtl =
let nl_fl_l__wt__l =
let nl_fl_cal_l__wt__l =
(* Draw n formula *)
map2 (Wtree.choose_n_formula (Solver.is_satisfiable input) n) cn_ll wtl
map2 (Wtree.choose_n_formula n) cn_ll wtl
in
let (nl_fl_ll, new_wtl) =
let (nl_fl_cal_ll, new_wtl) =
fold_left
(fun (acc1, acc2) (nl_fl_l, wt) ->
((append acc1 [nl_fl_l]), (append acc2 [wt])))
(fun (acc1, acc2) (nl_fl_cal_l, wt) ->
((append acc1 [nl_fl_cal_l]), (append acc2 [wt])))
([], [])
nl_fl_l__wt__l
nl_fl_cal_l__wt__l
in
let nll_fll_l = merge_lll nl_fl_ll in
let nll_fll_call_l = merge_lll nl_fl_cal_ll in
(* Draw p solutions for each of the n formula *)
let nll_sl_sl_ll = List.map (solve_formula_list_list input p) nll_fll_l in
let l = Util.count_empty_list nll_sl_sl_ll in
let nll_call_sl_sl_ll = List.map (solve_formula_list_list input p) nll_fll_call_l in
let l = Util.count_empty_list nll_call_sl_sl_ll in
if l = 0
then nll_sl_sl_ll
then nll_call_sl_sl_ll
else
(* At least one formula was not satisfiable because of numeric
constraints. We redraw as many times (l) as necessary. *)
append nll_sl_sl_ll (draw_n_p_values input l p cn_ll new_wtl)
append nll_call_sl_sl_ll (draw_n_p_values input l p cn_ll new_wtl)
(* Exported *)
let (env_try: int -> int -> env_in ->
(node list list * env_out * env_loc) list) =
(nll * call * env_out * env_loc) list) =
fun n p input ->
let cn_ll = (Env_state.current_nodes ())
and wtt = (Env_state.wtree_table ())
in
let wtl = get_wtrees cn_ll wtt in
let nll_sl_sl_ll = draw_n_p_values input n p cn_ll wtl in
let nll_sl_sl_l = flatten nll_sl_sl_ll in
let _ = Env_state.set_input input in
let cn_ll = (Env_state.current_nodes ()) in
let wtl = compute_wtrees cn_ll in
let nll_call_sl_sl_ll = draw_n_p_values input n p cn_ll wtl in
let nll_call_sl_sl_l = flatten nll_call_sl_sl_ll in
assert (length nll_sl_sl_l = (n*p));
Env_state.set_input input;
nll_sl_sl_l
assert (length nll_call_sl_sl_l = (n*p));
nll_call_sl_sl_l
(*****************************************************************************)
(*****************************************************************************)
(* env_step *)
let (update_loop_cpt_tbl : Wtree.cpt_action -> unit) =
fun action ->
match action with
Wtree.Init(node, f) -> Env_state.set_loop_cpt node f
| Wtree.Dec(node) -> Env_state.dec_loop_cpt node
(* Exported *)
let (env_step : node list list -> env_out -> env_loc -> unit) =
fun nodes_to output local ->
Env_state.set_current_nodes nodes_to ;
Env_state.set_output output ;
Env_state.set_local local
let (env_step : nll -> call -> env_out -> env_loc -> unit) =
fun nodes_to call output local ->
let cal = flatten call in
List.iter (update_loop_cpt_tbl) cal;
Env_state.set_current_nodes nodes_to ;
Env_state.set_output output ;
Env_state.set_local local
(****************************************************************************)
......
......@@ -26,25 +26,28 @@ open Env_state
(*---------------------------------------------------------------------*)
val env_try : int -> int -> env_in -> (node list list * env_out * env_loc) list
val env_try : int -> int -> env_in
-> (node list list * Wtree.cpt_action list list * env_out * env_loc) list
(**
[env_try n p input] returns a list of [n*p] possible outputs of
the environment with input [input]. This function actually
returns a list of 4-tuple because we need to know which arcs