From 09c930a830d487f8cfe03fe46ddfba227804fc5b Mon Sep 17 00:00:00 2001 From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr> Date: Mon, 24 Aug 2020 09:38:18 +0200 Subject: [PATCH] Update: add the potential value of the current state as an output of sasa programs in the rdbg plugin if the potentioal function is provided --- lib/algo/algo.mli | 2 +- lib/sasa/sasaRun.ml | 193 +++++++++++++++++++++++++------------------- 2 files changed, 110 insertions(+), 85 deletions(-) diff --git a/lib/algo/algo.mli b/lib/algo/algo.mli index 1f20009f..78a662dc 100644 --- a/lib/algo/algo.mli +++ b/lib/algo/algo.mli @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 08/07/2020 (at 16:01) by Erwan Jahier> *) +(* Time-stamp: <modified the 21/08/2020 (at 16:11) by Erwan Jahier> *) (** {1 The Algorithm programming Interface.} *) (** {1 What's need to be provided by users.} diff --git a/lib/sasa/sasaRun.ml b/lib/sasa/sasaRun.ml index f9bcecd9..8b9dcd54 100644 --- a/lib/sasa/sasaRun.ml +++ b/lib/sasa/sasaRun.ml @@ -38,74 +38,99 @@ let (get_sl_out: bool -> 'v Process.t list -> bool list list -> RdbgPlugin.sl) = pl ll ) +type 'v pna = 'v Process.t * 'v Register.neighbor list * Register.action +let (compute_potentiel : 'v pna list -> ('v Process.t * 'v Register.neighbor list) list -> + 'v Env.t -> RdbgPlugin.sl) = + fun pnal p_nl_l e -> + match Register.get_potential () with + | None -> [] + | Some user_pf -> + let pidl = List.map (fun (p,_) -> p.Process.pid) p_nl_l in + let p_a_l = List.map (fun (p,_,a) -> p.Process.pid, a) pnal in + let ne = Step.f pnal e in + let get_info pid = + { + Register.neighbors = snd (List.find (fun (p,_) -> p.Process.pid = pid) p_nl_l); + Register.curr = Env.get e pid ; + Register.next = Env.get ne pid ; + Register.action = List.assoc_opt pid p_a_l + } + in + let p = (user_pf pidl get_info) in + [("potential", Data.F p)] + let (make_do: string array -> SasArg.t -> ('v Process.t * 'v Register.neighbor list) list -> 'v Env.t -> RdbgPlugin.t) = fun argv args p_nl_l e -> - let pl = fst (List.split p_nl_l) in - let prog_id = Printf.sprintf "%s (with sasa Version %s)" - (String.concat " " (Array.to_list argv)) SasaVersion.str - in - let vntl_i = - List.map (fun (vn,vt) -> vn, Data.type_of_string vt) - (Sasacore.Main.get_inputs_rif_decl args pl) - in - let vntl_o = - List.map (fun (vn,vt) -> vn, Data.type_of_string vt) - (Sasacore.Main.get_outputs_rif_decl args pl) - in - let pre_enable_processes_opt = ref None in - let sasa_env = ref e in - let reset () = - pre_enable_processes_opt := None; - sasa_env := e - in - (* Do the same job as SasaMain.simustep *) - let (step: RdbgPlugin.sl -> RdbgPlugin.sl) = - fun sl_in -> - let e = !sasa_env in - match !pre_enable_processes_opt with - | None -> (* the first step *) - (* 1: Get enable processes *) - let pnall, enab_ll = Sasacore.Main.get_enable_processes p_nl_l e in - let sasa_nenv = from_sasa_env p_nl_l e in - pre_enable_processes_opt := Some(pnall, enab_ll); - sasa_nenv @ (get_sl_out true pl enab_ll) - | Some (pre_pnall, pre_enab_ll) -> - (* 2: read the actions from the outside process, i.e., from sl_in *) - let _, pnal = Daemon.f args.dummy_input - (args.verbose > 1) args.daemon p_nl_l e pre_pnall pre_enab_ll - (get_action_value sl_in) - in - (* 3: Do the steps *) - let ne = Sasacore.Step.f pnal e in - let sasa_nenv = from_sasa_env p_nl_l ne in - (* 1': Get enable processes *) - let pnall, enab_ll = Sasacore.Main.get_enable_processes p_nl_l ne in - pre_enable_processes_opt := Some(pnall, enab_ll); - sasa_env := ne; - sasa_nenv @ (get_sl_out true pl enab_ll) - in - let (step_internal_daemon: RdbgPlugin.sl -> RdbgPlugin.sl) = - fun sl_in -> - (* in this mode, sasa does not play first *) - let e = !sasa_env in + let pl = fst (List.split p_nl_l) in + let prog_id = Printf.sprintf "%s (with sasa Version %s)" + (String.concat " " (Array.to_list argv)) SasaVersion.str + in + let vntl_i = + List.map (fun (vn,vt) -> vn, Data.type_of_string vt) + (Sasacore.Main.get_inputs_rif_decl args pl) + in + let vntl_o = + List.map (fun (vn,vt) -> vn, Data.type_of_string vt) + (Sasacore.Main.get_outputs_rif_decl args pl) + in + let vntl_o = + if Register.get_potential () = None then vntl_o else ("potential", Data.Real)::vntl_o in + let pre_enable_processes_opt = ref None in + let sasa_env = ref e in + let reset () = + pre_enable_processes_opt := None; + sasa_env := e + in + (* Do the same job as SasaMain.simustep *) + let (step: RdbgPlugin.sl -> RdbgPlugin.sl) = + fun sl_in -> + let e = !sasa_env in + match !pre_enable_processes_opt with + | None -> (* the first step *) (* 1: Get enable processes *) let pnall, enab_ll = Sasacore.Main.get_enable_processes p_nl_l e in + let sasa_nenv = from_sasa_env p_nl_l e in + pre_enable_processes_opt := Some(pnall, enab_ll); + sasa_nenv @ (get_sl_out true pl enab_ll) + | Some (pre_pnall, pre_enab_ll) -> (* 2: read the actions from the outside process, i.e., from sl_in *) - let activate_val, pnal = Daemon.f args.dummy_input - (args.verbose > 1) args.daemon p_nl_l e pnall enab_ll + let _, pnal = Daemon.f args.dummy_input + (args.verbose > 1) args.daemon p_nl_l e pre_pnall pre_enab_ll (get_action_value sl_in) in (* 3: Do the steps *) let ne = Sasacore.Step.f pnal e in - sasa_env := ne; - (from_sasa_env p_nl_l e) @ (get_sl_out true pl enab_ll) @ - (get_sl_out false pl activate_val) - in - let step = if args.daemon = Daemon.Custom then step else step_internal_daemon in - let ss_table = Hashtbl.create 10 in - let step_dbg sl_in ctx cont = cont (step sl_in) ctx in + let sasa_nenv = from_sasa_env p_nl_l ne in + (* 1': Get enable processes *) + let pnall, enab_ll = Sasacore.Main.get_enable_processes p_nl_l ne in + let pot_sl = compute_potentiel pnal p_nl_l ne in + pre_enable_processes_opt := Some(pnall, enab_ll); + sasa_env := ne; + sasa_nenv @ (get_sl_out true pl enab_ll) @ pot_sl + in + let (step_internal_daemon: RdbgPlugin.sl -> RdbgPlugin.sl) = + fun sl_in -> + (* in this mode, sasa does not play first *) + let e = !sasa_env in + (* 1: Get enable processes *) + let pnall, enab_ll = Sasacore.Main.get_enable_processes p_nl_l e in + (* 2: read the actions from the outside process, i.e., from sl_in *) + let activate_val, pnal = Daemon.f args.dummy_input + (args.verbose > 1) args.daemon p_nl_l e pnall enab_ll + (get_action_value sl_in) + in + (* 3: Do the steps *) + let ne = Sasacore.Step.f pnal e in + let pot_sl = compute_potentiel pnal p_nl_l ne in + sasa_env := ne; + (from_sasa_env p_nl_l e) @ (get_sl_out true pl enab_ll) @ + (get_sl_out false pl activate_val) @ pot_sl + in + let step = if args.daemon = Daemon.Custom then step else step_internal_daemon in + let ss_table = Hashtbl.create 10 in + let step_dbg sl_in ctx cont = cont (step sl_in) ctx in (* this event is useless actually; the same information is available at Rtop { ctx with @@ -123,33 +148,33 @@ let (make_do: string array -> SasArg.t -> } in *) - let (mems_in : Data.subst list) = [] in - let (mems_out : Data.subst list) = [] in - { - id = prog_id; - inputs = vntl_i; - outputs= vntl_o; - reset=(fun () -> reset()); - kill=(fun _ -> flush stdout; flush stderr); - init_inputs=mems_in; - init_outputs=mems_out; - step=step; - step_dbg = step_dbg; - save_state = (fun i -> - let prgs = Random.get_state () in - Hashtbl.replace ss_table i - (prgs, !sasa_env, !pre_enable_processes_opt) - ); - restore_state = (fun i -> - match Hashtbl.find_opt ss_table i with - | Some (prgs, e, pepo) -> - Random.set_state prgs; - sasa_env := e; pre_enable_processes_opt := pepo - | None -> - Printf.eprintf "Cannot restore state %i from sasa\n" i; - flush stderr - ); - } + let (mems_in : Data.subst list) = [] in + let (mems_out : Data.subst list) = [] in + { + id = prog_id; + inputs = vntl_i; + outputs= vntl_o; + reset=(fun () -> reset()); + kill=(fun _ -> flush stdout; flush stderr); + init_inputs=mems_in; + init_outputs=mems_out; + step=step; + step_dbg = step_dbg; + save_state = (fun i -> + let prgs = Random.get_state () in + Hashtbl.replace ss_table i + (prgs, !sasa_env, !pre_enable_processes_opt) + ); + restore_state = (fun i -> + match Hashtbl.find_opt ss_table i with + | Some (prgs, e, pepo) -> + Random.set_state prgs; + sasa_env := e; pre_enable_processes_opt := pepo + | None -> + Printf.eprintf "Cannot restore state %i from sasa\n" i; + flush stderr + ); + } let (make: string array -> RdbgPlugin.t) = -- GitLab