From a1eb0c8e58495358e96d864c72613de162a32f38 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Fri, 13 Jun 2014 17:47:26 +0200 Subject: Add fail updown test (using pre instead of last). --- tests/Makefile | 2 +- tests/result/updown_fail.out | 31 +++++++++++++++++++++++++++++++ tests/source/updown_fail.scade | 23 +++++++++++++++++++++++ 3 files changed, 55 insertions(+), 1 deletion(-) create mode 100644 tests/result/updown_fail.out create mode 100644 tests/source/updown_fail.scade 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 -- cgit v1.2.3