From 4d08c6e12b0d829d9d245b9bdee63b4e07171a1d Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Tue, 7 Jul 2020 16:30:53 +0200
Subject: [PATCH] Update: Use the user-defined legitimate function if provided

---
 lib/algo/algo.ml     | 23 ++++++++++++++++++----
 lib/algo/algo.mli    |  2 +-
 src/sasaMain.ml      | 47 ++++++++++++++++++++++++++++++++++----------
 test/unison/state.ml | 14 ++++++++++++-
 4 files changed, 70 insertions(+), 16 deletions(-)

diff --git a/lib/algo/algo.ml b/lib/algo/algo.ml
index 35775ae9..7a4b780d 100644
--- a/lib/algo/algo.ml
+++ b/lib/algo/algo.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 07/07/2020 (at 14:41) by Erwan Jahier> *)
+(* Time-stamp: <modified the 07/07/2020 (at 16:11) by Erwan Jahier> *)
 
 open Sasacore
 (* Process programmer API *)
@@ -35,15 +35,16 @@ let (reply : 's neighbor -> int) = fun s -> s.reply ()
                 
 (** Makes sense in directed graphs only *)
 let (weight : 's neighbor -> int) = fun s -> s.weight ()
-                    
+                
+module PidMap = Map.Make(String)
 
+type pid = string
 type 's enable_fun = 's -> 's neighbor list -> action list
 type 's step_fun   = 's -> 's neighbor list -> action -> 's
 type 's state_init_fun = int -> string -> 's
 type 's fault_fun = int -> string -> 's -> 's
-type 's legitimate_fun = string list -> (string -> 's * 's neighbor list) -> bool
+type 's legitimate_fun = pid list -> (pid -> 's * 's neighbor list) -> bool
 
-type pid = string
 type 's pf_info = { neighbors: 's neighbor list; curr: 's ; next: 's; action: action }
 type 's potential_fun = pid list -> (pid -> 's pf_info) -> float
 
@@ -100,6 +101,16 @@ let (to_reg_potential_fun :
   let nf pid = to_reg_info (f pid) in
   pf pidl nf
 
+let (to_reg_legitimate_fun :
+       's legitimate_fun -> pid list -> (pid -> 's * 's Register.neighbor list) -> bool) =
+  fun lf pidl from_pid ->
+  let n_from_pid pid =
+    let s, nl = from_pid pid in
+    s, List.map to_reg_neigbor nl
+  in
+    lf pidl n_from_pid
+  
+  
 let (register1 : 's algo_to_register -> unit) =
   fun s ->
     Register.reg_enable     s.algo_id (to_reg_enable_fun s.enab);
@@ -122,6 +133,10 @@ let (register : 's to_register -> unit) =
      | None -> ()
      | Some pf -> Register.reg_potential (Some (to_reg_potential_fun pf))
     );
+    (match s.legitimate_function with
+     | None -> ()
+     | Some ff -> Register.reg_legitimate (Some (to_reg_legitimate_fun ff))
+    );
     (match s.fault_function with
      | None -> ()
      | Some ff -> Register.reg_fault (Some ff)
diff --git a/lib/algo/algo.mli b/lib/algo/algo.mli
index 62920092..801bd0ba 100644
--- a/lib/algo/algo.mli
+++ b/lib/algo/algo.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 07/07/2020 (at 14:41) by Erwan Jahier> *)
+(* Time-stamp: <modified the 07/07/2020 (at 16:11) by Erwan Jahier> *)
 (** {1 The Algorithm programming Interface.} *)
 (** 
     {1 What's need to be provided by users.}
diff --git a/src/sasaMain.ml b/src/sasaMain.ml
index 13513467..95ff58e6 100644
--- a/src/sasaMain.ml
+++ b/src/sasaMain.ml
@@ -31,6 +31,7 @@ let (print_step : int -> int -> SasArg.t -> 'v Env.t -> 'v Process.t list -> str
   )
   
 exception Silent of int
+exception Legitimate of int 
 let moves  = ref 0
 let rounds = ref 0
 let round_mask = ref []
@@ -45,13 +46,26 @@ let (update_round : bool list list -> bool list list -> unit) =
     incr rounds
   );
   ()
+
+let legitimate p_nl_l e =
+  match Register.get_legitimate () with
+  | None -> false
+  | Some ulf ->
+     let pidl =  List.map (fun (p,_) -> p.Process.pid) p_nl_l in
+     let rec from_pid p_nl_l pid = (* XXX use StringMap instead *)
+       match p_nl_l with
+       | [] -> assert false (* sno *)
+       | (p,nl)::tail ->
+          if p.Process.pid = pid then Env.get e pid, nl else from_pid tail pid
+     in
+     ulf pidl (from_pid p_nl_l)
   
 let (simustep: int -> int -> SasArg.t -> string -> 
       ('v Process.t * 'v Register.neighbor list) list -> 'v Env.t -> 'v Env.t * string) =
-  fun n i args activate_val pl_n e ->
+  fun n i args activate_val p_nl e ->
     (* 1: Get enable processes *)
-    let all, enab_ll = Sasacore.Main.get_enable_processes pl_n e in
-    let pl = fst(List.split pl_n) in
+    let all, enab_ll = Sasacore.Main.get_enable_processes p_nl e in
+    let pl = fst(List.split p_nl) in
     List.iter (List.iter (fun b -> if b then incr moves)) enab_ll;
     
     if
@@ -60,7 +74,12 @@ let (simustep: int -> int -> SasArg.t -> string ->
       print_step n i args e pl activate_val enab_ll;
       incr rounds;
       raise (Silent (n-i+1))
-    ) else 
+    ) else if legitimate p_nl e then (
+      print_step n i args e pl activate_val enab_ll;
+      raise (Legitimate (n-i+1))
+    )
+    else 
+
     if args.daemon = Daemon.Custom then
       print_step n i args e pl activate_val enab_ll;
     (* 2: read the actions *)
@@ -82,20 +101,19 @@ let (simustep: int -> int -> SasArg.t -> string ->
       print_step n i args e pl next_activate_val enab_ll;
     ne, next_activate_val
 
-
 let rec (simuloop: int -> int -> SasArg.t -> string -> 
          ('v Process.t * 'v Register.neighbor list) list -> 'v Env.t -> unit) =
-  fun n i args activate_val pl_n e ->
-  let ne, next_activate_val = simustep n i args activate_val pl_n e in
-  if i > 0 then simuloop n (i-1) args next_activate_val pl_n ne else (
+  fun n i args activate_val p_nl e ->
+  let ne, next_activate_val = simustep n i args activate_val p_nl e in
+  if i > 0 then simuloop n (i-1) args next_activate_val p_nl ne else (
     print_string "#q\n"; flush stdout
   )
 
 let () =
-  let args, pl_n, e = Sasacore.Main.make true Sys.argv in
+  let args, p_nl, e = Sasacore.Main.make true Sys.argv in
   try
     let n = args.length in
-    simuloop n n args "" pl_n e
+    simuloop n n args "" p_nl e
   with
   | Failure msg -> Printf.eprintf " [sasa] Error: %s\n%!" msg
   | Silent i ->
@@ -107,3 +125,12 @@ let () =
     print_string "\n#quit\n"; 
     flush stderr;
     flush stdout
+  | Legitimate i ->
+    let str = if args.rif then "#" else "" in
+    Printf.eprintf "\n%sThis algo Reached a legitimate configuration after %i moves, %i steps, %i rounds.\n"
+      str !moves i !rounds;
+    flush stderr;
+    flush stdout;
+    print_string "\n#quit\n"; 
+    flush stderr;
+    flush stdout
diff --git a/test/unison/state.ml b/test/unison/state.ml
index 8c9164f1..2b1f745b 100644
--- a/test/unison/state.ml
+++ b/test/unison/state.ml
@@ -5,5 +5,17 @@ let of_string = None
 let copy x = x
 let actions = ["g"]
 let potential = None
-let legitimate = None
 let fault = None
+
+let legitimate pidl from_pid =
+  (* a legitimate configuration is reached when all states have the same values *)
+  let v = fst(from_pid (List.hd pidl)) in
+  List.fold_left
+    (fun acc pid -> acc && fst(from_pid pid) = v)
+    true
+    (List.tl pidl)
+  
+  
+let legitimate = Some legitimate
+                   
+                     
-- 
GitLab