rdbg: add the legitimate value in the rdbg event

lib/sasa/sasaRun.ml

@@ -51,6 +51,21 @@ let (compute_potentiel: ('v Process.t * 'v Register.neighbor list) list ->
     in 
     let p = (user_pf pidl get_info) in
     [("potential", Data.F p)]
+    
+let (compute_legitimate: bool -> ('v Process.t * 'v Register.neighbor list) list ->
+     'v Env.t -> bool) =
+  fun silent p_nl_l ne ->
+  silent ||
+  match Register.get_legitimate () with
+  | None -> silent 
+  | Some f ->
+    let pidl = List.map (fun (p,_) -> p.Process.pid) p_nl_l in
+    let get_info pid =
+      let nl = snd (List.find (fun (p,_) -> p.Process.pid = pid) p_nl_l) in
+      Env.get ne pid,
+      List.map (fun n -> n, n.Register.pid) nl
+    in 
+    f pidl get_info
 
 (* The nl local state needs to be updated w.r.t. e *)
 let update_p_nl_l e p_nl_l = List.map
@@ -74,7 +89,7 @@ let (make_do: string array -> SasArg.t ->
     in
     let vntl_o =
       if Register.get_potential () = None then vntl_o else ("potential", Data.Real)::vntl_o in
-    let vntl_o = ("silent", Data.Bool)::vntl_o in
+    let vntl_o = ("silent", Data.Bool)::("legitimate", Data.Bool)::vntl_o in
     let pre_enable_processes_opt = ref None in
     let sasa_env = ref e in
     let reset () =
@@ -93,8 +108,9 @@ let (make_do: string array -> SasArg.t ->
             let sasa_nenv = from_sasa_env p_nl_l e in 
             let pot_sl = compute_potentiel p_nl_l e in
             let silent = List.for_all (fun b -> not b) (List.flatten enab_ll) in
+            let legit = compute_legitimate silent p_nl_l e in
             pre_enable_processes_opt := Some(pnall, enab_ll);
-            ("silent", Data.B silent)::pot_sl @ sasa_nenv @ (get_sl_out true pl enab_ll)
+            ("legitimate", Data.B legit)::pot_sl @ 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 *)
@@ -108,11 +124,12 @@ let (make_do: string array -> SasArg.t ->
           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 silent = List.for_all (fun b -> not b) (List.flatten enab_ll) in
           let pot_sl = compute_potentiel new_p_nl_l ne in
+          let silent = List.for_all (fun b -> not b) (List.flatten enab_ll) in
+          let legit = compute_legitimate silent p_nl_l e in
           pre_enable_processes_opt := Some(pnall, enab_ll);
           sasa_env := ne;    
-          ("silent", Data.B silent)::pot_sl @ sasa_nenv @ (get_sl_out true pl enab_ll) 
+          ("legitimate", Data.B legit)::pot_sl @ sasa_nenv @ (get_sl_out true pl enab_ll) 
     in
     let (step_internal_daemon: RdbgPlugin.sl -> RdbgPlugin.sl) =
       fun sl_in ->
@@ -123,8 +140,10 @@ let (make_do: string array -> SasArg.t ->
         let pnall, enab_ll = Sasacore.Main.get_enable_processes p_nl_l e in
         let pot_sl = compute_potentiel p_nl_l e in
         let silent = List.for_all (fun b -> not b) (List.flatten enab_ll) in
+        let legit = compute_legitimate silent p_nl_l e in
         if silent then (
-          ("silent", Data.B true)::(from_sasa_env p_nl_l e) @ (get_sl_out true pl enab_ll) 
+          ("silent", Data.B silent)::("legitimate", Data.B legit)::
+          (from_sasa_env p_nl_l e) @ (get_sl_out true pl enab_ll) 
         )
         else
           (* 2: read the actions from the outside process, i.e., from sl_in *)
@@ -135,7 +154,7 @@ let (make_do: string array -> SasArg.t ->
           (* 3: Do the steps *)
           let ne = Sasacore.Step.f pnal e in
           sasa_env := ne;
-          ("silent", Data.B false)::pot_sl @
+          ("silent", Data.B silent)::("legitimate", Data.B legit)::pot_sl @
           (from_sasa_env p_nl_l e) @ (get_sl_out true pl enab_ll) @
           (get_sl_out false pl activate_val)
     in

test/dijkstra-ring/Makefile

-# Time-stamp: <modified the 01/09/2020 (at 17:18) by Erwan Jahier>
+# Time-stamp: <modified the 04/11/2020 (at 09:42) by Erwan Jahier>
 
 
 test: ring.cmxs lurette1 rdbg_test
@@ -18,6 +18,8 @@ gnuplot: dijkstra-ring.rif
 
 rdbg: ring.ml ring.lut
 	ledit rdbg -o ring.rif -sut "$(sasa) ring.dot -dd -rif"
+rdbgui: ring.ml ring.lut
+	 rdbgui4sasa -o ring.rif -sut "$(sasa) ring.dot -dd -rif"
 
 rdbg2: ring.ml ring.lut
 	ledit rdbg -o ring.rif  \

test/sasa-rdbg-cmds.ml

@@ -244,8 +244,13 @@ let _ = add_doc_entry
     "is the event correspond to a silent configuration? (i.e., no enable node)"
     "sasa" "sasa-rdbg-cmds.ml";;
 
+let is_legitimate e =
+  match List.assoc_opt "legitimate" e.data with
+  | Some B b -> b
+  | _ -> assert false
 
-let legitimate = silence;;
+let goto_legitimate e = next_cond e is_legitimate 
+let legitimate () =  e:=goto_legitimate !e; !dot_view ();;
 let _ = add_doc_entry
     "legitimate" "unit -> unit"
     "  Move forward until a legitimate configuration is reached (uses 'silence' by default)"