Commit 9689b826 authored by erwan's avatar erwan
Browse files

Update: make sure the round number is always correct.

parent 6ab7b451
(* Time-stamp: <modified the 28/05/2021 (at 11:47) by Erwan Jahier> *)
(* Time-stamp: <modified the 31/05/2021 (at 11:56) by Erwan Jahier> *)
#thread
#require "lablgtk3"
......@@ -430,7 +430,7 @@ let custom_daemon p gtext vbox step_button round_button legitimate_button =
let nodes = List.filter (fun (_,b) -> b) nodes_enabled in
let nodes = get_higher_prioriry nodes in
(* p ("==> gtkgui: CALL =" ^ (string_of_event !e)); *)
match !daemon_kind with
(match !daemon_kind with
| Distributed -> (
let nodes = List.map (fun x -> [x]) nodes in
let to_activate = Daemon.distributed nodes in
......@@ -438,14 +438,12 @@ let custom_daemon p gtext vbox step_button round_button legitimate_button =
List.iter (fun n -> Hashtbl.replace daemongui_activate n true) to_activate;
goto_hook_exit ();
goto_hook_call ();
d ()
)
| Synchronous -> (
Hashtbl.clear daemongui_activate;
List.iter (fun n -> Hashtbl.replace daemongui_activate n true) nodes;
goto_hook_exit ();
goto_hook_call ();
d ()
)
| Central -> (
let nodes = List.map (fun x -> [x]) nodes in
......@@ -456,7 +454,6 @@ let custom_daemon p gtext vbox step_button round_button legitimate_button =
Hashtbl.replace daemongui_activate n true) to_activate;
goto_hook_exit ();
goto_hook_call ();
d ()
)
| LocCentral -> (
let get_neigbors x =
......@@ -472,14 +469,17 @@ let custom_daemon p gtext vbox step_button round_button legitimate_button =
List.iter (fun n -> Hashtbl.replace daemongui_activate n true) to_activate;
goto_hook_exit ();
goto_hook_call ();
d ()
)
| ManualCentral -> () (* SNO; the step is done in pushbox callbacks *)
| Manual ->
goto_hook_exit ();
goto_hook_call ();
store !e.nb;
d ()
);
if not args.salut_mode && is_silent !e then
(* go to Ltop so that the round number can be updated *)
e := next_cond !e (fun e -> e.kind = Ltop);
d ()
in
step
......@@ -567,7 +567,7 @@ let main () =
let ze_step =
if custom_mode then
custom_daemon p text_out w step_button round_button legitimate_button
custom_daemon p text_out w step_button round_button legitimate_button
else
s (* cf sasa-rdbg-cmds.ml *)
in
......@@ -577,7 +577,7 @@ let main () =
in
let rec legitimate_gui () =
ze_step();
if is_legitimate !e || is_silent !e then () else (legitimate_gui ())
if is_legitimate !e || is_silent !e then () else (legitimate_gui ());
in
(* change_label legitimate_button "Silen_t"; *)
ignore (legitimate_button#connect#clicked ~callback:
......@@ -589,7 +589,7 @@ let main () =
(* indeed, in the defaut mode (manual central), it should be hided *)
let rec next_round_gui rn =
ze_step();
if rn < !roundnb || is_silent !e then () else (next_round_gui rn)
if rn < !roundnb || is_silent !e then () else (next_round_gui rn);
in
set_tooltip step_button "Move FORWARD to the next STEP";
......
......@@ -9,10 +9,102 @@ open Sasacore.Topology;;
#use "dot4sasa.ml";;
(**********************************************************************)
(* Dealing with rounds *)
let roundnb = ref 1
let roundtbl = Hashtbl.create 1;;
let _ = Hashtbl.add roundtbl 1 (1,true);;
(** Computing rounds *)
let roundnb = ref (-666)
let mask = ref [] (* nodes we look the activation of *) (* XXX use an array! *)
let roundtbl = Hashtbl.create 10;;
(* let _ = Hashtbl.add roundtbl 1 (1,true);; *)
let verbose = ref false
let round_init () =
roundnb := 1;
mask := [];
Hashtbl.clear roundtbl
let _ = round_init ();;
(* a process can be removed from the mask if one action of p is triggered
or if no action of p is enabled *)
let get_removable pl =
let pl = List.filter
(fun p ->
(List.exists (fun (_,_,acti) -> acti) p.actions) ||
(List.for_all (fun (_,enab,_) -> (not enab)) p.actions)
)
pl
in
List.map (fun p -> p.name) pl
let enabled pl = (* returns the enabled processes *)
let el = List.filter
(fun p -> List.exists (fun (_,enab,_) -> enab) p.actions)
pl
in
List.map (fun p -> p.name) el
(* called at each event via the time-travel hook *)
let (round : RdbgEvent.t -> bool) = fun e ->
match Hashtbl.find_opt roundtbl e.nb with
| Some (croundnb, round) ->
(* Printf.printf "round tabulated at e.nb %d: croundnb=%d round = %b\n%!" *)
(* e.nb croundnb round; *)
roundnb := croundnb;
round
| None ->
let round =
( (* we check if a round occurs when activated processes are available *)
if args.salut_mode then
e.kind = Exit && e.name = "mv_hook" && e.step > 1
else
e.kind = Ltop
)
&&
let (pl : process list) = get_processes e in
if !mask = [] then mask := enabled pl; (* occurs at the first possible round *)
let rm_me = get_removable pl in
if !verbose then (
Printf.printf "\nMask (event %d): %s\n" e.nb (String.concat "," !mask);
Printf.printf "To remove from mask: %s\n%!" (String.concat "," rm_me)
);
mask := List.filter (fun pid -> not (List.mem pid rm_me)) !mask;
if !verbose then
Printf.printf "New Mask: %s\n%!" (String.concat "," !mask);
let res = !mask = [] in
if res then (
mask := (
let mask =
List.filter
(fun p -> List.exists (fun (_,e,a) -> e && not(a)) p.actions)
pl
in
let mask = List.map (fun p -> p.name) mask in
if !verbose then (
let mask = List.rev mask in
Printf.printf "Next mask : %s\n%!" (String.concat "," mask);
flush stdout
);
mask
)
);
res
in
if round then incr roundnb;
Hashtbl.add roundtbl e.nb (!roundnb, round);
(* Printf.printf "round computed at e.nb %d: croundnb=%d round = %b\n%!"
e.nb !roundnb round; *)
round
let update_round_nb e =
match Hashtbl.find_opt roundtbl e.nb with
| None -> ()
| Some (n,_) -> roundnb := n
(* go to next round *)
let next_round e =
let ne = next_cond e round in
ne
(**********************************************************************)
(* redefine (more meaningful) step and back-step for sasa *)
......@@ -58,92 +150,6 @@ let sd () = s();!dot_view();;
let bd()= e:=prev !e ; emacs_udate !e; pe();!dot_view();;
(**********************************************************************)
(** Computing rounds *)
(* a process can be removed from the mask if one action of p is triggered
or if no action of p is enabled *)
let get_removable pl =
let pl = List.filter
(fun p ->
(List.exists (fun (_,_,acti) -> acti) p.actions) ||
(List.for_all (fun (_,enab,_) -> (not enab)) p.actions)
)
pl
in
List.map (fun p -> p.name) pl
let verbose = ref false
let last_round = ref 0
let mask = ref [] (* nodes we look the activation of *)
(* called at each event via the time-travel hook *)
let (round : RdbgEvent.t -> bool) =
fun e ->
try
let croundnb, round = Hashtbl.find roundtbl e.nb in
(* Printf.printf "round tabulated at e.nb %d: croundnb=%d round = %b\n%!" *)
(* e.nb croundnb round; *)
roundnb := croundnb;
round
with Not_found ->
let round =
( if args.salut_mode then
e.kind = Exit && e.name = "mv_hook" && e.step > 1
else
e.kind = Ltop
)
&&
let (pl : process list) = get_processes e in
let rm_me = get_removable pl in
if !verbose then (
Printf.printf "Mask : %s\n" (String.concat "," !mask);
Printf.printf "To remove from mask: %s\n" (String.concat "," rm_me);
flush stdout;
);
mask := List.filter (fun pid -> not (List.mem pid rm_me)) !mask;
let res = !mask = [] ||
(* when round is called twice, it should have the same
result *)
!last_round = e.nb / 2
in
if !mask = [] then (
last_round := e.nb / 2;
mask := (
let p_with_enable_action =
List.filter
(fun p -> List.exists
(fun (_,enab,acti) -> enab && not(acti)) p.actions)
pl
in
let pidl = List.map (fun p -> p.name) p_with_enable_action in
let pidl = List.rev pidl in
if !verbose then (
Printf.printf "Next mask : %s\n" (String.concat "," pidl);
flush stdout
);
pidl
)
);
res
in
if round && e.nb > 2 then incr roundnb;
Hashtbl.add roundtbl e.nb (!roundnb, round);
(* Printf.printf "round computed at e.nb %d: croundnb=%d round = %b\n%!"
e.nb !roundnb round; *)
round
let update_round_nb e =
match Hashtbl.find_opt roundtbl e.nb with
| None -> ()
| Some (n,_) -> roundnb := n
(* go to next round *)
let next_round e =
let ne = next_cond e round in
ne
let nr () = e:=next_round !e; store !e.nb; !dot_view ();;
let pr () =
......@@ -157,10 +163,10 @@ let pr () =
let u () = undo (); ignore (round !e);;
let r () =
r ();
roundnb := 1;
Hashtbl.clear roundtbl;
ckpt_list := [!e];
ignore (round !e);;
round_init ();
ignore (round !e);
(* if the first event is not a round, add it as a check_point *)
if !ckpt_list = [] then ckpt_list := [!e];;
(**********************************************************************)
(* print_event tuning *)
......@@ -312,7 +318,7 @@ let _ =
(**********************************************************************)
(* Perform the checkpointing at rounds! *)
let _ = check_ref := round;;
let _ = check_ref := fun e -> e.nb = 1 || round e;;
(**********************************************************************)
let _ =
......
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