From a34d6243a11a78225d753bb5df35d42e22c1f7d3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nathan=20R=C3=A9biscoul?= <nathan.rebiscoul38@gmail.com>
Date: Thu, 4 Jul 2019 11:58:03 +0200
Subject: [PATCH] Add some oracles

---
 test/bfs-spanning-tree/Makefile               |   7 +
 .../fig5.1-noinit_oracle.lus                  |   2 +-
 test/bfs-spanning-tree/oracle_lemma5_16.lus   |  38 +++++
 test/coloring/Makefile                        |  14 +-
 test/coloring/oracle_lemma3_14.lus            |  22 +++
 test/coloring/oracle_theorem3_17.lus          |  23 +++
 test/coloring/round.lus                       | 132 ++++++++++++++++++
 test/dijkstra-ring/Makefile                   |  26 +++-
 test/dijkstra-ring/oracle_lemma6_28.lus       |  24 ++++
 test/dijkstra-ring/oracle_theorem6_29.lus     |  24 ++++
 test/dijkstra-ring/round.lus                  | 132 ++++++++++++++++++
 test/unison/Makefile                          |  27 +++-
 test/unison/oracle_lemma4_10.lus              |  25 ++++
 test/unison/oracle_theorem4_11.lus            |  27 ++++
 test/unison/round.lus                         | 132 ++++++++++++++++++
 15 files changed, 642 insertions(+), 13 deletions(-)
 create mode 100644 test/bfs-spanning-tree/oracle_lemma5_16.lus
 create mode 100644 test/coloring/oracle_lemma3_14.lus
 create mode 100644 test/coloring/oracle_theorem3_17.lus
 create mode 100644 test/coloring/round.lus
 create mode 100644 test/dijkstra-ring/oracle_lemma6_28.lus
 create mode 100644 test/dijkstra-ring/oracle_theorem6_29.lus
 create mode 100644 test/dijkstra-ring/round.lus
 create mode 100644 test/unison/oracle_lemma4_10.lus
 create mode 100644 test/unison/oracle_theorem4_11.lus
 create mode 100644 test/unison/round.lus

diff --git a/test/bfs-spanning-tree/Makefile b/test/bfs-spanning-tree/Makefile
index f28ef9a0..cc56816e 100644
--- a/test/bfs-spanning-tree/Makefile
+++ b/test/bfs-spanning-tree/Makefile
@@ -37,6 +37,13 @@ lurette1:cmxs fig5.1-noinit.lut
       -sut "lutin fig5.1-noinit.lut -n distributed" \
 		-oracle "lv6 fig5.1-noinit_oracle.lus -n oracle"
 
+lemma5.16:cmxs fig5.1-noinit.lut
+	rdbg -lurette -o lurette.rif  \
+      -env "$(sasa) fig5.1-noinit.dot -custd -rif" \
+      -sut "lutin fig5.1-noinit.lut -n distributed" \
+		-oracle "lv6 oracle_lemma5_16.lus -n oracle"
+
+
 lurette: lurette0
 	sim2chrogtk -ecran -in lurette.rif > /dev/null
 	gnuplot-rif lurette.rif
diff --git a/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus b/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus
index d1a7e835..93b8643a 100644
--- a/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus
+++ b/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus
@@ -27,5 +27,5 @@ let
   Round = round <<m,n>>(Enab,Acti);
   RoundNb = count(Round); 
   Silent = silent<<m,n>>(Enab);
-  ok = (RoundNb>=diameter+2) => Silent; -- from theorem 5.18 page 57
+  ok = (RoundNb>=diameter+2) => Silent ; -- from theorem 5.18 page 57
 tel
diff --git a/test/bfs-spanning-tree/oracle_lemma5_16.lus b/test/bfs-spanning-tree/oracle_lemma5_16.lus
new file mode 100644
index 00000000..ff53296a
--- /dev/null
+++ b/test/bfs-spanning-tree/oracle_lemma5_16.lus
@@ -0,0 +1,38 @@
+-- Automatically generated by /home/nathan/.opam/4.07.0/bin/sasa version "2.5.0-1-g0c65445" ("0c65445")
+-- on Nathan-PC the 26/6/2019 at 16:13:39
+--sasa -glos fig5.2-noinit.dot
+
+include "round.lus"
+
+const n=8;
+const m=2;
+const degree=2;
+const diameter=4;
+
+node ou_CD (X,Y:bool^m) returns (Z:bool^2);
+let
+  Z = [(X[0] or Y[0]),true] ;
+tel 
+
+node all_falseCD (tab_enab:bool^m^n) returns (res:bool);
+let
+  res = not (red<<ou_CD,n>>(false^m,tab_enab))[0] ;
+tel
+
+
+
+node oracle(root_CD,root_CP,p1_CD,p1_CP,p2_CD,p2_CP,p3_CD,p3_CP,p4_CD,p4_CP,p5_CD,p5_CP,p6_CD,p6_CP,p7_CD,p7_CP,Enab_root_CD,Enab_root_CP,Enab_p1_CD,Enab_p1_CP,Enab_p2_CD,Enab_p2_CP,Enab_p3_CD,Enab_p3_CP,Enab_p4_CD,Enab_p4_CP,Enab_p5_CD,Enab_p5_CP,Enab_p6_CD,Enab_p6_CP,Enab_p7_CD,Enab_p7_CP:bool) returns (ok,Round,CD_disable:bool; RoundNb:int);
+
+var
+  	Acti:bool^2^8;
+	Enab:bool^2^8;
+let
+  	Acti = [[root_CD,root_CP],[p1_CD,p1_CP],[p2_CD,p2_CP],[p3_CD,p3_CP],[p4_CD,p4_CP],[p5_CD,p5_CP],[p6_CD,p6_CP],[p7_CD,p7_CP]];
+
+  	Enab = [[Enab_root_CD,Enab_root_CP],[Enab_p1_CD,Enab_p1_CP],[Enab_p2_CD,Enab_p2_CP],[Enab_p3_CD,Enab_p3_CP],[Enab_p4_CD,Enab_p4_CP],[Enab_p5_CD,Enab_p5_CP],[Enab_p6_CD,Enab_p6_CP],[Enab_p7_CD,Enab_p7_CP]];
+  
+  Round = round <<m,n>>(Enab,Acti);
+  RoundNb = count(Round); 
+  CD_disable = all_falseCD(Enab); 
+  ok = (RoundNb>=diameter+1) => CD_disable ; -- Lemma 5.16 !             
+tel
diff --git a/test/coloring/Makefile b/test/coloring/Makefile
index 944ff3d8..b2d24bc3 100644
--- a/test/coloring/Makefile
+++ b/test/coloring/Makefile
@@ -2,7 +2,7 @@
 
 
 test: p.cmxs ring.lut lurette
-	$(sasa) -l 200 ring.dot 
+	$(sasa)  200 ring.dot
 
 
 cmxs: p.cmxs  p.cma
@@ -32,6 +32,16 @@ lurette:cmxs ring.lut
 	lurette   \
       -env "$(sasa) ring.dot -custd " \
       -sut "lutin ring.lut -n distributed" \
-		-oracle "lv6 oracle.lus -n silence "
 
+lemma3.14:cmxs ring.lut
+	lurette   \
+      -env "$(sasa) ring.dot -custd " \
+      -sut "lutin ring.lut -n distributed" \
+		-oracle "lv6 oracle_lemma3_14.lus -n oracle "
+
+theorem3.17:cmxs ring.lut
+	lurette   \
+      -env "$(sasa) ring.dot -custd " \
+      -sut "lutin ring.lut -n distributed" \
+		-oracle "lv6 oracle_theorem3_17.lus -n oracle "
 -include ../Makefile.inc
diff --git a/test/coloring/oracle_lemma3_14.lus b/test/coloring/oracle_lemma3_14.lus
new file mode 100644
index 00000000..97b92162
--- /dev/null
+++ b/test/coloring/oracle_lemma3_14.lus
@@ -0,0 +1,22 @@
+-- Automatically generated by /home/nathan/.opam/4.07.0/bin/sasa version "2.5.0-1-g0c65445" ("0c65445")
+-- on Nathan-PC the 26/6/2019 at 16:18:58
+--sasa -glos ring.dot
+include "round.lus"
+
+const n=7;
+const m=1;
+const degree=0;
+const diameter=0;
+
+  
+node oracle(p1_conflict,p2_conflict,p3_conflict,p4_conflict,p5_conflict,p6_conflict,p7_conflict,Enab_p1_conflict,Enab_p2_conflict,Enab_p3_conflict,Enab_p4_conflict,Enab_p5_conflict,Enab_p6_conflict,Enab_p7_conflict:bool) returns (ok:bool;MoveNb:int);
+var
+  	Acti:bool^1^7;
+	Enab:bool^1^7;
+let
+  	Acti = [[p1_conflict],[p2_conflict],[p3_conflict],[p4_conflict],[p5_conflict],[p6_conflict],[p7_conflict]];
+
+  	Enab = [[Enab_p1_conflict],[Enab_p2_conflict],[Enab_p3_conflict],[Enab_p4_conflict],[Enab_p5_conflict],[Enab_p6_conflict],[Enab_p7_conflict]];
+  MoveNb =  compt_move(Acti);    
+  ok = MoveNb <= n-1;   -- from Lemma 3.14 page 29          
+tel
diff --git a/test/coloring/oracle_theorem3_17.lus b/test/coloring/oracle_theorem3_17.lus
new file mode 100644
index 00000000..aca17a7b
--- /dev/null
+++ b/test/coloring/oracle_theorem3_17.lus
@@ -0,0 +1,23 @@
+-- Automatically generated by /home/nathan/.opam/4.07.0/bin/sasa version "2.5.0-1-g0c65445" ("0c65445")
+-- on Nathan-PC the 26/6/2019 at 16:18:58
+--sasa -glos ring.dot
+include "round.lus"
+
+const n=7;
+const m=1;
+const degree=0;
+const diameter=0;
+
+  
+node oracle(p1_conflict,p2_conflict,p3_conflict,p4_conflict,p5_conflict,p6_conflict,p7_conflict,Enab_p1_conflict,Enab_p2_conflict,Enab_p3_conflict,Enab_p4_conflict,Enab_p5_conflict,Enab_p6_conflict,Enab_p7_conflict:bool) returns (ok,Round:bool;RoundNb:int);
+var
+        Acti:bool^1^7;
+        Enab:bool^1^7;
+let
+        Acti = [[p1_conflict],[p2_conflict],[p3_conflict],[p4_conflict],[p5_conflict],[p6_conflict],[p7_conflict]];
+
+        Enab = [[Enab_p1_conflict],[Enab_p2_conflict],[Enab_p3_conflict],[Enab_p4_conflict],[Enab_p5_conflict],[Enab_p6_conflict],[Enab_p7_conflict]];
+  Round = round <<m,n>>(Enab,Acti);
+  RoundNb = count(Round);
+  ok = RoundNb <= 1;   -- from Lemma 3.14 page 29          
+tel
diff --git a/test/coloring/round.lus b/test/coloring/round.lus
new file mode 100644
index 00000000..94dfbc6b
--- /dev/null
+++ b/test/coloring/round.lus
@@ -0,0 +1,132 @@
+-- -- Time-stamp: <modified the 26/06/2019 (at 15:13) by Erwan Jahier>
+--  
+-- Computing rounds in Lustre
+-- The inputs are 2 arrays Enab and Acti, where:
+--     - Enab[i][j] is true iff action i of process j is enabled
+--     - Acti[i][j] is true iff action i of process j is active
+ 
+-- n holds the number of processes
+-- m holds the number of actions per process
+node round<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
+var 
+  mask: bool^n;
+  pres: bool;
+let
+  pres = true -> pre res;
+  mask = merge pres (true  -> mask_init<<m, n>>  (Enab, Acti) when pres)
+                    (false -> mask_update<<m, n>>(Enab, Acti, pre mask) when not pres);       
+
+  res = boolred<<0,0,n>>(mask); -- when all are false, 
+tel
+
+node mask_init <<const m:int; const n:int>> (E,A: bool^m^n) returns (res : bool^n);
+var
+  enab:bool^n; -- at least one action is enabled
+  acti:bool^n; -- at least one action is active  
+let
+  enab = map<< red<<or, m>>, n >>(false^n, E);
+  acti = map<< red<<or, m>>, n >>(false^n, A);
+  res  = map<<not_implies, n>>(enab,acti);
+tel
+
+function not_implies(a,b:bool) returns (res:bool);
+let
+  res = not(a=>b);
+tel
+
+node mask_update<<const m: int; const n: int>> (E,A: bool^m^n; pmask:bool^n) returns (res : bool^n);
+var
+  acti:bool^n; -- at least one action is active
+let
+  acti = map<< red<<or, m>>, n >>(false^n, A);
+  res = map<<not_implies, n>>(pmask,acti);
+tel
+
+
+node test53=round<< 5,3 >>
+node test52=round<< 5,2 >>
+
+-----------------------------------------------------------------------------
+node count(x:bool) returns(cpt:int);
+let
+  cpt = 0 -> if x then pre cpt + 1 else pre cpt;
+tel
+-----------------------------------------------------------------------------
+
+node silent<<const m: int; const n: int>> (Enab: bool^m^n) returns (ok:bool);
+var
+  enab:bool^n; -- at least one action is enabled
+let
+  enab = map<< red<<or, m>>, n >>(false^n, Enab);
+  ok = not(red<<or, n>>(false, enab)); 
+tel
+
+-----------------------------------------------------------------------------
+node after_n(n:int; x:bool) returns (res:bool);
+var cpt:int;
+let
+  cpt = 0 -> pre cpt + 1;
+  res = cpt <= n or x;
+tel
+
+-----------------------------------------------------------------------------
+-----------------------------------------------------------------------------
+node bool_to_int(X:int; Y:bool) returns (Z:int);
+let
+  Z = if(Y) then X+1 else X;
+tel
+
+-----------------------------------------------------------------------------
+node map_and (X,Y:bool^m) returns (Z:bool^m);
+let
+  Z = map<<and,m>>(X,Y) ;
+tel 
+
+-----------------------------------------------------------------------------
+node implies_list(A,B:bool^m) returns (res:bool^m);
+let
+  res = map<<=>,m>>(A,B) ;
+tel
+
+-----------------------------------------------------------------------------
+node add_int_true(X:int; Y:bool^m) returns (Z:int);
+let
+  Z = red<<bool_to_int,m>>(X,Y);
+tel
+
+-----------------------------------------------------------------------------
+node one_true (tab:bool^m^n) returns (res:bool);
+let
+  res = (((red<<add_int_true,n>>(0,tab)))=1);
+tel
+
+-----------------------------------------------------------------------------
+node all_true (tab_acti:bool^m^n) returns (res:bool);
+let
+  res = boolred<<m,m,m>>((red<<map_and,n>>(true^m,tab_acti))) ;
+tel
+
+-----------------------------------------------------------------------------
+node compt_move (tab_acti:bool^m^n) returns (nb_act:int);
+let
+  nb_act = 0 -> pre(nb_act) + (red<<add_int_true,n>>(0,tab_acti));    
+tel
+
+-----------------------------------------------------------------------------
+node is_distributed(acti,enab:bool^m^n) returns (res:bool);
+let
+  res = true ->  (((red<<add_int_true,n>>(0,acti))>=1) or silent<<m,n>>(enab)) and pre(res);
+tel
+
+-----------------------------------------------------------------------------
+node is_central(acti:bool^m^n) returns (res:bool);
+let
+  res = true ->  (one_true(acti)) and pre(res);
+tel
+
+-----------------------------------------------------------------------------
+node is_synchronous(enab,acti:bool^m^n) returns (res:bool);
+let
+  res = true -> all_true(map<<implies_list,n>>(enab,acti)) and pre(res);
+tel
+
diff --git a/test/dijkstra-ring/Makefile b/test/dijkstra-ring/Makefile
index 388bbbf6..a1995f4e 100644
--- a/test/dijkstra-ring/Makefile
+++ b/test/dijkstra-ring/Makefile
@@ -1,8 +1,10 @@
 # Time-stamp: <modified the 07/06/2019 (at 10:05) by Erwan Jahier>
 
 
-test: cmxs 
-	$(sasa)  ring.dot 
+test: cmxs lurette1 
+	$(sasa) ring.dot
+
+
 cmxs: ring.cmxs ringroot.cmxs  ring.cma ringroot.cma
 
 sim2chrogtk: ring.rif
@@ -15,7 +17,25 @@ gnuplot: ring.rif
 rdbg: cmxs ring.lut
 	rdbg -o ring.rif  \
       -env "$(sasa) ring.dot -custd -rif" \
-      -sut-nd "lutin ring.lut -n distributed"
+      -sut-nd "lutin ring.lut -n distributed"\
+
+
+lurette1:cmxs ring.lut
+	lurette \
+      -env "$(sasa) ring.dot -custd " \
+      -sut "lutin ring.lut -n distributed" \
+
+lemma6.28:cmxs ring.lut
+	lurette \
+      -env "$(sasa) ring.dot -custd " \
+      -sut "lutin ring.lut -n distributed" \
+       -oracle "lv6 oracle_lemma6_28.lus -n oracle "
+
+theorem6.29:cmxs ring.lut
+	lurette \
+      -env "$(sasa) ring.dot -custd " \
+      -sut "lutin ring.lut -n distributed" \
+       -oracle "lv6 oracle_theorem6_29.lus -n oracle "
 
 
 -include ../Makefile.inc
diff --git a/test/dijkstra-ring/oracle_lemma6_28.lus b/test/dijkstra-ring/oracle_lemma6_28.lus
new file mode 100644
index 00000000..70cc3cb7
--- /dev/null
+++ b/test/dijkstra-ring/oracle_lemma6_28.lus
@@ -0,0 +1,24 @@
+-- Automatically generated by /home/nathan/.opam/4.07.0/bin/sasa version "2.5.0-1-g0c65445" ("0c65445")
+-- on Nathan-PC the 2/7/2019 at 11:24:08
+--sasa -glos ring.dot
+include "round.lus"
+
+const n=8;
+const m=1;
+const degree=0;
+const diameter=0;
+
+
+node oracle(p1_a,p2_a,p3_a,p4_a,p5_a,p6_a,p7_a,p8_a,Enab_p1_a,Enab_p2_a,Enab_p3_a,Enab_p4_a,Enab_p5_a,Enab_p6_a,Enab_p7_a,Enab_p8_a:bool) returns (ok,Silent:bool;MoveNb,Xn:int);
+var
+        Acti:bool^1^8;
+        Enab:bool^1^8;
+let
+        Acti = [[p1_a],[p2_a],[p3_a],[p4_a],[p5_a],[p6_a],[p7_a],[p8_a]];
+
+        Enab = [[Enab_p1_a],[Enab_p2_a],[Enab_p3_a],[Enab_p4_a],[Enab_p5_a],[Enab_p6_a],[Enab_p7_a],[Enab_p8_a]];
+  Xn = 0 -> if(Acti[0][0]) then pre(Xn) + 1 else pre(Xn) ;
+  Silent = silent<<m,n>>(Enab);
+  MoveNb =  compt_move(Acti);    
+  ok = (((n*(n-1)/2) + Xn*n)<MoveNb) => Silent ;  -- Lemma 6.28           
+tel
diff --git a/test/dijkstra-ring/oracle_theorem6_29.lus b/test/dijkstra-ring/oracle_theorem6_29.lus
new file mode 100644
index 00000000..c47d88b3
--- /dev/null
+++ b/test/dijkstra-ring/oracle_theorem6_29.lus
@@ -0,0 +1,24 @@
+-- Automatically generated by /home/nathan/.opam/4.07.0/bin/sasa version "2.5.0-1-g0c65445" ("0c65445")
+-- on Nathan-PC the 2/7/2019 at 11:24:08
+--sasa -glos ring.dot
+include "round.lus"
+
+const n=8;
+const m=1;
+const degree=0;
+const diameter=0;
+const k = 42;
+
+
+node oracle(p1_a,p2_a,p3_a,p4_a,p5_a,p6_a,p7_a,p8_a,Enab_p1_a,Enab_p2_a,Enab_p3_a,Enab_p4_a,Enab_p5_a,Enab_p6_a,Enab_p7_a,Enab_p8_a:bool) returns (ok,Silent:bool;MoveNb:int);
+var
+        Acti:bool^1^8;
+        Enab:bool^1^8;
+let
+        Acti = [[p1_a],[p2_a],[p3_a],[p4_a],[p5_a],[p6_a],[p7_a],[p8_a]];
+
+        Enab = [[Enab_p1_a],[Enab_p2_a],[Enab_p3_a],[Enab_p4_a],[Enab_p5_a],[Enab_p6_a],[Enab_p7_a],[Enab_p8_a]];
+  Silent = silent<<m,n>>(Enab);
+  MoveNb =  1 -> pre(MoveNb) + 1;
+  ok = (k>=n)=>((((3*n*(n-1))/2)<MoveNb)=>Silent) ; -- Theorem 6.29             
+tel
diff --git a/test/dijkstra-ring/round.lus b/test/dijkstra-ring/round.lus
new file mode 100644
index 00000000..94dfbc6b
--- /dev/null
+++ b/test/dijkstra-ring/round.lus
@@ -0,0 +1,132 @@
+-- -- Time-stamp: <modified the 26/06/2019 (at 15:13) by Erwan Jahier>
+--  
+-- Computing rounds in Lustre
+-- The inputs are 2 arrays Enab and Acti, where:
+--     - Enab[i][j] is true iff action i of process j is enabled
+--     - Acti[i][j] is true iff action i of process j is active
+ 
+-- n holds the number of processes
+-- m holds the number of actions per process
+node round<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
+var 
+  mask: bool^n;
+  pres: bool;
+let
+  pres = true -> pre res;
+  mask = merge pres (true  -> mask_init<<m, n>>  (Enab, Acti) when pres)
+                    (false -> mask_update<<m, n>>(Enab, Acti, pre mask) when not pres);       
+
+  res = boolred<<0,0,n>>(mask); -- when all are false, 
+tel
+
+node mask_init <<const m:int; const n:int>> (E,A: bool^m^n) returns (res : bool^n);
+var
+  enab:bool^n; -- at least one action is enabled
+  acti:bool^n; -- at least one action is active  
+let
+  enab = map<< red<<or, m>>, n >>(false^n, E);
+  acti = map<< red<<or, m>>, n >>(false^n, A);
+  res  = map<<not_implies, n>>(enab,acti);
+tel
+
+function not_implies(a,b:bool) returns (res:bool);
+let
+  res = not(a=>b);
+tel
+
+node mask_update<<const m: int; const n: int>> (E,A: bool^m^n; pmask:bool^n) returns (res : bool^n);
+var
+  acti:bool^n; -- at least one action is active
+let
+  acti = map<< red<<or, m>>, n >>(false^n, A);
+  res = map<<not_implies, n>>(pmask,acti);
+tel
+
+
+node test53=round<< 5,3 >>
+node test52=round<< 5,2 >>
+
+-----------------------------------------------------------------------------
+node count(x:bool) returns(cpt:int);
+let
+  cpt = 0 -> if x then pre cpt + 1 else pre cpt;
+tel
+-----------------------------------------------------------------------------
+
+node silent<<const m: int; const n: int>> (Enab: bool^m^n) returns (ok:bool);
+var
+  enab:bool^n; -- at least one action is enabled
+let
+  enab = map<< red<<or, m>>, n >>(false^n, Enab);
+  ok = not(red<<or, n>>(false, enab)); 
+tel
+
+-----------------------------------------------------------------------------
+node after_n(n:int; x:bool) returns (res:bool);
+var cpt:int;
+let
+  cpt = 0 -> pre cpt + 1;
+  res = cpt <= n or x;
+tel
+
+-----------------------------------------------------------------------------
+-----------------------------------------------------------------------------
+node bool_to_int(X:int; Y:bool) returns (Z:int);
+let
+  Z = if(Y) then X+1 else X;
+tel
+
+-----------------------------------------------------------------------------
+node map_and (X,Y:bool^m) returns (Z:bool^m);
+let
+  Z = map<<and,m>>(X,Y) ;
+tel 
+
+-----------------------------------------------------------------------------
+node implies_list(A,B:bool^m) returns (res:bool^m);
+let
+  res = map<<=>,m>>(A,B) ;
+tel
+
+-----------------------------------------------------------------------------
+node add_int_true(X:int; Y:bool^m) returns (Z:int);
+let
+  Z = red<<bool_to_int,m>>(X,Y);
+tel
+
+-----------------------------------------------------------------------------
+node one_true (tab:bool^m^n) returns (res:bool);
+let
+  res = (((red<<add_int_true,n>>(0,tab)))=1);
+tel
+
+-----------------------------------------------------------------------------
+node all_true (tab_acti:bool^m^n) returns (res:bool);
+let
+  res = boolred<<m,m,m>>((red<<map_and,n>>(true^m,tab_acti))) ;
+tel
+
+-----------------------------------------------------------------------------
+node compt_move (tab_acti:bool^m^n) returns (nb_act:int);
+let
+  nb_act = 0 -> pre(nb_act) + (red<<add_int_true,n>>(0,tab_acti));    
+tel
+
+-----------------------------------------------------------------------------
+node is_distributed(acti,enab:bool^m^n) returns (res:bool);
+let
+  res = true ->  (((red<<add_int_true,n>>(0,acti))>=1) or silent<<m,n>>(enab)) and pre(res);
+tel
+
+-----------------------------------------------------------------------------
+node is_central(acti:bool^m^n) returns (res:bool);
+let
+  res = true ->  (one_true(acti)) and pre(res);
+tel
+
+-----------------------------------------------------------------------------
+node is_synchronous(enab,acti:bool^m^n) returns (res:bool);
+let
+  res = true -> all_true(map<<implies_list,n>>(enab,acti)) and pre(res);
+tel
+
diff --git a/test/unison/Makefile b/test/unison/Makefile
index 59fa948c..a2ff818a 100644
--- a/test/unison/Makefile
+++ b/test/unison/Makefile
@@ -2,10 +2,10 @@
 
 test: test1 test2 lurette0
 
-test1: unison.cmxs 
+test1: unison.cmxs
 	$(sasa) -l 5 fig4.1.dot -sd  -rif
 
-test2: unison.cmxs 	
+test2: unison.cmxs
 	$(sasa) -l 50 ring.dot -rif
 
 sasaopt=-sd
@@ -14,23 +14,36 @@ cmxs: unison.cmxs unison.cma
 sim2chrogtk: ring.rif
 	sim2chrogtk -ecran -in $< > /dev/null
 
-gnuplot: ring.rif 
-	gnuplot-rif $< 
+gnuplot: ring.rif
+	gnuplot-rif $<
 
 luciole:
 	luciole-rif $(sasa) ring.dot -custd  -rif -ifi
 
+
 lurette0:cmxs ring.lut
 	lurette -o lurette.rif \
       -env "$(sasa) ring.dot -custd -rif" \
-      -sut "lutin ring.lut -n synchronous"  
+      -sut "lutin ring.lut -n synchronous" 
+
+lemma4_10:cmxs ring.lut
+	lurette -o lurette.rif \
+      -env "$(sasa) ring.dot -custd -rif" \
+      -sut "lutin ring.lut -n synchronous" \
+      -oracle "lv6 oracle_lemma4_10.lus -n oracle"
+
+theorem4_11:cmxs ring.lut
+	lurette -o lurette.rif \
+      -env "$(sasa) ring.dot -custd -rif" \
+      -sut "lutin ring.lut -n synchronous" \
+      -oracle "lv6 oracle_theorem4_11.lus -n oracle"
+
 
 lurette: lurette0 s g
 
-rdbg: unison.cma unison.cmxs ring.lut 
+rdbg: unison.cma unison.cmxs ring.lut
 	rdbg -o unison.rif  \
       -env "$(sasa) ring.dot -custd -rif" \
       -sut-nd "lutin ring.lut -n synchronous"
 
 -include ../Makefile.inc
-
diff --git a/test/unison/oracle_lemma4_10.lus b/test/unison/oracle_lemma4_10.lus
new file mode 100644
index 00000000..e14c4e42
--- /dev/null
+++ b/test/unison/oracle_lemma4_10.lus
@@ -0,0 +1,25 @@
+-- Automatically generated by /home/nathan/.opam/4.07.0/bin/sasa version "2.5.0-1-g0c65445" ("0c65445")
+-- on Nathan-PC the 27/6/2019 at 16:00:12
+--sasa -glos ring.dot
+-- 
+include "round.lus"
+
+const n=7;
+const m=1;
+const degree=0;
+const diameter=3;
+
+
+node oracle(p1_g,p2_g,p3_g,p4_g,p5_g,p6_g,p7_g,Enab_p1_g,Enab_p2_g,Enab_p3_g,Enab_p4_g,Enab_p5_g,Enab_p6_g,Enab_p7_g:bool) returns (ok:bool;nb_step:int;Silent,All_Acti:bool);
+var
+  	Acti:bool^1^7;
+	Enab:bool^1^7;
+let
+  	Acti = [[p1_g],[p2_g],[p3_g],[p4_g],[p5_g],[p6_g],[p7_g]];
+
+  	Enab = [[Enab_p1_g],[Enab_p2_g],[Enab_p3_g],[Enab_p4_g],[Enab_p5_g],[Enab_p6_g],[Enab_p7_g]];
+  nb_step = 0 -> pre nb_step + 1 ; 
+  Silent = silent<<m,n>>(Enab);
+  All_Acti = all_true(Acti);
+  ok = (nb_step>=((3*diameter)-2)) => All_Acti ; -- from Lemma 4.10 page 40
+tel
diff --git a/test/unison/oracle_theorem4_11.lus b/test/unison/oracle_theorem4_11.lus
new file mode 100644
index 00000000..55d85efa
--- /dev/null
+++ b/test/unison/oracle_theorem4_11.lus
@@ -0,0 +1,27 @@
+-- Automatically generated by /home/nathan/.opam/4.07.0/bin/sasa version "2.5.0-1-g0c65445" ("0c65445")
+-- on Nathan-PC the 27/6/2019 at 16:00:12
+--sasa -glos ring.dot
+-- 
+include "round.lus"
+
+const n=7;
+const m=1;
+const degree=0;
+const diameter=3;
+const max_clock =10 ;
+const is_connected = true; 
+
+
+
+node oracle(p1_g,p2_g,p3_g,p4_g,p5_g,p6_g,p7_g,Enab_p1_g,Enab_p2_g,Enab_p3_g,Enab_p4_g,Enab_p5_g,Enab_p6_g,Enab_p7_g:bool) returns (ok:bool;nb_step:int;All_Acti:bool);
+var
+        Acti:bool^1^7;
+        Enab:bool^1^7;
+let
+        Acti = [[p1_g],[p2_g],[p3_g],[p4_g],[p5_g],[p6_g],[p7_g]];
+
+        Enab = [[Enab_p1_g],[Enab_p2_g],[Enab_p3_g],[Enab_p4_g],[Enab_p5_g],[Enab_p6_g],[Enab_p7_g]];
+  nb_step = 1 -> pre(nb_step) + 1 ; 
+  All_Acti = all_true(Acti);
+  ok =((max_clock>= 5) and is_connected) => (nb_step>=(3*diameter-2)) => All_Acti  ; -- from Lemma 4.10 page 40
+tel
diff --git a/test/unison/round.lus b/test/unison/round.lus
new file mode 100644
index 00000000..94dfbc6b
--- /dev/null
+++ b/test/unison/round.lus
@@ -0,0 +1,132 @@
+-- -- Time-stamp: <modified the 26/06/2019 (at 15:13) by Erwan Jahier>
+--  
+-- Computing rounds in Lustre
+-- The inputs are 2 arrays Enab and Acti, where:
+--     - Enab[i][j] is true iff action i of process j is enabled
+--     - Acti[i][j] is true iff action i of process j is active
+ 
+-- n holds the number of processes
+-- m holds the number of actions per process
+node round<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
+var 
+  mask: bool^n;
+  pres: bool;
+let
+  pres = true -> pre res;
+  mask = merge pres (true  -> mask_init<<m, n>>  (Enab, Acti) when pres)
+                    (false -> mask_update<<m, n>>(Enab, Acti, pre mask) when not pres);       
+
+  res = boolred<<0,0,n>>(mask); -- when all are false, 
+tel
+
+node mask_init <<const m:int; const n:int>> (E,A: bool^m^n) returns (res : bool^n);
+var
+  enab:bool^n; -- at least one action is enabled
+  acti:bool^n; -- at least one action is active  
+let
+  enab = map<< red<<or, m>>, n >>(false^n, E);
+  acti = map<< red<<or, m>>, n >>(false^n, A);
+  res  = map<<not_implies, n>>(enab,acti);
+tel
+
+function not_implies(a,b:bool) returns (res:bool);
+let
+  res = not(a=>b);
+tel
+
+node mask_update<<const m: int; const n: int>> (E,A: bool^m^n; pmask:bool^n) returns (res : bool^n);
+var
+  acti:bool^n; -- at least one action is active
+let
+  acti = map<< red<<or, m>>, n >>(false^n, A);
+  res = map<<not_implies, n>>(pmask,acti);
+tel
+
+
+node test53=round<< 5,3 >>
+node test52=round<< 5,2 >>
+
+-----------------------------------------------------------------------------
+node count(x:bool) returns(cpt:int);
+let
+  cpt = 0 -> if x then pre cpt + 1 else pre cpt;
+tel
+-----------------------------------------------------------------------------
+
+node silent<<const m: int; const n: int>> (Enab: bool^m^n) returns (ok:bool);
+var
+  enab:bool^n; -- at least one action is enabled
+let
+  enab = map<< red<<or, m>>, n >>(false^n, Enab);
+  ok = not(red<<or, n>>(false, enab)); 
+tel
+
+-----------------------------------------------------------------------------
+node after_n(n:int; x:bool) returns (res:bool);
+var cpt:int;
+let
+  cpt = 0 -> pre cpt + 1;
+  res = cpt <= n or x;
+tel
+
+-----------------------------------------------------------------------------
+-----------------------------------------------------------------------------
+node bool_to_int(X:int; Y:bool) returns (Z:int);
+let
+  Z = if(Y) then X+1 else X;
+tel
+
+-----------------------------------------------------------------------------
+node map_and (X,Y:bool^m) returns (Z:bool^m);
+let
+  Z = map<<and,m>>(X,Y) ;
+tel 
+
+-----------------------------------------------------------------------------
+node implies_list(A,B:bool^m) returns (res:bool^m);
+let
+  res = map<<=>,m>>(A,B) ;
+tel
+
+-----------------------------------------------------------------------------
+node add_int_true(X:int; Y:bool^m) returns (Z:int);
+let
+  Z = red<<bool_to_int,m>>(X,Y);
+tel
+
+-----------------------------------------------------------------------------
+node one_true (tab:bool^m^n) returns (res:bool);
+let
+  res = (((red<<add_int_true,n>>(0,tab)))=1);
+tel
+
+-----------------------------------------------------------------------------
+node all_true (tab_acti:bool^m^n) returns (res:bool);
+let
+  res = boolred<<m,m,m>>((red<<map_and,n>>(true^m,tab_acti))) ;
+tel
+
+-----------------------------------------------------------------------------
+node compt_move (tab_acti:bool^m^n) returns (nb_act:int);
+let
+  nb_act = 0 -> pre(nb_act) + (red<<add_int_true,n>>(0,tab_acti));    
+tel
+
+-----------------------------------------------------------------------------
+node is_distributed(acti,enab:bool^m^n) returns (res:bool);
+let
+  res = true ->  (((red<<add_int_true,n>>(0,acti))>=1) or silent<<m,n>>(enab)) and pre(res);
+tel
+
+-----------------------------------------------------------------------------
+node is_central(acti:bool^m^n) returns (res:bool);
+let
+  res = true ->  (one_true(acti)) and pre(res);
+tel
+
+-----------------------------------------------------------------------------
+node is_synchronous(enab,acti:bool^m^n) returns (res:bool);
+let
+  res = true -> all_true(map<<implies_list,n>>(enab,acti)) and pre(res);
+tel
+
-- 
GitLab