From 878e4854e8619f471e3a40e7f62c5cbbb5fbc45d Mon Sep 17 00:00:00 2001 From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr> Date: Fri, 26 May 2023 16:36:36 +0200 Subject: [PATCH] perf: fine-tune the local search in the provided exemples --- test/async-unison/config.ml | 42 ++++++++++++---------- test/coloring/config.ml | 2 +- test/dijkstra-ring/config.ml | 63 +++++++++++++++++++++------------ test/k-clustering/config.ml | 4 ++- test/st-KK06-algo1/config.ml | 10 +++++- test/st-KK06-algo2/config.ml | 2 +- test/toy-example-a5sf/config.ml | 11 +++--- 7 files changed, 85 insertions(+), 49 deletions(-) diff --git a/test/async-unison/config.ml b/test/async-unison/config.ml index e2be8f30..fb04d19a 100644 --- a/test/async-unison/config.ml +++ b/test/async-unison/config.ml @@ -1,8 +1,6 @@ open Algo -let is_close s1 s2 = - (* The absolute value of the difference modulo k is <= 1 *) - (s1 = s2) || P.modulo (s1 - s2 - 1) P.k = 0 || P.modulo (s1 - s2 + 1) P.k = 0 +let is_close s1 s2 = not (P.far s1 s2) (* A configuration is legitimate when all neigbhors are close *) let all_true = List.fold_left (&&) true @@ -14,16 +12,21 @@ let legitimate pidl get = let legitimate = Some legitimate let fault = None -let init_search_utils = None +let n2s nl _s = + match nl with + | [I(_, i, _)] -> i + | _ -> assert false +let s2vl i = [I (min 0 (i-1), i, max P.k (i+1))] + +let init_search_utils = Some(s2vl, n2s) let sumi l = List.fold_left (+) 0 l let sumf l = List.fold_left (+.) 0. l let count b = if b then 1 else 0 -(* It's actually only a pseudo-potential function (i.e., it measure a - distance to the set of stable configurations, but it is not - strictly decreasing), which is ok for simulation purposes. -*) +(* It's actually only a pseudo-potential function (i.e., it measures + a distance to the set of stable configurations, but that is not + strictly decreasing), which is ok for simulation purposes. *) let _pseudo_pot pidl get = let count_behind (clock, nl) = let nl = fst (List.split nl) in @@ -33,19 +36,20 @@ let _pseudo_pot pidl get = let count b = if b then 0. else 1. -let __pseudo_pot pidl get = - let count_far (s, nl) = - List.fold_left (fun acc (n,_) -> acc +. count (is_close s (state n))) 0. nl in - List.map (fun pid -> count_far (get pid)) pidl |> sumf -let pseudo_pot pidl get = - let count_far (s, nl) = - List.fold_left (fun acc (n,_) -> - let res = (acc +. count (is_close s (state n))) in - if res>=1.0 then 1.0 else 0.0) 0. nl - in +let count_far (s, nl) = + List.fold_left (fun acc (n,_) -> acc +. count (is_close s (state n))) 0. nl + +let count_edges pidl get = + (* count the number of edges that are out of sync *) List.map (fun pid -> count_far (get pid)) pidl |> sumf +let count_nodes pidl get = + (* count the number of nodes that are out of sync *) + List.map (fun pid -> count_far (get pid)) pidl |> List.map (min 1.0) |> sumf + + (* *) -let potential = Some pseudo_pot +(* let potential = Some count_edges *) +let potential = Some count_nodes diff --git a/test/coloring/config.ml b/test/coloring/config.ml index 2a6fba53..7284ba43 100644 --- a/test/coloring/config.ml +++ b/test/coloring/config.ml @@ -16,7 +16,7 @@ let fault = None let md = max_degree () -let s2n s = [I (0, s, md)] +let s2n s = [I (min 0 (s-1), s, max (md+1) (s+1))] let n2s nl _s = match nl with | [I(_, i, _)] -> i diff --git a/test/dijkstra-ring/config.ml b/test/dijkstra-ring/config.ml index 97f0c070..4db94dcd 100644 --- a/test/dijkstra-ring/config.ml +++ b/test/dijkstra-ring/config.ml @@ -3,24 +3,26 @@ open State (** 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 configuration is convex if there is no value that is the same than the root + is different to every other value of the ring. + + A configuration 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, z=0 2 4 5 3 0 1 3 -> convex, z=0 2 2 2 3 0 2 3 -> not convex, z=2 *) module IntSet = Set.Make(Int) - -let compute_Z root root_st (get: Algo.pid -> State.t * (State.t Algo.neighbor * Algo.pid) list) = + +let verb = false + +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 = ref IntSet.empty 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 + 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 @@ -45,54 +47,68 @@ let compute_Z root root_st (get: Algo.pid -> State.t * (State.t Algo.neighbor * (* 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 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 + 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 + if pid = root then ( + if verb then Printf.printf "\t%s=%d enabled=%b rang=%d total=%d\n%!" + pid st.v ([]<>Root.enable_f st [n_state]) rang total; + total + ) + else let total = if (P.enable_f st [n_state]) <> [] then total + rang else total in + if verb then Printf.printf "\t%s=%d enabled=%b rang=%d total=%d\n%!" + pid st.v ([]<>P.enable_f st [n_state]) rang total; compute neighbor total (rang+1) in - let succ: pid = - match get root with + let succ_root: 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 + if verb then Printf.printf " - Computing the sum_dist: \n" ; + compute succ_root 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 = match List.find_opt (fun p -> (fst (get p)).root) pidl with + | Some res -> res + | None -> assert false + in + if verb then Printf.printf "- Computing the potential: \n" ; 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 verb then Printf.printf " sum_dist=%d \n\n" sum_dist; if res < 0 then 0 else res in + if verb then Printf.printf " potential=%d z=%d \n%!" c z; float_of_int c ;; let potential = Some cost -let fault = None -(* For the Dijkstra ring, a configuration is legitimate iff there is +let fault = None + +(* For the Dijkstra ring, a configuration is legitimate iff there is exactly one token. nb: there are as many tokens as enabled nodes. So let's count enable nodes! *) let (legitimate: pid list -> (pid -> t * (t neighbor * pid) list) -> bool) = - fun pidl get -> + fun pidl get -> (* increment the token number i if pid is enabled *) let incr_token i pid = let s, nl = get pid in @@ -109,10 +125,13 @@ let legitimate = Some legitimate (* init search *) let maxi = card () + 1 -let s2n s = [I (0, s.v, maxi)] + +let _s2n s = [I (0, s.v, maxi)] +let s2n s = [I (min 0 (s.v - 1), s.v, max maxi (s.v + 1))] + let n2s nl s = match nl with | [I(_, i, _)] -> { s with v = i } | _ -> assert false - + let init_search_utils = Some (s2n, n2s) diff --git a/test/k-clustering/config.ml b/test/k-clustering/config.ml index 8ee15431..02fc2c07 100644 --- a/test/k-clustering/config.ml +++ b/test/k-clustering/config.ml @@ -84,7 +84,9 @@ let fault = None open State let maxi = 2*k+1 -let s2n s = [I (0, s.alpha, maxi)] +let _s2n s = [I (0, s.alpha, maxi)] +let s2n s = [I (min 0 (s.alpha - 1), s.alpha, max maxi (s.alpha + 1))] + let n2s nl s = match nl with | [I(_, i, _)] -> { s with alpha = i } diff --git a/test/st-KK06-algo1/config.ml b/test/st-KK06-algo1/config.ml index a739ae06..1cc94b72 100644 --- a/test/st-KK06-algo1/config.ml +++ b/test/st-KK06-algo1/config.ml @@ -1,5 +1,13 @@ +open Algo let legitimate = None let fault = None -let init_search_utils = None let potential = Some Potential.f + + +let n2s nl _s = + match nl with + | [I(_, i, _)] -> i + | _ -> assert false +let s2vl i = [I (min 0 (i-1), i, i+1)] +let init_search_utils = Some(s2vl, n2s) diff --git a/test/st-KK06-algo2/config.ml b/test/st-KK06-algo2/config.ml index f61e2eed..3fdb05a9 100644 --- a/test/st-KK06-algo2/config.ml +++ b/test/st-KK06-algo2/config.ml @@ -3,7 +3,7 @@ (*sasa -reg ring.dot*) -let potential = None (* None => only -sd, -cd, -lcd, -dd, or -custd are possible *) +let potential = Some Potential.f (* None => only -sd, -cd, -lcd, -dd, or -custd are possible *) let legitimate = None (* None => only silent configuration are legitimate *) let fault = None (* None => the simulation stop once a legitimate configuration is reached *) let init_search_utils = None diff --git a/test/toy-example-a5sf/config.ml b/test/toy-example-a5sf/config.ml index c1abf6a7..df8ed356 100644 --- a/test/toy-example-a5sf/config.ml +++ b/test/toy-example-a5sf/config.ml @@ -49,12 +49,15 @@ let fault = None let mini= 0 let maxi = max_degree () -let s2n s = [I(mini, s.input, 100); I(mini, s.par, maxi); - I(mini, s.sub, 100); I(mini, s.res, 100)] +(* the par field is an input of the algorithm that should not be + modified *) + +let s2n s = [I(min mini (s.input-1), s.input, s.input+1); + I(min mini (s.sub-1), s.sub, s.sub+1); I(min mini (s.res-1), s.res, s.res+1)] let n2s nl s = match nl with - | [I(_, input, _); I(_, par, _); I(_, sub, _); I(_, res, _)] -> - { s with input; par; sub; res } + | [I(_, input, _); I(_, sub, _); I(_, res, _)] -> + { s with input; sub; res } | _ -> assert false let init_search_utils = Some (s2n, n2s) -- GitLab