summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/Makefile2
-rw-r--r--tests/result/updown_fail.out31
-rw-r--r--tests/source/updown_fail.scade23
3 files changed, 55 insertions, 1 deletions
diff --git a/tests/Makefile b/tests/Makefile
index d306161..f51eb61 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -1,6 +1,6 @@
ALL_OUT=result/limiter.out result/limitera.out result/locals.out \
result/test4.out result/test5.out result/test7.out \
- result/train.out result/updown.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
diff --git a/tests/result/updown_fail.out b/tests/result/updown_fail.out
new file mode 100644
index 0000000..a5feccb
--- /dev/null
+++ b/tests/result/updown_fail.out
@@ -0,0 +1,31 @@
+0. 1 0 0
+1. 2 0 0
+2. 3 0 0
+3. 4 0 0
+4. 5 0 0
+5. 6 0 0
+6. 7 0 0
+7. -1 0 0
+8. -2 0 0
+9. -3 0 0
+10. -4 0 0
+11. -5 0 0
+12. -6 0 0
+13. -7 0 0
+14. 8 0 0
+15. -8 0 0
+16. 9 0 0
+17. -9 0 0
+18. 10 0 0
+19. -10 0 0
+20. 11 0 0
+21. -11 0 0
+22. 12 0 0
+23. -12 0 0
+24. 13 0 0
+25. -13 0 0
+26. 14 0 0
+27. -14 0 0
+28. 15 0 0
+29. -15 0 0
+30. 16 0 0
diff --git a/tests/source/updown_fail.scade b/tests/source/updown_fail.scade
new file mode 100644
index 0000000..b6280ef
--- /dev/null
+++ b/tests/source/updown_fail.scade
@@ -0,0 +1,23 @@
+const bound: int = 7;
+
+node updown() returns(probe x: int)
+let
+ automaton
+ initial state UP
+ let x = (0 -> pre x) + 1; tel
+ until if x >= bound resume DOWN;
+
+ state DOWN
+ let x = (0 -> pre x) - 1; tel
+ until if x <= -bound resume UP;
+
+ returns x;
+tel
+
+node test(i: int) returns(a, b, c: int; exit: bool)
+let
+ exit = i >= 30;
+ a = updown();
+ b = 0;
+ c = 0;
+tel