From 7befc1db16412b94431e5669dccf052a4521e1e2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nathan=20R=C3=A9biscoul?= <nathan.rebiscoul38@gmail.com>
Date: Fri, 5 Jul 2019 23:34:29 +0200
Subject: [PATCH] Add all correction for merge request. Except the internal
demon matter
---
.../bfs_spanning_tree_oracle.lus | 47 +++++++++++++++++++
.../fig5.1-noinit_oracle.lus | 9 ++--
test/bfs-spanning-tree/oracle_lemma5_16.lus | 25 ++--------
test/coloring/coloring_oracle.lus | 24 ++++++++++
test/coloring/oracle_lemma3_14.lus | 11 ++---
test/coloring/oracle_theorem3_17.lus | 12 ++---
test/dijkstra-ring/dijkstra_ring.lus | 25 ++++++++++
test/dijkstra-ring/oracle_lemma6_28.lus | 14 ++----
test/dijkstra-ring/oracle_theorem6_29.lus | 13 ++---
test/lustre/round.lus | 33 +++++++------
test/unison/oracle_lemma4_10.lus | 14 ++----
test/unison/oracle_theorem4_11.lus | 14 ++----
test/unison/unison_oracle.lus | 28 +++++++++++
13 files changed, 175 insertions(+), 94 deletions(-)
create mode 100644 test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
create mode 100644 test/coloring/coloring_oracle.lus
create mode 100644 test/dijkstra-ring/dijkstra_ring.lus
create mode 100644 test/unison/unison_oracle.lus
diff --git a/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
new file mode 100644
index 00000000..fb0fa03f
--- /dev/null
+++ b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
@@ -0,0 +1,47 @@
+include "../lustre/round.lus"
+
+
+
+-----------------------------------------------------------------------------
+
+function first_element (X:bool^m) returns (res:bool);
+let
+ res = X[0];
+tel
+function first_column (X:bool^m^n) returns (Z:bool^n);
+let
+ Z = map<<first_element,n>>(X);
+tel
+function all_CD_are_false (tab_enab:bool^m^n) returns (res:bool);
+let
+ res = not (red<<or,n>>(false,first_column(tab_enab))) ;
+tel
+
+
+
+
+node lemma_5_16<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
+var
+ Round:bool;
+ RoundNb:int;
+ CD_disable:bool;
+let
+ Round = round <<m,n>>(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 m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
+var
+ Round:bool;
+ RoundNb:int;
+ Silent:bool;
+let
+ Round = round <<m,n>>(Enab,Acti);
+ RoundNb = count(Round);
+ Silent = silent<<m,n>>(Enab);
+ res = (RoundNb>=diameter+2) => Silent ; -- from theorem 5.18 page 57
+tel
diff --git a/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus b/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus
index 93b8643a..285de9c6 100644
--- a/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus
+++ b/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus
@@ -1,5 +1,5 @@
-include "round.lus"
+include "bfs_spanning_tree_oracle.lus"
const n=8;
const m=2;
@@ -12,7 +12,7 @@ node oracle(root_CD,root_CP,p1_CD,p1_CP,p2_CD,p2_CP,p3_CD,p3_CP,p4_CD,p4_CP,p5_C
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, Silent:bool; RoundNb:int);
+returns (ok:bool);
var
Acti:bool^2^8;
Enab:bool^2^8;
@@ -24,8 +24,5 @@ let
[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);
- Silent = silent<<m,n>>(Enab);
- ok = (RoundNb>=diameter+2) => Silent ; -- from theorem 5.18 page 57
+ ok = theorem_5_18<<m,n>>(Enab,Acti); -- 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
index ff53296a..e1f1cd21 100644
--- a/test/bfs-spanning-tree/oracle_lemma5_16.lus
+++ b/test/bfs-spanning-tree/oracle_lemma5_16.lus
@@ -1,27 +1,13 @@
--- 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"
+include "bfs_spanning_tree_oracle.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);
+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;
@@ -30,9 +16,6 @@ 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 !
+
+ ok = lemma_5_16<<m,n>>(Enab,Acti) ;
tel
diff --git a/test/coloring/coloring_oracle.lus b/test/coloring/coloring_oracle.lus
new file mode 100644
index 00000000..b85f5c69
--- /dev/null
+++ b/test/coloring/coloring_oracle.lus
@@ -0,0 +1,24 @@
+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
diff --git a/test/coloring/oracle_lemma3_14.lus b/test/coloring/oracle_lemma3_14.lus
index 97b92162..30ed692c 100644
--- a/test/coloring/oracle_lemma3_14.lus
+++ b/test/coloring/oracle_lemma3_14.lus
@@ -1,7 +1,5 @@
--- 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"
+
+include "coloring_oracle.lus"
const n=7;
const m=1;
@@ -9,7 +7,7 @@ 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);
+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;
@@ -17,6 +15,5 @@ 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
+ ok = lemma_3_14<<m,n>>(Enab,Acti); -- from Lemma 3.14 page 29
tel
diff --git a/test/coloring/oracle_theorem3_17.lus b/test/coloring/oracle_theorem3_17.lus
index aca17a7b..dcd87e70 100644
--- a/test/coloring/oracle_theorem3_17.lus
+++ b/test/coloring/oracle_theorem3_17.lus
@@ -1,7 +1,5 @@
--- 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"
+
+include "coloring_oracle.lus"
const n=7;
const m=1;
@@ -9,7 +7,7 @@ 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);
+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;
@@ -17,7 +15,5 @@ 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
+ ok = theorem_3_17<<m,n>>(Enab,Acti); -- from theorem 3.17
tel
diff --git a/test/dijkstra-ring/dijkstra_ring.lus b/test/dijkstra-ring/dijkstra_ring.lus
new file mode 100644
index 00000000..3dfb0fc7
--- /dev/null
+++ b/test/dijkstra-ring/dijkstra_ring.lus
@@ -0,0 +1,25 @@
+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
diff --git a/test/dijkstra-ring/oracle_lemma6_28.lus b/test/dijkstra-ring/oracle_lemma6_28.lus
index 70cc3cb7..1a3645da 100644
--- a/test/dijkstra-ring/oracle_lemma6_28.lus
+++ b/test/dijkstra-ring/oracle_lemma6_28.lus
@@ -1,7 +1,5 @@
--- 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"
+
+include "dijkstra_ring.lus"
const n=8;
const m=1;
@@ -9,7 +7,7 @@ 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);
+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;
@@ -17,8 +15,6 @@ 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
+
+ ok = lemma_6_28<<m,n>>(Enab,Acti) ; -- Lemma 6.28
tel
diff --git a/test/dijkstra-ring/oracle_theorem6_29.lus b/test/dijkstra-ring/oracle_theorem6_29.lus
index c47d88b3..8d7c8e37 100644
--- a/test/dijkstra-ring/oracle_theorem6_29.lus
+++ b/test/dijkstra-ring/oracle_theorem6_29.lus
@@ -1,7 +1,5 @@
--- 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"
+
+include "dijkstra_ring.lus"
const n=8;
const m=1;
@@ -10,7 +8,7 @@ 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);
+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;
@@ -18,7 +16,6 @@ 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
+
+ ok = theorem_6_29<<m,n>>(Enab,Acti) ; -- Theorem 6.29
tel
diff --git a/test/lustre/round.lus b/test/lustre/round.lus
index 94dfbc6b..a52bd635 100644
--- a/test/lustre/round.lus
+++ b/test/lustre/round.lus
@@ -71,9 +71,15 @@ tel
-----------------------------------------------------------------------------
-----------------------------------------------------------------------------
-node bool_to_int(X:int; Y:bool) returns (Z:int);
+function add_one_if_true(i:int;Y:bool) returns (res:int);
let
- Z = if(Y) then X+1 else X;
+ res= if Y then i+1 else i;
+tel
+
+-----------------------------------------------------------------------------
+function count_true<<const m:int>>(Acc:int;Y:bool^m) returns (Z:int);
+let
+ Z=red<<add_one_if_true,m>>(Acc,Y);
tel
-----------------------------------------------------------------------------
@@ -88,16 +94,10 @@ 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);
+ res = (((red<<count_true<<m>>,n>>(0,tab)))=1);
tel
-----------------------------------------------------------------------------
@@ -107,26 +107,29 @@ let
tel
-----------------------------------------------------------------------------
-node compt_move (tab_acti:bool^m^n) returns (nb_act:int);
+node move_count (tab_acti:bool^m^n) returns (nb_act:int);
let
- nb_act = 0 -> pre(nb_act) + (red<<add_int_true,n>>(0,tab_acti));
+ nb_act = 0 -> pre(nb_act) + (red<<count_true<<m>>,n>>(0,tab_acti));
tel
-----------------------------------------------------------------------------
-node is_distributed(acti,enab:bool^m^n) returns (res:bool);
+node is_distributed<<const m : int; const n: int>> (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);
+ res = true -> (((red<<count_true<<m>>,n>>(0,acti))>=1) or silent<<m,n>>(enab)) and pre(res);
tel
-----------------------------------------------------------------------------
-node is_central(acti:bool^m^n) returns (res:bool);
+node is_central <<const m : int; const n: int>> (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);
+node is_synchronous <<const m : int; const n: int>> (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/oracle_lemma4_10.lus b/test/unison/oracle_lemma4_10.lus
index e14c4e42..0f309c88 100644
--- a/test/unison/oracle_lemma4_10.lus
+++ b/test/unison/oracle_lemma4_10.lus
@@ -1,8 +1,4 @@
--- 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"
+include "unison_oracle.lus"
const n=7;
const m=1;
@@ -10,7 +6,7 @@ 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);
+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;
@@ -18,8 +14,6 @@ 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
+
+ ok = lemma_4_10<<m,n>>(Enab,Acti) ; -- from Lemma 4.10 page 40
tel
diff --git a/test/unison/oracle_theorem4_11.lus b/test/unison/oracle_theorem4_11.lus
index 55d85efa..b957e9aa 100644
--- a/test/unison/oracle_theorem4_11.lus
+++ b/test/unison/oracle_theorem4_11.lus
@@ -1,19 +1,15 @@
--- 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"
+include "unison_oracle.lus"
const n=7;
const m=1;
const degree=0;
const diameter=3;
const max_clock =10 ;
-const is_connected = true;
+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);
+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;
@@ -21,7 +17,5 @@ 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
+ ok = theorem_4_11<<m,n>>(Enab,Acti,is_connected,max_clock); -- from theorem 4.11 page 40
tel
diff --git a/test/unison/unison_oracle.lus b/test/unison/unison_oracle.lus
new file mode 100644
index 00000000..f6b98e29
--- /dev/null
+++ b/test/unison/unison_oracle.lus
@@ -0,0 +1,28 @@
+include "../lustre/round.lus"
+
+
+-----------------------------------------------------------------------------
+
+node theorem_4_11<<const m : int; const n: int>> (Enab, Acti: bool^m^n;is_connected:bool;max_clock:int) returns (res:bool);
+var
+ nb_step:int;
+ All_Acti:bool;
+let
+ nb_step = 1 -> pre(nb_step) + 1 ;
+ All_Acti = all_true(Acti);
+ res =((max_clock>= (2*diameter-1)) and is_connected) => (nb_step>=(3*diameter-2)) => All_Acti ; -- Theorem 4.11 page 40
+tel
+
+-----------------------------------------------------------------------------
+
+node lemma_4_10<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
+var
+ nb_step:int;
+ All_Acti:bool;
+ Silent:bool;
+let
+ nb_step = 0 -> pre nb_step + 1 ;
+ Silent = silent<<m,n>>(Enab);
+ All_Acti = all_true(Acti);
+ res = (nb_step>=((3*diameter)-2)) => All_Acti ; -- from Lemma 4.10 page 40
+tel
\ No newline at end of file
--
GitLab