diff --git a/lutin/src/auto2Lucky.ml b/lutin/src/auto2Lucky.ml index 632dad078511b844e41bcdc1ad0b3512fc8a17f9..08176d7fcd696696d7f7707684445c11488bf60a 100644 --- a/lutin/src/auto2Lucky.ml +++ b/lutin/src/auto2Lucky.ml @@ -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) ; diff --git a/lutin/src/autoGen.ml b/lutin/src/autoGen.ml index 59bc885d7ed0553bc94d15749e64b4530d9e9fed..0b19be4198f72fd4f75451c663fcf2867a5bd6ff 100644 --- a/lutin/src/autoGen.ml +++ b/lutin/src/autoGen.ml @@ -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)); - 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 - (* top-level cont *) - let top_cont a = ( - Verbose.exe ~flag:dbg - (fun () -> Printf.printf "-- top_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 - | _ -> Some c - ) - ) in - Verbose.exe ~flag:dbg (fun () -> Printf.printf "=================\ngentrans \"%s\"\n" - (CoTraceExp.dumps x)); - let res = rec_gentrans data x Guard.empty top_cont in - (*dump_ttree res;*) - res - ) + (* top-level cont *) + let top_cont a = ( + Verbose.exe ~flag:dbg + (fun () -> Printf.printf "-- top_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 + | _ -> Some c + ) + ) in + Verbose.exe ~flag:dbg (fun () -> Printf.printf "=================\ngentrans \"%s\"\n" + (CoTraceExp.dumps x)); + let res = rec_gentrans data x Guard.empty top_cont in + (*dump_ttree res;*) + res + ) (**************************************************************************** GENERATION DE L'AUTOMATE COMPLET @@ -803,136 +819,148 @@ printf "]\n" ) let new_stable_state (it: t) (e : CoTraceExp.t) = ( - let ssi = it.nb_stables in - it.nb_stables <- it.nb_stables + 1; - let res = sprintf "state%d" ssi in - Hashtbl.add it.states res (SS_stable e); - res + let ssi = it.nb_stables in + let res = sprintf "state%d" ssi in + let it = { it with + nb_stables = it.nb_stables + 1; + states = StringMap.add res (SS_stable e) it.states + } + in + res, it ) let new_transient_state (it: t) (father: string) (index: int) = ( - it.nb_transients <- it.nb_transients + 1; - let res = sprintf "%s_%d" father index in - Hashtbl.add it.states res SS_transient; - res + let res = sprintf "%s_%d" father index in + let it = { it with + nb_transients = it.nb_transients + 1; + states = StringMap.add res SS_transient it.states; + } + in + res, it ) (** recherche/crée une association trace/state *) let get_stable (it:t) e = ( - try ( - Util.hfind it._trace2state e - ) with Not_found -> ( - let res = new_stable_state it e in -Verbose.exe ~level:3 (fun () -> Printf.printf "##new state=\"%s\" exp=%s\n" res (CoTraceExp.dumps e)); - Hashtbl.add it._trace2state e res; - Hashtbl.add it._state2trace res e ; - it.todo <- res :: it.todo; - res - ) + try TraceMap.find e it._trace2state, it + with Not_found -> ( + let res, it = new_stable_state it e in + Verbose.exe ~level:3 + (fun () -> Printf.printf "##new state=\"%s\" exp=%s\n" res (CoTraceExp.dumps e)); + let it = { it with + _trace2state = TraceMap.add e res it._trace2state; + _state2trace = StringMap.add res e it._state2trace; + todo = res :: it.todo + } + in + res, it + ) ) (** recherche/crée un état puits N.B, on garde tel que l'ident qui est suppose être unique ! *) -let get_sink (it:t) x = ( - try ( - let _ = Util.hfind it.states x in x - ) with Not_found -> ( -Verbose.put ~level:3 "##new sink=\"%s\"\n" x ; - Hashtbl.add it.states x (SS_final x); - it.nb_sinks <- it.nb_sinks + 1 ; - x - ) -) - -let init (xenv : Expand.t) = ( - let res = { - source_code = xenv; - nb_stables = 0; - nb_transients = 0; - init_control = ""; - (** L'état final est un puit *) - final_control = ""; - states = Hashtbl.create 100; - transitions = []; - - nb_sinks = 0; - _state2trace = Hashtbl.create 50; - _trace2state = Hashtbl.create 50; - _config2ttree = Hashtbl.create 50; - - (* liste des inexplorés *) - todo = []; - } in - let is = Expand.main_trace xenv in - let ie = (Util.hfind (Expand.trace_tab xenv) is).ti_def_exp in - res.init_control <- get_stable res ie; - res.final_control <- get_sink res "vanish"; - res -) +let get_sink (it:t) x = + match StringMap.find_opt x it.states with + | None -> + Verbose.put ~level:3 "##new sink=\"%s\"\n" x ; + x, { it with + nb_sinks = it.nb_sinks + 1; + states = StringMap.add x (SS_final x) it.states; + } + | Some _ -> x, it + +let init (xenv : Expand.t) = + let res = { + source_code = xenv; + nb_stables = 0; + nb_transients = 0; + init_control = ""; + (** L'état final est un puit *) + final_control = ""; + states = StringMap.empty; + transitions = []; + + nb_sinks = 0; + _state2trace = StringMap.empty; + _trace2state = TraceMap.empty; + _config2ttree = ConfigMap.empty; + + (* liste des inexplorés *) + todo = []; + } + in + let is = Expand.main_trace xenv in + let ie = (Util.hfind (Expand.trace_tab xenv) is).ti_def_exp in + let init_control, res = get_stable res ie in + let final_control, res = get_sink res "vanish" in + { res with + init_control = init_control; + final_control =final_control; + } let rec ttree2trans (it:t) (src: string) (tt : ttree) = ( - match tt with - | Vanish -> - [ { src = src; wgt = None ; form = Guard.empty; dest = it.final_control } ] - | Raise x -> - [ { src = src; wgt = None ; form = Guard.empty; dest = get_sink it x; } ] - | Goto (cl, n) -> - [ { src = src; wgt = None ; form = cl; dest = get_stable it n; } ] - | Split twl -> ( + match tt with + | Vanish -> + [ { src = src; wgt = None ; form = Guard.empty; dest = it.final_control } ], it + | Raise x -> + let dest, it = get_sink it x in + [ { src = src; wgt = None ; form = Guard.empty; dest = dest } ], it + | Goto (cl, n) -> + let dest, it = get_stable it n in + [ { src = src; wgt = None ; form = cl; dest = dest ; } ], it + | Split twl -> ( let child_cpt = ref 0 in - let treat_choice trs (t, wo, a) = ( - let dest = new_transient_state it src !child_cpt in - incr child_cpt; - let t0 = { src = src; wgt = wo ; form = a ; dest = dest; } in - (ttree2trans it dest t) @ (t0 :: trs) - ) in - ( List.fold_left treat_choice [] twl) - ) + let treat_choice (trs,it) (t, wo, a) = + let dest, it = new_transient_state it src !child_cpt in + incr child_cpt; + let t0 = { src = src; wgt = wo ; form = a ; dest = dest; } in + let trs, it = ttree2trans it dest t in + trs @ (t0 :: trs), it + in + List.fold_left treat_choice ([],it) twl + ) ) -let get_state_def (it:t) (ix: string) = ( - Util.hfind it._state2trace ix -) +let get_state_def (it:t) (ix: string) = + StringMap.find ix it._state2trace -let get_state_info (it:t) (ix: string) = ( - Util.hfind it.states ix -) + +let get_state_info (it:t) (ix: string) = + StringMap.find ix it.states (* *) let config2ttree (it:t) (cfg: config) = ( - let ix = cfg.control in - let e = Util.hfind it._state2trace ix in - let data = cfg.data in - (* use cash *) - let res = try ( - let tt = Util.hfind it._config2ttree cfg in - Verbose.put ~level:2 "##config2ttree: \"%s\" cached\n" ix ; - if (Utils.paranoid ()) then ( - let tt' = gentrans it.source_code data e in - if(tt' <> (Some tt)) then assert false - ); - tt - ) with Not_found -> ( - Verbose.exe ~level:2 + let ix = cfg.control in + let e = StringMap.find ix it._state2trace in + let data = cfg.data in + (* use cash *) + try + let tt = ConfigMap.find cfg it._config2ttree in + Verbose.put ~level:2 "##config2ttree: \"%s\" cached\n" ix ; + if (Utils.paranoid ()) then ( + let tt' = gentrans it.source_code data e in + assert (tt' = (Some tt)) + ); + tt, it + with Not_found -> ( + Verbose.exe ~level:2 (fun () -> Printf.printf "##config2ttree: \"%s\" = %s\n" - ix (CoTraceExp.dumps e)); - match ( gentrans it.source_code data e) with - (* match ( gentrans_old it.source_code e) with *) - Some tt -> ( - Hashtbl.add it._config2ttree cfg tt; - (* ttree2trans it ix tt *) - tt - ) | - None -> raise (Failure "unexpected toplevel Deadlock") - ) in - res + ix (CoTraceExp.dumps e)); + match ( gentrans it.source_code data e) with + (* match ( gentrans_old it.source_code e) with *) + Some tt -> + let it = { it with _config2ttree = ConfigMap.add cfg tt it._config2ttree } in + (* (* TODO: *)tree2trans it ix tt *) + tt, it + | None -> raise (Failure "unexpected toplevel Deadlock") + ) ) + type gtree = string * gtree_node and gtree_node = | GT_leaf of (cond * string) @@ -941,44 +969,47 @@ and gtree_node = (* debug : size ? *) let rec gtree_size (_,gt) = ( - match gt with - | GT_leaf _ -> 1 - | GT_stop _ -> 1 - | GT_choice ll -> ( - List.fold_left (fun a (_, g) -> a + (gtree_size g)) 1 ll - ) + match gt with + | GT_leaf _ -> 1 + | GT_stop _ -> 1 + | GT_choice ll -> ( + List.fold_left (fun a (_, g) -> a + (gtree_size g)) 1 ll + ) ) - -let rec ttree2gtree (it:t) (src: string) (acc: cond) (tt : ttree) = ( - match tt with - | Vanish -> (src, GT_stop it.final_control) - | Raise x -> (src, GT_stop (get_sink it x)) - | Goto (cl, n) -> (src, GT_leaf (Guard.merge acc cl, get_stable it n)) - | Split twl -> ( -(* | Split of (ttree * weightexp option * CoAlgExp.t list) list *) + +let rec ttree2gtree (it:t) (src: string) (acc: cond) (tt : ttree) = + match tt with + | Vanish -> (src, GT_stop it.final_control), it + | Raise x -> + let sink, it = get_sink it x in + (src, GT_stop sink), it + | Goto (cl, n) -> + let st, it = get_stable it n in + (src, GT_leaf (Guard.merge acc cl, st)), it + | Split twl -> ( + (* | Split of (ttree * weightexp option * CoAlgExp.t list) list *) let child_cpt = ref 0 in - let treat_choice : - (ttree * weightexp option * cond) -> (weightexp option * gtree) = - fun (t, wo, a) -> ( - - let dest = new_transient_state it src !child_cpt in - incr child_cpt; - let cht = ttree2gtree it dest (Guard.merge acc a) t in - (wo, cht) - ) in - (src, GT_choice (List.map treat_choice twl)) - ) -) + let treat_choice : (weightexp option * gtree) list * t -> + (ttree * weightexp option * cond) -> (weightexp option * gtree) list * t = + fun (choices, it) (t, wo, a) -> + let dest, it = new_transient_state it src !child_cpt in + incr child_cpt; + let cht, it = ttree2gtree it dest (Guard.merge acc a) t in + (wo, cht)::choices, it + in + let choices, it = List.fold_left treat_choice ([],it) twl in + (src, GT_choice (List.rev choices)), it + ) let rec config2gtree (it:t) (cfg: config) = ( - let ix = cfg.control in - let tt = config2ttree it cfg in + let ix = cfg.control in + let tt, it = config2ttree it cfg in ttree2gtree it ix Guard.empty tt ) let config2trans (it:t) (cfg: config) = ( - let ix = cfg.control in - let tt = config2ttree it cfg in + let ix = cfg.control in + let tt, it = config2ttree it cfg in ttree2trans it ix tt ) @@ -987,27 +1018,22 @@ Builds a full automaton from an expanded Lutin program the "store" in config if always EMPTY *) let make (xenv : Expand.t) = ( - - let it = init xenv in - let (tlist : trans list ref) = ref [] in - - let rec explore () = ( - match it.todo with - [] -> () (* FINI *) - | s::tail -> ( - (* on l'enlève *) - it.todo <- tail; - let curconf = { data = None; control = s} in - let trs = config2trans it curconf in - tlist := trs @ !tlist; - (* on continue *) - explore () + let it = init xenv in + let rec explore (tlist, it) = + match it.todo with + | [] -> (tlist, it) + | s::tail -> ( + (* on l'enlève *) + let it = { it with todo = tail } in + let curconf = { data = None; control = s} in + let trs, it = config2trans it curconf in + let tlist = trs @ tlist in + (* on continue *) + explore (tlist, it) ) - ) - in - explore () ; - it.transitions <- List.rev !tlist; - it + in + let tlist, it = explore ([],it) in + { it with transitions = List.rev tlist } ) let dump (auto : t) = ( diff --git a/lutin/src/autoGen.mli b/lutin/src/autoGen.mli index 989db694993b2d49d9e8d1720286cb6bd178c074..59ab338255f3bbe5a3420424cb63376150688d9c 100644 --- a/lutin/src/autoGen.mli +++ b/lutin/src/autoGen.mli @@ -70,8 +70,8 @@ val init_control : t -> string val transitions : t -> trans list (* Explore le sous-graphe du state *) -val config2gtree : t -> config -> gtree -val config2trans : t -> config -> trans list +val config2gtree : t -> config -> gtree * t +val config2trans : t -> config -> trans list * t (* MUST BE INITIALIZED WITH A FUNCTION : CoAlgExp.t -> Exp.t @@ -86,7 +86,7 @@ val get_state_def : t -> string -> CoTraceExp.t val get_state_info : t -> string -> state_info (* Table des états connus *) -val states : t -> (string, state_info) Hashtbl.t +val states : t -> state_info Util.StringMap.t val dump : t -> unit diff --git a/lutin/src/lutProg.ml b/lutin/src/lutProg.ml index 2de0ba54df1e956dc68ea65247151defe433ae2d..d5367cb51a3d5409d20951cd3ab38c3bf20e3561 100644 --- a/lutin/src/lutProg.ml +++ b/lutin/src/lutProg.ml @@ -494,11 +494,12 @@ let lut_get_wtl (zelut:t) (input:Var.env_in) (st:Prog.state) (ctrlst:Prog.ctrl_s Verbose.exe ~level:2 (fun () -> Verbose.put "# -> state2gtree\n"); Utils.time_C "state2gtree"; - let gt = AutoGen.config2gtree zelut.auto zecfg in - + let gt, auto = AutoGen.config2gtree zelut.auto zecfg in + let zelut = { zelut with auto = auto } in Utils.time_R "state2gtree"; Verbose.exe ~level:2 ( - fun () -> Verbose.put "# <- state2gtree, done: %d nodes\n" (AutoGen.gtree_size gt) + fun () -> Verbose.put "# <- state2gtree, done: %d nodes\n" + (AutoGen.gtree_size gt) ); (* traduction gtree -> Prog.wt *)