Commit 2e09ef45 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Fix a bug (in LucFGen) where the exception Invalid_argument("Random.int") was...

Fix a bug (in LucFGen) where the exception Invalid_argument("Random.int") was raised on some Lutin programs.

It was occuring when all outgoing transitions were labelled by the
null weigth.
parent f51debc4
......@@ -87,7 +87,10 @@ let (set_between : string -> int -> int -> int -> state -> state) =
(* exported *)
let (draw_between : string -> int -> int -> state -> state) =
fun id min max st ->
let draw = min + (Random.int (max - min + 1)) in
let draw =
assert(max - min + 1 > 0);
min + (Random.int (max - min + 1))
in
StringMap.add id (draw, (Some(min, max))) st
(* exported *)
......
......@@ -130,11 +130,11 @@ and
| _,_ -> And(f,facc)
in
let ctx_msg = Prog.ctrl_state_to_string_long state.d.ctrl_state in
Utils.time_C "is_sat";
let sat = (Solver.is_satisfiable input state.d.memory state.d.verbose ctx_msg facc' "") in
Utils.time_R "is_sat";
if sat then (cont', facc', n)
else choose_one_formula_atomic input state facc cont'
Utils.time_C "is_sat";
let sat = (Solver.is_satisfiable input state.d.memory state.d.verbose ctx_msg facc' "") in
Utils.time_R "is_sat";
if sat then (cont', facc', n)
else choose_one_formula_atomic input state facc cont'
and (wt_to_cont : Var.env_in -> Prog.state -> wt -> wt_cont -> wt_cont) =
......@@ -153,31 +153,32 @@ and (wt_to_cont : Var.env_in -> Prog.state -> wt -> wt_cont -> wt_cont) =
| [] ->
let get_weigth dw =
match dw with
| V i -> i
| V i -> if i < 0 then 0 else i (* a negative weight means null weigth *)
| Infin -> assert false
in
let w_sum =
List.fold_left (fun acc (dw,_) -> acc+(get_weigth dw)) 0 l2
in
let j = 1 + Random.int w_sum in
let rec get_jth_trans j list acc =
match list with
[] -> assert false
| (dw,nt)::tail ->
let newj = j - (get_weigth dw) in
if (newj < 1) then
nt, (rev_append acc tail)
else
get_jth_trans newj tail ((dw,nt)::acc)
in
let (nt,l2') = get_jth_trans j l2 [] in
let tbl' = Util.StringMap.add n (Children l2') tbl in
let tbl'' = Util.StringMap.remove n tbl in (* to optimize mem *)
let cont' = WCont(fun () ->
call_wt_cont (wt_to_cont input state (tbl', n) cont)
)
in
wt_to_cont input state (tbl'', nt) cont'
if w_sum = 0 then cont else
let j = 1 + Random.int w_sum in
let rec get_jth_trans j list acc =
match list with
[] -> assert false
| (dw,nt)::tail ->
let newj = j - (get_weigth dw) in
if (newj < 1) then
nt, (rev_append acc tail)
else
get_jth_trans newj tail ((dw,nt)::acc)
in
let (nt,l2') = get_jth_trans j l2 [] in
let tbl' = Util.StringMap.add n (Children l2') tbl in
let tbl'' = Util.StringMap.remove n tbl in (* to optimize mem *)
let cont' = WCont(fun () ->
call_wt_cont (wt_to_cont input state (tbl', n) cont)
)
in
wt_to_cont input state (tbl'', nt) cont'
| [(_,nt)] ->
let tbl' = Util.StringMap.add n (Children l2) tbl in
......
Supports Markdown
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