From 3fdda0f49f466ac30e7b0d2b2a526a86c204a72b Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Fri, 7 Feb 2020 09:49:12 +0100
Subject: [PATCH] Test: yet another bfs spanning tree construction
---
test/Makefile | 2 +
test/README.md | 1 +
test/README.org | 8 +-
test/bfs-st-HC92/Makefile | 5 +-
test/bfs-st-HC92/root.ml | 12 +-
test/lustre/utils.lus | 4 +-
test/st-KK06/Makefile | 38 +++++
test/st-KK06/grid10.dot | 291 ++++++++++++++++++++++++++++++++
test/st-KK06/grid4.dot | 33 ++++
test/st-KK06/my-rdbg-tuning.ml | 6 +
test/st-KK06/p.ml | 49 ++++++
test/st-KK06/ring.dot | 13 ++
test/st-KK06/root.ml | 13 ++
test/st-KK06/st_KK06_oracle.lus | 12 ++
test/st-KK06/state.ml | 5 +
15 files changed, 474 insertions(+), 18 deletions(-)
create mode 100644 test/st-KK06/Makefile
create mode 100644 test/st-KK06/grid10.dot
create mode 100644 test/st-KK06/grid4.dot
create mode 100644 test/st-KK06/my-rdbg-tuning.ml
create mode 100644 test/st-KK06/p.ml
create mode 100644 test/st-KK06/ring.dot
create mode 100644 test/st-KK06/root.ml
create mode 100644 test/st-KK06/st_KK06_oracle.lus
create mode 100644 test/st-KK06/state.ml
diff --git a/test/Makefile b/test/Makefile
index 55fb441c..5e89bb30 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -9,6 +9,7 @@ test:
cd dfs/ && make
cd dfs-list/ && make
cd st-CYH91/ && make
+ cd st-KK06/ && make
cd bfs-st-HC92/ && make
echo "Every test went fine!"
@@ -22,6 +23,7 @@ clean:
cd dfs/ && make clean
cd dfs-list/ && make clean
cd st-CYH91/ && make clean
+ cd st-KK06/ && make clean
cd bfs-st-HC92/ && make clean
-include Makefile.untracked
diff --git a/test/README.md b/test/README.md
index 4902def8..96fa8ed0 100644
--- a/test/README.md
+++ b/test/README.md
@@ -9,6 +9,7 @@ The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/t
- `test/bfs-spanning-tree/`: a Breadth First Search Spanning tree construction
- `test/bfs-st-HC92`: another BFS Spanning tree construction ("A self-stabilizing algorithm for constructing breadth-first trees" by Huang and Chen in 1992)
- `test/st-CYH91`: another Spanning tree construction ("A self-stabilizing algorithm for constructing spanning trees" by Chen, Yu, and Huang in 1991)
+- `test/st-KK06`: another Spanning tree construction ("A Self-stabilizing Algorithm for Finding a Spanning Tree in a Polynomial Number of Moves" by Kosowski and Kuszner, 2006)
- `test/dfs/`: a Depth First Search using arrays (the \`\`atomic state model'' version of a [Depth First Search algorithm proposed by Collin and Dolev in 1994](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf))
- `test/dfs-list/`: a Depth First Search using lists
diff --git a/test/README.org b/test/README.org
index 672cf2d2..f23860d8 100644
--- a/test/README.org
+++ b/test/README.org
@@ -15,8 +15,12 @@ Self-Stabilizing Algorithms'' By Altisen, Devismes, Dubois, and Petit.
- =test/bfs-st-HC92=: another BFS Spanning tree construction ("A
self-stabilizing algorithm for constructing breadth-first trees" by
Huang and Chen in 1992)
-- =test/st-CYH91=: another Spanning tree construction ("A self-stabilizing algorithm for constructing
- spanning trees" by Chen, Yu, and Huang in 1991)
+- =test/st-CYH91=: another Spanning tree construction ("A
+ self-stabilizing algorithm for constructing spanning trees" by Chen,
+ Yu, and Huang in 1991)
+- =test/st-KK06=: another Spanning tree construction ("A
+ Self-stabilizing Algorithm for Finding a Spanning Tree in a
+ Polynomial Number of Moves" by Kosowski and Kuszner, 2006)
- =test/dfs/=: a Depth First Search using arrays (the ``atomic state
model'' version of a [[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf][Depth First Search algorithm proposed by Collin and Dolev in 1994]])
- =test/dfs-list/=: a Depth First Search using lists
diff --git a/test/bfs-st-HC92/Makefile b/test/bfs-st-HC92/Makefile
index fa29cbbe..c5e7d3f3 100644
--- a/test/bfs-st-HC92/Makefile
+++ b/test/bfs-st-HC92/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 06/02/2020 (at 14:20) by Erwan Jahier>
+# Time-stamp: <modified the 06/02/2020 (at 17:25) by Erwan Jahier>
test: test0 lurette
@@ -20,9 +20,8 @@ rdbg: grid4.ml
rdbg10: grid10.ml
rdbg -o rdbg.rif -sut "sasa grid10.dot" -l 1000
-
lurette: grid4.cmxs
- lurette -o rdbg.rif -sut "sasa grid4.dot" -l 1000
+ lurette -o rdbg.rif -sut "sasa -rif grid4.dot" -l 1000
rdbg-ring: ring.ml
rdbg -o rdbg.rif -sut "sasa ring.dot" -l 1000
diff --git a/test/bfs-st-HC92/root.ml b/test/bfs-st-HC92/root.ml
index 743c2e8c..a6b39842 100644
--- a/test/bfs-st-HC92/root.ml
+++ b/test/bfs-st-HC92/root.ml
@@ -1,14 +1,4 @@
-(* Time-stamp: <modified the 04/02/2020 (at 11:06) by Erwan Jahier> *)
-
-(* "A self-stabilizing algoritm for constructing spanning trees"
- Nian-Shing Chen, Wey-Pyng Yu and Shing-Tsaan Huang
- Information Processing Letters 39 (1991) 147-151
-
-Hyp:
-- central daemon
-- connected unidirected graph
-
-*)
+(* Time-stamp: <modified the 06/02/2020 (at 14:56) by Erwan Jahier> *)
let (init_state: int -> 'st) =
fun i ->
diff --git a/test/lustre/utils.lus b/test/lustre/utils.lus
index 4b3fa973..0b51e7a0 100644
--- a/test/lustre/utils.lus
+++ b/test/lustre/utils.lus
@@ -71,8 +71,8 @@ let
tel
-----------------------------------------------------------------------------
-node compt_move (tab_acti:bool^m^n) returns (nb_act:int);
+node count_move <<const m:int ; const n:int>>(tab_acti:bool^m^n) returns (nb_act:int);
let
- nb_act = 0 -> pre(nb_act) + (red<<count_true_acc,n>>(0,tab_acti));
+ nb_act = 0 -> pre(nb_act) + (red<<count_true_acc<<m>>,n>>(0,tab_acti));
tel
diff --git a/test/st-KK06/Makefile b/test/st-KK06/Makefile
new file mode 100644
index 00000000..afcc32dc
--- /dev/null
+++ b/test/st-KK06/Makefile
@@ -0,0 +1,38 @@
+# Time-stamp: <modified the 07/02/2020 (at 08:30) by Erwan Jahier>
+
+
+test: test0 lurette lurette-alt
+test0: ring.cmxs
+ sasa -l 200 ring.dot
+
+sim2chrogtk: ring.rif
+ sim2chrogtk -ecran -in $< > /dev/null
+
+gnuplot: ring.rif
+ gnuplot-rif $<
+
+ocd: grid4.ml grid4.cma
+ rdbg --ocamldebug -sut "sasa grid4.dot" -l 1000
+
+rdbg: grid4.ml
+ rdbg -o rdbg.rif -sut "sasa grid4.dot" -l 1000
+
+lurette: grid4.cmxs grid4_oracle.lus
+ lurette -o rdbg.rif -sut "sasa grid4.dot -rif" \
+ -oracle "lv6 grid4_oracle.lus -n oracle -exec" -l 1000
+
+lurette-alt: grid4.cmxs grid4_oracle.lus
+ rdbg -lurette -o rdbg.rif -sut "sasa grid4.dot -rif" \
+ -oracle "lv6 grid4_oracle.lus -n oracle -exec" -l 1000
+
+
+
+rdbg-ring: ring.ml
+ rdbg -o rdbg.rif -sut "sasa ring.dot" -l 1000
+
+
+clean: genclean
+ rm -f ring.ml grid*.ml grid*.lus
+
+-include ../Makefile.inc
+-include Makefile.untracked
diff --git a/test/st-KK06/grid10.dot b/test/st-KK06/grid10.dot
new file mode 100644
index 00000000..af743260
--- /dev/null
+++ b/test/st-KK06/grid10.dot
@@ -0,0 +1,291 @@
+graph grid {
+graph [min_deg=2
+ mean_deg=3.6
+ max_deg=4
+ is_connected=true
+ is_cyclic=true
+ is_tree=true
+ links_number=180]
+ p0 [algo="root.ml"]
+ p1 [algo="p.ml"]
+ p2 [algo="p.ml"]
+ p3 [algo="p.ml"]
+ p4 [algo="p.ml"]
+ p5 [algo="p.ml"]
+ p6 [algo="p.ml"]
+ p7 [algo="p.ml"]
+ p8 [algo="p.ml"]
+ p9 [algo="p.ml"]
+ p10 [algo="p.ml"]
+ p11 [algo="p.ml"]
+ p12 [algo="p.ml"]
+ p13 [algo="p.ml"]
+ p14 [algo="p.ml"]
+ p15 [algo="p.ml"]
+ p16 [algo="p.ml"]
+ p17 [algo="p.ml"]
+ p18 [algo="p.ml"]
+ p19 [algo="p.ml"]
+ p20 [algo="p.ml"]
+ p21 [algo="p.ml"]
+ p22 [algo="p.ml"]
+ p23 [algo="p.ml"]
+ p24 [algo="p.ml"]
+ p25 [algo="p.ml"]
+ p26 [algo="p.ml"]
+ p27 [algo="p.ml"]
+ p28 [algo="p.ml"]
+ p29 [algo="p.ml"]
+ p30 [algo="p.ml"]
+ p31 [algo="p.ml"]
+ p32 [algo="p.ml"]
+ p33 [algo="p.ml"]
+ p34 [algo="p.ml"]
+ p35 [algo="p.ml"]
+ p36 [algo="p.ml"]
+ p37 [algo="p.ml"]
+ p38 [algo="p.ml"]
+ p39 [algo="p.ml"]
+ p40 [algo="p.ml"]
+ p41 [algo="p.ml"]
+ p42 [algo="p.ml"]
+ p43 [algo="p.ml"]
+ p44 [algo="p.ml"]
+ p45 [algo="p.ml"]
+ p46 [algo="p.ml"]
+ p47 [algo="p.ml"]
+ p48 [algo="p.ml"]
+ p49 [algo="p.ml"]
+ p50 [algo="p.ml"]
+ p51 [algo="p.ml"]
+ p52 [algo="p.ml"]
+ p53 [algo="p.ml"]
+ p54 [algo="p.ml"]
+ p55 [algo="p.ml"]
+ p56 [algo="p.ml"]
+ p57 [algo="p.ml"]
+ p58 [algo="p.ml"]
+ p59 [algo="p.ml"]
+ p60 [algo="p.ml"]
+ p61 [algo="p.ml"]
+ p62 [algo="p.ml"]
+ p63 [algo="p.ml"]
+ p64 [algo="p.ml"]
+ p65 [algo="p.ml"]
+ p66 [algo="p.ml"]
+ p67 [algo="p.ml"]
+ p68 [algo="p.ml"]
+ p69 [algo="p.ml"]
+ p70 [algo="p.ml"]
+ p71 [algo="p.ml"]
+ p72 [algo="p.ml"]
+ p73 [algo="p.ml"]
+ p74 [algo="p.ml"]
+ p75 [algo="p.ml"]
+ p76 [algo="p.ml"]
+ p77 [algo="p.ml"]
+ p78 [algo="p.ml"]
+ p79 [algo="p.ml"]
+ p80 [algo="p.ml"]
+ p81 [algo="p.ml"]
+ p82 [algo="p.ml"]
+ p83 [algo="p.ml"]
+ p84 [algo="p.ml"]
+ p85 [algo="p.ml"]
+ p86 [algo="p.ml"]
+ p87 [algo="p.ml"]
+ p88 [algo="p.ml"]
+ p89 [algo="p.ml"]
+ p90 [algo="p.ml"]
+ p91 [algo="p.ml"]
+ p92 [algo="p.ml"]
+ p93 [algo="p.ml"]
+ p94 [algo="p.ml"]
+ p95 [algo="p.ml"]
+ p96 [algo="p.ml"]
+ p97 [algo="p.ml"]
+ p98 [algo="p.ml"]
+ p99 [algo="p.ml"]
+
+ p0 -- p1
+ p0 -- p10
+ p1 -- p11
+ p1 -- p2
+ p10 -- p11
+ p10 -- p20
+ p11 -- p12
+ p11 -- p21
+ p12 -- p13
+ p12 -- p2
+ p12 -- p22
+ p13 -- p14
+ p13 -- p23
+ p13 -- p3
+ p14 -- p15
+ p14 -- p24
+ p14 -- p4
+ p15 -- p16
+ p15 -- p25
+ p15 -- p5
+ p16 -- p17
+ p16 -- p26
+ p16 -- p6
+ p17 -- p18
+ p17 -- p27
+ p17 -- p7
+ p18 -- p19
+ p18 -- p28
+ p18 -- p8
+ p19 -- p29
+ p19 -- p9
+ p2 -- p3
+ p20 -- p21
+ p20 -- p30
+ p21 -- p22
+ p21 -- p31
+ p22 -- p23
+ p22 -- p32
+ p23 -- p24
+ p23 -- p33
+ p24 -- p25
+ p24 -- p34
+ p25 -- p26
+ p25 -- p35
+ p26 -- p27
+ p26 -- p36
+ p27 -- p28
+ p27 -- p37
+ p28 -- p29
+ p28 -- p38
+ p29 -- p39
+ p3 -- p4
+ p30 -- p31
+ p30 -- p40
+ p31 -- p32
+ p31 -- p41
+ p32 -- p33
+ p32 -- p42
+ p33 -- p34
+ p33 -- p43
+ p34 -- p35
+ p34 -- p44
+ p35 -- p36
+ p35 -- p45
+ p36 -- p37
+ p36 -- p46
+ p37 -- p38
+ p37 -- p47
+ p38 -- p39
+ p38 -- p48
+ p39 -- p49
+ p4 -- p5
+ p40 -- p41
+ p40 -- p50
+ p41 -- p42
+ p41 -- p51
+ p42 -- p43
+ p42 -- p52
+ p43 -- p44
+ p43 -- p53
+ p44 -- p45
+ p44 -- p54
+ p45 -- p46
+ p45 -- p55
+ p46 -- p47
+ p46 -- p56
+ p47 -- p48
+ p47 -- p57
+ p48 -- p49
+ p48 -- p58
+ p49 -- p59
+ p5 -- p6
+ p50 -- p51
+ p50 -- p60
+ p51 -- p52
+ p51 -- p61
+ p52 -- p53
+ p52 -- p62
+ p53 -- p54
+ p53 -- p63
+ p54 -- p55
+ p54 -- p64
+ p55 -- p56
+ p55 -- p65
+ p56 -- p57
+ p56 -- p66
+ p57 -- p58
+ p57 -- p67
+ p58 -- p59
+ p58 -- p68
+ p59 -- p69
+ p6 -- p7
+ p60 -- p61
+ p60 -- p70
+ p61 -- p62
+ p61 -- p71
+ p62 -- p63
+ p62 -- p72
+ p63 -- p64
+ p63 -- p73
+ p64 -- p65
+ p64 -- p74
+ p65 -- p66
+ p65 -- p75
+ p66 -- p67
+ p66 -- p76
+ p67 -- p68
+ p67 -- p77
+ p68 -- p69
+ p68 -- p78
+ p69 -- p79
+ p7 -- p8
+ p70 -- p71
+ p70 -- p80
+ p71 -- p72
+ p71 -- p81
+ p72 -- p73
+ p72 -- p82
+ p73 -- p74
+ p73 -- p83
+ p74 -- p75
+ p74 -- p84
+ p75 -- p76
+ p75 -- p85
+ p76 -- p77
+ p76 -- p86
+ p77 -- p78
+ p77 -- p87
+ p78 -- p79
+ p78 -- p88
+ p79 -- p89
+ p8 -- p9
+ p80 -- p81
+ p80 -- p90
+ p81 -- p82
+ p81 -- p91
+ p82 -- p83
+ p82 -- p92
+ p83 -- p84
+ p83 -- p93
+ p84 -- p85
+ p84 -- p94
+ p85 -- p86
+ p85 -- p95
+ p86 -- p87
+ p86 -- p96
+ p87 -- p88
+ p87 -- p97
+ p88 -- p89
+ p88 -- p98
+ p89 -- p99
+ p90 -- p91
+ p91 -- p92
+ p92 -- p93
+ p93 -- p94
+ p94 -- p95
+ p95 -- p96
+ p96 -- p97
+ p97 -- p98
+ p98 -- p99
+}
+
diff --git a/test/st-KK06/grid4.dot b/test/st-KK06/grid4.dot
new file mode 100644
index 00000000..b7f16c5b
--- /dev/null
+++ b/test/st-KK06/grid4.dot
@@ -0,0 +1,33 @@
+graph g {
+ p0 [algo="p.ml" ]
+ p1 [algo="p.ml" ]
+ p2 [algo="p.ml" ]
+ p3 [algo="p.ml" ]
+ p4 [algo="root.ml" ]
+ p5 [algo="p.ml" ]
+ p6 [algo="p.ml" ]
+ p7 [algo="p.ml" ]
+ p8 [algo="p.ml" ]
+ p9 [algo="p.ml" ]
+ p10 [algo="p.ml" ]
+ p11 [algo="p.ml" ]
+ p12 [algo="p.ml" ]
+ p13 [algo="p.ml" ]
+ p14 [algo="p.ml" ]
+ p15 [algo="p.ml" ]
+
+ p0 -- p1 -- p2 -- p3 -- p7
+ p0 -- p4 -- p5 -- p6
+ p11-- p15
+ p1 -- p5 -- p9
+ p10 -- p11 -- p7
+ p10 -- p14 -- p15
+ p10 -- p6
+ p10 -- p9
+ p12 -- p13 -- p14
+ p12 -- p8 -- p9
+ p13 -- p9
+ p2 -- p6 -- p7
+ p4 -- p8
+}
+
diff --git a/test/st-KK06/my-rdbg-tuning.ml b/test/st-KK06/my-rdbg-tuning.ml
new file mode 100644
index 00000000..9ba333d8
--- /dev/null
+++ b/test/st-KK06/my-rdbg-tuning.ml
@@ -0,0 +1,6 @@
+
+#use "../my-rdbg-tuning.ml";;
+
+
+
+
diff --git a/test/st-KK06/p.ml b/test/st-KK06/p.ml
new file mode 100644
index 00000000..5f282b54
--- /dev/null
+++ b/test/st-KK06/p.ml
@@ -0,0 +1,49 @@
+(* Time-stamp: <modified the 07/02/2020 (at 09:48) by Erwan Jahier> *)
+
+(*
+ A Self-stabilizing Algorithm for Finding a Spanning Tree in a Polynomial Number of Moves
+ Adrian Kosowski and Lukasz Kuszner
+ PPAM 2005, LNCS 3911, pp. 75–82, 2006.
+
+Hyp:
+- distributed daemon
+- connected un-directed graph
+
+ *)
+
+open Algo
+
+let (init_state: int -> 'st) =
+ fun _nl -> (Random.int 10)
+
+
+let min_n nl = (* returns the min of the neigbhors *)
+ List.fold_left
+ (fun acc n -> if acc < state n then acc else state n)
+ (state (List.hd nl))
+ (List.tl nl)
+
+let max_n nl = (* returns the max of the neigbhors *)
+ List.fold_left
+ (fun acc n -> if acc > state n then acc else state n)
+ (state (List.hd nl))
+ (List.tl nl)
+
+let (enable_f: 'st -> 'st neighbor list -> action list) =
+ fun e nl ->
+ if (* R: v <> root ∧ f (v) ≤ min_u∈N(v) f (u)
+ ---> f (v) = max_u∈N(v) f (u) + 1 *)
+ e <= min_n nl
+ then ["R"]
+ else []
+
+
+let (step_f : 'st -> 'st neighbor list -> action -> 'st ) =
+ fun e nl ->
+ function
+ | "R" -> 1+ max_n nl
+ | _ -> e
+
+let actions = Some ["R"];
+
+
diff --git a/test/st-KK06/ring.dot b/test/st-KK06/ring.dot
new file mode 100644
index 00000000..dbb0da3d
--- /dev/null
+++ b/test/st-KK06/ring.dot
@@ -0,0 +1,13 @@
+graph ring7 {
+
+ p1 [algo="p.ml"]
+ p2 [algo="p.ml" ]
+ p3 [algo="p.ml"]
+ p4 [algo="p.ml"]
+ p5 [algo="p.ml"]
+ p6 [algo="p.ml"]
+ p7 [algo="p.ml"]
+
+ p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1
+
+}
diff --git a/test/st-KK06/root.ml b/test/st-KK06/root.ml
new file mode 100644
index 00000000..81077890
--- /dev/null
+++ b/test/st-KK06/root.ml
@@ -0,0 +1,13 @@
+(* Time-stamp: <modified the 06/02/2020 (at 15:39) by Erwan Jahier> *)
+
+let (init_state: int -> 'st) =
+ fun i -> 0
+
+(* The root is never enabled... *)
+let enable_f = fun _ _ -> []
+
+(* ... nor activated! *)
+let step_f = fun e _nl _a -> e
+let actions = Some ["R"];
+
+
diff --git a/test/st-KK06/st_KK06_oracle.lus b/test/st-KK06/st_KK06_oracle.lus
new file mode 100644
index 00000000..b799e13c
--- /dev/null
+++ b/test/st-KK06/st_KK06_oracle.lus
@@ -0,0 +1,12 @@
+
+include "../lustre/utils.lus"
+
+node st_KK06_oracle<<const an:int; const pn:int>>(Enab,Acti:bool^an^pn)
+returns (ok:bool);
+var
+ moves : int;
+let
+-- Theorem 2. Algorithm 1 stabilizes in O(n diam(G)) moves.
+ moves = count_move<<an,pn>>(Acti);
+ ok = moves <= card * diameter ;
+tel
\ No newline at end of file
diff --git a/test/st-KK06/state.ml b/test/st-KK06/state.ml
new file mode 100644
index 00000000..3b98f247
--- /dev/null
+++ b/test/st-KK06/state.ml
@@ -0,0 +1,5 @@
+
+type t = int
+let to_string = (fun s -> Printf.sprintf "f=%i" s)
+let of_string = Some int_of_string
+let copy x = x
--
GitLab