summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-06-18 17:53:11 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-06-18 17:53:11 +0200
commit5a4165f55002876033c718303f86e9e1b7417745 (patch)
treeaa17967d9b952b3df9a6b6fce215997ea2c9f7e5 /tests
parent96753a375e814be6bde6c41cfdfa4b4cc06bd28e (diff)
downloadscade-analyzer-5a4165f55002876033c718303f86e9e1b7417745.tar.gz
scade-analyzer-5a4165f55002876033c718303f86e9e1b7417745.zip
Nice view of guarantees ; add half test, proved.
Diffstat (limited to 'tests')
-rw-r--r--tests/Makefile2
-rw-r--r--tests/result/half.out21
-rw-r--r--tests/source/gilbreath.scade2
-rw-r--r--tests/source/half.scade29
-rw-r--r--tests/source/limiter.scade2
-rw-r--r--tests/source/limitera.scade1
6 files changed, 55 insertions, 2 deletions
diff --git a/tests/Makefile b/tests/Makefile
index 7d5aac0..165f4ec 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -3,7 +3,7 @@ ALL_OUT=result/limiter.out result/limitera.out result/locals.out \
result/train.out result/updown.out result/updown_fail.out \
result/test0.out result/test1.out result/test2.out result/test3.out \
result/test6.out result/testc.out \
- result/gilbreath.out
+ result/gilbreath.out result/half.out
bin/%.test: source/%.scade test.c
rm kcg/*
diff --git a/tests/result/half.out b/tests/result/half.out
new file mode 100644
index 0000000..c2085c5
--- /dev/null
+++ b/tests/result/half.out
@@ -0,0 +1,21 @@
+0. 1 0 1
+1. 1 1 0
+2. 2 1 1
+3. 2 2 0
+4. 3 2 1
+5. 3 3 0
+6. 4 3 1
+7. 4 4 0
+8. 5 4 1
+9. 5 5 0
+10. 6 5 1
+11. 6 6 0
+12. 7 6 1
+13. 7 7 0
+14. 8 7 1
+15. 8 8 0
+16. 9 8 1
+17. 9 9 0
+18. 10 9 1
+19. 10 10 0
+20. 11 10 1
diff --git a/tests/source/gilbreath.scade b/tests/source/gilbreath.scade
index 2723f9f..e0b7245 100644
--- a/tests/source/gilbreath.scade
+++ b/tests/source/gilbreath.scade
@@ -16,6 +16,8 @@ let
half = false -> not pre half;
property = true -> not (half and (o = pre o));
+
+ guarantee p_true : property;
tel
node test(i: int) returns (a, b, c: int; exit: bool)
diff --git a/tests/source/half.scade b/tests/source/half.scade
new file mode 100644
index 0000000..da90586
--- /dev/null
+++ b/tests/source/half.scade
@@ -0,0 +1,29 @@
+node test(i: int) returns (a, b, probe c: int; exit: bool)
+var
+ la, lb: int;
+ half: bool;
+let
+ exit = i >= 20;
+
+ half = true -> not pre half;
+
+ la = 0 -> pre a;
+ lb = 0 -> pre b;
+ activate
+ if half then
+ let
+ a = la + 1;
+ b = lb;
+ tel
+ else
+ let
+ a = la;
+ b = lb + 1;
+ tel
+ returns a, b;
+
+ c = a - b;
+
+ guarantee c_bounded: c >= 0 and c <= 1;
+ guarantee link_c_half: (half and c = 1) or ((not half) and c = 0);
+tel
diff --git a/tests/source/limiter.scade b/tests/source/limiter.scade
index fc9fb30..05cb2b7 100644
--- a/tests/source/limiter.scade
+++ b/tests/source/limiter.scade
@@ -4,7 +4,7 @@ node limiter(x: int; d: int) returns (probe y: int)
var s, r: int;
let
assume in_bounded: x >= -bound and x <= bound;
- assume d_bounded: d >= 0 and d >= 16;
+ assume d_bounded: d >= 0 and d <= 16;
guarantee out_bounded: y >= -bound and y <= bound;
s = 0 -> pre y;
r = x - s;
diff --git a/tests/source/limitera.scade b/tests/source/limitera.scade
index e6db4e2..2b87278 100644
--- a/tests/source/limitera.scade
+++ b/tests/source/limitera.scade
@@ -4,6 +4,7 @@ node limiter(x: int; d: int) returns (probe y: int)
var s, r: int;
let
assume in_bounded: x >= -bound and x <= bound;
+ assume d_bounded: d = 16;
guarantee out_bounded: y >= -bound and y <= bound;
s = 0 -> pre y;
r = x - s;