From 4aa645f4be744ddfce243d3d232d4e41d88c3da4 Mon Sep 17 00:00:00 2001
From: invite <invite@debian>
Date: Fri, 1 Jul 2022 09:47:03 +0200
Subject: [PATCH] add kclustering
---
test/coloring/Makefile | 4 +-
test/coloring/dice5_oracle.lus | 26 -----
test/kclustering/Makefile | 27 ++++++
test/kclustering/config.ml | 1 +
test/kclustering/cost.lus | 33 +++++++
test/kclustering/kclustering_oracle.lus | 31 ++++++
test/kclustering/p.lus | 121 ++++++++++++++++++++++++
test/kclustering/p.ml | 1 +
test/kclustering/state.ml | 1 +
test/kclustering/verify.lus | 55 +++++++++++
10 files changed, 272 insertions(+), 28 deletions(-)
delete mode 100644 test/coloring/dice5_oracle.lus
create mode 100644 test/kclustering/Makefile
create mode 120000 test/kclustering/config.ml
create mode 100644 test/kclustering/cost.lus
create mode 100644 test/kclustering/kclustering_oracle.lus
create mode 100644 test/kclustering/p.lus
create mode 120000 test/kclustering/p.ml
create mode 120000 test/kclustering/state.ml
create mode 100644 test/kclustering/verify.lus
diff --git a/test/coloring/Makefile b/test/coloring/Makefile
index 952d8bca..2fa29b08 100644
--- a/test/coloring/Makefile
+++ b/test/coloring/Makefile
@@ -26,8 +26,8 @@ simu: clique3.simu
# Compare the ocaml version with the lustre one
# XXX todo : write a coloring_oracle.lus similar to ../dijkstra-ring/dijkstra_ring_oracle.lus
-#compare: clique3.lurette
-# cat dijkstra-ring.rif
+compare: clique3.lurette
+ cat coloring.rif
kind2: clique3.kind2
diff --git a/test/coloring/dice5_oracle.lus b/test/coloring/dice5_oracle.lus
deleted file mode 100644
index dbce57df..00000000
--- a/test/coloring/dice5_oracle.lus
+++ /dev/null
@@ -1,26 +0,0 @@
-include "dice5.lus"
-include "verify.lus"
-
-node topology = dice5;
-const an = actions_number;
-const pn = card;
-
-node oracle(
- p0_color:int;p1_color:int;p2_color:int;p3_color:int;p4_color:int;
- Enab_p0_recolor,Enab_p1_recolor,Enab_p2_recolor,Enab_p3_recolor,Enab_p4_recolor:bool;
- p0_recolor,p1_recolor,p2_recolor,p3_recolor,p4_recolor:bool)
-returns (ok:bool);
-var
- Acti:bool^an^pn;
- Enab:bool^an^pn;
- Stat : state^pn;
- nodes : state^pn;
- enables : bool^an^pn;
-let
- Acti = [[p0_recolor],[p1_recolor],[p2_recolor],[p3_recolor],[p4_recolor]];
- Enab = [[Enab_p0_recolor],[Enab_p1_recolor],[Enab_p2_recolor],[Enab_p3_recolor],[Enab_p4_recolor]];
- Stat = [ p0_color, p1_color, p2_color, p3_color, p4_color ];
-
- nodes, enables = topology(pre(Acti), Stat);
- ok = enables = Enab and boolred<<pn,pn,pn>>(map<<=,pn>>(nodes, Stat));
-tel;
diff --git a/test/kclustering/Makefile b/test/kclustering/Makefile
new file mode 100644
index 00000000..19d67dcf
--- /dev/null
+++ b/test/kclustering/Makefile
@@ -0,0 +1,27 @@
+TOPOLOGY ?= tree3
+DOT2LUSFLAGS ?=
+SASA_ALGOS := p.ml
+DECO_PATTERN="0-:p.ml"
+
+
+include ~/sasa/salut/test/Makefile.inc
+-include ~/sasa/salut/test/Makefile.dot
+
+clean: genclean
+ rm -f tree*.*
+
+## Some examples of use of ../Makefile.inc
+
+
+# run a simulation with luciole
+simu: tree3.simu
+
+# Compare the ocaml version with the lustre one
+compare: tree3.lurette
+ cat kclustering.rif
+
+# make diring4.simu
+kind2: tree3.kind2
+
+## do not work because there is a modulo in p.lus, which is not (yet) implemented in ../../bit-blast/*.lus
+lesar: tree3.lesar
diff --git a/test/kclustering/config.ml b/test/kclustering/config.ml
new file mode 120000
index 00000000..cd1408a5
--- /dev/null
+++ b/test/kclustering/config.ml
@@ -0,0 +1 @@
+../../../test/k-clustering/config.ml
\ No newline at end of file
diff --git a/test/kclustering/cost.lus b/test/kclustering/cost.lus
new file mode 100644
index 00000000..c9d2c121
--- /dev/null
+++ b/test/kclustering/cost.lus
@@ -0,0 +1,33 @@
+include "p.lus"
+const debug=false;
+
+function parentd<<const card:int;const n:int>>(p:state ; config:state^card) returns (parp:state);
+let
+parp=with (card=n) then config[card-1]
+ else if p.par=n then config[n] else parentd<<card,(n+1)>>(p,config);
+tel
+
+node depth<<const card:int>> (p:state; config:state^card) returns (nat:int);
+var parp:state;
+let
+parp=parentd<<card;0>>(p,config);
+nat= with (card=1) then 1
+ else if isRoot(p) then 1 else 1+ depth<<card-1>>(parp,config[1..(card-1)]);
+tel
+
+node pot<<const card:int>>(p:state;config:state^card) returns (nat:int);
+let
+nat= if p_enable<<n>>(p,config)= [true] then depth<<card>>(p,config) else 0;
+tel
+
+node sum<<const card:int>>(enabled : bool^actions_number^card; config : state^card) returns (pf:int);
+let
+pf= with (card=1) then if enabled[0][0]=true then depth<<card>>(config[0],config) else 0
+ else if enabled[0][0]=true then depth<<card>>(config[0],config) + sum<<card-1>>(enabled[1..(card-1)],config[1..(card-1)])
+ else sum<<card-1>>(enabled[1..(card-1)],config[1..(card-1)]);
+tel
+
+node cost(enabled : bool^actions_number^card; config : state^card) returns (res: int);
+let
+res=sum<<card>>(enabled,config);
+tel
\ No newline at end of file
diff --git a/test/kclustering/kclustering_oracle.lus b/test/kclustering/kclustering_oracle.lus
new file mode 100644
index 00000000..9b623fc2
--- /dev/null
+++ b/test/kclustering/kclustering_oracle.lus
@@ -0,0 +1,31 @@
+-- Here, we use the Lustre version of the algorithm as an oracle for the ocaml version
+
+include "../../sasa/salut/lib/utils.lus"
+--include "cost.lus"
+node kclustering_oracle(
+ legitimate : bool;
+ -- ocaml_cost : real;
+ ocaml_enabled : bool^actions_number^card;
+ active : bool^actions_number^card;
+ ocaml_config : state^card;
+)
+returns (ok : bool)
+var
+ lustre_config : state^card;
+ lustre_enabled : bool^actions_number^card;
+-- lustre_cost:int;
+let
+ lustre_config, lustre_enabled =
+ topology(active -> pre active, -- ignored at the first step
+ ocaml_config -- used at the first step only
+ );
+ -- lustre_cost = cost(lustre_enabled, lustre_config);
+ ok = lustre_enabled = ocaml_enabled
+ -- compare the sasa dot interpretation and the salut dot to lustre compilation
+ and lustre_config = ocaml_config ;
+ -- compare the lustre and the ocaml version of the processes
+ -- and Lustre::real2int(ocaml_cost) = lustre_cost;
+ -- compare the cost functions
+tel
+
+
diff --git a/test/kclustering/p.lus b/test/kclustering/p.lus
new file mode 100644
index 00000000..3b2f8457
--- /dev/null
+++ b/test/kclustering/p.lus
@@ -0,0 +1,121 @@
+type state= struct{isRoot:bool; alpha:int ; par:int};
+type action=enum{change_alpha};
+const actions_number=1;
+const k= 2 ;
+function action_of_int (i:int) returns (a:action);
+let
+a=change_alpha;
+tel
+
+function isRoot(p:state) returns (b:bool);
+let
+b=p.isRoot;
+tel
+
+function isShort (p:state) returns (b:bool);
+let
+b= p.alpha < k;
+tel
+
+function isTall (p:state) returns (b:bool);
+let
+b= p.alpha >= k;
+tel
+
+function kDominator (p:state) returns (b:bool);
+let
+b= (p.alpha = k) or (isShort(p) and isRoot(p));
+tel
+
+function reply<<const n:int>>(p:state;nl:state^n;rl:int^n) returns (r:int);
+let
+r=with (n=1) then rl[0]
+ else if p=nl[0] then rl[0] else reply<<n-1>>(p,nl[1..(n-1)],rl[1..(n-1)]);
+tel
+
+function children<<const n:int>>(p:state; nl:state^n; rl:int^n) returns (cl:bool^n);
+let
+cl= with (n=1) then [ nl[0].par=reply<<n>>(nl[0],nl,rl) ]
+ else [nl[0].par=reply<<n>>(nl[0],nl,rl)] | children<<n-1>>(p,nl[1..(n-1)],rl[1..(n-1)])
+;
+tel
+
+function shortChildren<<const n:int>>(p:state; nl:state^n;rl:int^n) returns (sl:bool^n);
+var c:bool^n;
+let
+c=children<<n>>(p,nl,rl);
+sl= with (n=1) then [c[0]=true and isShort(nl[0])]
+ else [(c[0]=true and isShort(nl[0]))] | shortChildren <<n-1>>(p,nl[1..(n-1)],rl[1..(n-1)]) ;
+
+tel
+
+function tallChildren<<const n:int>>(p:state; nl: state^n;rl:int^n) returns (tl:bool^n) ;
+var c:bool^n;
+let
+c=children<<n>>(p,nl,rl);
+tl=with (n=1) then [c[0]=true and isTall(nl[0])]
+ else [c[0]=true and isTall(nl[0])] | tallChildren <<n-1>>(p,nl[1..(n-1)],rl[1..(n-1)]) ;
+tel
+
+function max<<const n:int>>(p:state;nl:state^n;rl:int^n) returns (m:int);
+var scd:bool^n;
+let
+scd=shortChildren<<n>>(p,nl,rl);
+m=with (n=1) then if scd[0]=true then nl[0].alpha else 0
+ else if scd[0]=true then if nl[0].alpha > max<<n-1>>(p,nl[1..(n-1)],rl[1..(n-1)]) then nl[0].alpha
+ else max<<n-1>>(p,nl[1..(n-1)],rl[1..(n-1)])
+ else max<<n-1>>(p,nl[1..(n-1)],rl[1..(n-1)]);
+tel
+
+function min<<const n:int>>(p:state;nl:state^n;rl:int^n) returns (m:int);
+var tcd: bool^n;
+let
+tcd=tallChildren<<n>>(p,nl,rl);
+m=with (n=1) then if tcd[0]=true then nl[0].alpha else -1
+ else if tcd[0]=true then if min<<n-1>>(p,nl[1..(n-1)],rl[1..(n-1)])<>(-1)
+
+ then if nl[0].alpha < min<<n-1>>(p,nl[1..(n-1)],rl[1..(n-1)])
+ then nl[0].alpha
+ else min<<n-1>>(p,nl[1..(n-1)],rl[1..(n-1)])
+ else nl[0].alpha
+
+ else min<<n-1>>(p,nl[1..(n-1)],rl[1..(n-1)]);
+tel
+
+function maxAshort<<const n:int>>(p:state ; nl:state^n;rl:int^n) returns (max:int);
+var scd:bool^n;
+let
+scd=shortChildren<<n>>(p,nl,rl);
+max= if boolred<<0,0,n>>(scd) then -1 else max<<n>>(p,nl,rl);
+tel
+
+function minAtall<<const n:int>>(p:state ; nl:state^n; rl:int^n) returns (min:int);
+var tcd:bool^n;
+let
+tcd=tallChildren<<n>>(p,nl,rl);
+min= if boolred<<0,0,n>>(tcd) then (2*k + 1)else min<<n>>(p,nl,rl);
+tel
+
+function newAlpha<<const n:int>>(p:state; nl:state^n;rl:int^n) returns (x:int);
+var mas,mit:int;
+let
+mas=maxAshort<<n>>(p,nl,rl);
+mit=minAtall<<n>>(p,nl,rl);
+x=if (mas + mit) <= ((2*k)-2)
+ then (mit + 1)
+ else (mas + 1 );
+tel
+
+function p_enable<<const n:int>>(p:state ; nl:state^n; rl:int^n) returns
+(a:bool^actions_number);
+let
+a= [p.alpha <> newAlpha<<n>>(p,nl,rl)];
+tel
+
+function p_step <<const n:int>>(p:state; nl:state^n;rl:int^n; a:action)
+returns (pnew:state);
+let
+pnew = state{isRoot=p.isRoot; alpha=newAlpha<<n>>(p,nl,rl); par=p.par} ;
+tel
+
+--rl=reply list
\ No newline at end of file
diff --git a/test/kclustering/p.ml b/test/kclustering/p.ml
new file mode 120000
index 00000000..24d41e87
--- /dev/null
+++ b/test/kclustering/p.ml
@@ -0,0 +1 @@
+../../../test/k-clustering/p.ml
\ No newline at end of file
diff --git a/test/kclustering/state.ml b/test/kclustering/state.ml
new file mode 120000
index 00000000..833567ba
--- /dev/null
+++ b/test/kclustering/state.ml
@@ -0,0 +1 @@
+../../../test/k-clustering/state.ml
\ No newline at end of file
diff --git a/test/kclustering/verify.lus b/test/kclustering/verify.lus
new file mode 100644
index 00000000..9a5d06e4
--- /dev/null
+++ b/test/kclustering/verify.lus
@@ -0,0 +1,55 @@
+include "../../sasa/salut/lib/sas.lus"
+include "../../sasa/salut/lib/utils.lus"
+
+include "cost.lus"
+const worst_case=3*card*(card-1)/2 - card - 1;
+
+node verify(
+ active : bool^actions_number^card;
+ init_config : state^card
+)
+returns (ok : bool);
+var
+ config : state^card;
+ enabled : bool^actions_number^card;
+ legitimate, closure : bool;
+ steps, cost : int;
+let
+ assert(true -> daemon_is_distributed<<actions_number,card>>(active, pre enabled));
+-- assert(true -> daemon_is_synchronous<<actions_number,card>>(active, pre enabled));
+ assert(rangei<<0,card>>(init_config));
+
+ config, enabled = topology(active, init_config);
+ assert(config = init_config -> true);
+
+ -- stability in this algo means mutual exclusion: exactly 1 node is enabled at a time
+ legitimate = n_xor<<card>>(map<<n_or<<actions_number>>,card>> (enabled));
+ closure = true -> (pre(legitimate) => legitimate);
+
+ cost = cost(enabled, config);
+ -- converge = (true -> legitimate or pre(cost)>cost);
+
+ steps = 0 -> (pre(steps) + 1);
+ ok = closure
+ -- and (steps > worst_case) => legitimate -- the worst-case stabilization
+
+ -- and (steps > worst_case - 1) => legitimate -- is tigth!
+;
+tel;
+
+node stVint<<const card:int>>(c:state^card) returns (ca:int^card);
+let
+ca=with (card=1) then [c[0].alpha]
+ else [c[0].alpha] | stVint<<card-1>>(c[1..(card-1)]);
+tel
+
+node rangei<<const low:int; const card:int>>(c:state^card) returns (res:bool);
+var
+ ranges_min, ranges_max : bool^card;ca:int^card;
+let
+ ca=stVint<<card>>(c);
+ ranges_min = map<< <= , card>>(low^card, ca);
+ ranges_max = map<< < , card>>(ca, card^card);
+ res = boolall<<card>>(ranges_min) and boolall<<card>>(ranges_max);
+tel
+
--
GitLab