Skip to content
Snippets Groups Projects
Commit c97c8333 authored by erwan's avatar erwan
Browse files

feat: sort neighbors alpha-numerically (to automate k-clustering tests)

+ finish/fix the k-clustering algo
+ add it in the non-reg test list
parent 8c26df18
No related branches found
No related tags found
No related merge requests found
Pipeline #100311 failed
(* Time-stamp: <modified the 25/04/2022 (at 15:40) by Erwan Jahier> *) (* Time-stamp: <modified the 26/05/2022 (at 12:16) by Erwan Jahier> *)
(** {1 The Algorithm programming Interface} (** {1 The Algorithm programming Interface}
A SASA process is an instance of an algorithm defined via this A SASA process is an instance of an algorithm defined via this
...@@ -83,13 +83,14 @@ type 's fault_fun = int -> string -> 's -> 's ...@@ -83,13 +83,14 @@ type 's fault_fun = int -> string -> 's -> 's
(** Returns the neighbor processes local state *) (** Returns the neighbor processes local state *)
val state : 's neighbor -> 's val state : 's neighbor -> 's
(** Returns the neighbor channel number, that let this neighbor access (** Returns the neighbor channel number, that let this neighbor
to the content of the current process, if its neighbor can access access to the content of the current process, if its neighbor can
it. The channel number is the rank, starting at 0, in the access it. The channel number is the rank, starting at 0, in the
neighbors' list. Returns -1 if the neighbor can not access to the neighbors' list, which are sorted alphabetically. Returns -1 if
process, which may happen in directed graphs. the neighbor can not access to the process, which may happen in
directed graphs.
An algorithm that uses reply, and not the pid, is called An algorithm that uses reply, and not the pid, is called
semi-anonymous. It is called anonymous if it can access none. *) semi-anonymous. It is called anonymous if it can access none. *)
val reply : 's neighbor -> int val reply : 's neighbor -> int
...@@ -133,7 +134,7 @@ val is_out_tree : unit -> bool ...@@ -133,7 +134,7 @@ val is_out_tree : unit -> bool
A rooted tree in a tree where one vertex is distinguished. A rooted tree in a tree where one vertex is distinguished.
By convention, sasa considers a tree to be rooted if exactly one By convention, sasa considers a tree to be rooted if exactly one
node id contains the string "root". node id contains the string "root" or "Root".
The following 4 functions only work on rooted trees The following 4 functions only work on rooted trees
*) *)
...@@ -152,7 +153,7 @@ val level : string (* the node id *) -> int ...@@ -152,7 +153,7 @@ val level : string (* the node id *) -> int
val parent : string (* the node id *) -> int option val parent : string (* the node id *) -> int option
(** returns [true] iff [is_tree] returns [true], and exactly one node (** returns [true] iff [is_tree] returns [true], and exactly one node
name contains the string "root" *) name contains the string "root" or "Root" *)
val is_rooted_tree : unit -> bool val is_rooted_tree : unit -> bool
(** It is possible to set some global parameters in the dot file (** It is possible to set some global parameters in the dot file
......
(* Time-stamp: <modified the 24/05/2022 (at 23:03) by Erwan Jahier> *) (* Time-stamp: <modified the 30/05/2022 (at 14:49) by Erwan Jahier> *)
open Graph open Graph
open Graph.Dot_ast open Graph.Dot_ast
...@@ -68,6 +68,19 @@ let (get_init: Dot_ast.attr list -> string) = ...@@ -68,6 +68,19 @@ let (get_init: Dot_ast.attr list -> string) =
in in
init_list init_list
let compare_alpha_num str1 str2 =
(* if str1 and str2 are of the form [^0-9][0-9]+, we use the alphabetic
order for the first part, and the numeric order for the second part.
nb : this is the case for node names generated by gg
*)
try
let to_int s = int_of_string (String.sub s 1 (String.length s - 1)) in
compare (str1.[0], to_int str1) (str2.[0], to_int str2)
with
_ -> String.compare str1 str2
let compare_alpha_num_2 p1 p2 = compare_alpha_num (snd p1) (snd p2)
let rec (get_weight: Dot_ast.attr -> int) = let rec (get_weight: Dot_ast.attr -> int) =
function function
| (Ident "weight", Some Number n)::_ | (Ident "weight", Some Number n)::_
...@@ -145,8 +158,8 @@ let (read: string -> t) = fun f -> ...@@ -145,8 +158,8 @@ let (read: string -> t) = fun f ->
Hashtbl.add node_succ pid pid_pred Hashtbl.add node_succ pid pid_pred
) )
node_pred; node_pred;
let succ str = List.sort compare (Hashtbl.find_all node_succ str) in let succ str = List.sort compare_alpha_num (Hashtbl.find_all node_succ str) in
let pred str = List.sort compare (Hashtbl.find_all node_pred str) in let pred str = List.sort compare_alpha_num_2 (Hashtbl.find_all node_pred str) in
{ {
nodes = List.rev nodes; nodes = List.rev nodes;
succ = succ; succ = succ;
...@@ -289,7 +302,7 @@ let is_tree : t -> bool = ...@@ -289,7 +302,7 @@ let is_tree : t -> bool =
fun g -> fun g ->
(not (is_cyclic g)) && (is_connected g) (not (is_cyclic g)) && (is_connected g)
let is_root_pid pid = Str.string_match (Str.regexp ".*root.*") pid 0 let is_root_pid pid = Str.string_match (Str.regexp ".*[rR]oot.*") pid 0
let is_root_node n = is_root_pid n.id let is_root_node n = is_root_pid n.id
(* cf algo.mli for the spec *) (* cf algo.mli for the spec *)
......
# Time-stamp: <modified the 02/09/2021 (at 10:38) by Erwan Jahier> # Time-stamp: <modified the 26/05/2022 (at 10:28) by Erwan Jahier>
# Rules to generate various dot files. # Rules to generate various dot files.
# The DECO_PATTERN variable should be defined # The DECO_PATTERN variable should be defined
...@@ -40,6 +40,10 @@ tree%.dot: ...@@ -40,6 +40,10 @@ tree%.dot:
gg tree -n $* -o $@ $(SEED) gg tree -n $* -o $@ $(SEED)
gg-deco $(DECO_PATTERN) $@ -o $@ gg-deco $(DECO_PATTERN) $@ -o $@
rtree%.dot:
gg tree --rooted-tree -n $* -o $@ $(SEED)
gg-deco $(DECO_PATTERN) $@ -o $@
intree%.dot: intree%.dot:
gg tree --in-tree -n $* -o $@ $(SEED) gg tree --in-tree -n $* -o $@ $(SEED)
gg-deco $(DECO_PATTERN) $@ -o $@ gg-deco $(DECO_PATTERN) $@ -o $@
......
# Time-stamp: <modified the 11/05/2021 (at 16:49) by Erwan Jahier> # Time-stamp: <modified the 30/05/2022 (at 14:49) by Erwan Jahier>
DECO_PATTERN="0-:p.ml"
-include ../Makefile.inc
-include Makefile.untracked
# dot files cannot be autommatically generated as the algo inputs a spanning tree
-include ../Makefile.dot
test: fig52_kcl.cmxs ##############################################################################
sasa -gcd fig52_kcl.dot # Non-regression tests
test: fig52_kcl.cmxs fig52_kcl.rdbg-test
sasa -gcd fig52_kcl.dot && make clean
clean: genclean
rm -f fig52_kcl.ml
##############################################################################
# Other examples of use
cd: fig52_kcl.cmxs cd: fig52_kcl.cmxs
sasa -cd fig52_kcl.dot sasa -cd fig52_kcl.dot
DECO_PATTERN="0-:p.ml"
-include ../Makefile.dot
sim2chrogtk: fig52_kcl.rif sim2chrogtk: fig52_kcl.rif
sim2chrogtk -ecran -in $< > /dev/null sim2chrogtk -ecran -in $< > /dev/null
...@@ -19,14 +31,10 @@ gnuplot: fig52_kcl.rif ...@@ -19,14 +31,10 @@ gnuplot: fig52_kcl.rif
rdbg: fig52_kcl.ml rdbg: fig52_kcl.ml
rdbg --sasa -o fig52_kcl.rif -env "sasa fig52_kcl.dot -gcd" rdbg --sasa -o fig52_kcl.rif -env "sasa fig52_kcl.dot -gcd"
rdbgcd: fig52_kcl.ml rdbg: fig52_kcl.ml
rdbg --sasa -o fig52_kcl.rif -env "sasa fig52_kcl.dot -cd" rdbg --sasa -o fig52_kcl.rif -env "sasa fig52_kcl.dot -cd"
dtree50: dtree50.cmxs dtree50: dtree50.cmxs
sasa -cd dtree50.dot sasa -cd dtree50.dot
clean: genclean
rm -f fig52_kcl.ml
-include ../Makefile.inc
-include Makefile.untracked
digraph fig52 { digraph fig52 {
root [algo="p.ml" init="{is_root=1 ; alpha=0}"] root [algo="p.ml" init="{is_root=1 ; alpha=0; par=-1}"]
p2 [algo="p.ml" init="{is_root=0 ; alpha=0}"] p2 [algo="p.ml" init="{is_root=0 ; alpha=0; par=1}"]
p3 [algo="p.ml" init="{is_root=0 ; alpha=0}"] p3 [algo="p.ml" init="{is_root=0 ; alpha=0; par=1}"]
p4 [algo="p.ml" init="{is_root=0 ; alpha=0}"] p4 [algo="p.ml" init="{is_root=0 ; alpha=0; par=1}"]
p5 [algo="p.ml" init="{is_root=0 ; alpha=0}"] p5 [algo="p.ml" init="{is_root=0 ; alpha=0; par=2}"]
p6 [algo="p.ml" init="{is_root=0 ; alpha=0}"] p6 [algo="p.ml" init="{is_root=0 ; alpha=0; par=1}"]
p7 [algo="p.ml" init="{is_root=0 ; alpha=0}"] p7 [algo="p.ml" init="{is_root=0 ; alpha=0; par=0}"]
root -> p2 -> p3 -> p4 -> p5 -> p6 root -> p2 -> p3 -> p4 -> p5 -> p6
p5 -> p7 p5 -> p7
} }
\ No newline at end of file
...@@ -3,62 +3,72 @@ Algorithm 1 of: ...@@ -3,62 +3,72 @@ Algorithm 1 of:
A Framework for Certified Self-Stabilization A Framework for Certified Self-Stabilization
Case Study: Silent Self-Stabilizing k-Dominating Set on a Tree Case Study: Silent Self-Stabilizing k-Dominating Set on a Tree
https://hal.archives-ouvertes.fr/hal-01272158/document https://hal.archives-ouvertes.fr/hal-01272158/document
Encoded by Hugo Hannot
*) *)
(* nb: it is meant to start with a spanning trees. The rtree%i.dot
rules in ../Makefile.dot generates rooted tree. We can use them as
spanning trees by taking advantage of the fact that the nodes are
sorted alphabetically if we perform a bread-first traversal of the
tree : we then the just need to consider the first neigbor as the
parent in the tree. *)
open Algo open Algo
open State open State
type s = State.t
(* State predicates *) type sl = s list
type n = State.t neighbor
type nl = n list
let isRoot p = p.isRoot let isRoot p = (state p).isRoot
let (isShort: State.t -> bool) = let (isShort: n -> bool) =
fun p -> p.alpha < k fun p -> (state p).alpha < k
let (isTall: State.t -> bool) = let (isTall: n -> bool) =
fun p -> p.alpha >= k fun p -> (state p).alpha >= k
(* Actually unused *) (* Actually unused *)
let (kDominator: 'v -> bool) = let (_kDominator: 'v -> bool) =
fun p -> (p.alpha = k) || ((isShort p) && (isRoot p)) fun p -> ((state p).alpha = k) || ((isShort p) && (isRoot p))
let (children: State.t -> State.t list -> State.t list) = let (children: s -> nl -> nl) =
fun p nl -> fun _p nl ->
List.filter (fun q -> q.par = reply q) nl List.filter (fun q -> (state q).par = reply q) nl
let (shortChildren: State.t -> State.t list -> State.t list) = let (shortChildren: s -> nl -> nl) =
fun p nl -> fun p nl ->
let cl = List.filter (children p) nl in List.filter isShort (children p nl)
List.filter isShort cl
let (tallChildren: State.t -> State.t list -> State.t list) = let (tallChildren: s -> nl -> nl) =
fun p nl -> fun p nl ->
let cl = List.filter (children p) nl in List.filter isTall (children p nl)
List.filter isTall cl
let rec (max: State.t list -> int -> int) = let rec (max: nl -> int -> int) =
fun sl cur -> fun sl cur ->
match sl with match sl with
[] -> cur | [] -> cur
| s::liste -> if (s.alpha) > cur then max liste (s.alpha) else max liste cur | n::tail ->
let s = state n in
let rec (min: State.t list -> int -> int) = if (s.alpha) > cur then max tail (s.alpha) else max tail cur
let rec (min: nl -> int -> int) =
fun sl cur -> fun sl cur ->
match sl with match sl with
[] -> cur | [] -> cur
| s::liste -> if (s.alpha) < cur then min liste (s.alpha) else min liste cur | n::tail ->
let s = state n in
if (s.alpha) < cur then min tail (s.alpha) else min tail cur
let (maxAShort: State.t -> State.t list -> int) = let (maxAShort: s -> nl -> int) =
fun p nl -> max (shortChildren p nl) (-1) fun p nl -> max (shortChildren p nl) (-1)
let (minATall: State.t -> State.t list -> int) = let (minATall: s -> nl -> int) =
fun p nl -> min (tallChildren p nl) (2*k+1) fun p nl -> min (tallChildren p nl) (2*k+1)
let (newAlpha: State.t -> State.t neighbor list -> int) = let (newAlpha: s -> nl -> int) =
fun p nl -> fun p nl ->
let nl = List.map state nl in
let mas = (maxAShort p nl) in let mas = (maxAShort p nl) in
let mit = (minATall p nl) in let mit = (minATall p nl) in
let res = if (mas + mit) <= (2*k - 2) then (mit + 1) else (mas + 1) in let res = if (mas + mit) <= (2*k - 2) then (mit + 1) else (mas + 1) in
...@@ -66,16 +76,18 @@ let (newAlpha: State.t -> State.t neighbor list -> int) = ...@@ -66,16 +76,18 @@ let (newAlpha: State.t -> State.t neighbor list -> int) =
res res
(*end macros*) (*end macros*)
let (init_state: int -> string -> State.t) = let (init_state: int -> string -> s) =
fun _ pid -> fun _ pid ->
(* assert(is_tree()); *) assert(is_rooted_tree());
{ {
isRoot = pid = "root"; (* ZZZ: The root of the tree should be named "root"! *) isRoot = pid = "Root"; (* ZZZ: The root of the tree should be named "Root"! *)
alpha = Random.int (2*k+1) alpha = Random.int (2*k+1);
par = 0 (* the input tree should be sorted alphabetically (wrt a bf traversal) *)
} }
let (enable_f: State.t -> State.t neighbor list -> action list) = let (enable_f: s -> nl -> action list) =
fun p nl -> if (p.alpha <> (newAlpha p nl)) then ["change_alpha"] else [] fun p nl -> if (p.alpha <> (newAlpha p nl)) then ["change_alpha"] else []
let (step_f : State.t -> State.t neighbor list -> action -> State.t ) = let (step_f : s -> nl -> action -> s) =
fun p nl a -> if a = "change_alpha" then {p with alpha = (newAlpha nl)} else assert false fun p nl a ->
if a = "change_alpha" then {p with alpha = (newAlpha p nl)} else assert false
...@@ -5,6 +5,7 @@ let d = max_degree() ...@@ -5,6 +5,7 @@ let d = max_degree()
type t = { type t = {
isRoot:bool; isRoot:bool;
alpha:int; alpha:int;
par:int
} }
let (to_string: (t -> string)) = let (to_string: (t -> string)) =
...@@ -13,8 +14,8 @@ let (to_string: (t -> string)) = ...@@ -13,8 +14,8 @@ let (to_string: (t -> string)) =
let (of_string: (string -> t) option) = let (of_string: (string -> t) option) =
Some (fun s -> Some (fun s ->
Scanf.sscanf s "{is_root=%d ; alpha=%d}" Scanf.sscanf s "{is_root=%d ; alpha=%d ; par=%d}"
(fun i alpha -> {isRoot = (i=1) ; alpha = alpha})) (fun i alpha p -> {isRoot = (i=1) ; alpha = alpha ; par = p }))
let (copy : ('v -> 'v)) = fun x -> x let (copy : ('v -> 'v)) = fun x -> x
let actions = ["change_alpha"] let actions = ["change_alpha"]
......
...@@ -250,7 +250,7 @@ let () = ( ...@@ -250,7 +250,7 @@ let () = (
| "HC" -> (gen_hyper_cube dir t.n) | "HC" -> (gen_hyper_cube dir t.n)
| "ER" -> (gen_ER dir t.n t.er) | "ER" -> (gen_ER dir t.n t.er)
| "BA" -> (gen_BA dir t.n t.ba) | "BA" -> (gen_BA dir t.n t.ba)
| "tree" -> (rand_tree t.tree_edge dir t.n) | "tree" -> (rand_tree t.tree_edge t.rooted dir t.n)
| "UDG" -> | "UDG" ->
let (graph, plan) = let (graph, plan) =
gen_udg dir t.n t.qudg.width t.qudg.height t.qudg.radius gen_udg dir t.n t.qudg.width t.qudg.height t.qudg.radius
......
...@@ -195,11 +195,12 @@ let (pre_rand_tree : bool -> GraphGen_arg.tree_edge -> node_succ_t -> ...@@ -195,11 +195,12 @@ let (pre_rand_tree : bool -> GraphGen_arg.tree_edge -> node_succ_t ->
(fun n -> Hashtbl.find_all node_succ n), (fun n -> Hashtbl.find_all node_succ n),
(fun n -> Hashtbl.find_all node_pred n) (fun n -> Hashtbl.find_all node_pred n)
let (rand_tree: GraphGen_arg.tree_edge -> bool -> int -> Topology.t) = let (rand_tree: GraphGen_arg.tree_edge -> bool -> bool -> int -> Topology.t) =
fun tree_edge directed nb -> fun tree_edge _rooted directed nb ->
let (node_succ:node_succ_t) = Hashtbl.create nb in let (node_succ:node_succ_t) = Hashtbl.create nb in
let (node_pred:node_pred_t) = Hashtbl.create nb in let (node_pred:node_pred_t) = Hashtbl.create nb in
let nodes = "root"::(create_nodes "p" (1,nb)) in let node_base_name = "p" in
let nodes = "Root"::(create_nodes node_base_name (1,nb)) in
let nl = id_to_empty_nodes nodes in let nl = id_to_empty_nodes nodes in
let succ, pred = pre_rand_tree directed tree_edge node_succ node_pred nodes in let succ, pred = pre_rand_tree directed tree_edge node_succ node_pred nodes in
{ {
......
...@@ -19,8 +19,8 @@ val gen_ER : bool -> int -> probability -> Topology.t ...@@ -19,8 +19,8 @@ val gen_ER : bool -> int -> probability -> Topology.t
val gen_BA : bool -> int -> int -> Topology.t val gen_BA : bool -> int -> int -> Topology.t
(** [rand_tree n] generate a random tree of n nodes *) (** [rand_tree rooted directed n] generate a random tree of n nodes *)
val rand_tree: GraphGen_arg.tree_edge -> bool -> int -> Topology.t val rand_tree: GraphGen_arg.tree_edge -> bool -> bool -> int -> Topology.t
(** [gen_udg nb x y r] generate a graph using the Unit Disc Graph (** [gen_udg nb x y r] generate a graph using the Unit Disc Graph
model, of n nodes. w and h are the width and the height of the model, of n nodes. w and h are the width and the height of the
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment