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

lurette 0.64 Fri, 10 May 2002 16:32:32 +0200 by jahier

Parent-Version:      0.63
Version-Log:

Add support for loop Gauss.

Fix a bug in the handling of loops where lurette (and ima_exe) was
stopping whenever the body of a loop contains no satisfiable formula
whereas the endLoop branch should be taken in that case.

Project-Description: Lurette
parent 9d1e0221
......@@ -4,11 +4,11 @@
(test/usager.env 523 1019479246 b/14_usager.env 1.7)
(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 13131 1020777170 51_env_state. 1.19)
(source/env_state.ml 13457 1021041152 51_env_state. 1.20)
(source/graph.ml 1819 1016011748 14_graph.ml 1.5)
(bin/Makefile.ima_exe 1926 1020420514 b/41_Makefile.i 1.2)
(source/util.ml 12330 1020777170 35_util.ml 1.19)
(source/wtree.ml 11388 1020420514 b/1_wtree.ml 1.11)
(source/util.ml 13368 1021041152 35_util.ml 1.20)
(source/wtree.ml 13232 1021041152 b/1_wtree.ml 1.12)
(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)
......@@ -17,7 +17,7 @@
(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 8072 1020420514 16_env.ml 1.25)
(source/env.ml 8154 1021041152 16_env.ml 1.26)
(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)
......@@ -27,26 +27,26 @@
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(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 9327 1020777170 b/32_ima_exe.ml 1.8)
(source/ima_exe.ml 9687 1021041152 b/32_ima_exe.ml 1.9)
(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 36477 1020777170 24_generate_l 1.25)
(source/parse_env.ml 18485 1020420514 41_parse_env. 1.18)
(source/parse_env.ml 18459 1021041152 41_parse_env. 1.19)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/sim2chro.ml 2653 1020777170 b/24_sim2chro.m 1.8)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/formula.mli 3646 1020420514 44_formula.ml 1.12)
(source/formula.mli 3640 1021041152 44_formula.ml 1.13)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/command_line.mli 1421 1017929190 b/21_command_li 1.6)
(source/wtree.mli 3417 1020420514 b/0_wtree.mli 1.9)
(source/wtree.mli 3417 1021041152 b/0_wtree.mli 1.10)
(test/porte.env 1130 1019479246 b/16_porte.env 1.6)
(source/env_state.mli 5850 1020420514 50_env_state. 1.17)
(source/env_state.mli 5887 1021041152 50_env_state. 1.18)
(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 22285 1020777170 17_OcamlMakef 1.28)
(OcamlMakefile 22550 1021041152 17_OcamlMakef 1.29)
(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)
......@@ -61,12 +61,12 @@
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(test/heater_float.lus 175 1020068208 b/44_heater_flo 1.1)
(test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
(source/print.mli 789 1016803757 46_print.mli 1.8)
(source/print.mli 844 1021041152 46_print.mli 1.9)
(test/heater_int.lus 170 1020068208 b/43_heater_int 1.1)
(source/graph.mli 1499 1020432102 13_graph.mli 1.7)
(test/heater_int.rif.exp 858 1017837703 b/28_heater_int 1.2)
(source/formula.ml 7348 1020777170 45_formula.ml 1.14)
(source/formula.ml 7387 1021041152 45_formula.ml 1.15)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/print.ml 6587 1020420514 47_print.ml 1.15)
(source/print.ml 6771 1021041152 47_print.ml 1.16)
(test/vrai_tram.h 2468 1012914629 b/7_vrai_tram. 1.2)
(bin/Makefile.show_ima 958 1020432102 b/40_Makefile.s 1.3)
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.28 Tue, 07 May 2002 15:12:50 +0200 jahier $
# $Id: OcamlMakefile 1.29 Fri, 10 May 2002 16:32:32 +0200 jahier $
#
###########################################################################
# Set these variables to the names of the sources to be processed and
......@@ -520,7 +520,14 @@ test:
\
ls -l test1.res test2.res test3.res
ima:
pushd ~/lurette/bin ; make -k dc -f Makefile.ima_exe OCAMLFLAGS=""; popd
ima_nc:
pushd ~/lurette/bin ; make -k clean -f Makefile.ima_exe ; make -k nc -f Makefile.ima_exe ; popd
show:
pushd ~/lurette/bin ; make -k dc -f Makefile.sho_ima OCAMLFLAGS=""; popd
heater:
$(LURETTE_PATH)/make_lurette heater_int; \
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 63)
(Parent-Version lurette 0 62)
(Project-Version lurette 0 64)
(Parent-Version lurette 0 63)
(Version-Log "
Reimplement the rif parsing in ima_exe.ml so that it is correct wrt the BLA-RIF doc.
Add support for loop Gauss.
Fix a bug in the handling of loops where lurette (and ima_exe) was
stopping whenever the body of a loop contains no satisfiable formula
whereas the endLoop branch should be taken in that case.
")
(New-Version-Log "")
(Checkin-Time "Tue, 07 May 2002 15:12:50 +0200")
(Checkin-Time "Fri, 10 May 2002 16:32:32 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -20,7 +24,7 @@ Reimplement the rif parsing in ima_exe.ml so that it is correct wrt the BLA-RIF
;; 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.8 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.9 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))
......@@ -37,9 +41,9 @@ Reimplement the rif parsing in ima_exe.ml so that it is correct wrt the BLA-RIF
(source/graph.ml (lurette/14_graph.ml 1.5 644))
(source/env.mli (lurette/15_env.mli 1.13 644))
(source/env.ml (lurette/16_env.ml 1.25 644))
(source/env.ml (lurette/16_env.ml 1.26 644))
(source/util.ml (lurette/35_util.ml 1.19 644))
(source/util.ml (lurette/35_util.ml 1.20 644))
(source/solver.mli (lurette/38_solver.mli 1.11 644))
(source/solver.ml (lurette/39_solver.ml 1.21 644))
......@@ -48,25 +52,25 @@ Reimplement the rif parsing in ima_exe.ml so that it is correct wrt the BLA-RIF
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.6 644))
(source/parse_env.mli (lurette/40_parse_env. 1.7 644))
(source/parse_env.ml (lurette/41_parse_env. 1.18 644))
(source/parse_env.ml (lurette/41_parse_env. 1.19 644))
(source/show_env.mli (lurette/42_show_env.m 1.6 644))
(source/show_env.ml (lurette/43_show_env.m 1.7 644))
(source/formula.mli (lurette/44_formula.ml 1.12 644))
(source/formula.ml (lurette/45_formula.ml 1.14 644))
(source/formula.mli (lurette/44_formula.ml 1.13 644))
(source/formula.ml (lurette/45_formula.ml 1.15 644))
(source/print.mli (lurette/46_print.mli 1.8 644))
(source/print.ml (lurette/47_print.ml 1.15 644))
(source/print.mli (lurette/46_print.mli 1.9 644))
(source/print.ml (lurette/47_print.ml 1.16 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.17 644))
(source/env_state.ml (lurette/51_env_state. 1.19 644))
(source/env_state.mli (lurette/50_env_state. 1.18 644))
(source/env_state.ml (lurette/51_env_state. 1.20 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.9 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.11 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.10 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.12 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.4 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.8 644))
......@@ -80,7 +84,7 @@ Reimplement the rif parsing in ima_exe.ml so that it is correct wrt the BLA-RIF
(make_lurette (lurette/27_make_luret 1.12 744))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.28 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.29 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.3 644))
(bin/Makefile.show_ima (lurette/b/40_Makefile.s 1.3 644))
......
......@@ -95,6 +95,8 @@ let (solve_formula_list_list: env_in -> int
in
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
......@@ -104,6 +106,8 @@ let (compute_wtrees: node list list -> Wtree.wtree list) =
[[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 * 'c list) list list ->
('a list list * 'f list list * 'c list list) list) =
......@@ -135,13 +139,12 @@ let _ = assert (
[([3], [Bvar("c")], []);
([6], [Bvar("f")], [])]])
=
[[[3]; [1; 2]], [[Bvar "c"]; [Bvar "a"; Bvar "b"]], [[];[]];
[[6]; [4; 5]], [[Bvar "f"]; [Bvar "d"; Bvar "e"]], [[];[]]
]
)
[[[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_cal_l__wt__l =
(* Draw n formula *)
......@@ -163,10 +166,9 @@ let rec draw_n_p_values input n p cn_ll wtl =
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. *)
constraints. We redraw as many times ([l]) as necessary. *)
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 ->
......
......@@ -271,6 +271,20 @@ let (dec_loop_cpt: node -> unit) =
let f = Hashtbl.find env_state.loop_cpt_tbl node in
Hashtbl.replace env_state.loop_cpt_tbl node (f -. 1.)
(* Exported *)
let (print_loop_cpt_tbl: unit -> unit) =
fun _ ->
print_string "loop counter table:\n";
Hashtbl.iter
(fun i f ->
print_string "Node " ;
print_int i ;
print_string (" -> " ^ (string_of_float f) ^ "\n")
)
env_state.loop_cpt_tbl;
print_string "\n";
flush stdout
(****************************************************************************)
let (bdd : formula -> Bdd.t) =
fun f ->
......@@ -293,7 +307,6 @@ let (set_bdd_global : formula -> Bdd.t -> unit) =
fun f bdd ->
Hashtbl.replace env_state.bdd_tbl_global f bdd
(****************************************************************************)
let (index_cpt: unit -> int) =
fun _ ->
......
......@@ -177,3 +177,4 @@ val set_loop_cpt: node -> float -> unit
val get_loop_cpt: node -> float
val dec_loop_cpt: node -> unit
val print_loop_cpt_tbl: unit -> unit
......@@ -55,11 +55,11 @@ type cpt_init =
| LoopInf
| Loop of int
| LoopBetween of int * int
(* | LoopGauss of float * float *)
| LoopGauss of float * float
type arc = node * node
type arc_info = weigth * formula_eps * cpt_init
type arc_info = weigth * formula_eps * cpt_init
type var_name = string
type vn = var_name
......@@ -197,7 +197,7 @@ let (cpt_init_to_string: cpt_init -> string) =
| LoopBetween(min, max) ->
(" : Loop [" ^ (string_of_int min) ^ ", "
^ (string_of_int max) ^ "]")
| LoopGauss(mean, var) -> assert false
let (arc_info_to_string : arc_info -> string) =
fun (weigth, formula_eps, cpt_init) ->
......
......@@ -58,7 +58,7 @@ type cpt_init =
| LoopInf
| Loop of int
| LoopBetween of int * int
(* | LoopGauss of float * float *)
| LoopGauss of float * float
type arc = node * node
type arc_info = weigth * formula_eps * cpt_init
......
......@@ -291,9 +291,27 @@ and
and
main_loop t =
let _ = print_string ("\n# step " ^ (string_of_int t) ^ ":\n"); flush stdout in
let previous_nodes = (Env_state.current_nodes ()) in
let nl = List.flatten previous_nodes in
let _ =
print_string ("\n# step " ^ (string_of_int t) ^ " (") ;
if (List.length nl) > 1
then
(
print_string "current nodes are ";
List.iter
(fun n -> print_string ((string_of_int n) ^ " "))
(List.tl nl)
)
else
(
print_string "current node is ";
print_string (string_of_int (List.hd nl))
);
print_string ("):\n") ;
flush stdout
in
let input = read_rif_input (Env_state.in_env_unsorted ()) in
let nll_call_out_loc_list = Env.env_try 1 1 input in
......
......@@ -345,8 +345,8 @@ and (parse_cpt_init: vnt list -> aut_token -> cpt_init) =
| [< 'Genlex.Ident "loop_inf" >] -> LoopInf
| [< 'Genlex.Ident "loop_between" ; 'Genlex.Int min ; 'Genlex.Int max
>] -> LoopBetween(min, max)
| [< 'Genlex.Ident "loop_gauss" ; 'Genlex.Float i ; 'Genlex.Float i
>] -> failwith "*** loop_gauss not yet handled, sorry.\n"
| [< 'Genlex.Ident "loop_gauss" ; 'Genlex.Float mean ; 'Genlex.Float var
>] -> LoopGauss(mean, var)
with e ->
print_err_msg tok_list "parse_cpt_init" ;
raise e
......
......@@ -38,6 +38,12 @@ let (int_string_hashtbl: (int, string) Hashtbl.t -> unit) =
(fun i str -> print_int i ; print_string (" : " ^ str ^ "\n"))
t
let (int_float_hashtbl: (int, float) Hashtbl.t -> unit) =
fun t ->
Hashtbl.iter
(fun i f -> print_int i ; print_string (" : " ^ (string_of_float f) ^ "\n"))
t
let (string_int_hashtbl: (string, int) Hashtbl.t -> unit) =
fun t ->
Hashtbl.iter
......@@ -132,6 +138,7 @@ let (pwtt: wtree_table -> unit) =
) wtt ;
flush stdout
(*
let (comb2: Bdd.t -> unit) =
fun supp ->
......
......@@ -5,6 +5,7 @@ open Formula
val atomic_formula : Formula.atomic_formula -> unit
val int_string_hashtbl : (int, string) Hashtbl.t -> unit
val int_float_hashtbl : (int, float) Hashtbl.t -> unit
val string_int_hashtbl : (string, int) Hashtbl.t -> unit
val string_var_value_hashtbl: (string, var_value) Hashtbl.t -> unit
......
......@@ -130,8 +130,8 @@ let rec list_fold_left3 f accu l1 l2 l3 =
(** A special kind of map that applies a function that returns an
[option] value, and which only returns the list of success
values (I.e., the non [None] ones). *)
[option] value, and which only returns the list of successes
(i.e., the non [None] ones). *)
let rec (list_map_option: ('a -> 'b option) -> 'a list -> 'b list) =
fun f l ->
match l with
......@@ -282,6 +282,39 @@ let rec (is_substring: string -> string -> bool) =
true
with Not_found -> false
(** [gauss_draw m d] generates a gaussian pseudo-random number of
mean [m] and deviation [d]. The generation algorithm is based on the
so-called << polar form of the Box-Muller transformation >> that I
found it at the url http://www.taygeta.com/random/gaussian.html
*)
let rec (gauss_draw : float -> float -> float) =
fun m d ->
let x1 = ((Random.float 2.) -. 1.)
and x2 = ((Random.float 2.) -. 1.) in
let w = x1 *. x1 +. x2 *. x2 in
if w >= 1.
then gauss_draw m d
else
let w2 = sqrt( (-2.0 *. (log w) ) /. w ) in
(x1 *.w2 *. d) +. m
(** Ditto, but returns 2 numbers. Indeed, the Box-Muller algorithm
computes 2 of them anyway... *)
let rec (gauss_draw2 : float -> float -> float * float) =
fun m d ->
let x1 = ((Random.float 2.) -. 1.)
and x2 = ((Random.float 2.) -. 1.) in
let w = x1 *. x1 +. x2 *. x2 in
if w >= 1.
then gauss_draw2 m d
else
let w2 = sqrt( (-2.0 *. (log w) ) /. w ) in
let y1 = (x1 *.w2 *. d) +. m
and y2 = (x2 *.w2 *. d) +. m in
(y1, y2)
(****************************************************************************)
(* XXX How can I dynamically choose among one of those ? *)
......
......@@ -174,20 +174,50 @@ and
(* exported *)
let rec (build_wtree: wgraph -> node -> wtree) =
fun graph node ->
(**
Builds the wtree of [graph] starting from [node].
*)
let wt = build_wtree_acc graph [] node in
wt
(** Builds the [wtree] of [graph] starting from [node]. *)
let wt = build_wtree_acc false graph [] node in
try
let nlc = Env_state.get_loop_cpt node in
if nlc = 0.
then wt
else
(*
If the current node is a loop node and if its loop cpt
is different from 0, then we also compute the [wtree]
corresponding to the case where this cpt is 0, because
it will be needed whenever no formula is satisfiable
in the loop. Note that we compute it in a second pass
to avoid loops via epsilon transitions. A boolean flag
is used in argument of build_wtree_acc to associate a
weigth of 0 to that branch. Then later, when drawing a
formula in the wtree, those formula with weigth 0 will
be taken if no more formula with non-0 weigth can be
taken (because all of them are insatisfiable).
*)
let _ = Env_state.set_loop_cpt node 0. in
let wt_backtrack = build_wtree_acc true graph [] node in
Env_state.set_loop_cpt node nlc ;
(append wt wt_backtrack)
with Not_found
(* Current node is not a loop node *)
-> wt
and
(build_wtree_acc: wgraph -> cpt_action list -> node -> wtree) =
fun graph actions node ->
let list = Graph.get_list_of_target_nodes graph node in
Util.list_map_option (target_nodes_to_wnode graph actions node) list
(build_wtree_acc: bool -> wgraph -> cpt_action list -> node -> wtree) =
fun flag graph actions node ->
(*
The flag in first argument says whether to put a weigth of
1 or 0 to arcs that correspond to end of loops (flag iff
weigth = 0).
*)
let tnl = Graph.get_list_of_target_nodes graph node in
Util.list_map_option (target_nodes_to_wnode flag graph actions node) tnl
and
(target_nodes_to_wnode: wgraph -> cpt_action list -> node
-> node * (weigth * formula_eps * cpt_init) -> wnode option) =
fun graph actions0 nf (nt, (w, f_eps, cpt_init)) ->
(target_nodes_to_wnode: bool -> wgraph -> cpt_action list -> node
-> node * arc_info -> wnode option) =
fun flag graph actions0 nf (nt, (w, f_eps, cpt_init)) ->
(* Returns an option type because some arcs migth be labelled by
a 0 weigth (Loop body for which the loop counter is 0) so we
do not want to have them in the resulting [wtree] *)
let actions1 =
match cpt_init with
NoLoop -> actions0
......@@ -196,11 +226,14 @@ and
| LoopBetween(min, max) ->
let i = min + (Random.int (max - min + 1)) in
(append actions0 [Init(nt, float_of_int i)])
(* | LoopGauss(min, max) -> *)
| LoopGauss(mean, var) ->
let f = Util.gauss_draw mean var in
let i = if f -. (ceil f) < 0.5 then f else f +. 1. in
(append actions0 [Init(nt, i)])
in
let rec (search_init_nf: cpt_action list -> cpt_action list) =
fun cal ->
(** remove from [cal] all the left-most elts of [cal] that do
(** Removes from [cal] all the left-most elts of [cal] that do
not match with Init(nf, _) *)
match cal with
(Dec(_))::tail -> search_init_nf tail
......@@ -210,40 +243,39 @@ and
else search_init_nf tail
| [] -> []
in
let (cpt_loop0, actions_foo) =
let (cpt_loop0, actions_to_perform) =
match (search_init_nf actions0) with
(Init(nf, i))::tail -> (i, tail)
| [] -> (
try ((Env_state.get_loop_cpt nf), actions0)
with Not_found -> (0., actions0)
with Not_found ->
(* iff [nf] is not a loop node *)
(0., actions0)
)
| _::_ -> assert false
in
let (count_number_of_dec: node -> cpt_action list -> float) =
fun node cal ->
let match_dec = fun x -> match x with Dec(node) -> true | _ -> false in
float_of_int (length (find_all (match_dec) cal))
in
let cpt_loop = (cpt_loop0 -. (count_number_of_dec nf actions_foo)) in
let cpt_loop = (cpt_loop0 -. (count_number_of_dec nf actions_to_perform)) in
match (w, f_eps) with
(LoopBody, Eps) ->
if (cpt_loop = 0.)
then None
else Some (N(1, (build_wtree_acc graph (append actions1 [Dec(nf)]) nt)))
else Some (N(1, (build_wtree_acc false graph (append actions1 [Dec(nf)]) nt)))
| (LoopEnd, Eps) ->
if (cpt_loop = 0.)
then Some (N(1, (build_wtree_acc graph actions1 nt)))
then
if flag
then Some (N(0, (build_wtree_acc false graph actions1 nt)))
else Some (N(1, (build_wtree_acc false graph actions1 nt)))
else None
| (W(w), Eps) -> Some (N(w, (build_wtree_acc graph actions1 nt)))
| (W(w), Eps) -> Some (N(w, (build_wtree_acc flag graph actions1 nt)))
| (W(w), Form(f)) -> Some (L(w, [nt], [f], actions1))
| (LoopBody, Form(_)) -> assert false
| (LoopEnd, Form(_)) -> assert false
(****************************************************************************)
(****************************************************************************)
(****************************************************************************)
(****************************************************************************)
......@@ -286,20 +318,30 @@ let rec (choose_a_formula: wtree -> node list * formula list * cpt_action list)
(** Draws a formula in [wt] according to node weigths; also
returns the list of their corresponding target nodes. *)
let wt_size = sigma_wtree wt in
let _ =
if (wt_size = 0)
then
raise Not_found
in
let j =
if (wt_size = 1)
then 1
else (Random.int wt_size) + 1
in
let wn = pick_jth_elt wt j in
match wn with
L(_, nodes_to, fl, actions) -> (nodes_to, fl, actions)
| N(_, swt) -> choose_a_formula swt
(* If no more formula with non-0 weigth are left, we take the
transition with weigth 0 (EndLoop branches) if any. By
construction, there should not be more than one such
transition. *)
match wt with
[N(0, swt)] -> choose_a_formula swt
| [] -> raise Not_found
| _::_ -> assert false
else
let j =
if (wt_size = 1)
then 1
else (Random.int wt_size) + 1
in
let wn = pick_jth_elt wt j in
match wn with
L(w1, nodes_to, fl, actions) ->
assert (w1 <> 0);
(nodes_to, fl, actions)
| N(w1, swt) ->
assert (w1 <> 0);
choose_a_formula swt
type fooT = ((node list * formula list * cpt_action list) list * wtree)
......
......@@ -82,8 +82,8 @@ val wtree_product: wtree -> wtree -> wtree
val build_wtree: wgraph -> node -> wtree
(** [build_wtree graph node] builds the wtree of [graph]
starting from [node]. *)
(** [build_wtree graph node] builds the wtree of [graph] starting
from [node]. *)
val cpt_action_to_string : cpt_action -> string
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment