From 5609e280dd76af953363fc9c29b27b306585a7fc Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Wed, 23 Sep 2015 15:53:55 +0200
Subject: [PATCH] non-reg test: add assert to help lutin to generate sensible
stimuli.
---
test/should_work/CURRENT.lus | 1 +
test/should_work/PCOND.lus | 1 +
test/should_work/X.lus | 1 +
test/should_work/X2.lus | 1 +
test/should_work/X6.lus | 1 +
test/should_work/aa.lus | 4 ++--
test/should_work/bob.lus | 2 +-
test/should_work/ck2.lus | 1 +
test/should_work/ck3.lus | 2 ++
test/should_work/ck4.lus | 1 +
test/should_work/ck6.lus | 2 ++
test/should_work/ck7.lus | 1 +
test/should_work/clock1_2ms.lus | 1 +
test/should_work/clock_ite.lus | 1 +
test/should_work/filliter.lus | 1 +
test/should_work/hanane.lus | 1 +
test/should_work/lustre_test1_ok.lus | 2 ++
test/should_work/multiclock.lus | 1 +
test/should_work/onlyroll.lus | 2 +-
test/should_work/pack1.lus | 1 +
test/should_work/sincos.lus | 2 +-
test/should_work/testBoite.lus | 1 +
test/should_work/testCapt.lus | 1 +
test/should_work/testPilote.lus | 2 ++
test/should_work/zzz.lus | 2 +-
25 files changed, 30 insertions(+), 6 deletions(-)
diff --git a/test/should_work/CURRENT.lus b/test/should_work/CURRENT.lus
index 44edc791..54dbfbe2 100644
--- a/test/should_work/CURRENT.lus
+++ b/test/should_work/CURRENT.lus
@@ -1,6 +1,7 @@
node CURRENT(x: bool; y: bool)
returns (z: bool);
let
+ assert(x->true);
z = current(CURRENT_clk(x,y when x));
tel
diff --git a/test/should_work/PCOND.lus b/test/should_work/PCOND.lus
index 1cbf2f4b..acb0c9aa 100644
--- a/test/should_work/PCOND.lus
+++ b/test/should_work/PCOND.lus
@@ -14,6 +14,7 @@ var
hD_when_hC_when_h0 : bool when hC_when_h0;
let
assert((h0=true)->true);
+ assert((hC=true)->true);
assert((hD=true)->true);
hX = current(hX1);
diff --git a/test/should_work/X.lus b/test/should_work/X.lus
index 8a824698..833741f7 100644
--- a/test/should_work/X.lus
+++ b/test/should_work/X.lus
@@ -5,6 +5,7 @@ var
p_on_d:int when d;
let
+ assert(c->true);
d,m_on_c,p_on_d = X_clk(c, n when c);
m = current (m_on_c);
p = current (p_on_d);
diff --git a/test/should_work/X2.lus b/test/should_work/X2.lus
index 7c5153f4..743230c5 100644
--- a/test/should_work/X2.lus
+++ b/test/should_work/X2.lus
@@ -1,6 +1,7 @@
node X2 (b: bool; n: int)
returns (m: int);
let
+ assert(b->true);
m = 0 -> current(n when b);
tel
diff --git a/test/should_work/X6.lus b/test/should_work/X6.lus
index 48d5d6c3..b7c1cd1b 100644
--- a/test/should_work/X6.lus
+++ b/test/should_work/X6.lus
@@ -12,6 +12,7 @@ var
p1,u1 : int when b;
q1,r1: int when c1 ;
let
+ assert(b->true);
m,c1,d1,p1,u1,q1,r1= X6_clk(n,true->b);
c = current(c1);
d = current(current(d1));
diff --git a/test/should_work/aa.lus b/test/should_work/aa.lus
index 226c4276..e575740e 100644
--- a/test/should_work/aa.lus
+++ b/test/should_work/aa.lus
@@ -1,6 +1,6 @@
const m = 2;
const n = 2;
-node n_node_alias(i1:int; i2_0:int; i2_1:int) returns (o:int);
+function n_node_alias(i1:int; i2_0:int; i2_1:int) returns (o:int);
var
_acc1:int;
let
@@ -8,7 +8,7 @@ let
_acc1 = Lustre::plus(i1, i2_0);
tel
-- end of node n_node_alias
-node aa(a:int) returns (res:int);
+function aa(a:int) returns (res:int);
var
_acc1:int;
_v1_0:int;
diff --git a/test/should_work/bob.lus b/test/should_work/bob.lus
index 60a94d3d..95513fb2 100644
--- a/test/should_work/bob.lus
+++ b/test/should_work/bob.lus
@@ -1,7 +1,7 @@
node bob(i : bool ) returns (o : bool);
let
+ assert (i -> true) ;
o = current(bob_clk(true -> i));
- assert (true -> i <> pre(i)) ;
tel
diff --git a/test/should_work/ck2.lus b/test/should_work/ck2.lus
index 9d04932c..4f3857fc 100644
--- a/test/should_work/ck2.lus
+++ b/test/should_work/ck2.lus
@@ -5,6 +5,7 @@ var
d_on_c : bool when c;
let
+ assert(c->true);
d_on_c = d when c;
n = ck2_clk(c, d_on_c , e when d_on_c);
tel
diff --git a/test/should_work/ck3.lus b/test/should_work/ck3.lus
index 34dc16ca..3d61e1ba 100644
--- a/test/should_work/ck3.lus
+++ b/test/should_work/ck3.lus
@@ -3,6 +3,8 @@ returns (x: bool);
var
b_on_a : bool when a;
let
+ assert(a->true);
+ assert(b->true);
b_on_a = b when a;
x = ck3_clk(a,b when a, c when b_on_a);
tel
diff --git a/test/should_work/ck4.lus b/test/should_work/ck4.lus
index 5e58459a..ff51168a 100644
--- a/test/should_work/ck4.lus
+++ b/test/should_work/ck4.lus
@@ -1,6 +1,7 @@
node ck4 (a: int; b: bool)
returns (c: int);
let
+ assert(b->true);
c = ck4_clk(a when b, b);
tel
node ck4_clk (a: int when b; b: bool)
diff --git a/test/should_work/ck6.lus b/test/should_work/ck6.lus
index 7ec38b23..ec65ec44 100644
--- a/test/should_work/ck6.lus
+++ b/test/should_work/ck6.lus
@@ -4,6 +4,8 @@ var u,v,w: int when b;
x: int when cc;
cc: bool when b;
let
+ assert(b->true);
+
(u,v) = p(n when b);
(w,x) = N(cc, u, v);
cc = c when b;
diff --git a/test/should_work/ck7.lus b/test/should_work/ck7.lus
index cd0a839b..8c9aae28 100644
--- a/test/should_work/ck7.lus
+++ b/test/should_work/ck7.lus
@@ -3,6 +3,7 @@ returns(q:int; r: int);
var
r_on_a : int when a;
let
+ assert(a->true);
q,r_on_a = ck7_clk(a,m,n);
r = current (r_on_a);
tel
diff --git a/test/should_work/clock1_2ms.lus b/test/should_work/clock1_2ms.lus
index 1ebac921..068173b0 100644
--- a/test/should_work/clock1_2ms.lus
+++ b/test/should_work/clock1_2ms.lus
@@ -14,6 +14,7 @@ tel
node clock1_2ms_clk(dummy : bool)
returns (Clock1ms: bool; Clock2ms : bool when Clock1ms) ;
let
+ assert(Clock1ms->true);
Clock1ms = Clock1ms_node(dummy);
Clock2ms = Clock2ms_node(dummy when Clock1ms);
tel
diff --git a/test/should_work/clock_ite.lus b/test/should_work/clock_ite.lus
index a639db83..c5f43969 100644
--- a/test/should_work/clock_ite.lus
+++ b/test/should_work/clock_ite.lus
@@ -5,6 +5,7 @@ node clock_ite(a: bool; b: bool) returns (c: bool);
c_on_a: bool when a;
let
+ assert(a->true);
c_on_a = clock_ite_clk(a,b);
c = current(c_on_a);
tel
diff --git a/test/should_work/filliter.lus b/test/should_work/filliter.lus
index e29f7ff2..70ffe75c 100644
--- a/test/should_work/filliter.lus
+++ b/test/should_work/filliter.lus
@@ -20,6 +20,7 @@ node filliter(c: bool; i1, i2: int) returns (s1, s2: int^NBC);
var
s1_on_c,s2_on_c: int^NBC when c;
let
+ assert(c->true);
s1_on_c,s2_on_c = filliter_clk(c, i1 when c, i2 when c);
s1 = current (s1_on_c);
s2 = current (s2_on_c);
diff --git a/test/should_work/hanane.lus b/test/should_work/hanane.lus
index b34c689f..1222a187 100644
--- a/test/should_work/hanane.lus
+++ b/test/should_work/hanane.lus
@@ -12,6 +12,7 @@ const
node hanane(a1: bool; b1: string2d; c1: tabStruct)
returns (res: bool);
let
+ assert(a1->true);
res = current(hanane_clk(a1,b1 when a1, c1 when a1));
tel
node hanane_clk(a1: bool; b1: string2d when a1; c1: tabStruct when a1)
diff --git a/test/should_work/lustre_test1_ok.lus b/test/should_work/lustre_test1_ok.lus
index cc56889c..9c5d457c 100644
--- a/test/should_work/lustre_test1_ok.lus
+++ b/test/should_work/lustre_test1_ok.lus
@@ -14,6 +14,8 @@ node lustre_test1_ok
returns (out1:real;Out2:real;Out3:real);
let
+ assert(cl1_2->true);
+ assert(cl1_4->true);
out1, Out2, Out3 = lustre_test1_ok_clk(In1,cl1_2,cl1_4, In2,cl2_6 when cl1_2, In3 when cl1_4);
tel
diff --git a/test/should_work/multiclock.lus b/test/should_work/multiclock.lus
index 814062a0..44dfaaf3 100644
--- a/test/should_work/multiclock.lus
+++ b/test/should_work/multiclock.lus
@@ -2,6 +2,7 @@ node multiclock ( x, y: int; c: bool; z: int )
returns ( s: int);
let
+ assert(c->true);
s = current(multiclock_clk ( x, y, c, z when c ));
tel
diff --git a/test/should_work/onlyroll.lus b/test/should_work/onlyroll.lus
index 8df4aeb3..4de90c7f 100644
--- a/test/should_work/onlyroll.lus
+++ b/test/should_work/onlyroll.lus
@@ -532,7 +532,7 @@ tel
node Average2(a, b: real) returns (z : real);
let
- z = (a+b)/2.0 ;
+ z = (a+b) / 2.0 ;
tel
diff --git a/test/should_work/pack1.lus b/test/should_work/pack1.lus
index 0a0410ec..372fd326 100644
--- a/test/should_work/pack1.lus
+++ b/test/should_work/pack1.lus
@@ -18,6 +18,7 @@ tel
node pack1(ck : bool; in : int) returns (out : int when ck);
let
+ assert(ck->true);
out = in when ck;
tel
diff --git a/test/should_work/sincos.lus b/test/should_work/sincos.lus
index ed8b0d80..2b113188 100644
--- a/test/should_work/sincos.lus
+++ b/test/should_work/sincos.lus
@@ -1,5 +1,5 @@
--
-node sincos(omega:real) returns (sin, cos: real);
+node sincos(omega : real) returns (sin, cos: real);
var pcos,psin: real;
let
pcos = 1.0 fby cos;
diff --git a/test/should_work/testBoite.lus b/test/should_work/testBoite.lus
index beb50ee1..d04de6a4 100644
--- a/test/should_work/testBoite.lus
+++ b/test/should_work/testBoite.lus
@@ -29,6 +29,7 @@ var localData_clock : bool;
localData : int when localData_clock;
-- pLocalData : int;
let
+ assert(localData_clock->true);
localData_clock = (dataPUT and (not dataGET))
-> (dataPUT and (not dataGET))
or (pre(localData_clock) and not(dataGET));
diff --git a/test/should_work/testCapt.lus b/test/should_work/testCapt.lus
index 7a171ba4..d1eae2a0 100644
--- a/test/should_work/testCapt.lus
+++ b/test/should_work/testCapt.lus
@@ -21,6 +21,7 @@ returns (dataPUT : bool;
var localCnt : int;
-- indCountTab : bool^10;
let
+ assert(Hcapt->true);
--recherche d'un indice libre
--for (localCnt=0;indCountTab[localCnt]=true,localCnt);
-- localCnt = 0 -> if Hcapt
diff --git a/test/should_work/testPilote.lus b/test/should_work/testPilote.lus
index 9e928651..73503861 100644
--- a/test/should_work/testPilote.lus
+++ b/test/should_work/testPilote.lus
@@ -30,6 +30,8 @@ returns (--semMemTakeP,
var localData : int when ckLocalData;
ckLocalData : bool;
let
+ assert(HupdatePiloteData->true);
+
dataGET = Hpilote;
ckLocalData = false -> true;
diff --git a/test/should_work/zzz.lus b/test/should_work/zzz.lus
index 99b35310..5224b12b 100644
--- a/test/should_work/zzz.lus
+++ b/test/should_work/zzz.lus
@@ -1,5 +1,5 @@
type A_int_2 = int^2;
-node zzz(i1:int; i2:A_int_2) returns (o:int);
+function zzz(i1:int; i2:A_int_2) returns (o:int);
var
_acc1:int;
let
--
GitLab