Commit 562a6ed5 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.71 Mon, 22 Jul 2002 16:51:44 +0200 by jahier

Parent-Version:      0.70
Version-Log:

automata.ml,mli:
env.ml,mli:
ima_exe.ml,mli:
lurette.ml,mli:
   Fix a bug where the control expr were evaluated twice, which
   migth produce strange behavior whenever a CS var was drawn to 0
   in the place, and a value different from 0 in the second place.
   The fix consist in attaching the control.state at automata.t leaves,
   instead of the control expr labels (which was a bit silly BTW).

show_env.ml:
   Fix a small bug in the dot output.

Project-Description: Lurette
parent da43be79
......@@ -4,21 +4,21 @@
(test/usager.env 493 1027066799 b/14_usager.env 1.8)
(source/command_line_ima_exe.mli 1082 1021651153 b/34_command_li 1.3)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 18696 1027066799 51_env_state. 1.23)
(source/env_state.ml 19663 1027092697 51_env_state. 1.24)
(source/graph.ml 2563 1027066799 14_graph.ml 1.7)
(bin/Makefile.ima_exe 2013 1027066799 b/41_Makefile.i 1.3)
(source/util.ml 13725 1027066799 35_util.ml 1.21)
(test/time.exp 5583 1027066799 b/48_time.exp 1.1)
(source/solver.ml 24576 1027066799 39_solver.ml 1.23)
(source/solver.ml 24250 1027092697 39_solver.ml 1.24)
(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 12622 1027066799 12_lurette.ml 1.40)
(source/lurette.ml 11706 1027349504 12_lurette.ml 1.42)
(test/temp_int.env 647 1027066799 b/50_temp_int.e 1.1)
(source/solver.mli 1071 1027066799 38_solver.mli 1.12)
(source/env.mli 2024 1027066799 15_env.mli 1.14)
(source/solver.mli 1003 1027092697 38_solver.mli 1.13)
(source/env.mli 2028 1027349504 15_env.mli 1.15)
(test/heater_float.rif.exp 1453 1027066799 b/30_heater_flo 1.3)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(source/env.ml 8305 1027066799 16_env.ml 1.28)
(source/env.ml 8013 1027349504 16_env.ml 1.29)
(make_lurette 1243 1027066799 27_make_luret 1.13)
(test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
......@@ -28,35 +28,35 @@
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/parse_env.mli 1025 1027066799 40_parse_env. 1.9)
(source/sim2chro.mli 1429 1017929190 b/23_sim2chro.m 1.4)
(source/ima_exe.ml 12058 1027066799 b/32_ima_exe.ml 1.13)
(source/ima_exe.ml 11851 1027349504 b/32_ima_exe.ml 1.15)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 7755 1027066799 49_eval.ml 1.13)
(source/gen_stubs.ml 36621 1021042464 24_generate_l 1.26)
(source/parse_env.ml 22104 1027066799 41_parse_env. 1.20)
(test/temp_float.env 719 1027066799 b/51_temp_float 1.1)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/automata.mli 3395 1027066799 b/46_automata.m 1.1)
(source/automata.mli 3397 1027349504 b/46_automata.m 1.2)
(source/sim2chro.ml 2653 1020777170 b/24_sim2chro.m 1.8)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/formula.mli 3638 1027066799 44_formula.ml 1.14)
(test/time.res 5578 1027066799 b/49_time.res 1.1)
(test/time.res 5577 1027349504 b/49_time.res 1.3)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/command_line.mli 1421 1017929190 b/21_command_li 1.6)
(test/porte.env 1021 1027066799 b/16_porte.env 1.7)
(source/env_state.mli 6423 1027066799 50_env_state. 1.20)
(source/env_state.mli 6453 1027092697 50_env_state. 1.21)
(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 1395 1027066799 48_eval.mli 1.10)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 24344 1027066799 17_OcamlMakef 1.30)
(OcamlMakefile 24425 1027092697 17_OcamlMakef 1.31)
(source/command_line_ima_exe.ml 2792 1021651153 b/33_command_li 1.4)
(test/ControleurPorte.rif.exp 4756 1027066799 b/29_Controleur 1.5)
(test/tram.env 1038 1027066799 b/15_tram.env 1.7)
(Makefile.lurette 1953 1027066799 b/38_Makefile.l 1.4)
(source/show_env.ml 3629 1027066799 43_show_env.m 1.10)
(source/show_env.ml 3653 1027349504 43_show_env.m 1.11)
(source/gne.mli 1079 1027066799 b/36_gne.mli 1.2)
(source/automata.ml 14972 1027066799 b/47_automata.m 1.1)
(source/automata.ml 15708 1027349504 b/47_automata.m 1.2)
(bin/Makefile.gen_stubs 467 1020068208 b/42_Makefile.g 1.1)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
......@@ -69,7 +69,7 @@
(source/print.mli 773 1027066799 46_print.mli 1.10)
(test/heater_int.lus 170 1020068208 b/43_heater_int 1.1)
(source/graph.mli 2218 1027066799 13_graph.mli 1.9)
(test/heater_int.rif.exp 857 1027066799 b/28_heater_int 1.3)
(test/heater_int.rif.exp 860 1027349504 b/28_heater_int 1.4)
(source/formula.ml 7287 1027066799 45_formula.ml 1.16)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/print.ml 5954 1027066799 47_print.ml 1.17)
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 70)
(Parent-Version lurette 0 69)
(Project-Version lurette 0 71)
(Parent-Version lurette 0 70)
(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.
automata.ml,mli:
env.ml,mli:
ima_exe.ml,mli:
lurette.ml,mli:
Fix a bug where the control expr were evaluated twice, which
migth produce strange behavior whenever a CS var was drawn to 0
in the place, and a value different from 0 in the second place.
The fix consist in attaching the control.state at automata.t leaves,
instead of the control expr labels (which was a bit silly BTW).
show_env.ml:
Fix a small bug in the dot output.
")
(New-Version-Log "")
(Checkin-Time "Fri, 19 Jul 2002 17:31:37 +0200")
(Checkin-Time "Mon, 22 Jul 2002 16:51:44 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -29,14 +32,14 @@ env_state.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.14 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.15 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.41 644))
(source/lurette.ml (lurette/12_lurette.ml 1.42 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))
......@@ -45,8 +48,8 @@ env_state.ml:
(source/graph.mli (lurette/13_graph.mli 1.9 644))
(source/graph.ml (lurette/14_graph.ml 1.7 644))
(source/env.mli (lurette/15_env.mli 1.14 644))
(source/env.ml (lurette/16_env.ml 1.28 644))
(source/env.mli (lurette/15_env.mli 1.15 644))
(source/env.ml (lurette/16_env.ml 1.29 644))
(source/util.ml (lurette/35_util.ml 1.21 644))
......@@ -60,7 +63,7 @@ env_state.ml:
(source/parse_env.ml (lurette/41_parse_env. 1.20 644))
(source/show_env.mli (lurette/42_show_env.m 1.7 644))
(source/show_env.ml (lurette/43_show_env.m 1.10 644))
(source/show_env.ml (lurette/43_show_env.m 1.11 644))
(source/formula.mli (lurette/44_formula.ml 1.14 644))
(source/formula.ml (lurette/45_formula.ml 1.16 644))
......@@ -74,8 +77,8 @@ env_state.ml:
(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))
(source/automata.mli (lurette/b/46_automata.m 1.2 644))
(source/automata.ml (lurette/b/47_automata.m 1.2 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.4 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.8 644))
......@@ -112,7 +115,7 @@ env_state.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.2 644))
(test/time.res (lurette/b/49_time.res 1.3 644))
;; Various files used for testing purposes
(test/usager.env (lurette/b/14_usager.env 1.8 644))
......@@ -130,7 +133,7 @@ env_state.ml:
(test/vrai_tram.c (lurette/b/8_vrai_tram. 1.3 644))
(test/tram_simple.h (lurette/b/25_tram_simpl 1.1 644))
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.3 644))
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.4 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.5 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.3 644))
(test/heater_int.lus (lurette/b/43_heater_int 1.1 644))
......
......@@ -30,12 +30,15 @@ let (intset_to_string : IntSet.t -> string) =
(****************************************************************************)
type arc_info_static = int * formula_eps * string list
type arc_info_static = int * formula_eps * Control.state option
(* We call it static in the sense that weights are no more dynamic. *)
let (arc_info_static_to_string : arc_info_static -> string) =
fun (w, formula_eps, pcl) ->
let pc_str = fold_left (fun acc str -> (acc^":"^str)) "" pcl in
let pc_str =
" XXX "
(* fold_left (fun acc str -> (acc^":"^str)) "" pcl *)
in
( (string_of_int w) ^ " " ^
(formula_eps_to_string formula_eps) ^ " " ^ pc_str)
......@@ -144,7 +147,7 @@ and
Graph.add_trans
t
(IntSet.singleton n)
((get_weight w st1), f, [pc])
(get_weight w st1, f, None)
(IntSet.singleton nt) ;
get_automaton_acc g n0 nt t st1
)
......@@ -159,7 +162,7 @@ and
Graph.add_trans
t
(IntSet.singleton n)
((get_weight w st1), f, [pc])
(get_weight w st1, f, Some st1)
(IntSet.singleton nt)
)
)
......@@ -184,6 +187,15 @@ and
| Wident_not_sig(id) -> if (Control.return id st) > 0 then 0 else 1
let (compose_state_option : Control.state option -> Control.state option ->
Control.state option) =
fun st1 st2 ->
match (st1, st2) with
None, None -> None
| None, Some s -> Some s
| Some s, None -> Some s
| Some s1, Some s2 -> Some (Control.compose_state s1 s2)
let rec (automata_x_automata : t -> t -> t) =
fun (n1, g1) (n2, g2) ->
......@@ -211,13 +223,13 @@ and
and
(trans_x_trans : stat_trans_list -> stat_trans_list -> stat_trans_list ->
transition -> transition -> unit) =
fun g g1 g2 (n1, (w1, f1, p1), n2) (n3, (w2, f2, p2), n4) ->
fun g g1 g2 (n1, (w1, f1, st1), n2) (n3, (w2, f2, st2), n4) ->
let n13 = IntSet.union n1 n3 in
match (f1, f2) with
Form(ff1), Form(ff2) ->
let n24 = IntSet.union n2 n4
and f = Form(And(ff1, ff2)) in
let arc = (w1*w2, f, append p1 p2) in
let arc = (w1*w2, f, compose_state_option st1 st2) in
if
not (Graph.contain_trans g n13 arc n24)
&& Solver.is_satisfiable (Env_state.input ()) (And(ff1, ff2))
......@@ -231,7 +243,7 @@ and
| Eps, Eps ->
let n24 = IntSet.union n2 n4
and arc = (w1*w2, Eps, (append p1 p2)) in
and arc = (w1*w2, Eps, (compose_state_option st1 st2)) in
if
not (Graph.contain_trans g n13 arc n24)
then
......@@ -244,7 +256,7 @@ and
| Eps, Form(ff2) ->
let n23 = IntSet.union n2 n3
and arc = (w1, Eps, p1) in
and arc = (w1, Eps, st1) in
if
not (Graph.contain_trans g n13 arc n23)
then
......@@ -257,7 +269,7 @@ and
| Form(ff1), Eps ->
let n14 = IntSet.union n1 n4
and arc = (w2, Eps, p2) in
and arc = (w2, Eps, st2) in
if
not (Graph.contain_trans g n13 arc n14)
then
......@@ -294,17 +306,17 @@ let _ = assert (
and n3_11 = IntSet.union n3 n11 and n4_11 = IntSet.union n4 n11
in
let _ =
Graph.add_trans g1 n1 (2, Eps, ["w1";"w2"]) n2 ;
Graph.add_trans g1 n2 (1, Form(Bvar("a")), ["w3"]) n3 ;
Graph.add_trans g1 n1 (4, Form(Bvar("b")), ["w4"]) n4 ;
Graph.add_trans g1 n1 (2, Eps, None) n2 ;
Graph.add_trans g1 n2 (1, Form(Bvar("a")), None) n3 ;
Graph.add_trans g1 n1 (4, Form(Bvar("b")), None) n4 ;
Graph.add_trans g2 n10 (3, Form(Bvar("o")), ["w11"]) n11 ;
Graph.add_trans g2 n10 (3, Form(Bvar("o")), None) n11 ;
Graph.add_trans g12 n1_10
(12, (Form(And(Bvar("b"), (Bvar("o"))))), ["w4";"w11"]) n4_11;
Graph.add_trans g12 n1_10 (2, Eps, ["w1";"w2"]) n2_10;
(12, (Form(And(Bvar("b"), (Bvar("o"))))), None) n4_11;
Graph.add_trans g12 n1_10 (2, Eps, None) n2_10;
Graph.add_trans g12 n2_10
(3, (Form(And(Bvar("a"), (Bvar("o"))))), ["w3";"w11"]) n3_11 ;
(3, (Form(And(Bvar("a"), (Bvar("o"))))), None) n3_11 ;
in
let a12 = automata_product [(n1, g1); (n10,g2)]
in
......@@ -329,27 +341,27 @@ let _ = assert (
and n1_6 = IntSet.union n1 n6 and n2_6 = IntSet.union n2 n6
in
let _ =
Graph.add_trans g1 n1 (1, Eps, ["init cpt"]) n2 ;
Graph.add_trans g1 n2 (1, Eps, ["dec cpt"]) n3 ;
Graph.add_trans g1 n3 (1, Form(Bvar("a")), []) n2 ;
Graph.add_trans g1 n2 (0, Eps, []) n4 ;
Graph.add_trans g1 n4 (1, Form(Bvar("b")), []) n1 ;
Graph.add_trans g1 n1 (1, Eps, None) n2 ;
Graph.add_trans g1 n2 (1, Eps, None) n3 ;
Graph.add_trans g1 n3 (1, Form(Bvar("a")), None) n2 ;
Graph.add_trans g1 n2 (0, Eps, None) n4 ;
Graph.add_trans g1 n4 (1, Form(Bvar("b")), None) n1 ;
Graph.add_trans g2 n5 (1, Form(Bvar("o")), ["w11"]) n6 ;
Graph.add_trans g2 n5 (3, Form(Bvar("p")), ["w11"]) n7 ;
Graph.add_trans g2 n5 (1, Form(Bvar("o")), None) n6 ;
Graph.add_trans g2 n5 (3, Form(Bvar("p")), None) n7 ;
Graph.add_trans g12 n1_5 (1, Eps, ["init cpt"]) n2_5;
Graph.add_trans g12 n2_5 (0, Eps, []) n4_5;
Graph.add_trans g12 n1_5 (1, Eps, None) n2_5;
Graph.add_trans g12 n2_5 (0, Eps, None) n4_5;
Graph.add_trans g12 n4_5
(3, (Form(And(Bvar("b"), (Bvar("p"))))), ["w11"]) n1_7;
(3, (Form(And(Bvar("b"), (Bvar("p"))))), None) n1_7;
Graph.add_trans g12 n4_5
(1, (Form(And(Bvar("b"), (Bvar("o"))))), ["w11"]) n1_6;
(1, (Form(And(Bvar("b"), (Bvar("o"))))), None) n1_6;
Graph.add_trans g12 n2_5
(1, Eps, ["dec cpt"]) n3_5;
(1, Eps, None) n3_5;
Graph.add_trans g12 n3_5
(3, (Form(And(Bvar("a"), (Bvar("p"))))), ["w11"]) n2_7;
(3, (Form(And(Bvar("a"), (Bvar("p"))))), None) n2_7;
Graph.add_trans g12 n3_5
(1, (Form(And(Bvar("a"), (Bvar("o"))))), ["w11"]) n2_6;
(1, (Form(And(Bvar("a"), (Bvar("o"))))), None) n2_6;
in
let a12 = automata_product [(n1, g1); (n5,g2)] in
......@@ -404,9 +416,8 @@ let (get : node list list -> t list) =
(****************************************************************************)
let rec (choose_a_formula: t -> string list
-> node list * formula * string list) =
fun (node, trans) ce0 ->
let rec (choose_a_formula: t -> node list * formula * Control.state) =
fun (node, trans) ->
(** Draws a formula in an automata (according to node weights);
also returns the list of their corresponding target nodes, and
control expression. *)
......@@ -423,13 +434,27 @@ let rec (choose_a_formula: t -> string list
if s2 = 0 then raise Not_found
else
let (nt, (_,f,ce)) = List.nth null_weigth_trans (Random.int s2) in
let ce1 = append ce0 ce in
match f with
Form(ff) -> (IntSet.elements nt, ff, ce1)
| Eps -> choose_a_formula (nt, trans) ce1
match f,ce with
Form(ff), Some st -> (IntSet.elements nt, ff, st)
| Eps, None -> choose_a_formula (nt, trans)
| Form(_), None -> assert false
| Eps, Some _ -> assert false
else
let w_sum = List.fold_left (fun acc (_,(w,_,_)) -> acc+w) 0 nt_arc_l in
let j = Random.int (w_sum + 1) in
let j =
try Random.int (w_sum + 1)
with _ ->
Control.print_state (Env_state.ctrl_state ());
(List.iter
(fun (nt,(w,f,st_opt)) ->
output_string stderr ("\n" ^ (string_of_int w) );
match st_opt with
None -> output_string stderr "None"
| Some st -> Control.print_state st
)
nt_arc_l );
assert false
in
let rec get_jth_trans j list =
match list with
[] -> assert false
......@@ -443,22 +468,24 @@ let rec (choose_a_formula: t -> string list
get_jth_trans newj tail
in
match get_jth_trans j nt_arc_l with
(nt, (w,Eps,ce)) -> choose_a_formula (nt, trans) (append ce0 ce)
| (nt, (w,Form(ff),ce)) -> (IntSet.elements nt, ff, append ce0 ce)
(nt, (w,Eps,None)) -> choose_a_formula (nt, trans)
| (nt, (w,Form(ff), Some st)) -> (IntSet.elements nt, ff, st)
| (nt, (w,Form(_), None)) -> assert false
| (nt, (w,Eps, Some _)) -> assert false
type accT = (node list * formula * string list) list
type accT = (node list * formula * Control.state) list
let rec (choose_n_formula_acc: int -> t -> accT -> accT) =
fun n a nt_f_ce_l0 ->
fun n a nt_f_st_l0 ->
if
n = 0
then
nt_f_ce_l0
nt_f_st_l0
else
try
let (ntl, f, ce) = choose_a_formula a [] in
choose_n_formula_acc (n-1) a ((ntl, f, ce)::nt_f_ce_l0)
let (ntl, f, st) = choose_a_formula a in
choose_n_formula_acc (n-1) a ((ntl, f, st)::nt_f_st_l0)
with Not_found ->
let nodes_str = intset_to_string (fst a) in
Env_state.dump_env_state_stat ();
......@@ -470,7 +497,7 @@ let rec (choose_n_formula_acc: int -> t -> accT -> accT) =
(* exported *)
let (choose_n_formula: int -> t -> (node list * formula * string list) list) =
let (choose_n_formula: int -> t -> (node list * formula * Control.state) list) =
fun n a ->
let l = choose_n_formula_acc n a [] in
assert ((List.length l) = n);
......
......@@ -65,7 +65,7 @@ val get : Formula.node list list -> t list
val choose_n_formula : int -> t ->
(Formula.node list * Formula.formula * string list) list
(Formula.node list * Formula.formula * Control.state) list
(** [choose_n_formula n a] draws a list of triple made of a formula,
its corresponding target node, and a post-cond control expression
label list to evaluate if this formula is elected to perform the
......
......@@ -24,16 +24,16 @@ type nl = node list
type nll = node list list
type sl = subst list
type ce = string list (* list of Control.expr label *)
type cel = ce list
type cs = Control.state (* list of Control.expr label *)
type csl = cs list
type acc_solve_formula = (nll * ce * sl * sl) list * Automata.t list
type acc_solve_formula = (nll * cs * sl * sl) list * Automata.t list
let (solve_formula: env_in -> int -> nll -> ce
let (solve_formula: env_in -> int -> nll -> cs
-> acc_solve_formula
-> formula -> Automata.t -> vn list -> vnt list
-> acc_solve_formula) =
fun input p nll ce (acc, al) f a bool_vars_to_gen num_vnt_to_gen ->
fun input p nll cs (acc, al) f a bool_vars_to_gen num_vnt_to_gen ->
(** Returns [p] solutions for the formula [f]; a solution is a
triple containing (1) the node list [nl], which are the target
nodes corresponding to the formula in [fl] (2) the operations
......@@ -56,23 +56,23 @@ let (solve_formula: env_in -> int -> nll -> ce
(* first formula *)
((List.rev_map
(fun (sl1, sl2) ->
(nll, ce, sl1, sl2))
(nll, cs, sl1, sl2))
sl_sl_l
), append al [new_a])
else
((List.rev_map2
(fun (sl1, sl2) (nll, ce, sl1_acc, sl2_acc) ->
(nll, ce, (rev_append sl1 sl1_acc), (rev_append sl2 sl2_acc)))
(fun (sl1, sl2) (nll, cs, sl1_acc, sl2_acc) ->
(nll, cs, (rev_append sl1 sl1_acc), (rev_append sl2 sl2_acc)))
sl_sl_l
acc
), append al [new_a])
let (solve_formula_list: env_in -> int
-> (nll * ce * sl * sl) list list * Automata.t list
-> node list list * formula list * ce
-> (nll * ce * sl * sl) list list * Automata.t list) =
fun input p (sol, al) (nll, fl, ce) ->
-> (nll * cs * sl * sl) list list * Automata.t list
-> node list list * formula list * cs
-> (nll * cs * sl * sl) list list * Automata.t list) =
fun input p (sol, al) (nll, fl, cs) ->
let (get_vars_from_node: (vn list * vnt list) -> node ->
(vn list * vnt list)) =
......@@ -105,113 +105,101 @@ let (solve_formula_list: env_in -> int
)
([], []) bvnl_nvntl_l
in
let (nll_ce_sl_sl_l, new_al) =
let (nll_cs_sl_sl_l, new_al) =
Util.list_fold_left4
(solve_formula input p nll ce)
(solve_formula input p nll cs)
([], [])
fl
al
bool_vars_to_gen_ll
num_vnt_to_gen_ll
in
(nll_ce_sl_sl_l::sol, new_al)
(nll_cs_sl_sl_l::sol, new_al)
(*****************************************************************************)
let (distribute_outter_list: ('a * 'f * 'c) list list ->
('a list * 'f list * 'c) list) =
fun nl_fl_cel_ll ->
(* Distributes the last ``[l]'' of [nl_fl_cel_ll] over [nl], [fl],
and [cel]. *)
match nl_fl_cel_ll with
let (distribute_outter_list: ('a * 'f * cs) list list ->
('a list * 'f list * cs) list) =
fun nl_fl_csl_ll ->
(* Distributes the last ``[l]'' of [nl_fl_csl_ll] over [nl], [fl],
and [csl]. *)
match nl_fl_csl_ll with
[] -> assert false
| nl_fl_cel_l0::nl_fl_cel_ll_tail ->
let nll_fll_cel_l0 =
rev_map (fun (nl0, fl0, ce0) -> ([nl0], [fl0], ce0)) nl_fl_cel_l0
| nl_fl_csl_l0::nl_fl_csl_ll_tail ->
let nll_fll_csl_l0 =
rev_map (fun (nl0, fl0, cs0) -> ([nl0], [fl0], cs0)) nl_fl_csl_l0
in
(fold_left
(fun nll_fll_cel_l nl_fl_cel_l ->
(fun nll_fll_csl_l nl_fl_csl_l ->
(rev_map2
(fun (nl, fl, cel) (nll, fll, cel2) ->
(nl::nll, fl::fll, (append cel cel2))
(fun (nl, fl, csl) (nll, fll, csl2) ->
(nl::nll, fl::fll, (Control.compose_state csl csl2))
)
nl_fl_cel_l
nll_fll_cel_l
nl_fl_csl_l
nll_fll_csl_l
)
)
nll_fll_cel_l0
nl_fl_cel_ll_tail)
nll_fll_csl_l0
nl_fl_csl_ll_tail)
let _ = assert (
let st = Control.new_state () in
(* n = 2, env1 x env2 env3 *)
(distribute_outter_list
[[([1;2], [Bvar("a");Bvar("b")], []);
([4;5], [Bvar("d");Bvar("e")], [])];
[([3], [Bvar("c")], []);
([6], [Bvar("f")], [])]])
[[([1;2], [Bvar("a");Bvar("b")], st);
([4;5], [Bvar("d");Bvar("e")], st)];
[([3], [Bvar("c")], st);
([6], [Bvar("f")], st)]])
=
[([[6]; [1; 2]], [[Bvar "f"]; [Bvar "a"; Bvar "b"]], []);
([[3]; [4; 5]], [[Bvar "c"]; [Bvar "d"; Bvar "e"]], [])]
[([[6]; [1; 2]], [[Bvar "f"]; [Bvar "a"; Bvar "b"]], st);
([[3]; [4; 5]], [[Bvar "c"]; [Bvar "d"; Bvar "e"]], st)]
)
let rec (draw_n_p_values : env_in -> int -> int -> Automata.t list->
(nll * ce * sl * sl) list list) =
(nll * cs * sl * sl) list list) =
fun input n p al ->
(* Draw n formula *)
let nl_f_ce_ll = rev_map (Automata.choose_n_formula n) al in
let nll_fl_ce_l = distribute_outter_list nl_f_ce_ll in
let nl_f_cs_ll = rev_map (Automata.choose_n_formula n) al in
let nll_fl_cs_l = distribute_outter_list nl_f_cs_ll in
(* Draw [p] solutions for each of the [n] formula. Whenever a formula
is unsatisfiable for numerical reasons, the automata a is
updated by [solve_formula_list] and returned in [new_a]. *)
let (nll_ce_sl_sl_ll, new_al) =
List.fold_left (solve_formula_list input p) ([], al) nll_fl_ce_l
let (nll_cs_sl_sl_ll, new_al) =
List.fold_left (solve_formula_list input p) ([], al) nll_fl_cs_l
in
let l = Util.count_empty_list nll_ce_sl_sl_ll in
let l = Util.count_empty_list nll_cs_sl_sl_ll in
if l = 0
then nll_ce_sl_sl_ll
then nll_cs_sl_sl_ll
else
(* At least one formula was not satisfiable because of numeric
constraints. We redraw as many times ([l]) as necessary. *)
rev_append nll_ce_sl_sl_ll (draw_n_p_values input l p new_al)
rev_append nll_cs_sl_sl_ll (draw_n_p_values input l p new_al)
(* Exported *)
let (env_try: int -> int -> env_in -> (nll * ce * env_out * env_loc) list) =
let (env_try: int -> int -> env_in -> (nll * cs * env_out * env_loc) list) =
fun n p input ->
let _ = Env_state.set_input input in
let cn_ll = (Env_state.current_nodes ()) in
let al = Automata.get cn_ll in
let nll_ce_sl_sl_ll = draw_n_p_values input n p al in
let nll_ce_sl_sl_l = flatten nll_ce_sl_sl_ll
let nll_cs_sl_sl_ll = draw_n_p_values input n p al in