diff --git a/lib/algo/algo.mli b/lib/algo/algo.mli
index efdf853f555fdd01be52f04068cf85c0e2d662c2..6b823fc12c5fe9a378f2dfb3c6eb3979a2ec7afc 100644
--- a/lib/algo/algo.mli
+++ b/lib/algo/algo.mli
@@ -1,4 +1,4 @@
-(* 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}
A SASA process is an instance of an algorithm defined via this
@@ -83,13 +83,14 @@ type 's fault_fun = int -> string -> 's -> 's
(** Returns the neighbor processes local state *)
val state : 's neighbor -> 's
-(** Returns the neighbor channel number, that let this neighbor access
- to the content of the current process, if its neighbor can 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
- process, which may happen in directed graphs.
+(** Returns the neighbor channel number, that let this neighbor
+ access to the content of the current process, if its neighbor can
+ access it. The channel number is the rank, starting at 0, in the
+ neighbors' list, which are sorted alphabetically. Returns -1 if
+ 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. *)
val reply : 's neighbor -> int
@@ -133,7 +134,7 @@ val is_out_tree : unit -> bool
A rooted tree in a tree where one vertex is distinguished.
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
*)
@@ -152,7 +153,7 @@ val level : string (* the node id *) -> int
val parent : string (* the node id *) -> int option
(** 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
(** It is possible to set some global parameters in the dot file
diff --git a/lib/sasacore/topology.ml b/lib/sasacore/topology.ml
index de3de7d4030ff1bce5b8d963dfcf948bcd5ef2fa..60574d2189b6c4182bd7b76988322d230221592c 100644
--- a/lib/sasacore/topology.ml
+++ b/lib/sasacore/topology.ml
@@ -1,4 +1,4 @@
-(* 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.Dot_ast
@@ -68,6 +68,19 @@ let (get_init: Dot_ast.attr list -> string) =
in
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) =
function
| (Ident "weight", Some Number n)::_
@@ -145,8 +158,8 @@ let (read: string -> t) = fun f ->
Hashtbl.add node_succ pid pid_pred
)
node_pred;
- let succ str = List.sort compare (Hashtbl.find_all node_succ str) in
- let pred str = List.sort compare (Hashtbl.find_all node_pred str) in
+ let succ str = List.sort compare_alpha_num (Hashtbl.find_all node_succ str) in
+ let pred str = List.sort compare_alpha_num_2 (Hashtbl.find_all node_pred str) in
{
nodes = List.rev nodes;
succ = succ;
@@ -289,7 +302,7 @@ let is_tree : t -> bool =
fun 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
(* cf algo.mli for the spec *)
diff --git a/test/Makefile.dot b/test/Makefile.dot
index fa1d7ae1c4080f386fb26559775875e95f0ac023..ca52b491d0e75c0baf33ef8926b8b0a0370ca168 100644
--- a/test/Makefile.dot
+++ b/test/Makefile.dot
@@ -1,4 +1,4 @@
-# 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.
# The DECO_PATTERN variable should be defined
@@ -40,6 +40,10 @@ tree%.dot:
gg tree -n $* -o $@ $(SEED)
gg-deco $(DECO_PATTERN) $@ -o $@
+rtree%.dot:
+ gg tree --rooted-tree -n $* -o $@ $(SEED)
+ gg-deco $(DECO_PATTERN) $@ -o $@
+
intree%.dot:
gg tree --in-tree -n $* -o $@ $(SEED)
gg-deco $(DECO_PATTERN) $@ -o $@
diff --git a/test/k-clustering/Makefile b/test/k-clustering/Makefile
index f97a71c398ac5cdf3c0a5bf6e72686f56b815d70..ff0ccbdd041dfb5dbd94a18ef204f4f73d6fea58 100644
--- a/test/k-clustering/Makefile
+++ b/test/k-clustering/Makefile
@@ -1,15 +1,27 @@
-# 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
sasa -cd fig52_kcl.dot
-DECO_PATTERN="0-:p.ml"
--include ../Makefile.dot
-
sim2chrogtk: fig52_kcl.rif
sim2chrogtk -ecran -in $< > /dev/null
@@ -19,14 +31,10 @@ gnuplot: fig52_kcl.rif
rdbg: fig52_kcl.ml
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"
dtree50: dtree50.cmxs
sasa -cd dtree50.dot
-clean: genclean
- rm -f fig52_kcl.ml
--include ../Makefile.inc
--include Makefile.untracked
diff --git a/test/k-clustering/fig52_kcl.dot b/test/k-clustering/fig52_kcl.dot
index 8e94c2cdfaee2a0b609fe64483a27254e63930b7..8fb08ebbeaa67e70e389cb96999168ab4a6e965c 100644
--- a/test/k-clustering/fig52_kcl.dot
+++ b/test/k-clustering/fig52_kcl.dot
@@ -1,14 +1,14 @@
digraph fig52 {
- root [algo="p.ml" init="{is_root=1 ; alpha=0}"]
- p2 [algo="p.ml" init="{is_root=0 ; alpha=0}"]
- p3 [algo="p.ml" init="{is_root=0 ; alpha=0}"]
- p4 [algo="p.ml" init="{is_root=0 ; alpha=0}"]
- p5 [algo="p.ml" init="{is_root=0 ; alpha=0}"]
- p6 [algo="p.ml" init="{is_root=0 ; alpha=0}"]
- p7 [algo="p.ml" init="{is_root=0 ; alpha=0}"]
+ root [algo="p.ml" init="{is_root=1 ; alpha=0; par=-1}"]
+ p2 [algo="p.ml" init="{is_root=0 ; alpha=0; par=1}"]
+ p3 [algo="p.ml" init="{is_root=0 ; alpha=0; par=1}"]
+ p4 [algo="p.ml" init="{is_root=0 ; alpha=0; par=1}"]
+ p5 [algo="p.ml" init="{is_root=0 ; alpha=0; par=2}"]
+ p6 [algo="p.ml" init="{is_root=0 ; alpha=0; par=1}"]
+ p7 [algo="p.ml" init="{is_root=0 ; alpha=0; par=0}"]
root -> p2 -> p3 -> p4 -> p5 -> p6
p5 -> p7
}
-
\ No newline at end of file
+
diff --git a/test/k-clustering/p.ml b/test/k-clustering/p.ml
index 7309645f94ac42cb823a103625af1b62f8408be0..490ab21ac69334180140b01835ff6accbe370042 100644
--- a/test/k-clustering/p.ml
+++ b/test/k-clustering/p.ml
@@ -3,62 +3,72 @@ 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
+
+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 State
-
-(* State predicates *)
+type s = State.t
+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) =
- fun p -> p.alpha < k
+let (isShort: n -> bool) =
+ fun p -> (state p).alpha < k
-let (isTall: State.t -> bool) =
- fun p -> p.alpha >= k
+let (isTall: n -> bool) =
+ fun p -> (state p).alpha >= k
(* Actually unused *)
-let (kDominator: 'v -> bool) =
- fun p -> (p.alpha = k) || ((isShort p) && (isRoot p))
-
+let (_kDominator: 'v -> bool) =
+ fun p -> ((state p).alpha = k) || ((isShort p) && (isRoot p))
-let (children: State.t -> State.t list -> State.t list) =
- fun p nl ->
- List.filter (fun q -> q.par = reply q) nl
+let (children: s -> nl -> nl) =
+ fun _p 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 ->
- let cl = List.filter (children p) nl in
- List.filter isShort cl
+ List.filter isShort (children p nl)
-let (tallChildren: State.t -> State.t list -> State.t list) =
+let (tallChildren: s -> nl -> nl) =
fun p nl ->
- let cl = List.filter (children p) nl in
- List.filter isTall cl
+ List.filter isTall (children p nl)
-let rec (max: State.t list -> int -> int) =
+let rec (max: nl -> int -> int) =
fun sl cur ->
match sl with
- [] -> cur
- | s::liste -> if (s.alpha) > cur then max liste (s.alpha) else max liste cur
-
-let rec (min: State.t list -> int -> int) =
+ | [] -> cur
+ | n::tail ->
+ let s = state n in
+ if (s.alpha) > cur then max tail (s.alpha) else max tail cur
+
+let rec (min: nl -> int -> int) =
fun sl cur ->
match sl with
- [] -> cur
- | s::liste -> if (s.alpha) < cur then min liste (s.alpha) else min liste cur
+ | [] -> 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)
-let (minATall: State.t -> State.t list -> int) =
+let (minATall: s -> nl -> int) =
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 ->
- let nl = List.map state nl in
let mas = (maxAShort p nl) in
let mit = (minATall p nl) 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) =
res
(*end macros*)
-let (init_state: int -> string -> State.t) =
+let (init_state: int -> string -> s) =
fun _ pid ->
- (* assert(is_tree()); *)
+ assert(is_rooted_tree());
{
- isRoot = pid = "root"; (* ZZZ: The root of the tree should be named "root"! *)
- alpha = Random.int (2*k+1)
+ isRoot = pid = "Root"; (* ZZZ: The root of the tree should be named "Root"! *)
+ 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 []
-let (step_f : State.t -> State.t neighbor list -> action -> State.t ) =
- fun p nl a -> if a = "change_alpha" then {p with alpha = (newAlpha nl)} else assert false
+let (step_f : s -> nl -> action -> s) =
+ fun p nl a ->
+ if a = "change_alpha" then {p with alpha = (newAlpha p nl)} else assert false
diff --git a/test/k-clustering/state.ml b/test/k-clustering/state.ml
index 8985084259ea5adc24ce690f037f930688b111ed..00b9556c555dbaf984d68132aa80492557609844 100644
--- a/test/k-clustering/state.ml
+++ b/test/k-clustering/state.ml
@@ -5,6 +5,7 @@ let d = max_degree()
type t = {
isRoot:bool;
alpha:int;
+ par:int
}
let (to_string: (t -> string)) =
@@ -13,8 +14,8 @@ let (to_string: (t -> string)) =
let (of_string: (string -> t) option) =
Some (fun s ->
- Scanf.sscanf s "{is_root=%d ; alpha=%d}"
- (fun i alpha -> {isRoot = (i=1) ; alpha = alpha}))
+ Scanf.sscanf s "{is_root=%d ; alpha=%d ; par=%d}"
+ (fun i alpha p -> {isRoot = (i=1) ; alpha = alpha ; par = p }))
let (copy : ('v -> 'v)) = fun x -> x
let actions = ["change_alpha"]
diff --git a/tools/gg/graphGen.ml b/tools/gg/graphGen.ml
index ae4418d38174893a3a353a297a4a8b5d3bf269e8..90e5a6e5e50428ddeb91eaa2958420e072a7a97b 100644
--- a/tools/gg/graphGen.ml
+++ b/tools/gg/graphGen.ml
@@ -250,7 +250,7 @@ let () = (
| "HC" -> (gen_hyper_cube dir t.n)
| "ER" -> (gen_ER dir t.n t.er)
| "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" ->
let (graph, plan) =
gen_udg dir t.n t.qudg.width t.qudg.height t.qudg.radius
diff --git a/tools/gg/randomGraph.ml b/tools/gg/randomGraph.ml
index 6abfefa08204a2e991b4128deaf4c84dcb7113eb..cb8f62837ba044d786978ba730af59db036cc0c6 100644
--- a/tools/gg/randomGraph.ml
+++ b/tools/gg/randomGraph.ml
@@ -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_pred n)
-let (rand_tree: GraphGen_arg.tree_edge -> bool -> int -> Topology.t) =
- fun tree_edge directed nb ->
+let (rand_tree: GraphGen_arg.tree_edge -> bool -> bool -> int -> Topology.t) =
+ fun tree_edge _rooted directed nb ->
let (node_succ:node_succ_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 succ, pred = pre_rand_tree directed tree_edge node_succ node_pred nodes in
{
diff --git a/tools/gg/randomGraph.mli b/tools/gg/randomGraph.mli
index 90bdfcdd99ecbb559847525663524609382a3c1a..31116bf1ad58fbe014e18ed506c86838beabf26c 100644
--- a/tools/gg/randomGraph.mli
+++ b/tools/gg/randomGraph.mli
@@ -19,8 +19,8 @@ val gen_ER : bool -> int -> probability -> Topology.t
val gen_BA : bool -> int -> int -> Topology.t
-(** [rand_tree n] generate a random tree of n nodes *)
-val rand_tree: GraphGen_arg.tree_edge -> bool -> int -> Topology.t
+(** [rand_tree rooted directed n] generate a random tree of n nodes *)
+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
model, of n nodes. w and h are the width and the height of the