From dedc98b0c14262c53e8573d7fe1dcaa370e43fb5 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Fri, 13 Jun 2014 14:17:22 +0200 Subject: Move a lot of things. --- tests/Makefile | 13 +++++- tests/count.scade | 36 ---------------- tests/limiter.scade | 21 --------- tests/limitera.scade | 26 ------------ tests/merge.scade | 22 ---------- tests/result/limiter.out | 31 ++++++++++++++ tests/result/limitera.out | 31 ++++++++++++++ tests/result/locals.out | 13 ++++++ tests/result/test0.out | 6 +++ tests/result/test1.out | 6 +++ tests/result/test2.out | 6 +++ tests/result/test3.out | 6 +++ tests/result/test4.out | 6 +++ tests/result/test5.out | 11 +++++ tests/result/test6.out | 6 +++ tests/result/test7.out | 6 +++ tests/result/testc.out | 1 + tests/result/train.out | 101 ++++++++++++++++++++++++++++++++++++++++++++ tests/result/updown.out | 31 ++++++++++++++ tests/source/limiter.scade | 21 +++++++++ tests/source/limitera.scade | 26 ++++++++++++ tests/source/locals.scade | 20 +++++++++ tests/source/test0.scade | 7 +++ tests/source/test1.scade | 8 ++++ tests/source/test2.scade | 8 ++++ tests/source/test3.scade | 7 +++ tests/source/test4.scade | 7 +++ tests/source/test5.scade | 8 ++++ tests/source/test6.scade | 9 ++++ tests/source/test7.scade | 7 +++ tests/source/testc.scade | 11 +++++ tests/source/train.scade | 69 ++++++++++++++++++++++++++++++ tests/source/updown.scade | 26 ++++++++++++ tests/tests/test0.scade | 7 --- tests/tests/test1.scade | 8 ---- tests/tests/test2.scade | 8 ---- tests/tests/test3.scade | 7 --- tests/tests/test4.scade | 7 --- tests/tests/test5.scade | 8 ---- tests/tests/test6.scade | 9 ---- tests/tests/test7.scade | 7 --- tests/tests/testc.scade | 11 ----- tests/train.scade | 69 ------------------------------ tests/updown.scade | 26 ------------ 44 files changed, 507 insertions(+), 273 deletions(-) delete mode 100644 tests/count.scade delete mode 100644 tests/limiter.scade delete mode 100644 tests/limitera.scade delete mode 100644 tests/merge.scade create mode 100644 tests/result/limiter.out create mode 100644 tests/result/limitera.out create mode 100644 tests/result/locals.out create mode 100644 tests/result/test0.out create mode 100644 tests/result/test1.out create mode 100644 tests/result/test2.out create mode 100644 tests/result/test3.out create mode 100644 tests/result/test4.out create mode 100644 tests/result/test5.out create mode 100644 tests/result/test6.out create mode 100644 tests/result/test7.out create mode 100644 tests/result/testc.out create mode 100644 tests/result/train.out create mode 100644 tests/result/updown.out create mode 100644 tests/source/limiter.scade create mode 100644 tests/source/limitera.scade create mode 100644 tests/source/locals.scade create mode 100644 tests/source/test0.scade create mode 100644 tests/source/test1.scade create mode 100644 tests/source/test2.scade create mode 100644 tests/source/test3.scade create mode 100644 tests/source/test4.scade create mode 100644 tests/source/test5.scade create mode 100644 tests/source/test6.scade create mode 100644 tests/source/test7.scade create mode 100644 tests/source/testc.scade create mode 100644 tests/source/train.scade create mode 100644 tests/source/updown.scade delete mode 100644 tests/tests/test0.scade delete mode 100644 tests/tests/test1.scade delete mode 100644 tests/tests/test2.scade delete mode 100644 tests/tests/test3.scade delete mode 100644 tests/tests/test4.scade delete mode 100644 tests/tests/test5.scade delete mode 100644 tests/tests/test6.scade delete mode 100644 tests/tests/test7.scade delete mode 100644 tests/tests/testc.scade delete mode 100644 tests/train.scade delete mode 100644 tests/updown.scade (limited to 'tests') diff --git a/tests/Makefile b/tests/Makefile index 4073cad..d306161 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -1,4 +1,15 @@ -%.test: %.scade test.c +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/test0.out result/test1.out result/test2.out result/test3.out \ + result/test6.out result/testc.out + +bin/%.test: source/%.scade test.c rm kcg/* kcg64 -target C -node test $< gcc -o $@ test.c kcg/*.c -I./kcg + +result/%.out: bin/%.test + $< > $@ + +all: $(ALL_OUT) diff --git a/tests/count.scade b/tests/count.scade deleted file mode 100644 index c5ce47d..0000000 --- a/tests/count.scade +++ /dev/null @@ -1,36 +0,0 @@ -node count() returns (c: int) -let - c = 0 -> (1 + pre c); -tel - -node resettable_count (r: bool) returns (c: int) -let - c = (restart count every r)(); -tel - -node nat() returns (s: int) s = 1 -> (1 + pre s); - -node rst_clk(rst: bool; clock h: bool) - returns (s: int; t: int) -let - s = (restart nat every rst) (); - t = merge(h; ((restart nat every rst) (() when h)); 0 when not h); -tel - -node even_times(c: bool; i: int) returns (o: int) -let - automaton - initial state EVEN - unless if c resume ODD; - let - o = i+1; - tel - - state ODD - unless if c resume EVEN; - let - o = -2 * i; - tel - returns o; -tel - diff --git a/tests/limiter.scade b/tests/limiter.scade deleted file mode 100644 index a611d98..0000000 --- a/tests/limiter.scade +++ /dev/null @@ -1,21 +0,0 @@ -const bound: int = 128; - -node limiter(x: int; d: int) returns (probe y: int) - var s, r: int; - let - assume in_bounded: x >= -bound and x <= bound; - guarantee out_bounded: y >= -bound and y <= bound; - s = 0 -> pre y; - r = x - s; - y = if r <= -d then s - d - else if r >= d then s + d - else x; - tel - -node test(i: int) returns(a, b, c: int; exit: bool) - let - exit = i >= 30; - a = (i * 21 + 122) mod (2 * bound) - bound; -- not really random - b = 16; - c = limiter(a, b); - tel diff --git a/tests/limitera.scade b/tests/limitera.scade deleted file mode 100644 index 1e4927e..0000000 --- a/tests/limitera.scade +++ /dev/null @@ -1,26 +0,0 @@ -const bound: int = 128; - -node limiter(x: int; d: int) returns (probe y: int) - var s, r: int; - let - assume in_bounded: x >= -bound and x <= bound; - guarantee out_bounded: y >= -bound and y <= bound; - s = 0 -> pre y; - r = x - s; - activate - if r <= -d then - let y = s - d; tel - else if r >= d then - let y = s + d; tel - else - let y = x; tel - returns y; - tel - -node test(i: int) returns(a, b, c: int; exit: bool) - let - exit = i >= 30; - a = (i * 21 + 122) mod (2 * bound) - bound; -- not really random - b = 16; - c = limiter(a, b); - tel diff --git a/tests/merge.scade b/tests/merge.scade deleted file mode 100644 index 9e666a1..0000000 --- a/tests/merge.scade +++ /dev/null @@ -1,22 +0,0 @@ -type t1 = enum { True, False, Error }; - -node #pragma kcg expand #end - mm(clock clk: t1; v: int when (clk match True)) returns(r: int) -var lr: int; -let - lr = 0 -> pre r; - r = merge(clk; - v; - lr when (clk match False); - -1 when (clk match Error)); -tel - -node test(i: int) returns (a, b, c: int; exit: bool) -var clock clk: t1; -let - exit = i >= 30; - clk = if i mod 5 = 0 then True else if i mod 9 = 8 then Error else False; - a = mm(clk, i when (clk match True)); - b = if clk = True then 1 else 0; - c = if clk = Error then 1 else 0; -tel diff --git a/tests/result/limiter.out b/tests/result/limiter.out new file mode 100644 index 0000000..1851c7d --- /dev/null +++ b/tests/result/limiter.out @@ -0,0 +1,31 @@ +0. -6 16 -6 +1. 15 16 10 +2. 36 16 26 +3. 57 16 42 +4. 78 16 58 +5. 99 16 74 +6. 120 16 90 +7. -115 16 74 +8. -94 16 58 +9. -73 16 42 +10. -52 16 26 +11. -31 16 10 +12. -10 16 -6 +13. 11 16 10 +14. 32 16 26 +15. 53 16 42 +16. 74 16 58 +17. 95 16 74 +18. 116 16 90 +19. -119 16 74 +20. -98 16 58 +21. -77 16 42 +22. -56 16 26 +23. -35 16 10 +24. -14 16 -6 +25. 7 16 7 +26. 28 16 23 +27. 49 16 39 +28. 70 16 55 +29. 91 16 71 +30. 112 16 87 diff --git a/tests/result/limitera.out b/tests/result/limitera.out new file mode 100644 index 0000000..1851c7d --- /dev/null +++ b/tests/result/limitera.out @@ -0,0 +1,31 @@ +0. -6 16 -6 +1. 15 16 10 +2. 36 16 26 +3. 57 16 42 +4. 78 16 58 +5. 99 16 74 +6. 120 16 90 +7. -115 16 74 +8. -94 16 58 +9. -73 16 42 +10. -52 16 26 +11. -31 16 10 +12. -10 16 -6 +13. 11 16 10 +14. 32 16 26 +15. 53 16 42 +16. 74 16 58 +17. 95 16 74 +18. 116 16 90 +19. -119 16 74 +20. -98 16 58 +21. -77 16 42 +22. -56 16 26 +23. -35 16 10 +24. -14 16 -6 +25. 7 16 7 +26. 28 16 23 +27. 49 16 39 +28. 70 16 55 +29. 91 16 71 +30. 112 16 87 diff --git a/tests/result/locals.out b/tests/result/locals.out new file mode 100644 index 0000000..e111948 --- /dev/null +++ b/tests/result/locals.out @@ -0,0 +1,13 @@ +0. 0 0 0 +1. 0 0 0 +2. 1 0 0 +3. 2 0 0 +4. 3 0 0 +5. 5 0 0 +6. 4 0 0 +7. 6 0 0 +8. 7 0 0 +9. 8 0 0 +10. 10 0 0 +11. 9 0 0 +12. 11 0 0 diff --git a/tests/result/test0.out b/tests/result/test0.out new file mode 100644 index 0000000..fa316b4 --- /dev/null +++ b/tests/result/test0.out @@ -0,0 +1,6 @@ +0. 0 0 0 +1. 1 0 0 +2. 2 0 0 +3. 3 0 0 +4. 4 0 0 +5. 5 0 0 diff --git a/tests/result/test1.out b/tests/result/test1.out new file mode 100644 index 0000000..fa316b4 --- /dev/null +++ b/tests/result/test1.out @@ -0,0 +1,6 @@ +0. 0 0 0 +1. 1 0 0 +2. 2 0 0 +3. 3 0 0 +4. 4 0 0 +5. 5 0 0 diff --git a/tests/result/test2.out b/tests/result/test2.out new file mode 100644 index 0000000..d080f21 --- /dev/null +++ b/tests/result/test2.out @@ -0,0 +1,6 @@ +0. 12 0 0 +1. 12 0 0 +2. 12 0 0 +3. 12 0 0 +4. 12 0 0 +5. 12 0 0 diff --git a/tests/result/test3.out b/tests/result/test3.out new file mode 100644 index 0000000..fa316b4 --- /dev/null +++ b/tests/result/test3.out @@ -0,0 +1,6 @@ +0. 0 0 0 +1. 1 0 0 +2. 2 0 0 +3. 3 0 0 +4. 4 0 0 +5. 5 0 0 diff --git a/tests/result/test4.out b/tests/result/test4.out new file mode 100644 index 0000000..f5ad578 --- /dev/null +++ b/tests/result/test4.out @@ -0,0 +1,6 @@ +0. 0 0 0 +1. 1 0 0 +2. 2 1 0 +3. 3 2 0 +4. 4 3 0 +5. 5 4 0 diff --git a/tests/result/test5.out b/tests/result/test5.out new file mode 100644 index 0000000..388c744 --- /dev/null +++ b/tests/result/test5.out @@ -0,0 +1,11 @@ +0. 1 0 0 +1. 2 1 0 +2. 3 2 0 +3. 4 3 0 +4. 5 4 0 +5. 0 5 0 +6. 1 0 0 +7. 2 1 0 +8. 3 2 0 +9. 4 3 0 +10. 5 4 0 diff --git a/tests/result/test6.out b/tests/result/test6.out new file mode 100644 index 0000000..fa316b4 --- /dev/null +++ b/tests/result/test6.out @@ -0,0 +1,6 @@ +0. 0 0 0 +1. 1 0 0 +2. 2 0 0 +3. 3 0 0 +4. 4 0 0 +5. 5 0 0 diff --git a/tests/result/test7.out b/tests/result/test7.out new file mode 100644 index 0000000..90ae696 --- /dev/null +++ b/tests/result/test7.out @@ -0,0 +1,6 @@ +0. 0 0 0 +1. 0 0 1 +2. 0 0 2 +3. 0 0 3 +4. 0 0 4 +5. 0 0 5 diff --git a/tests/result/testc.out b/tests/result/testc.out new file mode 100644 index 0000000..5553419 --- /dev/null +++ b/tests/result/testc.out @@ -0,0 +1 @@ +0. 12 27 24 diff --git a/tests/result/train.out b/tests/result/train.out new file mode 100644 index 0000000..4af78b5 --- /dev/null +++ b/tests/result/train.out @@ -0,0 +1,101 @@ +0. 0 0 0 +1. 0 0 0 +2. 0 0 0 +3. 0 0 0 +4. 0 0 0 +5. 0 0 0 +6. 0 0 0 +7. 0 0 0 +8. 0 0 0 +9. 0 0 0 +10. 0 0 0 +11. 0 0 0 +12. 0 0 0 +13. 0 0 0 +14. 0 0 0 +15. 0 0 0 +16. 0 0 0 +17. 0 0 0 +18. 0 0 0 +19. 0 0 0 +20. 0 0 0 +21. 0 0 0 +22. 0 0 0 +23. 0 0 0 +24. 0 0 0 +25. 0 0 0 +26. 0 0 0 +27. 0 0 0 +28. 0 0 0 +29. 0 0 0 +30. 0 0 0 +31. 0 0 0 +32. 0 0 0 +33. 0 0 0 +34. 0 0 0 +35. 0 0 0 +36. 0 0 0 +37. 0 0 0 +38. 0 0 0 +39. 0 0 0 +40. 0 0 0 +41. 0 0 0 +42. 0 0 0 +43. 0 0 0 +44. 0 0 0 +45. 0 0 0 +46. 0 0 0 +47. 0 0 0 +48. 0 0 0 +49. 0 0 0 +50. 0 0 0 +51. 0 0 0 +52. 0 0 0 +53. 0 0 0 +54. 0 0 0 +55. 0 0 0 +56. 0 0 0 +57. 0 0 0 +58. 0 0 0 +59. 0 0 0 +60. 1 0 0 +61. 1 0 0 +62. 1 0 0 +63. 1 0 0 +64. 1 0 0 +65. 1 0 0 +66. 1 0 0 +67. 1 0 0 +68. 1 0 0 +69. 1 0 0 +70. 1 0 0 +71. 1 0 0 +72. 1 0 0 +73. 1 0 0 +74. 1 0 0 +75. 1 0 0 +76. 1 0 0 +77. 1 0 0 +78. 1 0 0 +79. 1 0 0 +80. 1 0 0 +81. 1 0 0 +82. 1 0 0 +83. 1 0 0 +84. 1 0 0 +85. 1 0 0 +86. 1 0 0 +87. 1 0 0 +88. 1 0 0 +89. 1 0 0 +90. 1 0 0 +91. 1 0 0 +92. 1 0 0 +93. 1 0 0 +94. 1 0 0 +95. 1 0 0 +96. 1 0 0 +97. 1 0 0 +98. 1 0 0 +99. 1 0 0 +100. 1 0 0 diff --git a/tests/result/updown.out b/tests/result/updown.out new file mode 100644 index 0000000..89e38ca --- /dev/null +++ b/tests/result/updown.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. 6 0 0 +8. 5 0 0 +9. 4 0 0 +10. 3 0 0 +11. 2 0 0 +12. 1 0 0 +13. 0 0 0 +14. -1 0 0 +15. -2 0 0 +16. -3 0 0 +17. -4 0 0 +18. -5 0 0 +19. -6 0 0 +20. -7 0 0 +21. -6 0 0 +22. -5 0 0 +23. -4 0 0 +24. -3 0 0 +25. -2 0 0 +26. -1 0 0 +27. 0 0 0 +28. 1 0 0 +29. 2 0 0 +30. 3 0 0 diff --git a/tests/source/limiter.scade b/tests/source/limiter.scade new file mode 100644 index 0000000..a611d98 --- /dev/null +++ b/tests/source/limiter.scade @@ -0,0 +1,21 @@ +const bound: int = 128; + +node limiter(x: int; d: int) returns (probe y: int) + var s, r: int; + let + assume in_bounded: x >= -bound and x <= bound; + guarantee out_bounded: y >= -bound and y <= bound; + s = 0 -> pre y; + r = x - s; + y = if r <= -d then s - d + else if r >= d then s + d + else x; + tel + +node test(i: int) returns(a, b, c: int; exit: bool) + let + exit = i >= 30; + a = (i * 21 + 122) mod (2 * bound) - bound; -- not really random + b = 16; + c = limiter(a, b); + tel diff --git a/tests/source/limitera.scade b/tests/source/limitera.scade new file mode 100644 index 0000000..1e4927e --- /dev/null +++ b/tests/source/limitera.scade @@ -0,0 +1,26 @@ +const bound: int = 128; + +node limiter(x: int; d: int) returns (probe y: int) + var s, r: int; + let + assume in_bounded: x >= -bound and x <= bound; + guarantee out_bounded: y >= -bound and y <= bound; + s = 0 -> pre y; + r = x - s; + activate + if r <= -d then + let y = s - d; tel + else if r >= d then + let y = s + d; tel + else + let y = x; tel + returns y; + tel + +node test(i: int) returns(a, b, c: int; exit: bool) + let + exit = i >= 30; + a = (i * 21 + 122) mod (2 * bound) - bound; -- not really random + b = 16; + c = limiter(a, b); + tel diff --git a/tests/source/locals.scade b/tests/source/locals.scade new file mode 100644 index 0000000..379cbde --- /dev/null +++ b/tests/source/locals.scade @@ -0,0 +1,20 @@ +node test(i: int) returns(a, b, c: int; exit: bool) +let + activate + if i mod 5 = 0 then + var x: int; + let + x = i; + a = x; + tel + else + var x: int; + let + x = (0 -> pre i); + a = x; + tel + returns a; + b = 0; + c = 0; + exit = i >= 12; +tel diff --git a/tests/source/test0.scade b/tests/source/test0.scade new file mode 100644 index 0000000..65a5331 --- /dev/null +++ b/tests/source/test0.scade @@ -0,0 +1,7 @@ +function test(i: int) returns(probe a, b, c: int; exit: bool) +let + exit = i >= 5; + a = i; + b = 0; + c = 0; +tel diff --git a/tests/source/test1.scade b/tests/source/test1.scade new file mode 100644 index 0000000..f247a57 --- /dev/null +++ b/tests/source/test1.scade @@ -0,0 +1,8 @@ +function test(i: int) returns(probe a, b, c: int; exit: bool) +let + assume i_pos : i >= 0; + exit = i >= 5; + a = i; + b = 0; + c = 0; +tel diff --git a/tests/source/test2.scade b/tests/source/test2.scade new file mode 100644 index 0000000..28a3e2d --- /dev/null +++ b/tests/source/test2.scade @@ -0,0 +1,8 @@ +function test(i: int) returns(probe a, b, c: int; exit: bool) +let + assume i_pos : i >= 0; + exit = i >= 5; + a = if i < 0 then 42 else 12; + b = 0; + c = 0; +tel diff --git a/tests/source/test3.scade b/tests/source/test3.scade new file mode 100644 index 0000000..541b9f5 --- /dev/null +++ b/tests/source/test3.scade @@ -0,0 +1,7 @@ +function test(i: int) returns(probe a, b, c: int; exit: bool) +let + exit = i >= 5; + a = if i < 0 then -i else i; + b = 0; + c = 0; +tel diff --git a/tests/source/test4.scade b/tests/source/test4.scade new file mode 100644 index 0000000..c66a56f --- /dev/null +++ b/tests/source/test4.scade @@ -0,0 +1,7 @@ +node test(i: int) returns(probe a, b, c: int; exit: bool) +let + exit = i >= 5; + a = 0 -> (if pre a > 10 then 0 else pre a + 1); + b = 0 -> pre i; + c = 0; +tel diff --git a/tests/source/test5.scade b/tests/source/test5.scade new file mode 100644 index 0000000..1de390d --- /dev/null +++ b/tests/source/test5.scade @@ -0,0 +1,8 @@ +node test(i: int) returns(probe a, b, c: int; exit: bool) +let + b = 0 -> pre a; + a = if b > 4 then 0 else b + 1; + c = 0; + exit = i >= 10; +tel + diff --git a/tests/source/test6.scade b/tests/source/test6.scade new file mode 100644 index 0000000..e3257cc --- /dev/null +++ b/tests/source/test6.scade @@ -0,0 +1,9 @@ +function test(probe i: int) returns(probe a, b, c: int; exit: bool) +let + assume i_bounded : i >= -10 and i <= 10; + a = i; + guarantee a_eq_i : a = i; + b = 0; + c = 0; + exit = i >= 5; +tel diff --git a/tests/source/test7.scade b/tests/source/test7.scade new file mode 100644 index 0000000..c756a9e --- /dev/null +++ b/tests/source/test7.scade @@ -0,0 +1,7 @@ +node test(i: int) returns(a, b, probe c: int; exit: bool) +let + a = 0; + b = 0; + c = 0 -> (pre c + 1); + exit = i >= 5; +tel diff --git a/tests/source/testc.scade b/tests/source/testc.scade new file mode 100644 index 0000000..40a04d3 --- /dev/null +++ b/tests/source/testc.scade @@ -0,0 +1,11 @@ +const x : int = 12; +const y : int = z + 3; +const z : int = x * 2; + +function test(i: int) returns (a, b, c: int; exit: bool) +let + exit = i >= 0; + a = x; + b = y; + c = z; +tel diff --git a/tests/source/train.scade b/tests/source/train.scade new file mode 100644 index 0000000..c51971e --- /dev/null +++ b/tests/source/train.scade @@ -0,0 +1,69 @@ +-- Cet exemple est clairement trop compliqué. + + +node diff(incr, decr: bool) returns (diff: int) +let + diff = (0 -> pre diff) + + (if incr and not decr then 1 + else if not incr and decr then -1 + else 0); +tel + +node train(beacon, second: bool) returns (early, late: bool) +var probe advance: int; +let + advance = diff(beacon, second); + + automaton + initial state NotEarly + let early = false; tel + until if advance >= 10 resume Early; + + state Early + let early = true; tel + until if advance = 0 resume NotEarly; + returns early; + + automaton + initial state NotLate + let late = false; tel + until if advance <= -10 resume Late; + + state Late + let late = true; tel + until if advance = 0 resume NotLate; + returns late; +tel + +node observer(early, late: bool) returns (alarm: bool) +var ontime: bool; +let + ontime = not (late or early); + automaton + initial state Ok + let alarm = false; tel + until if early resume Early; + + state Early + let alarm = late and not early; tel + until if ontime resume Ok; + returns alarm; +tel + +node train_check(beacon, second: bool) returns (early, late, alarm: bool) +let + early, late = train(beacon, second); + alarm = observer(early, late); + guarantee ok : not alarm; +tel + +node test(i: int) returns(a, b, c: int; exit: bool) +var early, late, alarm: bool; +let + exit = i >= 100; + early, late, alarm = train_check((i+1) mod 2 = 0, i mod 3 = 0); + c = if alarm then 1 else 0; + a = if early then 1 else 0; + b = if late then 1 else 0; +tel + diff --git a/tests/source/updown.scade b/tests/source/updown.scade new file mode 100644 index 0000000..089293a --- /dev/null +++ b/tests/source/updown.scade @@ -0,0 +1,26 @@ +const bound: int = 7; + +node updown() returns(probe x: int) +var last_x: int; +let + last_x = 0 -> pre x; + guarantee x_bounded: x >= -bound and x <= bound; + automaton + initial state UP + let x = last_x + 1; tel + until if x >= bound resume DOWN; + + state DOWN + let x = last_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 diff --git a/tests/tests/test0.scade b/tests/tests/test0.scade deleted file mode 100644 index 3d03be5..0000000 --- a/tests/tests/test0.scade +++ /dev/null @@ -1,7 +0,0 @@ -node test(i: int) returns(probe a, b, c: int; exit: bool) -let - exit = i >= 5; - a = i; - b = 0; - c = 0; -tel diff --git a/tests/tests/test1.scade b/tests/tests/test1.scade deleted file mode 100644 index 350b920..0000000 --- a/tests/tests/test1.scade +++ /dev/null @@ -1,8 +0,0 @@ -node test(i: int) returns(probe a, b, c: int; exit: bool) -let - assume i_pos : i >= 0; - exit = i >= 5; - a = i; - b = 0; - c = 0; -tel diff --git a/tests/tests/test2.scade b/tests/tests/test2.scade deleted file mode 100644 index 1777689..0000000 --- a/tests/tests/test2.scade +++ /dev/null @@ -1,8 +0,0 @@ -node test(i: int) returns(probe a, b, c: int; exit: bool) -let - assume i_pos : i >= 0; - exit = i >= 5; - a = if i < 0 then 42 else 12; - b = 0; - c = 0; -tel diff --git a/tests/tests/test3.scade b/tests/tests/test3.scade deleted file mode 100644 index 9380a49..0000000 --- a/tests/tests/test3.scade +++ /dev/null @@ -1,7 +0,0 @@ -node test(i: int) returns(probe a, b, c: int; exit: bool) -let - exit = i >= 5; - a = if i < 0 then -i else i; - b = 0; - c = 0; -tel diff --git a/tests/tests/test4.scade b/tests/tests/test4.scade deleted file mode 100644 index c66a56f..0000000 --- a/tests/tests/test4.scade +++ /dev/null @@ -1,7 +0,0 @@ -node test(i: int) returns(probe a, b, c: int; exit: bool) -let - exit = i >= 5; - a = 0 -> (if pre a > 10 then 0 else pre a + 1); - b = 0 -> pre i; - c = 0; -tel diff --git a/tests/tests/test5.scade b/tests/tests/test5.scade deleted file mode 100644 index 1de390d..0000000 --- a/tests/tests/test5.scade +++ /dev/null @@ -1,8 +0,0 @@ -node test(i: int) returns(probe a, b, c: int; exit: bool) -let - b = 0 -> pre a; - a = if b > 4 then 0 else b + 1; - c = 0; - exit = i >= 10; -tel - diff --git a/tests/tests/test6.scade b/tests/tests/test6.scade deleted file mode 100644 index 574e271..0000000 --- a/tests/tests/test6.scade +++ /dev/null @@ -1,9 +0,0 @@ -node test(probe i: int) returns(probe a, b, c: int; exit: bool) -let - assume i_bounded : i >= -10 and i <= 10; - a = i; - guarantee a_eq_i : a = i; - b = 0; - c = 0; - exit = i >= 5; -tel diff --git a/tests/tests/test7.scade b/tests/tests/test7.scade deleted file mode 100644 index c756a9e..0000000 --- a/tests/tests/test7.scade +++ /dev/null @@ -1,7 +0,0 @@ -node test(i: int) returns(a, b, probe c: int; exit: bool) -let - a = 0; - b = 0; - c = 0 -> (pre c + 1); - exit = i >= 5; -tel diff --git a/tests/tests/testc.scade b/tests/tests/testc.scade deleted file mode 100644 index 7c99b32..0000000 --- a/tests/tests/testc.scade +++ /dev/null @@ -1,11 +0,0 @@ -const x : int = 12; -const y : int = z + 3; -const z : int = x * 2; - -node test(i: int) returns (a, b, c: int; exit: bool) -let - exit = true; - a = x; - b = y; - c = z; -tel diff --git a/tests/train.scade b/tests/train.scade deleted file mode 100644 index d91df01..0000000 --- a/tests/train.scade +++ /dev/null @@ -1,69 +0,0 @@ --- Cet exemple est clairement trop compliqué. - - -node diff(incr, decr: bool) returns (diff: int) -let - diff = (0 -> pre diff) + - (if incr and not decr then 1 - else if not incr and decr then -1 - else 0); -tel - -node train(beacon, second: bool) returns (early, late: bool) -var probe advance: int; -let - advance = diff(beacon, second); - - automaton - initial state NotEarly - unless if advance > 10 resume Early; - let early = false; tel - - state Early - unless if advance = 0 resume NotEarly; - let early = true; tel - returns early; - - automaton - initial state NotLate - unless if advance < -10 resume Late; - let late = false; tel - - state Late - unless if advance = 0 resume NotLate; - let late = true; tel - returns late; -tel - -node observer(early, late: bool) returns (alarm: bool) -var ontime: bool; -let - ontime = not (late or early); - automaton - initial state Ok - unless if early resume Early; - let alarm = false; tel - - state Early - unless if ontime resume Ok; - let alarm = late; tel - returns alarm; -tel - -node train_check(beacon, second: bool) returns (early, late, alarm: bool) -let - early, late = train(beacon, second); - alarm = observer(early, late); - guarantee ok : not alarm; -tel - -node test(i: int) returns(a, b, c: int; exit: bool) -var early, late, alarm: bool; -let - exit = i >= 100; - early, late, alarm = train_check((i+1) mod 2 = 0, i mod 3 = 0); - c = if alarm then 1 else 0; - a = if early then 1 else 0; - b = if late then 1 else 0; -tel - diff --git a/tests/updown.scade b/tests/updown.scade deleted file mode 100644 index 089293a..0000000 --- a/tests/updown.scade +++ /dev/null @@ -1,26 +0,0 @@ -const bound: int = 7; - -node updown() returns(probe x: int) -var last_x: int; -let - last_x = 0 -> pre x; - guarantee x_bounded: x >= -bound and x <= bound; - automaton - initial state UP - let x = last_x + 1; tel - until if x >= bound resume DOWN; - - state DOWN - let x = last_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