Commit bd904a00 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Beautifying a little bit the code from places to places.

Actually, my first idea was to change Run_aut so that the fact that
several programs were run in parallel was hidden. But it turned out
to be a bad idea, because of numeric unsatisfiability + the
interaction between the module that choses a formula, and the one
that draw (performing the numeric satisfiability solving). Indeed,
when a formula appear to be unsatisfiable for numeric reason, we need
to backtrack in via Run_aut.choose_on_formula in one of the
Run_aut.t ; but of course if the list of Run_aut.t is hidden, we are
dead. One solution would have been to complicate a little bit the
Run_aut.t interface ; but my first motivation was actually to
simplify it...
parent 483092d0
......@@ -48,7 +48,7 @@ ldiff:
pdiff -r unstable
diff:
git diff HEAD -w > diff.diff
git diff HEAD -w > diff.diff && \
echo "il y a $(shell grep "+" diff.diff | wc -l) + et $(shell grep "-" diff.diff | wc -l) -"
touch:
......
......@@ -356,6 +356,7 @@ gnuplot-rif_clean:
##############################################################################"
.PHONY: lucky
lucky:
make -k nc -f Makefile.lucky OCAMLFLAGS=""
......@@ -714,10 +715,11 @@ allnc: libncnc lucky ltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c lu
static: libnc lucky_static ltop_static show_static stubs_static gen_luc_static
OTAGS=/local/jahier/jahier/bin/otags
tags:
$(OTAGS) -v $(shell ocamlc -where)/*.mli *.ml
tags: $(REALLY_ALL_SOURCES)
$(OTAGS) -v $(shell ocamlc -where)/*.mli $(REALLY_ALL_SOURCES)
# ne marche que si on lance cette commande A LA MAIN (!!!) depuis une fenetre DOS
strtopwin:
......
......@@ -134,5 +134,7 @@ all: nc
install: libinstall
-include $(OCAMLMAKEFILE)
......@@ -278,7 +278,7 @@ and
try
Lucky.env_step options.draw_mode htbl init_state ral
with
Run_aut.LuckyEnd ->
Run_aut.NoMoreFormula ->
List.iter
(fun n ->
output_string stdout ("# current node: " ^ (string_of_node n) ^ "\n"))
......@@ -343,7 +343,7 @@ and
try
Lucky.env_step options.draw_mode input state' ral
with
Run_aut.LuckyEnd ->
Run_aut.NoMoreFormula ->
List.iter
(fun n ->
output_string stdout ("# current node: " ^ (string_of_node n) ^ "\n"))
......
......@@ -26,54 +26,46 @@ type sl = subst list
(****************************************************************************)
let (draw_values : Var.env_in -> Env_state.t -> int ->
Thickness.numeric -> Run_aut.t list ->
Run_aut.t list * csl * (sl * sl) list) =
let (draw_values : Var.env_in -> Env_state.t -> int -> Thickness.numeric ->
Run_aut.t list -> Run_aut.t list * csl * (sl * sl) list) =
fun input state p num_thickness ral ->
let bool_to_gen_l = state.s.bool_vars_to_gen
and num_to_gen_l = state.s.num_vars_to_gen
and num_to_gen_l = state.s.num_vars_to_gen in
let list_to_formula l =
if l = [] then True else
List.fold_left (fun acc vn -> (And(Bvar(vn), acc)))
(Bvar(hd l)) (tl l)
in
let rec (draw_values_atomic : int -> Exp.var list -> Exp.var list ->
Run_aut.t -> Run_aut.t * cs * (sl * sl) list) =
fun p bool_to_gen num_to_gen ra ->
let bool_to_gen_f =
if bool_to_gen = [] then True else
List.fold_left
(fun acc vn -> (And(Bvar(vn), acc)))
(Bvar(hd bool_to_gen))
(tl bool_to_gen)
in
let (ra', f, cs) = Run_aut.choose_one_formula ra in
match
Solver.solve_formula input state p num_thickness f
bool_to_gen_f num_to_gen
with
| [] -> draw_values_atomic p bool_to_gen num_to_gen ra'
| outs_locs_l -> (ra', cs, outs_locs_l)
let bool_to_gen_fl = List.map list_to_formula bool_to_gen_l in
let rec loop_choose_formula bool_to_gen_f num_to_gen ra =
let ra, f, cs = Run_aut.choose_one_formula ra in
match Solver.solve_formula input state p num_thickness bool_to_gen_f num_to_gen f with
| [] -> (* The constraint is unsatisfiable because of the numerics *)
loop_choose_formula bool_to_gen_f num_to_gen ra
| sol_l -> ra, f, cs, sol_l
in
let ra_cs_slsll_l =
Util.list_map3 (draw_values_atomic p) bool_to_gen_l num_to_gen_l ral
let (ral, fl, csl, sol_ll) =
Util.list_split4(
Util.list_map3 loop_choose_formula bool_to_gen_fl num_to_gen_l ral)
in
let (ra0 ,cs0, slsl0) = List.hd ra_cs_slsll_l in
let (ral', csl, sl1_sl2_l) =
(* unknitting ...*)
List.fold_left
(fun (ral, csl, sl1_sl2_l) (ra, cs, slsll) ->
let sl1_sl2_l' =
List.map2
(fun (slacc1, slacc2) (sl1,sl2) ->
(rev_append sl1 slacc1, rev_append sl2 slacc2)
)
sl1_sl2_l
slsll
in
(ra::ral, cs::csl, sl1_sl2_l')
)
([ra0] ,[cs0], slsl0)
(List.tl ra_cs_slsll_l)
(* fl is a list of formula that should actually be considered
as a conjunction. But because of the thickness, when we
draw values in each formula in turn, we obtain a list of
list that ougth to be transposed. *)
let sol_ll : (sl * sl) list list = Util.transpose sol_ll in
let (merge_sol : (sl * sl) list -> sl * sl) =
fun sol_l -> (* Merge solutions coming from the fl: in other terms, we
interpret the formula list as a conjunction. *)
List.fold_left
(fun (acc1, acc2) (sl1,sl2) -> rev_append sl1 acc1, rev_append sl2 acc2)
([],[])
sol_l
in
(List.rev ral', List.rev csl, sl1_sl2_l)
let sol_l = List.map merge_sol sol_ll in
assert (List.length ral = List.length csl);
assert (List.length ral = List.length sol_l);
ral, csl, sol_l
(****************************************************************************)
(*****************************************************************************)
......@@ -166,7 +158,7 @@ let (env_try : Thickness.t -> env_in -> Env_state.t -> Run_aut.t list ->
let ral', _csl, acc' = env_try_do (snd bt,nt) input state ral acc in
f ral' acc'
with
Run_aut.LuckyEnd -> ral,acc
Run_aut.NoMoreFormula -> ral,acc
in
f ral []
else
......@@ -186,7 +178,7 @@ let (env_step : step_mode -> env_in -> Env_state.t -> Run_aut.t list ->
in
try
let (_ral', csl, soll) = env_try_do (1, thick) input state ral [] in
let (output, local) = List.hd soll in
let (output, local) = assert( soll <> []); List.hd soll in
let new_state_dyn = {
memory = update_pre input output local state;
ctrl_state = csl;
......@@ -203,7 +195,7 @@ let (env_step : step_mode -> env_in -> Env_state.t -> Run_aut.t list ->
previous_local := Some local;
(new_state, (output, local))
with
Run_aut.LuckyEnd ->
Run_aut.NoMoreFormula ->
match (!previous_output, !previous_local) with
| Some(out), Some(loc) ->
if state.s.reactive then
......@@ -222,7 +214,7 @@ let (env_step : step_mode -> env_in -> Env_state.t -> Run_aut.t list ->
"# No transition is labelled by a satisfiable formula.\n" ^
"# The Lucky automata is blocked.\n");
flush stdout;
raise Run_aut.LuckyEnd
raise Run_aut.NoMoreFormula
)
| _, _ -> raise Run_aut.LuckyEnd
| _, _ -> raise Run_aut.NoMoreFormula
......@@ -721,7 +721,7 @@ and
Lucky.env_try (bool_thickness, num_thickness) input state ral
with
| Not_found -> assert false
| Run_aut.LuckyEnd ->
| Run_aut.NoMoreFormula ->
List.iter
(fun n ->
output_string stdout ("# current node: " ^ (string_of_node n) ^ "\n "))
......@@ -753,7 +753,7 @@ and
let (next_state, (output, loc)) =
try
Lucky.env_step (options.step_mode) input state ral
with Run_aut.LuckyEnd ->
with Run_aut.NoMoreFormula ->
List.iter
(fun n ->
output_string stdout ("# current node: " ^ (string_of_node n) ^ "\n "))
......
......@@ -252,7 +252,6 @@ and
| Stream.Error e ->
syntax_error e ic tok "pragma_list" ""
(*******************************************************************************)
(* Parse a type of a typedef definition *)
......
......@@ -34,7 +34,8 @@ type dyn_weight = V of int | Infin
The automaton stops if one of the sub-automata stops.
*)
type t =
type t =
| Cont of (unit -> t * Exp.formula * Parse_luc.ctrl_state)
| Finish (* no more solutions *)
......@@ -219,18 +220,16 @@ and
tbl2, ntbl2
(****************************************************************************)
(* Exported *)
exception LuckyEnd
exception NoMoreFormula
let (call_cont : t -> t * formula * Parse_luc.ctrl_state) =
let (call_cont : t -> t * formula * Parse_luc.ctrl_state) =
fun cont ->
let _ = if debug then (print_string "XXX call_cont\n"; flush stdout) in
match cont with
| Cont f -> f ()
| Finish -> raise LuckyEnd
(* Finish, False, [] *)
match cont with
| Cont f -> f ()
| Finish -> raise NoMoreFormula
let (call_wt_cont : wt_cont -> wt_cont * formula * Parse_luc.node) =
fun cont ->
......@@ -240,62 +239,67 @@ let (call_wt_cont : wt_cont -> wt_cont * formula * Parse_luc.node) =
| WFinish -> WFinish, False, ""
(* exported *)
let (no_more_solution : t -> bool) = (fun t -> t = Finish)
let (choose_one_formula: t -> t * Exp.formula * Parse_luc.ctrl_state) = call_cont
(****************************************************************************)
let (no_more_formula : t -> bool) = fun t -> t = Finish
(* exported *)
let (choose_one_formula: t -> t * Exp.formula * Parse_luc.ctrl_state) = call_cont
let (get_all_formula: t -> formula list) =
fun a ->
let rec aux a acc =
let (a', f, _nl) = choose_one_formula a in
if no_more_formula a' then acc else (aux a' (f::acc))
in
aux a []
(****************************************************************************)
let rec (wt_list_to_cont : Var.env_in -> Env_state.t -> wt_cont list ->
formula -> Parse_luc.ctrl_state -> t -> t) =
fun input state wtl facc nl cont ->
fun input state wtl facc nl fgen ->
(* [nl] is the list of nodes that correspond to [facc] *)
let _ = if debug then (print_string "XXX wt_list_to_cont\n"; flush stdout) in
match wtl with
| [] -> Cont (fun () -> (cont, facc, nl))
| wt::wtl' ->
if wt = WFinish then
cont
(* let (cont', facc', nl') = call_cont cont in *)
(* wt_list_to_cont input state wtl facc' nl' cont' *)
else
match choose_one_formula_atomic input state facc wt with
| WFinish, False, "" ->
cont
(* let (cont', facc', nl') = call_cont cont in *)
(* wt_list_to_cont input state wtl facc' nl' cont' *)
| wt2, f2, n ->
let cont' =
Cont (fun () ->
call_cont (wt_list_to_cont input state (wt2::wtl') facc nl cont)
)
in
wt_list_to_cont input state wtl' f2 (n::nl) cont'
match wtl with
| [] -> Cont (fun () -> (fgen, facc, nl))
| wt::wtl' ->
if wt = WFinish then
fgen
else
match choose_one_formula_atomic input state facc wt with
| WFinish, False, "" ->
fgen
| wt2, f2, n ->
let fgen' =
Cont (fun () ->
call_cont (wt_list_to_cont input state (wt2::wtl') facc nl fgen))
in
wt_list_to_cont input state wtl' f2 (n::nl) fgen'
and
(choose_one_formula_atomic : Var.env_in -> Env_state.t ->
Exp.formula -> wt_cont -> wt_cont * formula * Parse_luc.node) =
(choose_one_formula_atomic : Var.env_in -> Env_state.t ->
Exp.formula -> wt_cont -> wt_cont * formula * Parse_luc.node) =
fun input state facc cont ->
let _ = if debug then (print_string "XXX choose_one_formula_atomic\n"; flush stdout) in
if cont = WFinish then
WFinish, False, ""
else
let (cont', f, n) = call_wt_cont cont in
let _ = if debug then (print_string ("XXX "^ n ^ "\n"); flush stdout) in
let facc' =
match f,facc with
True, True -> True
| True, f -> f
| f, True -> f
| _,_ -> And(f,facc)
in
if
(Solver.is_satisfiable input state facc' "")
then
(cont', facc', n)
else
choose_one_formula_atomic input state facc cont'
if cont = WFinish then
WFinish, False, ""
else
let (cont', f, n) = call_wt_cont cont in
let _ = if debug then (print_string ("XXX "^ n ^ "\n"); flush stdout) in
let facc' =
match f,facc with
True, True -> True
| True, f -> f
| f, True -> f
| _,_ -> And(f,facc)
in
if
(Solver.is_satisfiable input state facc' "")
then
(cont', facc', n)
else
choose_one_formula_atomic input state facc cont'
and (wt_to_cont : Var.env_in -> Env_state.t -> wt -> wt_cont -> wt_cont) =
fun input state (tbl, n) cont ->
......@@ -333,7 +337,7 @@ and (wt_to_cont : Var.env_in -> Env_state.t -> wt -> wt_cont -> wt_cont) =
let tbl' = NodeMap.add n (Children l2') tbl in
let tbl'' = NodeMap.remove n tbl in (* to optimize mem *)
let cont' = WCont(fun () ->
call_wt_cont (wt_to_cont input state (tbl', n) cont)
call_wt_cont (wt_to_cont input state (tbl', n) cont)
)
in
wt_to_cont input state (tbl'', nt) cont'
......@@ -342,7 +346,7 @@ and (wt_to_cont : Var.env_in -> Env_state.t -> wt -> wt_cont -> wt_cont) =
let tbl' = NodeMap.add n (Children l2) tbl in
let tbl'' = NodeMap.remove n tbl in
let cont' = WCont(fun () ->
call_wt_cont (wt_to_cont input state (tbl', n) cont)
call_wt_cont (wt_to_cont input state (tbl', n) cont)
)
in
wt_to_cont input state (tbl'', nt) cont'
......@@ -355,7 +359,6 @@ and (wt_to_cont : Var.env_in -> Env_state.t -> wt -> wt_cont -> wt_cont) =
(****************************************************************************)
(* exported *)
let (get : Var.env_in -> Env_state.t -> Parse_luc.ctrl_state list -> t list) =
fun input state nll ->
......@@ -369,11 +372,3 @@ let (get : Var.env_in -> Env_state.t -> Parse_luc.ctrl_state list -> t list) =
)
nll
(* exported *)
let (get_all_formula: t -> formula list) =
fun a ->
let rec aux a acc =
let (a', f, _nl) = choose_one_formula a in
if no_more_solution a' then acc else (aux a' (f::acc))
in
aux a []
......@@ -69,20 +69,18 @@ val get : Var.env_in -> Env_state.t -> Parse_luc.ctrl_state list -> t list
*)
val get_all_formula : t -> (Exp.formula) list
(** gets all the formulas accessible from the current node. *)
(** Raised by choose_one_formula no more transitions can be taken *)
exception LuckyEnd
exception NoMoreFormula
val choose_one_formula : t -> t * Exp.formula * Parse_luc.ctrl_state
val choose_one_formula : t -> t * Exp.formula * Parse_luc.ctrl_state
(** [choose_one_formula run_aut] draws a formula accessible from
the current node, and returns:
- a failure continuation to be used if the formula do not
have (numeric) solutions.
- a formula
- the corresponding nodes in the static automata
- a failure continuation to be used if one wants to draw another formula.
- A formula (nb1).
- The program point that corresponds to the choice that has been made.
*)
val no_more_solution : t -> bool
val get_all_formula : t -> (Exp.formula) list
(** gets all the formulas accessible from the current node. *)
......@@ -343,9 +343,9 @@ let (draw : Var.env_in -> Env_state.t -> Thickness.numeric ->
(* Exported *)
let (solve_formula: Var.env_in -> Env_state.t -> Thickness.formula_draw_nb ->
Thickness.numeric -> formula -> formula -> var list ->
Thickness.numeric -> formula -> var list -> formula ->
(subst list * subst list) list) =
fun input state p num_thickness f bool_vars_to_gen_f num_vars_to_gen ->
fun input state p num_thickness bool_vars_to_gen_f num_vars_to_gen f ->
let bdd = (Formula_to_bdd.f input state f) in
let _ =
......
......@@ -20,9 +20,9 @@ val is_satisfiable : Var.env_in -> Env_state.t -> Exp.formula -> string -> bool
*)
val solve_formula : Var.env_in -> Env_state.t -> Thickness.formula_draw_nb ->
Thickness.numeric -> Exp.formula -> Exp.formula -> Exp.var list ->
Thickness.numeric -> Exp.formula -> Exp.var list -> Exp.formula ->
(Var.subst list * Var.subst list) list
(** [solve_formula input state fdn tn f bools nums] randomly assigns
(** [solve_formula input state fdn tn bools nums f] randomly assigns
[tn] values to variables in [bools] and [nums] (which ought to
contains all output and local variables occurring in the formula
[f]). It returns a list (of length [tn]) of pairs, where the left
......
......@@ -290,6 +290,19 @@ let rec (list_map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) -> 'a list -> 'b li
(f e1 e2 e3 e4 e5 e6)::(list_map6 f t1 t2 t3 t4 t5 t6)
| _ -> failwith ("*** Error: list_map6 should be called with lists "
^ "of the same size.\n")
let rec (list_split3: ('a * 'b * 'c) list -> 'a list * 'b list * 'c list) =
function
| [] -> ([], [], [])
| (x,y,z)::l ->
let (rx, ry, rz) = list_split3 l in (x::rx, y::ry, z::rz)
let rec (list_split4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list) =
function
| [] -> ([], [], [], [])
| (x,y,z,t)::l ->
let (rx, ry, rz, rt) = list_split4 l in (x::rx, y::ry, z::rz, t::rt)
(** checks that a list does not contain any duplicate *)
......@@ -775,6 +788,15 @@ let print_fll std fll =
(********************************************************************)
let rec transpose m =
assert (m <> []);
if List.mem [] m then [] else
try
List.map List.hd m :: transpose (List.map List.tl m)
with _ -> assert false
(********************************************************************)
let safe_remove_file file =
try Sys.remove file
with Sys_error _ -> ()
......
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