From 2c564565f3d47bd151df1bdd35ace67ac64fc4e1 Mon Sep 17 00:00:00 2001
From: invite <invite@debian>
Date: Fri, 1 Jul 2022 09:52:27 +0200
Subject: [PATCH] add bfs spt
---
test/bfs-spanning-tree/Makefile | 27 +++++++++
test/bfs-spanning-tree/bfstreelus_oracle.lus | 37 +++++++++++++
test/bfs-spanning-tree/config.ml | 1 +
test/bfs-spanning-tree/p.lus | 58 ++++++++++++++++++++
test/bfs-spanning-tree/p.ml | 1 +
test/bfs-spanning-tree/root.lus | 20 +++++++
test/bfs-spanning-tree/root.ml | 1 +
test/bfs-spanning-tree/state.ml | 1 +
test/bfs-spanning-tree/verify.lus | 46 ++++++++++++++++
9 files changed, 192 insertions(+)
create mode 100644 test/bfs-spanning-tree/Makefile
create mode 100644 test/bfs-spanning-tree/bfstreelus_oracle.lus
create mode 120000 test/bfs-spanning-tree/config.ml
create mode 100644 test/bfs-spanning-tree/p.lus
create mode 120000 test/bfs-spanning-tree/p.ml
create mode 100644 test/bfs-spanning-tree/root.lus
create mode 120000 test/bfs-spanning-tree/root.ml
create mode 120000 test/bfs-spanning-tree/state.ml
create mode 100644 test/bfs-spanning-tree/verify.lus
diff --git a/test/bfs-spanning-tree/Makefile b/test/bfs-spanning-tree/Makefile
new file mode 100644
index 00000000..610dd54e
--- /dev/null
+++ b/test/bfs-spanning-tree/Makefile
@@ -0,0 +1,27 @@
+TOPOLOGY ?= tree3
+DOT2LUSFLAGS ?=
+SASA_ALGOS := p.ml root.ml
+DECO_PATTERN="0:root.ml 1-: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 bfstreelus.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/bfs-spanning-tree/bfstreelus_oracle.lus b/test/bfs-spanning-tree/bfstreelus_oracle.lus
new file mode 100644
index 00000000..fc3062b8
--- /dev/null
+++ b/test/bfs-spanning-tree/bfstreelus_oracle.lus
@@ -0,0 +1,37 @@
+-- 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/config.ml b/test/bfs-spanning-tree/config.ml
new file mode 120000
index 00000000..def7dd2f
--- /dev/null
+++ b/test/bfs-spanning-tree/config.ml
@@ -0,0 +1 @@
+../../../test/bfs-spanning-tree/config.ml
\ No newline at end of file
diff --git a/test/bfs-spanning-tree/p.lus b/test/bfs-spanning-tree/p.lus
new file mode 100644
index 00000000..f0c10fc3
--- /dev/null
+++ b/test/bfs-spanning-tree/p.lus
@@ -0,0 +1,58 @@
+ const D=diameter;
+
+function minl<<const degree:int>>(nl:state^degree) returns (m:int);
+let
+m=with (degree=1) then nl[0].d
+ else if nl[0].d <= minl<<degree-1>>(nl[1..(degree-1)]) then nl[0].d
+ else minl<<degree-1>>(nl[1..(degree-1)]);
+tel
+
+function distp<<const degree:int>>(p:state; nl:state^degree) returns (dp:int);
+var min:int;
+let
+min=minl<<degree>>(nl);
+dp=if (D-1)< min then (D-1)+1 else min +1 ;
+tel
+
+function dist_Ok<<const degree:int>>(p:state; nl:state^degree) returns (ok:bool);
+let
+ok= p.d -1 = minl<<degree>>(nl);
+tel
+
+function parentd<<const degree:int;const n:int>>(p:state ; nl:state^degree) returns (parp:state);
+let
+parp=with (degree=n) then nl[degree-1]
+ else if p.par=n then nl[n] else parentd<<degree,(n+1)>>(p,nl);
+tel
+
+function p_enable<<const degree:int>>(p:state; nl:state^degree) returns
+(a:bool^actions_number);
+var parp:state;
+let
+parp=parentd<<degree;0>>(p,nl);
+a=[p.d<>distp<<degree>>(p,nl) , dist_Ok<<degree>>(p,nl) and parp.d <> p.d - 1];
+tel
+
+function truelist<<const degree:int>>(p:state;nl:state^degree) returns (bl:bool^degree);
+let
+bl=with (degree=1) then [p.d-1=nl[0].d]
+ else [p.d-1=nl[0].d] | truelist<<degree-1>>(p,nl[1..(degree-1)]);
+tel
+
+function indicefsttrue<<const degree:int>> (bl:bool^degree) returns (i:int);
+let
+i= with (degree=1) then if bl[0]=true then 0 else -1
+ else if bl[0]=true then 0 else 1+ indicefsttrue<<degree-1>>(bl[1..(degree-1)]);
+tel
+
+function p_step<<const degree:int>>(p:state; nl:state^degree; a:action) returns
+(pnew:state);
+var bl:bool^degree;
+var i:int;
+let
+bl=truelist<<degree>>(p,nl);
+i=indicefsttrue<<degree>>(bl);
+pnew= if a= CD then state{d=distp<<degree>>(p,nl); par=p.par}
+ else if a=CP then state{d=p.d; par=i}
+ else p;
+tel
diff --git a/test/bfs-spanning-tree/p.ml b/test/bfs-spanning-tree/p.ml
new file mode 120000
index 00000000..ad883bb0
--- /dev/null
+++ b/test/bfs-spanning-tree/p.ml
@@ -0,0 +1 @@
+../../../test/bfs-spanning-tree/p.ml
\ No newline at end of file
diff --git a/test/bfs-spanning-tree/root.lus b/test/bfs-spanning-tree/root.lus
new file mode 100644
index 00000000..82a6ae95
--- /dev/null
+++ b/test/bfs-spanning-tree/root.lus
@@ -0,0 +1,20 @@
+type state=struct {d:int; par:int} ;
+type action=enum{CD,CP};
+const actions_number=2;
+
+function action_of_int (i:int) returns (a:action);
+let
+a=CD;
+tel
+
+function root_enable<<const degree:int>> (r:state ; nl:state^degree) returns
+ (al: bool^actions_number) ;
+let
+al=[r.d<>0,false];
+tel
+
+function root_step <<const degree:int>> (r:state ; nl:state^degree ; a:action)
+returns (rnew:state);
+let
+rnew= state {d=0; par=r.par};
+tel
diff --git a/test/bfs-spanning-tree/root.ml b/test/bfs-spanning-tree/root.ml
new file mode 120000
index 00000000..daedbf7b
--- /dev/null
+++ b/test/bfs-spanning-tree/root.ml
@@ -0,0 +1 @@
+../../../test/bfs-spanning-tree/root.ml
\ No newline at end of file
diff --git a/test/bfs-spanning-tree/state.ml b/test/bfs-spanning-tree/state.ml
new file mode 120000
index 00000000..740ce359
--- /dev/null
+++ b/test/bfs-spanning-tree/state.ml
@@ -0,0 +1 @@
+../../../test/bfs-spanning-tree/state.ml
\ No newline at end of file
diff --git a/test/bfs-spanning-tree/verify.lus b/test/bfs-spanning-tree/verify.lus
new file mode 100644
index 00000000..cf0aacdc
--- /dev/null
+++ b/test/bfs-spanning-tree/verify.lus
@@ -0,0 +1,46 @@
+include "../../sasa/salut/lib/sas.lus"
+
+node verify(activations : bool^actions_number^card; inits : state^card) returns (ok : bool);
+var
+ config : state^card;
+ enables : bool^actions_number^card;
+ legitimate, closure : bool;
+ steps : int;
+
+
+let
+-- assert(true -> daemon_is_locally_central<<actions_number,card>>(activations, pre enables, adjacency));
+ assert(true -> daemon_is_synchronous<<actions_number,card>>(activations, pre enables));
+ assert(rangei<<0,card>>(inits));
+
+ config, enables = topology(activations, inits);
+
+ legitimate = silent<<actions_number,card>>(enables);
+ closure = true -> (pre(legitimate) => legitimate);
+ steps = 0-> pre(steps) +1;
+
+ -- verify that the execution terminates after at most |N|−1 moves:
+ ok = closure
+ --and (true -> legitimate or pre(pot) > pot) -- much easier to prove
+ and (steps >= card => legitimate)
+;
+tel;
+
+
+node stVint<<const card:int>>(c:state^card) returns (cd:int^card);
+let
+cd=with (card=1) then [c[0].d]
+ else [c[0].d] | stVint<<card-1>>(c[1..(card-1)]);
+tel
+
+-- all states are initially in [0; card|[
+node rangei<<const low:int; const card:int>>(c:state^card) returns (res:bool);
+var
+ ranges_min, ranges_max : bool^card; cd:int^card;
+let
+ cd=stVint<<card>>(c);
+ ranges_min = map<< <= , card>>(low^card, cd);
+ ranges_max = map<< < , card>>(cd, card^card);
+ res = boolall<<card>>(ranges_min) and boolall<<card>>(ranges_max);
+tel
+
--
GitLab