diff options
Diffstat (limited to 'tests')
-rw-r--r-- | tests/Makefile | 2 | ||||
-rw-r--r-- | tests/result/half.out | 21 | ||||
-rw-r--r-- | tests/source/gilbreath.scade | 2 | ||||
-rw-r--r-- | tests/source/half.scade | 29 | ||||
-rw-r--r-- | tests/source/limiter.scade | 2 | ||||
-rw-r--r-- | tests/source/limitera.scade | 1 |
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; |