Test: merge !8 (close #11)

test/bfs-spanning-tree/Makefile

@@ -36,6 +36,13 @@ lurette1:cmxs fig5.1.lut fig5.1_oracle.lus
       -env "$(sasa) fig5.1.dot -dd -rif" \
 		-oracle "lv6 fig5.1_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

test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus

-
-include "round.lus"
+include "../lustre/oracle_utils.lus"
 
 node bfs_spanning_tree_oracle<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn) 
 returns (ok:bool);
+let
+  
+  ok = lemma_5_16  <<an,pn>> (Enab, Acti) and
+       theorem_5_18<<an,pn>> (Enab, Acti); 
+tel
+
+function first_element<<const an : int>> (X:bool^an) returns (res:bool);
+let
+   res = X[0];
+tel 
+function first_column<<const an : int; const pn: int>>(X:bool^an^pn) returns (Z:bool^pn);
+let
+   Z = map<<first_element<<an>>,pn>>(X); 
+tel
+function all_CD_are_false (tab_enab:bool^an^pn) returns (res:bool);
+let
+  res = not (red<<or,pn>>(false,first_column(tab_enab))) ;
+tel
+
+node lemma_5_16<<const an : int; const pn: int>> (Enab, Acti: bool^an^pn) 
+returns (res:bool);
+var
+  Round:bool;
+  RoundNb:int;
+  CD_disable:bool;
+let 
+  Round = round <<an,pn>>(Enab,Acti);
+  RoundNb = count(Round); 
+  CD_disable = all_CD_are_false(Enab); 
+  res = (RoundNb>=diameter+1) => CD_disable ; -- Lemma 5.16 ! 
+tel
+
+-----------------------------------------------------------------------------
+node theorem_5_18<<const an : int; const pn: int>> (Enab, Acti: bool^an^pn) 
+returns (res:bool);
 var
-  Round, Silent:bool;  
+  Round:bool;
   RoundNb:int;
+  Silent:bool;
 let
-  Silent = silent<<an,pn>>(Enab);
-  Round  = round <<an,pn>>(Enab,Acti);
+  Round = round <<an,pn>>(Enab,Acti);
   RoundNb = count(Round); 
-  ok = (RoundNb>=diameter+2) => Silent; -- from theorem 5.18 page 57
+  Silent = silent<<an,pn>>(Enab);
+  res = (RoundNb>=diameter+2) => Silent ; -- from theorem 5.18 page 57
 tel

test/bfs-spanning-tree/fig5.1-noinit_oracle.lus

+
+include "bfs_spanning_tree_oracle.lus"
+
+const n=8;
+const m=2;
+const degree=2;
+const diameter=8;
+
+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:bool);
+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]];
+
+  ok = theorem_5_18<<m,n>>(Enab,Acti); -- from theorem 5.18 page 57
+tel

test/bfs-spanning-tree/oracle_lemma5_16.lus

+include "bfs_spanning_tree_oracle.lus"
+
+const n=8;
+const m=2;
+const degree=2;
+const diameter=4;
+
+
+
+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:bool;);
+
+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]];
+ 
+ ok = lemma_5_16<<m,n>>(Enab,Acti) ;            
+tel

test/coloring/Makefile

@@ -2,7 +2,7 @@
 
 
 test: p.cmxs ring.lut lurette
-	$(sasa) -l 200 ring.dot 
+	$(sasa) -l 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

test/coloring/coloring_oracle.lus

+include "../lustre/round.lus"
+
+
+-----------------------------------------------------------------------------
+
+node lemma_3_14<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
+var 
+  MoveNb:int;
+let
+  MoveNb =  move_count(Acti);
+  res =  MoveNb <= n-1;
+tel
+
+-----------------------------------------------------------------------------
+
+node theorem_3_17<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
+var
+  Round:bool;
+  RoundNb:int;
+let
+  Round = round <<m,n>>(Enab,Acti);
+  RoundNb = count(Round);
+  res = RoundNb <= 1;   -- from theorem 3.17 page 29          
+tel

test/coloring/oracle_lemma3_14.lus

+
+include "coloring_oracle.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);
+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]];
+  ok = lemma_3_14<<m,n>>(Enab,Acti);   -- from Lemma 3.14 page 29          
+tel

test/coloring/oracle_theorem3_17.lus

+
+include "coloring_oracle.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);
+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]];
+  ok = theorem_3_17<<m,n>>(Enab,Acti);  -- from theorem 3.17           
+tel

test/coloring/round.lus

+-- -- 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 count_true_acc(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<<count_true_acc,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<<count_true_acc,n>>(0,tab_acti));    
+tel
+
+-----------------------------------------------------------------------------
+node is_distributed(acti,enab:bool^m^n) returns (res:bool);
+let
+  res = true ->  (((red<<count_true_acc,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
+

test/dijkstra-ring/Makefile

 # 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

test/dijkstra-ring/dijkstra_ring.lus

+include "../lustre/round.lus"
+
+node theorem_6_29<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
+var
+  Silent:bool;
+  MoveNb:int ;
+let
+  Silent = silent<<m,n>>(Enab);
+  MoveNb =  1 -> pre(MoveNb) + 1;
+  res = (k>=n)=>((((3*n*(n-1))/2)<MoveNb)=>Silent) ; -- Theorem 6.29      
+tel
+
+-----------------------------------------------------------------------------
+
+node lemma_6_28<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
+var
+  Xn:int;
+  Silent:bool;
+  MoveNb:int;
+let
+  Xn = 0 -> if(Acti[0][0]) then pre(Xn) + 1 else pre(Xn) ;
+  Silent = silent<<m,n>>(Enab);
+  MoveNb =  move_count(Acti);    
+  res = (((n*(n-1)/2) + Xn*n)<MoveNb) => Silent ;  -- Lemma 6.28     
+tel
\ No newline at end of file

test/dijkstra-ring/oracle_lemma6_28.lus

+
+include "dijkstra_ring.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:bool);
+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]];
+    
+  ok = lemma_6_28<<m,n>>(Enab,Acti) ;  -- Lemma 6.28           
+tel

test/dijkstra-ring/oracle_theorem6_29.lus

+
+include "dijkstra_ring.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:bool);
+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]];
+
+   ok = theorem_6_29<<m,n>>(Enab,Acti) ; -- Theorem 6.29             
+tel

test/dijkstra-ring/round.lus

+-- -- 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
+

test/lustre/demon.lus

+
+node is_distributed<<const an : int; const pn: int>> (acti,enab:bool^an^pn) 
+returns (res:bool);
+let
+  res = true ->
+    pre(res) and (((red<<count_true_acc<<an>>,n>>(0,acti))>=1) or silent<<an,n>>(enab));
+tel
+
+-----------------------------------------------------------------------------
+node is_central <<const an : int; const pn: int>> (acti:bool^an^pn) returns (res:bool);
+let
+  res = true -> pre(res) and one_true(acti)  ;
+tel
+
+-----------------------------------------------------------------------------
+node is_synchronous <<const an : int; const pn: int>> (enab,acti:bool^an^pn) 
+returns (res:bool);
+let
+  res = true -> pre(res) and all_true(map<<implies_list,n>>(enab,acti));
+tel

test/lustre/oracle_utils.lus

+include "round.lus"
+include "demon.lus"
+include "utils.lus"
+
+
+-----------------------------------------------------------------------------
+-- An algo is silent when no action is enable
+node silent<<const an: int; const pn: int>> (Enab: bool^an^pn) returns (ok:bool);
+var
+  enab:bool^pn; -- at least one action is enabled
+let
+  enab = map<< red<<or, an>>, pn >>(false^pn, Enab);
+  ok = not(red<<or, pn>>(false, enab)); 
+tel
+
+-----------------------------------------------------------------------------
+node move_count (tab_acti:bool^an^pn) returns (nb_act:int);
+let
+  nb_act = 0 -> pre(nb_act) + (red<<count_true_acc<<an>>,pn>>(0,tab_acti));    
+tel
+
+
+

test/lustre/round.lus

--- -- Time-stamp: <modified the 05/07/2019 (at 11:34) by Erwan Jahier>
+-- -- Time-stamp: <modified the 08/07/2019 (at 15:28) by Erwan Jahier>
 --  
 -- Computing rounds in Lustre
 -- The inputs are 2 arrays Enab and Acti, where:
@@ -7,25 +7,26 @@
  
 -- 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);
+node round<<const an : int; const pn: int>> (Enab, Acti: bool^an^pn) returns (res:bool);
 var 
-  mask: bool^n;
+  mask: bool^pn;
   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, 
+  mask = merge pres (true  -> mask_init<<an, pn>>  (Enab, Acti) when pres)
+                    (false -> mask_update<<an, pn>>(Enab, Acti, pre mask) when not pres);
+
+  res = boolred<<0,0,pn>>(mask); -- when all are false, 
 tel
 
-function mask_init <<const m:int; const n:int>> (E,A: bool^m^n) returns (res : bool^n);
+node mask_init <<const an:int; const pn:int>> (E,A: bool^an^pn) returns (res : bool^pn);
 var
-  enab:bool^n; -- at least one action is enabled
-  acti:bool^n; -- at least one action is active  
+  enab:bool^pn; -- at least one action is enabled
+  acti:bool^pn; -- 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);
+  enab = map<< red<<or, an>>, pn >>(false^pn, E);
+  acti = map<< red<<or, an>>, pn >>(false^pn, A);
+  res  = map<<not_implies, pn>>(enab,acti);
 tel
 
 function not_implies(a,b:bool) returns (res:bool);
@@ -33,38 +34,15 @@ let
   res = not(a=>b);
 tel
 
-function mask_update<<const m: int; const n: int>> (E,A: bool^m^n; pmask:bool^n)
-returns (res : bool^n);
+node mask_update<<const an: int; const pn: int>> (E,A: bool^an^pn; pmask:bool^pn) 
+returns (res : bool^pn);
 var
-  acti:bool^n; -- at least one action is active
+  acti:bool^pn; -- at least one action is active
 let
-  acti = map<< red<<or, m>>, n >>(false^n, A);
-  res = map<<not_implies, n>>(pmask,acti);
+  acti = map<< red<<or, an>>, pn >>(false^pn, A);
+  res = map<<not_implies, pn>>(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
------------------------------------------------------------------------------
-
-function 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

test/lustre/utils.lus

+-- Various nodes that are not specific to sasa 
+
+-----------------------------------------------------------------------------
+node count(x:bool) returns(cpt:int);
+let
+  cpt = 0 -> if x then pre cpt + 1 else pre cpt;
+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
+
+-----------------------------------------------------------------------------
+function add_one_if_true(i:int;Y:bool) returns (res:int);
+let
+  res= if Y then i+1 else i;
+tel
+
+function count_true_acc<<const n:int>>(Acc:int;Y:bool^n) returns (Z:int);
+let
+  Z=red<<add_one_if_true, n>>(Acc,Y);
+tel
+
+-----------------------------------------------------------------------------
+node map_and<<const n:int>> (X,Y:bool^n) returns (Z:bool^n);
+let
+  Z = map<<and,n>>(X,Y) ;
+tel 
+
+-----------------------------------------------------------------------------
+node implies_list(A,B:bool^m) returns (res:bool^m);
+let
+  res = map<<=>,an>>(A,B) ;
+tel
+
+-----------------------------------------------------------------------------
+node one_true (tab:bool^an^pn) returns (res:bool);
+let
+  res = (((red<<count_true_acc<<an>>,pn>>(0,tab)))=1);
+tel
+
+-----------------------------------------------------------------------------
+node all_true (t:bool^m^n) returns (res:bool);
+let
+  res = boolred<<m,m,m>>((red<<map_and<<m>>,n>>(true^m,t))) ;
+tel
+
+node all_false (t:bool^m^n) returns (res:bool);
+let
+  res = boolred<<0,0,m>>((red<<map_or<<m>>,n>>(false^m,t))) ;
+tel

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
-

test/unison/oracle_lemma4_10.lus

+include "unison_oracle.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);
+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]];
+
+  ok = lemma_4_10<<m,n>>(Enab,Acti) ; -- from Lemma 4.10 page 40
+tel