diff --git a/test/bfs-spanning-tree/bfstreelus_oracle.lus b/test/bfs-spanning-tree/bfstreelus_oracle.lus
deleted file mode 100644
index fc3062b816d33d918d445f01a966a26c46b796da..0000000000000000000000000000000000000000
--- a/test/bfs-spanning-tree/bfstreelus_oracle.lus
+++ /dev/null
@@ -1,37 +0,0 @@
--- Here, we use the Lustre version of the algorithm as an oracle for the ocaml version
-
-include "../../sasa/salut/lib/utils.lus"
-
-
-node bfstreelus_oracle(
- legitimate : bool;
- ocaml_enabled : bool^actions_number^card;
- active : bool^actions_number^card;
- ocaml_config : int^(card*2);
-)
-returns (ok : bool);
-var
- lustre_config : state^card;
- lustre_enabled : bool^actions_number^card;
-let
- lustre_config, lustre_enabled =
- topology(active -> pre active, -- ignored at the first step
- iVstate(ocaml_config) -- used at the first step only
- );
-
- ok = lustre_enabled = ocaml_enabled
- -- compare the sasa dot interpretation and the salut dot to lustre compilation
- and stateVi(lustre_config) =ocaml_config;
- -- compare the lustre and the ocaml version of the processes
-
- -- compare the cost functions
-tel
-
-function iVstate (oc:int^(card*2)) returns (ocs:state^card);
-let
-ocs=[state{d=oc[1];par=oc[0]} , state{d=oc[3];par=oc[2]}, state{d=oc[5];par=oc[4]}];
-tel
-function stateVi (lc:state^card) returns (lci:int^(card*2));
-let
-lci=[lc[0].par,lc[0].d,lc[1].par,lc[1].d,lc[2].par,lc[2].d];
-tel
\ No newline at end of file
diff --git a/test/bfs-spanning-tree/tree3.dot b/test/bfs-spanning-tree/tree3.dot
deleted file mode 100644
index b84e47390dfa52c77844d48fd6ea361933a87193..0000000000000000000000000000000000000000
--- a/test/bfs-spanning-tree/tree3.dot
+++ /dev/null
@@ -1,17 +0,0 @@
-graph tree3 {
-graph [min_deg=1
- mean_deg=1.33333333333
- max_deg=2
- is_connected=true
- is_cyclic=false
- is_tree=true
- links_number=2
- is_rooted=false]
- Root [algo="root.ml"]
- p1 [algo="p.ml"]
- p2 [algo="p.ml"]
-
- p1 -- Root
- p2 -- Root
-}
-
diff --git a/test/bfs-spanning-tree/tree3_oracle.lus b/test/bfs-spanning-tree/tree3_oracle.lus
deleted file mode 100644
index bf499e23975b1d4892c5f057e487190440f3e0d3..0000000000000000000000000000000000000000
--- a/test/bfs-spanning-tree/tree3_oracle.lus
+++ /dev/null
@@ -1,48 +0,0 @@
--- Automatically generated by /home/emile/.opam/4.12.0/bin/sasa version "v4.6.1" ("c3dfe95")
--- on PC-Travail the 22/6/2022 at 13:17:37
---sasa -glos tree3.dot
-
-include "bfs_spanning_tree_oracle.lus"
-const an=2; -- actions number
-const pn=3; -- processes number
-const degree=2;
-const min_degree=1;
-const mean_degree=1.333333;
-const diameter=2;
-const card=3;
-const links_number=2;
-const is_cyclic=false;
-const is_connected=true;
-const is_a_tree=true;
-const f=false;
-const t=true;
-const adjacency=[
- [f,t,t],
- [t,f,f],
- [t,f,f]];
-const mean_deg=1.33333333333;
-const max_deg=2;
-const is_tree=true;
-const is_rooted=false;
-const min_deg=1;
-
-node oracle(legitimate:bool;
- Root_par:int;Root_d:int;p1_par:int;p1_d:int;p2_par:int;p2_d:int;
- Enab_Root_CD,Enab_Root_CP,Enab_p1_CD,Enab_p1_CP,Enab_p2_CD,Enab_p2_CP:bool;
- Root_CD,Root_CP,p1_CD,p1_CP,p2_CD,p2_CP:bool)
-returns (ok:bool);
-var
- Acti:bool^an^pn;
- Enab:bool^an^pn;
- Config:state^card;
- a,b,c:state;
-let
- Acti = [[Root_CD,Root_CP],[p1_CD,p1_CP],[p2_CD,p2_CP]];
- Enab = [[Enab_Root_CD,Enab_Root_CP],[Enab_p1_CD,Enab_p1_CP],[Enab_p2_CD,Enab_p2_CP]];
- a = state { par=Root_par; d=Root_d};
- b = state { par=p1_par; d=p1_d};
- c = state { par=p2_par; d=p2_d};
- Config = [a,b,c];
-
- ok = bfs_spanning_tree_oracle(legitimate, Enab, Acti, Config);
-tel
diff --git a/test/dijkstra-ring/p.lus b/test/dijkstra-ring/p.lus
index 196daf81e5b252d354d38f13fba91075c5c6ccb4..71be3cd22078bd1cbab20f078c22b970554fbebd 100644
--- a/test/dijkstra-ring/p.lus
+++ b/test/dijkstra-ring/p.lus
@@ -1,13 +1,13 @@
-function p_enable<<const degree:int>>(this : state; neighbors : state^degree)
+function p_enable<<const degree:int>>(this : state; neighbors : neigh^degree)
returns (enabled : bool^actions_number);
let
- enabled = [ this <> neighbors[0] ];
+ enabled = [ this <> state(neighbors[0]) ];
tel;
function p_step<<const degree:int>>(
this : state;
- neighbors : state^degree; action : action)
+ neighbors : neigh^degree; action : action)
returns (new : state);
let
- new = neighbors[0];
+ new = state(neighbors[0]);
tel;
diff --git a/test/dijkstra-ring/root.lus b/test/dijkstra-ring/root.lus
index bc97347e1cd2b4424c489df09faa9f50badffe4e..ab3ac4ee649ace5f935841e40a0f4c94c6a2e322 100644
--- a/test/dijkstra-ring/root.lus
+++ b/test/dijkstra-ring/root.lus
@@ -1,22 +1,12 @@
-type state = int;
-
-type action = enum { T };
-const actions_number = 1;
-
-function action_of_int(i : int) returns (a : action);
-let
- a = T;
-tel;
-
-function root_enable<<const degree:int>>(this : state; neighbors : state^degree)
+function root_enable<<const degree:int>>(this : state; neighbors : neigh^degree)
returns (enabled : bool^actions_number);
let
- enabled = [ this = neighbors[0] ];
+ enabled = [ this = state(neighbors[0]) ];
tel;
function root_step<<const degree:int>>(
this : state;
- neighbors : state^degree;
+ neighbors : neigh^degree;
action : action)
returns (new : state);
let
diff --git a/test/kclustering/Makefile b/test/kclustering/Makefile
index 4e457463a32655d956b591738993567fbea0cf30..12f6d520f18c1bd5980d296cd535294b7d619243 100644
--- a/test/kclustering/Makefile
+++ b/test/kclustering/Makefile
@@ -1,27 +1,37 @@
-TOPOLOGY ?= tree3
+TOPOLOGY ?= tree5
DOT2LUSFLAGS ?=
SASA_ALGOS := p.ml
DECO_PATTERN="0-:p.ml"
-
include ../Makefile.inc
-include ../Makefile.dot
+##############################################################################
+# Non-regression tests
+
+test: tree3.kind2-test tree3.lurette #lesar not work because of the modulo.
+
clean: genclean
- rm -f tree*.*
+ rm -f $(TOPOLOGY)*.* tree3*.*
-## Some examples of use of ../Makefile.inc
+##############################################################################
+# Other examples of use
+## Some examples of use of ../Makefile.inc
# run a simulation with luciole
-simu: tree3.simu
+simu: $(TOPOLOGY).simu
+
+# Compare the ocaml version with the lustre one (with seed)
+compare_seed: $(TOPOLOGY).lurette
+ cat kclustering.rif
-# Compare the ocaml version with the lustre one
-compare: tree3.lurette
+# Compare the ocaml version with the lustre one (no seed)
+compare: $(TOPOLOGY).lurette_no_seed
cat kclustering.rif
# make diring4.simu
-kind2: tree3.kind2
+kind2: $(TOPOLOGY).kind2
## do not work because there is a modulo in p.lus, which is not (yet) implemented in ../../bit-blast/*.lus
-lesar: tree3.lesar
+lesar: $(TOPOLOGY).lesar
diff --git a/test/kclustering/kclustering_oracle.lus b/test/kclustering/kclustering_oracle.lus
index 62166f35a2633b3bc6bad9abdd56162748e934e5..3c246d53a8498243ec3a281c0bc0a621011b2cb8 100644
--- a/test/kclustering/kclustering_oracle.lus
+++ b/test/kclustering/kclustering_oracle.lus
@@ -1,32 +1,46 @@
-- Here, we use the Lustre version of the algorithm as an oracle for the ocaml version
include "../../lib/utils.lus"
---include "cost.lus"
+include "cost.lus"
+
+function to_state(par:int; alpha:int; isRoot:bool)
+returns ( res : state);
+let
+ res = state { isRoot=isRoot; par=par; alpha=alpha };
+tel;
+
node kclustering_oracle(
legitimate : bool;
- -- ocaml_cost : real;
+ ocaml_cost : real;
ocaml_enabled : bool^actions_number^card;
active : bool^actions_number^card;
ocaml_config : state^card;
+ round : bool;
+ round_nb : int;
)
returns (ok : bool;
+ lustre_cost:int;
lustre_config : state^card;
lustre_enabled : bool^actions_number^card;
-)
+ lustre_round:bool;
+ lustre_round_nb:int);
--var
--- lustre_cost:int;
+
let
- lustre_config, lustre_enabled =
+ lustre_config, lustre_enabled, lustre_round, lustre_round_nb =
topology(active -> pre active, -- ignored at the first step
ocaml_config -- used at the first step only
);
- -- lustre_cost = cost(lustre_enabled, lustre_config);
+ 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 ;
+ and lustre_config = ocaml_config
+-- and lustre_round = round
+-- and lustre_round_nb = round_nb
-- compare the lustre and the ocaml version of the processes
- -- and Lustre::real2int(ocaml_cost) = lustre_cost;
+ and Lustre::real2int(ocaml_cost) = lustre_cost
-- compare the cost functions
+ ;
tel
diff --git a/test/kclustering/p.lus b/test/kclustering/p.lus
index 3b2f8457a1adbe644c3d4359f88752ea0412c90a..40250d33904b5927c29cdc5d60e11fad25da6286 100644
--- a/test/kclustering/p.lus
+++ b/test/kclustering/p.lus
@@ -1,121 +1,138 @@
-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
+-----------------------------------------------------------------------------
+--Predicates:
function isRoot(p:state) returns (b:bool);
let
-b=p.isRoot;
+ b=p.isRoot;
tel
function isShort (p:state) returns (b:bool);
let
-b= p.alpha < k;
+ b= p.alpha < k;
tel
function isTall (p:state) returns (b:bool);
let
-b= p.alpha >= k;
+ 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)]);
+ b= (p.alpha = k) or (isShort(p) and isRoot(p));
tel
-function children<<const n:int>>(p:state; nl:state^n; rl:int^n) returns (cl:bool^n);
+-----------------------------------------------------------------------------
+--Macros:
+function children<<const n:int>>(p:state; nl:neigh^n)
+returns (cl:bool^n);
+var
+ elem:state;
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)])
+ elem = state(nl[0]);
+ cl = with (n=1) then [ elem.par=reply(nl[0]) ]
+ else [ elem.par=reply(nl[0]) ] | children<<n-1>>(p,nl[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;
+function shortChildren<<const n:int>>(p:state; nl:neigh^n; c:bool^n)
+returns (sl:bool^n);
+var
+ elem:state;
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)]) ;
-
+ elem = state(nl[0]);
+ sl= with (n=1) then [c[0] and isShort(elem)]
+ else [(c[0] and isShort(elem))] | shortChildren <<n-1>>(p,nl[1..(n-1)],c[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;
+function tallChildren<<const n:int>>(p:state; nl: neigh^n; c: bool^n)
+returns (tl:bool^n);
+var
+ elem:state;
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)]) ;
+ elem = state(nl[0]);
+ tl=with (n=1) then [c[0] and isTall(elem)]
+ else [c[0] and isTall(elem)] | tallChildren <<n-1>>(p,nl[1..(n-1)],c[1..(n-1)]) ;
tel
-
-function max<<const n:int>>(p:state;nl:state^n;rl:int^n) returns (m:int);
-var scd:bool^n;
+
+function max<<const n:int>>(scd:bool^n; nl:neigh^n; maxi:int)
+returns (m:int);
+var
+ elem:state;
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)]);
+ elem = state(nl[0]);
+ m=with (n=1) then if scd[0]
+ then if elem.alpha > maxi
+ then elem.alpha
+ else maxi
+ else maxi
+ else if scd[0] then if elem.alpha > maxi
+ then max<<n-1>>(scd[1..(n-1)],nl[1..(n-1)],elem.alpha)
+ else max<<n-1>>(scd[1..(n-1)],nl[1..(n-1)],maxi)
+ else max<<n-1>>(scd[1..(n-1)],nl[1..(n-1)],maxi);
tel
-
-function min<<const n:int>>(p:state;nl:state^n;rl:int^n) returns (m:int);
-var tcd: bool^n;
+
+function min<<const n:int>>(tcd:bool^n;nl:neigh^n;mini:int)
+returns (m:int);
+var
+ elem:state;
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)]);
+ elem = state(nl[0]);
+ m=with (n=1) then if tcd[0] then if mini = -1 then elem.alpha
+ else if elem.alpha < mini
+ then elem.alpha
+ else mini
+ else mini
+ else if tcd[0] then if mini = -1 then min<<n-1>>(tcd[1..(n-1)],nl[1..(n-1)],elem.alpha)
+ else if elem.alpha < mini
+ then min<<n-1>>(tcd[1..(n-1)],nl[1..(n-1)],elem.alpha)
+ else min<<n-1>>(tcd[1..(n-1)],nl[1..(n-1)],mini)
+ else min<<n-1>>(tcd[1..(n-1)],nl[1..(n-1)],mini);
tel
-
-function maxAshort<<const n:int>>(p:state ; nl:state^n;rl:int^n) returns (max:int);
-var scd:bool^n;
+
+function maxAshort<<const n:int>>(p:state ; nl:neigh^n; c:bool^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);
+ scd=shortChildren<<n>>(p,nl,c);
+ max= if boolred<<0,0,n>>(scd) then -1 else max<<n>>(scd,nl,0);
tel
-
-function minAtall<<const n:int>>(p:state ; nl:state^n; rl:int^n) returns (min:int);
-var tcd:bool^n;
+
+function minAtall<<const n:int>>(p:state ; nl:neigh^n; c:bool^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);
+ tcd=tallChildren<<n>>(p,nl,c);
+ min= if boolred<<0,0,n>>(tcd) then (2*k + 1)else min<<n>>(tcd,nl,-1);
tel
-
-function newAlpha<<const n:int>>(p:state; nl:state^n;rl:int^n) returns (x:int);
-var mas,mit:int;
+
+function newAlpha<<const n:int>>(p:state; nl:neigh^n)
+returns (x:int);
+var
+ mas,mit:int;
+ c:bool^n;
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 );
+ c=children<<n>>(p,nl);
+ mas=maxAshort<<n>>(p,nl,c);
+ mit=minAtall<<n>>(p,nl,c);
+ 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);
+-----------------------------------------------------------------------------
+--Step and Enable function:
+function p_enable<<const n:int>>(p:state ; nl:neigh^n)
+returns (a:bool^actions_number);
let
-a= [p.alpha <> newAlpha<<n>>(p,nl,rl)];
+ a= [p.alpha <> newAlpha<<n>>(p,nl)];
tel
-
-function p_step <<const n:int>>(p:state; nl:state^n;rl:int^n; a:action)
+
+function p_step <<const n:int>>(p:state; nl:neigh^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
+ pnew = state{isRoot=p.isRoot; alpha=newAlpha<<n>>(p,nl); par=p.par} ;
+tel
\ No newline at end of file
diff --git a/test/kclustering/state.lus b/test/kclustering/state.lus
new file mode 100644
index 0000000000000000000000000000000000000000..b8b89a5bfb788e9af5de375c76be7655db4ee587
--- /dev/null
+++ b/test/kclustering/state.lus
@@ -0,0 +1,17 @@
+-- automatically generated by salut
+
+type state = struct{isRoot:bool; alpha:int ; par:int};
+
+type action = enum{change_alpha};
+const actions_number = 1;
+
+function action_of_int(i : int) returns (a : action);
+let
+ a = change_alpha;
+tel;
+
+function legitimate<<const actions_number:int; const card:int>>(enables : bool^actions_number^card; config: state^card)
+returns (res : bool);
+let
+ res=silent<<actions_number,card>>(enables);
+tel;
diff --git a/test/kclustering/tree3.dot b/test/kclustering/tree3.dot
deleted file mode 100644
index a407730ceeac70b0db84445891f209dde2be4dd2..0000000000000000000000000000000000000000
--- a/test/kclustering/tree3.dot
+++ /dev/null
@@ -1,17 +0,0 @@
-graph tree3 {
-graph [min_deg=1
- mean_deg=1.33333333333
- max_deg=2
- is_connected=true
- is_cyclic=false
- is_tree=true
- links_number=2
- is_rooted=false]
- Root [algo="p.ml"]
- p1 [algo="p.ml"]
- p2 [algo="p.ml"]
-
- p1 -- Root
- p2 -- Root
-}
-
diff --git a/test/kclustering/tree3.lus b/test/kclustering/tree3.lus
deleted file mode 100644
index f5cbc7c248f2e9fa61ab00f0327bfbec84b3db12..0000000000000000000000000000000000000000
--- a/test/kclustering/tree3.lus
+++ /dev/null
@@ -1,68 +0,0 @@
--- automatically generated by salut
-include "p.lus"
-
-
-function dot2lus_first_set<<const N:int>>(s : bool^N) returns (x : int);
-var
- found : int;
-let
- found =
- with (N = 1) then (if s[0] then 0 else -1)
- else dot2lus_first_set<<N-1>>(s[1 .. N-1]);
- x =
- if s[0] then 0
- else if found < 0 then -1
- else found + 1;
-tel;
-
-function dot2lus_action_of_activation(activation : bool^actions_number) returns (action : action);
-let
- action = action_of_int(dot2lus_first_set<<actions_number>>(activation));
-tel;
-
-node tree3(p : bool^actions_number^card; initials : state^card)
-returns (p_c : state^card; Enab_p : bool^actions_number^card);
-var
- prev_p_c : state^card;
-
- sel_0 : bool;
- sel_1 : bool;
- sel_2 : bool;
-let
- prev_p_c = initials -> pre(p_c);
-
- sel_0 = false -> boolred<<1,actions_number,actions_number>>(p[0]);
- sel_1 = false -> boolred<<1,actions_number,actions_number>>(p[1]);
- sel_2 = false -> boolred<<1,actions_number,actions_number>>(p[2]);
-
- p_c[0] =
- if not sel_0 then prev_p_c[0]
- else p_step<<2>>(
- prev_p_c[0],
- [ prev_p_c[1], prev_p_c[2] ],
- [0,0],
- dot2lus_action_of_activation(p[0])
- );
- Enab_p[0] = p_enable<<2>>(p_c[0], [ p_c[1], p_c[2] ],[0,0]);
-
- p_c[1] =
- if not sel_1 then prev_p_c[1]
- else p_step<<1>>(
- prev_p_c[1],
- [ prev_p_c[0] ],
- [0],
- dot2lus_action_of_activation(p[1])
- );
- Enab_p[1] = p_enable<<1>>(p_c[1], [ p_c[0] ],[0]);
-
- p_c[2] =
- if not sel_2 then prev_p_c[2]
- else p_step<<1>>(
- prev_p_c[2],
- [ prev_p_c[0] ],
- [1],
- dot2lus_action_of_activation(p[2])
- );
- Enab_p[2] = p_enable<<1>>(p_c[2], [ p_c[0] ],[1]);
-tel;
-node topology = tree3;
diff --git a/test/kclustering/tree3_const.lus b/test/kclustering/tree3_const.lus
deleted file mode 100644
index 38d2bec933639334f02b76fa629d80cdcce9a66e..0000000000000000000000000000000000000000
--- a/test/kclustering/tree3_const.lus
+++ /dev/null
@@ -1,21 +0,0 @@
--- automatically generated by salut
-const card = 3;
-const links_number = 2;
-const max_degree = 2;
-const min_degree = 1;
-const mean_degree = 1.333333;
-const is_directed = false;
-const diameter= 2;
-const is_cyclic = false;
-const is_connected = true;
-const min_deg = 1;
-const mean_deg = 1.33333333333;
-const max_deg = 2;
-const is_tree = true;
-const is_rooted = false;
-const t = true;
-const f = false;
-const adjacency = [
- [f,t,t],
- [t,f,f],
- [t,f,f]];
diff --git a/test/kclustering/tree3_oracle.lus b/test/kclustering/tree3_oracle.lus
deleted file mode 100644
index 683c31e43fbd678c58bbbab5c09e80507b362042..0000000000000000000000000000000000000000
--- a/test/kclustering/tree3_oracle.lus
+++ /dev/null
@@ -1,48 +0,0 @@
--- Automatically generated by /home/invite/.opam/4.12.0/bin/sasa version "v4.6.0" ("opam")
--- on debian the 28/6/2022 at 11:54:15
---sasa -glos tree3.dot
-
-include "kclustering_oracle.lus"
-const an=1; -- actions number
-const pn=3; -- processes number
-const degree=2;
-const min_degree=1;
-const mean_degree=1.333333;
-const diameter=2;
-const card=3;
-const links_number=2;
-const is_cyclic=false;
-const is_connected=true;
-const is_a_tree=true;
-const f=false;
-const t=true;
-const adjacency=[
- [f,t,t],
- [t,f,f],
- [t,f,f]];
-const mean_deg=1.33333333333;
-const max_deg=2;
-const is_tree=true;
-const is_rooted=false;
-const min_deg=1;
-
-node oracle(legitimate:bool;
- Root_par:int;Root_alpha:int;Root_isRoot:bool;p1_par:int;p1_alpha:int;p1_isRoot:bool;p2_par:int;p2_alpha:int;p2_isRoot:bool;
- Enab_Root_change_alpha,Enab_p1_change_alpha,Enab_p2_change_alpha:bool;
- Root_change_alpha,p1_change_alpha,p2_change_alpha:bool)
-returns (ok:bool;
- lustre_e:bool^an^pn;
- lustre_c:state^card
-);
-var
- Acti:bool^an^pn;
- Enab:bool^an^pn;
- Config:state^card;
-let
- Acti = [[Root_change_alpha],[p1_change_alpha],[p2_change_alpha]];
- Enab = [[Enab_Root_change_alpha],[Enab_p1_change_alpha],[Enab_p2_change_alpha]];
- Config = [ state{isRoot=Root_isRoot;alpha=Root_alpha;par=Root_par}, state{isRoot=p1_isRoot;alpha=p1_alpha;par=p1_par},
- state{isRoot=p2_isRoot;alpha=p2_alpha;par=p2_par}];
-
- ok,lustre_c,lustre_e = kclustering_oracle(legitimate, Enab, Acti, Config);
-tel
diff --git a/test/kclustering/verify.lus b/test/kclustering/verify.lus
index 702ef10380e1946a1332835d3e36a9b70f49df24..9de69609ec7b17b3222edc2bb8d813e89707663e 100644
--- a/test/kclustering/verify.lus
+++ b/test/kclustering/verify.lus
@@ -1,8 +1,8 @@
include "../../lib/sas.lus"
include "../../lib/utils.lus"
-include "cost.lus"
-const worst_case=3*card*(card-1)/2 - card - 1;
+--include "cost.lus"
+--const worst_case=3*card*(card-1)/2 - card - 1;
node verify(
active : bool^actions_number^card;
@@ -11,45 +11,65 @@ node verify(
returns (ok : bool);
var
config : state^card;
- enabled : bool^actions_number^card;
- legitimate, closure,converge : bool;
- steps, cost : int;
+ enables : bool^actions_number^card;
+ legitimate, closure, lustre_round : bool;
+ lustre_round_nb:int;
+-- converge : 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));
+ assert(rangei<<0,card,card>>(init_config) and Root_is_Valid<<card>>(init_config));
+ assert(true -> daemon_is_valid<<actions_number,card>>(active, pre enables));
- config, enabled = topology(active, init_config);
- assert(config = init_config -> true);
+ config, enables, lustre_round, lustre_round_nb = topology(active, init_config);
+-- assert(config = init_config -> true);
- legitimate = silent<<actions_number,card>>(enabled);
+ legitimate = silent<<actions_number,card>>(enables);
closure = true -> (pre(legitimate) => legitimate);
- cost = cost(enabled, config);
- converge = (true -> legitimate or pre(cost)>cost);
+-- cost = cost(enabled, config);
+-- converge = (true -> legitimate or pre(cost)>cost);
- steps = 0 -> (pre(steps) + 1);
+-- steps = 0 -> (pre(steps) + 1);
ok = closure
- and converge
+-- and converge
-- 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);
+----------------------------------------------------------------------------
+-- all states are initially in correctly
+----------------------------------------------------------------------------
+node rangei<<const low:int; const card:int; const max:int>>(config:state^card) returns (res:bool);
+var
+ e:state;
let
-ca=with (card=1) then [c[0].alpha]
- else [c[0].alpha] | stVint<<card-1>>(c[1..(card-1)]);
+ e = config[card-1];
+ res = with (card=1) then ((e.alpha >= 0) and (e.alpha < card) and
+ if e.isRoot
+ then e.par = -1
+ else (e.par >=0) and (e.par < nb_neighbors[card-1]))
+ else ((e.alpha >= 0) and
+ (e.alpha < card) and
+ if e.isRoot
+ then e.par = -1
+ else (e.par >=0) and (e.par < nb_neighbors[card-1])
+ ) and rangei<<low; card-1; max>>(config[0..card-2]);
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;
+function extract_isRoot (elem:state)
+returns (res : bool);
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);
+ res = elem.isRoot;
tel
+function Root_is_Valid<<const card:int>>(config:state^card)
+returns (res:bool);
+var
+ tab_bool:bool^card;
+let
+ tab_bool = map<<extract_isRoot,card>>(config);
+ res = boolred<<1,1,card>>(tab_bool);
+tel
+----------------------------------------------------------------------------
\ No newline at end of file
diff --git a/test/rsp_tree/rsp_tree_oracle.lus b/test/rsp_tree/rsp_tree_oracle.lus
index afaabbb77b724cccd8bea4ce07752f06cba356ae..6b825f28fc4191edefc3b72ce54ab02517a95d1a 100644
--- a/test/rsp_tree/rsp_tree_oracle.lus
+++ b/test/rsp_tree/rsp_tree_oracle.lus
@@ -1,4 +1,3 @@
-
-- Here, we use the Lustre version of the algorithm as an oracle for the ocaml version
include "../../lib/utils.lus"
diff --git a/test/rsp_tree/verify.lus b/test/rsp_tree/verify.lus
index 77bb00349a179dad7e4b2627ed00caa4e22a1a44..c9a41ba5283e9d6e10ec39a462519867e2ef6dc8 100644
--- a/test/rsp_tree/verify.lus
+++ b/test/rsp_tree/verify.lus
@@ -33,11 +33,11 @@ var
let
e = config[card-1];
res = with (card=1) then (e.d = 0) and (e.st = C) and (e.par = -1)
- else ((e.d >= 0) and
- (e.d < nb_neighbors[card-1]) and
- (e.par >=0) and
- (e.par < nb_neighbors[card-1]) and
- ((e.st = I) or (e.st = C) or (e.st = EB) or (e.st = EF))
- ) and rangei<<low; card-1; max>>(config[0..card-2]);
+ else ((e.d >= 0) and
+ (e.d < card) and
+ (e.par >=0) and
+ (e.par < nb_neighbors[card-1]) and
+ ((e.st = I) or (e.st = C) or (e.st = EB) or (e.st = EF))
+ ) and rangei<<low; card-1; max>>(config[0..card-2]);
tel
----------------------------------------------------------------------------
\ No newline at end of file