diff --git a/test/k-clustering/fig52_kcl.dot b/test/k-clustering/fig52_kcl.dot index b9f15d3e85df3ea748c55f5eba2e8a9688ee06b6..b56453c8707af460c9a3d1a5441453a4a673be91 100644 --- a/test/k-clustering/fig52_kcl.dot +++ b/test/k-clustering/fig52_kcl.dot @@ -1,14 +1,13 @@ graph fig52 { - - Root [algo="p.ml" init="{is_root=1 ; alpha=0; par=-1}"] - p2 [algo="p.ml" init="{is_root=0 ; alpha=0; par=0}"] - p3 [algo="p.ml" init="{is_root=0 ; alpha=0; par=0}"] - p4 [algo="p.ml" init="{is_root=0 ; alpha=0; par=0}"] - p5 [algo="p.ml" init="{is_root=0 ; alpha=0; par=0}"] - p6 [algo="p.ml" init="{is_root=0 ; alpha=0; par=0}"] - p7 [algo="p.ml" init="{is_root=0 ; alpha=0; par=0}"] - Root -- p2 -- p3 -- p4 -- p5 -- p6 + Root [algo="p.ml" init="isRoot=true alpha=0 par=-1"] + p2 [algo="p.ml" init="isRoot=false alpha=0 par=0"] + p3 [algo="p.ml" init="isRoot=false alpha=0 par=0"] + p4 [algo="p.ml" init="isRoot=false alpha=0 par=0"] + p5 [algo="p.ml" init="isRoot=false alpha=0 par=0"] + p6 [algo="p.ml" init="isRoot=false alpha=0 par=0"] + p7 [algo="p.ml" init="isRoot=false alpha=0 par=0"] + + Root -- p2 -- p3 -- p4 -- p5 -- p6 p5 -- p7 } - diff --git a/test/k-clustering/p.ml b/test/k-clustering/p.ml index 9928fa0e3f3a89646d836f5c034278afb0ec8210..f0dcdc05682117eae9efd386aebe19b84babce0b 100644 --- a/test/k-clustering/p.ml +++ b/test/k-clustering/p.ml @@ -1,5 +1,5 @@ (* -Algorithm 1 of: +Algorithm 1 of: A Framework for Certified Self-Stabilization Case Study: Silent Self-Stabilizing k-Dominating Set on a Tree https://hal.archives-ouvertes.fr/hal-01272158/document @@ -15,12 +15,12 @@ Encoded by Hugo Hannot open Algo open State - + type s = State.t type sl = s list type n = State.t neighbor type nl = n list - + let isRoot p = (state p).isRoot let (isShort: n -> bool) = @@ -30,13 +30,13 @@ let (isTall: n -> bool) = fun p -> (state p).alpha >= k (* Actually unused *) -let (_kDominator: 'v -> bool) = - fun p -> ((state p).alpha = k) || ((isShort p) && (isRoot p)) +let (_kDominator: 'v -> bool) = + fun p -> ((state p).alpha = k) || ((isShort p) && (isRoot p)) let (children: s -> nl -> nl) = fun _p nl -> List.filter (fun q -> (state q).par = reply q) nl - + let (shortChildren: s -> nl -> nl) = fun p nl -> List.filter isShort (children p nl) @@ -60,7 +60,7 @@ let rec (min: nl -> int -> int) = | n::tail -> let s = state n in if (s.alpha) < cur then min tail (s.alpha) else min tail cur - + let (maxAShort: s -> nl -> int) = fun p nl -> max (shortChildren p nl) (-1) @@ -83,8 +83,8 @@ let (init_state: int -> string -> s) = isRoot = pid = "Root"; (* ZZZ: The root of the tree should be named "Root"! *) alpha = Random.int (2*k+1); par = if pid="Root" then -1 else 0 (* the input tree should be sorted alphabetically (wrt a bf traversal) *) - } - + } + let (enable_f: s -> nl -> action list) = fun p nl -> if (p.alpha <> (newAlpha p nl)) then ["change_alpha"] else [] diff --git a/test/k-clustering/state.ml b/test/k-clustering/state.ml index 9492421d24c7270f43354307a89f0d14db186aa0..a0d406f18795d4ad96f992d9e979bbc3f1f0cf96 100644 --- a/test/k-clustering/state.ml +++ b/test/k-clustering/state.ml @@ -1,8 +1,8 @@ -(* Time-stamp: <2022-07-12 11:01:25 emile> *) +(* Time-stamp: <modified the 12/02/2023 (at 22:18) by Erwan Jahier> *) open Algo - -let d = max_degree() + +let d = max_degree() type t = { isRoot:bool; @@ -10,20 +10,16 @@ type t = { par:int } -(*let boolVint (b:bool):int = - if b then 1 else 0*) - let (to_string: (t -> string)) = fun s -> - Printf.sprintf "isRoot=%b alpha=%d par=%d" s.isRoot s.alpha s.par + Printf.sprintf "isRoot=%b alpha=%d par=%d" s.isRoot s.alpha s.par let (of_string: (string -> t) option) = Some (fun s -> - Scanf.sscanf s "{is_root=%d ; alpha=%d ; par=%d}" - (fun i alpha p -> {isRoot = (i=1) ; alpha = alpha ; par = p })) + Scanf.sscanf s "isRoot=%B alpha=%d par=%d" + (fun b alpha p -> {isRoot = b ; alpha = alpha ; par = p })) let (copy : ('v -> 'v)) = fun x -> x let actions = ["change_alpha"] let k = 2 -