From c530ae325831f3998395c133121eab2c9ffe79bf Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Tue, 9 Jul 2019 09:44:38 +0200
Subject: [PATCH] Test: add a missing file to fic the CI

---
 test/dijkstra-ring/dijkstra_ring_oracle.lus | 34 +++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 test/dijkstra-ring/dijkstra_ring_oracle.lus

diff --git a/test/dijkstra-ring/dijkstra_ring_oracle.lus b/test/dijkstra-ring/dijkstra_ring_oracle.lus
new file mode 100644
index 00000000..ef8f958b
--- /dev/null
+++ b/test/dijkstra-ring/dijkstra_ring_oracle.lus
@@ -0,0 +1,34 @@
+include "../lustre/oracle_utils.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
+
+-----------------------------------------------------------------------------
+node dijkstra_ring_oracle<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn) 
+returns (ok:bool);
+let
+  
+  ok = lemma_6_28  <<an,pn>> (Enab, Acti) and
+       theorem_6_29<<an,pn>> (Enab, Acti); 
+tel
-- 
GitLab