From e2a2748bd2a1ef768475c6ba03aeab5786d0d592 Mon Sep 17 00:00:00 2001
From: erwan <erwan.jahier@univ-grenoble-alpes.fr>
Date: Sat, 31 Jul 2021 09:19:09 +0200
Subject: [PATCH] fix: the internal greedy daemons were wrong
---
lib/sasa/sasaRun.ml | 4 +-
lib/sasacore/daemon.ml | 5 ++-
lib/sasacore/daemon.mli | 4 +-
lib/sasacore/evil.ml | 10 ++---
lib/sasacore/evil.mli | 6 +--
src/sasaMain.ml | 2 +-
test/dijkstra-ring/config.ml | 79 +++++++++++++++++++++++++++++++++++-
7 files changed, 94 insertions(+), 16 deletions(-)
diff --git a/lib/sasa/sasaRun.ml b/lib/sasa/sasaRun.ml
index adac46d8..441686aa 100644
--- a/lib/sasa/sasaRun.ml
+++ b/lib/sasa/sasaRun.ml
@@ -104,7 +104,7 @@ let (make_do: string array -> 'v SimuState.t -> RdbgPlugin.t) =
(* 2: read the actions from the outside process, i.e., from sl_in *)
let _, pnal = Daemon.f st.sasarg.dummy_input
(st.sasarg.verbose > 0) st.sasarg.daemon st.network
- (SimuState.neigbors_of_pid st) st pre_pnall pre_enab_ll
+ SimuState.neigbors_of_pid st pre_pnall pre_enab_ll
(get_action_value sl_in) Step.f
in
(* 3: Do the steps *)
@@ -143,7 +143,7 @@ let (make_do: string array -> 'v SimuState.t -> RdbgPlugin.t) =
let activate_val, pnal =
Daemon.f st.sasarg.dummy_input
(st.sasarg.verbose > 0) st.sasarg.daemon st.network
- (SimuState.neigbors_of_pid st) st pnall enab_ll
+ SimuState.neigbors_of_pid st pnall enab_ll
(get_action_value sl_in) Step.f
in
(* 3: Do the steps *)
diff --git a/lib/sasacore/daemon.ml b/lib/sasacore/daemon.ml
index 3f475466..ea58b0fb 100644
--- a/lib/sasacore/daemon.ml
+++ b/lib/sasacore/daemon.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 18/06/2021 (at 16:23) by Erwan Jahier> *)
+(* Time-stamp: <modified the 31/07/2021 (at 09:15) by Erwan Jahier> *)
(* Enabled processes (with its enabling action + neighbors) *)
type 'v pna = 'v Process.t * 'v Register.neighbor list * Register.action
@@ -134,7 +134,8 @@ let (get_activate_val: 'v triggered -> 'v Process.t list -> bool list list)=
List.map (List.map (fun a -> List.mem a al)) actions
let (f: bool -> bool -> DaemonType.t -> 'v Process.t list ->
- (string -> 'v * ('v Register.neighbor * string) list) -> 'v SimuState.t ->
+ ('v SimuState.t -> string -> 'v * ('v Register.neighbor * string) list) ->
+ 'v SimuState.t ->
'v enabled -> bool list list -> (string -> string -> bool) -> 'v step ->
bool list list * 'v triggered) =
fun dummy_in verbose_mode daemon pl neigbors_of_pid st all enab get_action_value step ->
diff --git a/lib/sasacore/daemon.mli b/lib/sasacore/daemon.mli
index ae21beac..aa0ba559 100644
--- a/lib/sasacore/daemon.mli
+++ b/lib/sasacore/daemon.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 18/06/2021 (at 16:22) by Erwan Jahier> *)
+(* Time-stamp: <modified the 31/07/2021 (at 09:15) by Erwan Jahier> *)
type 'v pna = 'v Process.t * 'v Register.neighbor list * Register.action
type 'v enabled = 'v pna list list
@@ -33,7 +33,7 @@ nb: it is possible that we read on stdin that an action should be
type 'v step = 'v triggered -> 'v SimuState.t -> 'v SimuState.t
val f : bool -> bool -> DaemonType.t -> 'v Process.t list ->
- (string -> 'v * ('v Register.neighbor * string) list) ->
+ ('v SimuState.t -> string -> 'v * ('v Register.neighbor * string) list) ->
'v SimuState.t -> 'v enabled -> bool list list ->
(string -> string -> bool) -> 'v step -> bool list list * 'v triggered
diff --git a/lib/sasacore/evil.ml b/lib/sasacore/evil.ml
index 2612a0ad..6689d779 100644
--- a/lib/sasacore/evil.ml
+++ b/lib/sasacore/evil.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 18/06/2021 (at 16:25) by Erwan Jahier> *)
+(* Time-stamp: <modified the 31/07/2021 (at 09:15) by Erwan Jahier> *)
type 'v pna = 'v Process.t * 'v Register.neighbor list * Register.action
type 'v enabled = 'v pna list list
@@ -122,7 +122,7 @@ let time3 verb lbl f x y z =
fxy
let (greedy: bool -> 'v SimuState.t -> 'v Process.t list ->
- (string -> 'v * ('v Register.neighbor * string) list) ->
+ ('v SimuState.t -> string -> 'v * ('v Register.neighbor * string) list) ->
'v step -> 'v pna list list -> 'v pna list) =
fun verb st pl neigbors_of_pid step all ->
assert (all<>[]);
@@ -133,7 +133,7 @@ let (greedy: bool -> 'v SimuState.t -> 'v Process.t list ->
let pidl = List.map (fun p -> p.Process.pid) pl in
let nst = step pnal st in
let get_info pid =
- let _, nl = neigbors_of_pid pid in
+ let _, nl = neigbors_of_pid nst pid in
Env.get nst.config pid, nl
in
user_pf pidl get_info
@@ -167,7 +167,7 @@ let (greedy: bool -> 'v SimuState.t -> 'v Process.t list ->
(* val greedy_central: bool -> 'v Env.t -> ('v Process.t * 'v Register.neighbor list) list -> *)
let (greedy_central: bool -> 'v SimuState.t -> 'v Process.t list ->
- (string -> 'v * ('v Register.neighbor * string) list) ->
+ ('v SimuState.t -> string -> 'v * ('v Register.neighbor * string) list) ->
'v step -> 'v pna list list -> 'v pna list) =
fun verb st pl neigbors_of_pid step all ->
assert (all<>[]);
@@ -178,7 +178,7 @@ let (greedy_central: bool -> 'v SimuState.t -> 'v Process.t list ->
let pidl = List.map (fun p -> p.Process.pid) pl in
let nst = step [pna] st in
let get_info pid =
- let _, nl = neigbors_of_pid pid in
+ let _, nl = neigbors_of_pid nst pid in
Env.get nst.config pid, nl
in
user_pf pidl get_info
diff --git a/lib/sasacore/evil.mli b/lib/sasacore/evil.mli
index 5d6a5366..4ffc604b 100644
--- a/lib/sasacore/evil.mli
+++ b/lib/sasacore/evil.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 18/06/2021 (at 16:25) by Erwan Jahier> *)
+(* Time-stamp: <modified the 31/07/2021 (at 09:15) by Erwan Jahier> *)
(** This module gathers daemons that tries to reach the worst case with
@@ -13,13 +13,13 @@ type 'v step = 'v triggered -> 'v SimuState.t -> 'v SimuState.t
among the combinations of length 1, i.e., O(2^n) where n is the
number of enabled processes (|all|) *)
val greedy: bool -> 'v SimuState.t -> 'v Process.t list ->
- (string -> 'v * ('v Register.neighbor * string) list) ->
+ ('v SimuState.t -> string -> 'v * ('v Register.neighbor * string) list) ->
'v step -> 'v enabled -> 'v triggered
(** Ditto, but for central daemons (of a connected component) *)
val greedy_central:
bool -> 'v SimuState.t -> 'v Process.t list ->
- (string -> 'v * ('v Register.neighbor * string) list) ->
+ ('v SimuState.t -> string -> 'v * ('v Register.neighbor * string) list) ->
'v step -> 'v enabled -> 'v triggered
(** Returns the worst case among the combinations of length 1 for
diff --git a/src/sasaMain.ml b/src/sasaMain.ml
index dffad89e..4d51a689 100644
--- a/src/sasaMain.ml
+++ b/src/sasaMain.ml
@@ -144,7 +144,7 @@ let (simustep: int -> int -> string -> 'v SimuState.t -> 'v SimuState.t * string
if verb then Printf.eprintf "==> SasaSimuState.simustep : 2: read the actions\n%!";
let get_action_value = RifRead.bool (st.sasarg.verbose > 1) in
let next_activate_val, pnal = Daemon.f st.sasarg.dummy_input
- (st.sasarg.verbose >= 1) st.sasarg.daemon st.network (SimuState.neigbors_of_pid st)
+ (st.sasarg.verbose >= 1) st.sasarg.daemon st.network SimuState.neigbors_of_pid
st all enab_ll get_action_value Step.f
in
List.iter (List.iter (fun b -> if b then incr moves)) next_activate_val;
diff --git a/test/dijkstra-ring/config.ml b/test/dijkstra-ring/config.ml
index d017e2e0..495e7490 100644
--- a/test/dijkstra-ring/config.ml
+++ b/test/dijkstra-ring/config.ml
@@ -1,7 +1,84 @@
open Algo
open State
-let potential = None
+(** Computes the value Z of the book, that is 0 if the values are convex,
+ * and the minimum number of incrementations the root has to do so that its value
+ * is different to every other value of the ring.
+ *
+ * A disposition is convex if there is no value that is the same than the root seperated from the
+ * root with another value.
+ * 2 2 2 3 0 1 3 -> convex
+ * 2 4 5 3 0 1 3 -> convex
+ * 2 2 2 3 0 2 3 -> not convex
+ *)
+let compute_Z root root_st (get: Algo.pid -> State.t * (State.t Algo.neighbor * Algo.pid) list) =
+ let v = root_st.v in
+ let used = Array.make (card () + 1) false in
+ let rec convex pid encountered res =
+ (* Printf.eprintf (if encountered then "<" else "|"); *)
+ (* Printf.eprintf (if res then ">" else "|"); *)
+ let next_st, next =
+ match get pid with
+ (_, [s,n]) -> state s, n | _ -> failwith "Can't compute the cost of a topology that is not a directed ring"
+ in
+ if next = root then res
+ else
+ let next_v = next_st.v in
+ (* Printf.eprintf "%s %d" next next_v; *)
+ used.(next_v) <- true;
+ convex next (encountered || next_v = v) (res && (not encountered || next_v = v))
+ in
+ if convex root false true
+ then 0
+ else
+ let rec get_min_free cur_val dist =
+ if cur_val = v then assert false;
+ if not used.(cur_val) then dist
+ else
+ get_min_free ((cur_val + 1) mod (card () + 1)) (dist + 1)
+ in
+ get_min_free (v+1) 1
+;;
+
+(* Computes the sum_dist as described in the book. It is the sum of the distance
+ from each token to the root *)
+let compute_sd (root: pid) (get: Algo.pid -> State.t * (State.t Algo.neighbor * Algo.pid) list) =
+ let rec compute pid total rang =
+ if pid = root then total
+ else
+ let st, ((n_state, neighbor): 's * pid) =
+ match get pid with
+ (st, [n]) -> st, n | _ -> failwith "Can't compute the cost of a topology that is not a directed ring"
+ in
+ let total = if (P.enable_f st [n_state]) <> [] then total + rang else total in
+ compute neighbor total (rang+1)
+ in
+ let succ: pid =
+ match get root with
+ (_, [_, n]) -> n | _ -> failwith "Can't compute the cost of a topology that is not a directed ring"
+ in
+ compute succ 0 1
+;;
+
+(* Computes the cost (it's the regular cost not the tighter_cost) *)
+let cost : pid list -> (pid -> t * (t neighbor * pid) list) -> float =
+ fun pidl get ->
+ let root = List.find (fun p -> (fst (get p)).root) pidl in
+ let root_st = fst (get root) in
+ let n = card() in
+
+ let z = compute_Z root root_st get in
+ let c = if z = (n - 1)
+ then (3 * n * (n - 1) / 2) - n - 1
+ else
+ let sum_dist = compute_sd root get in
+ let res = z * n + sum_dist - 2 in
+ if res < 0 then 0 else res
+ in
+ float_of_int c
+;;
+
+let potential = Some cost
let fault = None
(* For the Dijkstra ring, a configuration is legitimate iff there is
--
GitLab