Skip to content

GitLab

L
lutin
Commit 7a6ac267 authored by erwan's avatar erwan
Browse files
Options

Update: monadisation of Lutin, part 3. 

Rationale: make rdbg time traveling work.
parent c2eb6c77
Hide whitespace changes
Inline Side-by-side
Showing with 639 additions and 612 deletions
lutin/src/auto2Lucky.ml
View file @ 7a6ac267
......@@ -175,7 +175,7 @@ let make
) in
fprintf os "nodes {\n" ;
Hashtbl.iter print_state (AutoGen.states auto) ;
Util.StringMap.iter print_state (AutoGen.states auto) ;
fprintf os "}\n" ;
fprintf os "start_node { %s }\n" (AutoGen.init_control auto) ;
......
lutin/src/autoGen.ml
View file @ 7a6ac267
......@@ -32,7 +32,6 @@ open CoTraceExp ;;
open LutPredef ;;
open Expand ;;
let dbg = Verbose.get_flag "AutoGen"
(** N.B. On utilise des AlgExp.t de type "CkTypeEff.weight" pour
......@@ -127,30 +126,40 @@ type trans = {
dest: string;
}
module TraceMap = struct
include Map.Make(struct type t = CoTraceExp.t let compare = compare end)
end
module ConfigMap = struct
include Map.Make(struct type t = config let compare = compare end)
end
open Util
(* THE MAIN TYPE
- (control) states are CoTraceExp.t
- (control) states are hashed, and labelled by a unique string
- a config is a variable config + a (control) state
*)
type t = {
source_code : Expand.t;
mutable nb_stables : int;
mutable nb_transients : int;
mutable init_control : string;
mutable final_control : string;
states : (string, state_info) Hashtbl.t ;
mutable transitions : trans list;
(* Gestion des puits *)
mutable nb_sinks : int;
_state2trace : (string, CoTraceExp.t) Hashtbl.t ;
_trace2state : (CoTraceExp.t, string) Hashtbl.t;
_config2ttree : (config, ttree) Hashtbl.t;
(* liste des control inexplorés *)
mutable todo : string list;
(* mode global/dynamique *)
source_code : Expand.t;
nb_stables : int;
nb_transients : int;
init_control : string;
final_control : string;
states : state_info StringMap.t ;
transitions : trans list;
(* Gestion des puits *)
nb_sinks : int;
_state2trace : CoTraceExp.t StringMap.t ;
_trace2state : string TraceMap.t ;
_config2ttree : ttree ConfigMap.t;
(* liste des control inexplorés *)
todo : string list;
(* mode global/dynamique *)
}
(* Misc infos *)
......@@ -340,441 +349,448 @@ let gentrans
(xenv : Expand.t)
(data : Guard.store option) (* data env = inputs + pres *)
(x : CoTraceExp.t) (* control = lutin trace *)
= (
(*-------------------------------------------*)
(* Correspondance id de trace -> trace exp
N.B. on traque les récursions ? *)
(*-------------------------------------------*)
let id2trace s = (
(Util.hfind (Expand.trace_tab xenv) s).ti_def_exp
) in
let unalias s = (
(Util.hfind (Expand.alias_tab xenv) s).ai_def_exp
= (
(*-------------------------------------------*)
(* Correspondance id de trace -> trace exp
N.B. on traque les récursions ? *)
(*-------------------------------------------*)
let id2trace s = (
(Util.hfind (Expand.trace_tab xenv) s).ti_def_exp
) in
let unalias s = (
(Util.hfind (Expand.alias_tab xenv) s).ai_def_exp
) in
(*-------------------------------------------*)
(* LA FONCTION RÉCURSIVE *)
(*-------------------------------------------*)
let rec rec_gentrans
(data : Guard.store option) (* data env = inputs + pres *)
(x : CoTraceExp.t)
(acc : cond)
(cont : callback)
= (
Verbose.exe ~flag:dbg
(fun () -> Printf.printf "++rec_gentrans \"%s\"\n" (CoTraceExp.dumps x));
match x with
(TE_erun (_, _, _, _)
| TE_dyn_erun (_, _, _, _, _)
| TE_dyn_erun_ldbg (_, _, _, _, _)
| TE_run (_, _, _, _, _, _)
| TE_dyn_run (_, _, _, _, _, _, _)
| TE_dyn_run_ldbg (_, _, _, _, _, _, _)) -> assert false
(***** EPSILON => vanish ... *****)
| TE_eps -> (
cont (Some Vanish)
)
(***** TRACE NOMMÉE => ON CHERCHE SA DEF ******)
| TE_ref s -> (
rec_gentrans data (id2trace s) acc cont
)
(***** CONTRAINTE => on appelle le callback *)
| TE_constraint (ae,si) -> (
(* HERE DO EVAL ! *)
let new_acc = Guard.add ~context:data ae acc si in
cont (Some (Goto (new_acc, TE_eps)))
)
(***** SEQUENCE *****)
(* on génère la trace de te1 avec :
- goto(cl,n) => goto(cl,n fby te2)
- vanish => te2
*)
| TE_fby (te1, te2) -> (
let fby_cont a = (
Verbose.exe ~flag:dbg
(fun () -> Printf.printf "-- fby_cont (%s)\n in context %s\n"
(string_of_ttree a) (CoTraceExp.dumps x));
match a with
| None -> None
| Some c -> (
match c with
| Split _ -> assert false
| Goto (cl,n) -> cont (Some (Goto (cl, put_in_seq n te2)))
| Vanish -> rec_gentrans data te2 acc cont
| _ -> cont (Some c)
)
) in
rec_gentrans data te1 acc fby_cont
)
(**** CHOIX *****)
(* chaque choix est traité dans
l'environnement global,
on décore la branche avec le poids
correspondant et une action vide *)
(* ICI *)
| TE_choice wtel -> (
let res = ref [] in
let tc (te, we) = (
match (rec_gentrans data te acc cont) with
None -> ()
| Some tt -> res := (tt, opt_weight_of_opt_algexp we,Guard.empty)::!res
) in
List.iter tc wtel;
match !res with
[] -> None
| ttlist -> Some (Split ttlist)
)
(*** PRIORITE ****)
| TE_prio tel -> (
let rec doit = ( function
[] -> assert false
| [te] -> (
rec_gentrans data te acc cont
)
| te::tail -> (
let first = rec_gentrans data te acc cont in
let others = doit tail in
match (first, others) with
(None,None) -> None
| (Some f, None) -> Some f
| (None, Some o) -> Some o
| (Some f, Some o) ->
Some
(Split [(f, Some huge_weight, Guard.empty) ;
(o, None, Guard.empty)])
)
) in doit tel
)
(*** BOUCLE "INFINIE" ***)
| TE_loop te -> (
let loop_goon_cont a = (
Verbose.exe ~flag:dbg
(fun () -> Printf.printf "-- loop_goon_cont (%s)\n in context %s\n"
(string_of_ttree a) (CoTraceExp.dumps x));
match a with
| None -> None
| Some c -> (
match c with
| Split _ -> assert false
| Goto (cl,n) -> cont (Some (Goto (cl, put_in_seq n x)))
| Vanish -> None
| _ -> cont (Some c)
)
) in
(* on génère en priorité les cas ``boucle'' *)
let goon = rec_gentrans data te acc loop_goon_cont in
Verbose.exe ~flag:dbg
(fun () -> Printf.printf "==== loop goon branch of %s\n gives: %s\n"
(CoTraceExp.dumps x) (string_of_ttree goon));
(* on considère aussi le cas vanish *)
let stop = cont (Some Vanish) in
Verbose.exe ~flag:dbg
(fun () -> Printf.printf "==== loop stop branch of %s\n gives: %s\n"
(CoTraceExp.dumps x) (string_of_ttree stop));
match (goon,stop) with
(None,None) -> None
| (Some g, None) -> Some g
| (None, Some s) -> Some s
| (Some g, Some s) -> Some
(Split [(g, Some huge_weight, Guard.empty) ; (s, None, Guard.empty)])
)
(*** BOUCLE intervale ****)
| TE_loopi (cpt,min,max,te,si) -> (
(* similaire à la boucle sauf pour les poids et les effets
de bord :
goon -> interval_goon(pre cpt, min, max)
+ loop_incr_exp cpt
stop -> interal_stop(pre cpt, min, max)
+ loop_reset_exp cpt
*)
let loopi_goon_cont a = (
Verbose.exe ~flag:dbg
(fun () -> Printf.printf "-- loopi_goon_cont (%s)\n in context %s\n"
(string_of_ttree a) (CoTraceExp.dumps x));
match a with
| None -> None
| Some c -> (
match c with
| Split _ -> assert false
| Goto (cl,n) -> cont (Some (Goto (cl, put_in_seq n x)))
| Vanish -> None
| _ -> cont (Some c)
)
) in
let goon = rec_gentrans data te acc loopi_goon_cont in
let stop = cont (Some Vanish) in
match (goon,stop) with
(None,None) -> None
| (Some g, None) -> Some g
| (None, Some s) -> Some s
| (Some g, Some s) -> (
let gw = dynamic_weight_exp LutPredef.kw_interval_goon cpt [min; max] in
let ga = incr_loop_cpt cpt in
let sw = dynamic_weight_exp LutPredef.kw_interval_stop cpt [min; max] in
let sa = reset_loop_cpt cpt in
Some
(Split [(g, Some (W_exp gw), Guard.of_exp ga si) ;
(s, Some (W_exp sw), Guard.of_exp sa si)])
)
)
(*** BOUCLE moyenne ****)
| TE_loopa (cpt,av, ecopt,te,si) -> (
(* similaire à la boucle sauf pour les poids :
goon -> loopa_goon(pre cpt, min, max)
stop -> loopa_stop(pre cpt, min, max)
*)
let loopa_goon_cont a = (
Verbose.exe ~flag:dbg
(fun () -> Printf.printf "-- loopi_goon_cont (%s)\n in context %s\n"
(string_of_ttree a) (CoTraceExp.dumps x));
match a with
| None -> None
| Some c -> (
match c with
| Split _ -> assert false
| Goto (cl,n) -> cont (Some (Goto (cl, put_in_seq n x)))
| Vanish -> None
| _ -> cont (Some c)
)
) in
let goon = rec_gentrans data te acc loopa_goon_cont in
let stop = cont (Some Vanish) in
match (goon,stop) with
(None,None) -> None
| (Some g, None) -> Some g
| (None, Some s) -> Some s
| (Some g, Some s) -> (
let ec = match ecopt with
Some x -> x
| None -> CoAlgExp.of_iconst "0"
in
let gw = dynamic_weight_exp LutPredef.kw_average_goon cpt [av; ec] in
let ga = incr_loop_cpt cpt in
let sw = dynamic_weight_exp LutPredef.kw_average_stop cpt [av; ec] in
let sa = reset_loop_cpt cpt in
Some
(Split [(g, Some (W_exp gw), Guard.of_exp ga si) ;
(s, Some (W_exp sw), Guard.of_exp sa si)])
)
)
(** Assert
*)
| TE_assert (a, te, si) -> (
let assert_cont act = (
Verbose.exe ~flag:dbg
(fun () -> Printf.printf "-- assert_cont (%s)\n in context %s\n"
(string_of_ttree act) (CoTraceExp.dumps x));
match act with
| None -> None
| Some c -> (
match c with
| Split _ -> assert false
| Goto (cl,n) -> cont (Some (Goto (cl, TE_assert (a,n,si))))
| _ -> cont (Some c)
)
) in
let rec_acc = Guard.add ~context:data a acc si in
rec_gentrans data te rec_acc assert_cont
)
(** init_pre
recursive call with a new store
*)
| TE_exist (ectx, te) -> (
let new_data = add_pres unalias data ectx in
rec_gentrans new_data te acc cont
)
(** RAISE
on appèle simplement le callback avec le nom de l'exception *)
| TE_raise s -> (
cont (Some (Raise s))
)
(** on appèle recursivement le traitement de e avec un nouveau raise callback :
- si le callback est levé avec i, appèle recursivement :
* si eco = Some ec : ec avec les callbacks de l'appel
* sinon le vanish de l'appel
- sinon appèle le callback raise de l'appel
ET avec un nouveau goto callback :
* goto(cl,n) => goto(cl, catch(i,n,eco))
*)
| TE_catch (i,e,eco) -> (
let catch_cont a = (
Verbose.exe ~flag:dbg
(fun () -> Printf.printf "-- catch_cont (%s)\n in context %s\n"
(string_of_ttree a) (CoTraceExp.dumps x));
match a with
| None -> None
| Some c -> (
match c with
| Split _ -> assert false
| Goto (cl,n) -> cont (Some (Goto (cl, TE_catch(i, n, eco))))
| Raise x -> (
if ( x == i) then (
match eco with
Some ec -> (
rec_gentrans data ec acc cont
) |
None -> cont (Some Vanish)
) else (
cont (Some (Raise x))
)
)
| _ -> cont (Some c)
)
) in
rec_gentrans data e acc catch_cont
)
(** TRY *)
(* optimisation : try(eps,_) = eps *)
| TE_try (TE_eps,_) -> cont (Some Vanish)
| TE_try (e,eco) -> (
(** on créé un choix binaire entre :
- priorité (poids infini) e avec un nouveau goto callback :
* goto(cl,n) -> goto(cl, try(n,eco))
- sinon :
* si "eco = Some ec" alors appel rec. sur ec
* si "eco = None" alors appel du vanish
*)
(* la branche prio *)
let try_cont a = (
Verbose.exe ~flag:dbg
(fun () -> Printf.printf "-- try_cont (%s)\n in context %s\n"
(string_of_ttree a) (CoTraceExp.dumps x));
match a with
| None -> None
| Some c -> (
match c with
| Split _ -> assert false
| Goto (cl,n) -> cont (Some (Goto (cl, TE_try(n,eco))))
| _ -> cont (Some c)
)
) in
let prio = rec_gentrans data e acc try_cont in
(* la branche par defaut *)
let defaut = ( match eco with
| Some ec -> (
rec_gentrans data ec acc cont
)
| None -> cont (Some Vanish)
) in
match (prio,defaut) with
(None,None) -> None
| (Some p, None) -> Some p
| (None, Some d) -> Some d
| (Some p, Some d) -> (
Some
(Split [(p, Some huge_weight, Guard.empty) ; (d, None, Guard.empty)])
)
)
(** Parallèle : il y en a toujours au - un ! *)
| TE_para ([]) -> assert false
| TE_para ([e]) -> (
(* le dernier continue son chemin *)
rec_gentrans data e acc cont
)
| TE_para (e::el) -> (
(* continuation for the head statement *)
let para_head_cont a = (
Verbose.exe ~flag:dbg
(fun () -> Printf.printf "-- para_head_cont (%s)\n in context %s\n"
(string_of_ttree a) (CoTraceExp.dumps x));
match a with
| None -> None
| Some c -> (
match c with
| Split _ -> assert false
| Vanish -> (
(* 1st vanishes: others continue *)
rec_gentrans data (TE_para(el)) acc cont
)
| Raise s -> (
(* 1st raises s: whole raises s *)
cont (Some (Raise s))
)
| Goto (cl,n) -> (
(* 1st REQUIRES TO DO cl,
That is, if cl is satisfiable, THEN
the others MUST find a behavior compatible
HERE: PROBLEM, impossible
to do that with Lucky ! (see the case Raise below)
*)
(* HERE: DO EVAL! *)
let tail_acc = Guard.merge ~context:data cl acc in
let para_tail_cont a = (
Verbose.exe ~flag:dbg
(fun () -> Printf.printf
"-- para_tail_cont (%s)\n in context %s\n"
(string_of_ttree a) (CoTraceExp.dumps x));
match a with
| None -> None
| Some c -> (
match c with
| Split _ -> assert false
| Vanish -> (
(* others vanish, 1st continue *)
cont (Some (Goto (cl,n)))
)
| Raise s -> (
(* SEMANTICS PROBLEM:
should the others be able to raise exception
IF cl is satisfiable ?
- no: we consider that the head has priority
and then others must find a way to respect it
either with a trans, or vanish (if possible)
- yes: we state that raising an exception is
a acceptable way (though strange !) to respect
the head
=> the "no" seems more acceptable ??
TECHNICAL PROBLEM: none of these solutions
can be expressed with "wt" because satisfiability
check are ONLY performed at leaves.
=> the "real" semantics will be implemented in
the "lutExe" only.
Lucky-wt based algos are FALSE in this case
For the time being:
- emit a warning
- choose an "intermediate" solution consisting
in rejecting locally this case
*)
(* cont (Some (Raise s)) *)
LutErrors.warning None
("raising exception "^s^" in a parallel cannot be safely compiled into Lucky");
cont None
)
| Goto (tcl, tn) -> (
(* HERE -> something to do ? *)
cont (Some (Goto (tcl, put_in_para n tn)))
)
)
) in
rec_gentrans data (TE_para(el)) tail_acc para_tail_cont
)
(* | _ -> cont (Some c) *)
)
) in
rec_gentrans data e acc para_head_cont
)
| TE_strong_assert (_, _, _)
| TE_dyn_loop (_, _, _)
| TE_omega _
| TE_noeps _
| TE_dyn_choice (_, _)
-> assert false
) in
(*-------------------------------------------*)
(* LA FONCTION RÉCURSIVE *)
(*-------------------------------------------*)
let rec rec_gentrans
(data : Guard.store option) (* data env = inputs + pres *)
(x : CoTraceExp.t)
(acc : cond)
(cont : callback)
= (
Verbose.exe ~flag:dbg
(fun () -> Printf.printf "++rec_gentrans \"%s\"\n" (CoTraceExp.dumps x));
match x with
(***** EPSILON => vanish ... *****)
| TE_eps -> (
cont (Some Vanish)
)
(***** TRACE NOMMÉE => ON CHERCHE SA DEF ******)
| TE_ref s -> (
rec_gentrans data (id2trace s) acc cont
)
(***** CONTRAINTE => on appelle le callback *)
| TE_constraint (ae,si) -> (
(* HERE DO EVAL ! *)
let new_acc = Guard.add ~context:data ae acc si in
cont (Some (Goto (new_acc, TE_eps)))
)
(***** SEQUENCE *****)
(* on génère la trace de te1 avec :
- goto(cl,n) => goto(cl,n fby te2)
- vanish => te2
*)
| TE_fby (te1, te2) -> (
let fby_cont a = (
Verbose.exe ~flag:dbg
(fun () -> Printf.printf "-- fby_cont (%s)\n in context %s\n"
(string_of_ttree a) (CoTraceExp.dumps x));
match a with
| None -> None
| Some c -> (
match c with
| Split _ -> assert false
| Goto (cl,n) -> cont (Some (Goto (cl, put_in_seq n te2)))
| Vanish -> rec_gentrans data te2 acc cont
| _ -> cont (Some c)
)
) in
rec_gentrans data te1 acc fby_cont
)
(**** CHOIX *****)
(* chaque choix est traité dans
l'environnement global,
on décore la branche avec le poids
correspondant et une action vide *)
(* ICI *)
| TE_choice wtel -> (
let res = ref [] in
let tc (te, we) = (
match (rec_gentrans data te acc cont) with
None -> ()
| Some tt -> res := (tt, opt_weight_of_opt_algexp we,Guard.empty)::!res
) in
List.iter tc wtel;
match !res with
[] -> None
| ttlist -> Some (Split ttlist)
)
(*** PRIORITE ****)
| TE_prio tel -> (
let rec doit = ( function
[] -> assert false
| [te] -> (
rec_gentrans data te acc cont
)
| te::tail -> (
let first = rec_gentrans data te acc cont in
let others = doit tail in
match (first, others) with
(None,None) -> None
| (Some f, None) -> Some f
| (None, Some o) -> Some o
| (Some f, Some o) -> Some
(Split [(f, Some huge_weight, Guard.empty) ; (o, None, Guard.empty)])
)
) in doit tel
)
(*** BOUCLE "INFINIE" ***)
| TE_loop te -> (
let loop_goon_cont a = (
Verbose.exe ~flag:dbg
(fun () -> Printf.printf "-- loop_goon_cont (%s)\n in context %s\n"
(string_of_ttree a) (CoTraceExp.dumps x));