summaryrefslogtreecommitdiff
path: root/tests/source
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-01 15:42:57 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-01 15:42:57 +0200
commitf97a886970bef9e1d6e8a1e217732d6ef8be087e (patch)
treef79d165af76f23fece80c5bcc5003d5e2b82bd38 /tests/source
parent2d322a06b882542bab3d98cf08abefa906a54942 (diff)
downloadscade-analyzer-f97a886970bef9e1d6e8a1e217732d6ef8be087e.tar.gz
scade-analyzer-f97a886970bef9e1d6e8a1e217732d6ef8be087e.zip
Adapt for real type with Apron ; not very efficient ATM.
Diffstat (limited to 'tests/source')
-rw-r--r--tests/source/cosinus.scade19
-rw-r--r--tests/source/rfollow.scade27
2 files changed, 46 insertions, 0 deletions
diff --git a/tests/source/cosinus.scade b/tests/source/cosinus.scade
new file mode 100644
index 0000000..a1596c2
--- /dev/null
+++ b/tests/source/cosinus.scade
@@ -0,0 +1,19 @@
+const dt: real = 0.1;
+
+node integrator(first: real; v: real; dt: real) returns (probe i: real)
+let
+ i = (first -> pre i) + (dt * v);
+tel
+
+node test(i: int) returns (a, b, c: int; exit: bool)
+var
+ probe cos, probe cosprime: real;
+let
+ cosprime = integrator(1.0, 0. -> pre (-cos), dt);
+ cos = integrator(0., cosprime, dt);
+ a = int(cos * 1000.);
+ b = int(cosprime * 1000.);
+ c = int(-cos * 1000.);
+ exit = (i > 8000);
+tel
+
diff --git a/tests/source/rfollow.scade b/tests/source/rfollow.scade
new file mode 100644
index 0000000..6ee1558
--- /dev/null
+++ b/tests/source/rfollow.scade
@@ -0,0 +1,27 @@
+node follow(a: real) returns (probe f: real)
+var
+ probe pf: real;
+let
+ assume h1: a >= 0. and a <= 1.;
+ guarantee g1: f >= 0. and f <= 1.;
+ guarantee g2: pf >= 0. and pf <= 1.;
+
+ pf = 0. -> pre f;
+ f = (pf + a) / 2.0;
+
+tel
+
+
+node test(i: int) returns (a, b, c: int; exit: bool)
+var
+ probe u, v: real;
+let
+ u = real(i mod 10) / 10.;
+ v = follow(u);
+ a = int(u * 1000.);
+ b = int(v * 1000.);
+ c = 0;
+ exit = (i > 100);
+tel
+
+