From abaa00b19cf5a590da117fdb8c6b7f14c09ee7a6 Mon Sep 17 00:00:00 2001 From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr> Date: Mon, 27 Feb 2023 16:59:56 +0100 Subject: [PATCH] test: change the state scan/parse conventions so that it is compatible with the dot output of --global-init-search --- test/k-clustering/fig52_kcl.dot | 19 +++++++++---------- test/k-clustering/p.ml | 18 +++++++++--------- test/k-clustering/state.ml | 16 ++++++---------- 3 files changed, 24 insertions(+), 29 deletions(-) diff --git a/test/k-clustering/fig52_kcl.dot b/test/k-clustering/fig52_kcl.dot index b9f15d3e..b56453c8 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 9928fa0e..f0dcdc05 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 9492421d..a0d406f1 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 - -- GitLab