Add gilbreath suite ; booleans are not represented in a good way.

6 files changed, 83 insertions, 26 deletions

diff --git a/tests/Makefile b/tests/Makefile
index f51eb61..7d5aac0 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -2,7 +2,8 @@ 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/updown_fail.out \
 		result/test0.out result/test1.out result/test2.out result/test3.out \
-		result/test6.out result/testc.out
+		result/test6.out result/testc.out \
+		result/gilbreath.out
 
 bin/%.test: source/%.scade test.c
 	rm kcg/*
diff --git a/tests/result/gilbreath.out b/tests/result/gilbreath.out
new file mode 100644
index 0000000..d6a0fa4
--- /dev/null
+++ b/tests/result/gilbreath.out
@@ -0,0 +1,21 @@
+0. 0 1 1
+1. 1 1 0
+2. 0 1 0
+3. 1 1 1
+4. 1 1 0
+5. 0 1 0
+6. 0 1 1
+7. 1 1 0
+8. 0 1 0
+9. 1 1 0
+10. 0 1 0
+11. 1 1 0
+12. 1 1 1
+13. 0 1 0
+14. 1 1 0
+15. 0 1 1
+16. 0 1 0
+17. 1 1 0
+18. 1 1 1
+19. 0 1 0
+20. 1 1 0
diff --git a/tests/result/limitera.out b/tests/result/limitera.out
index 1851c7d..f047b8f 100644
--- a/tests/result/limitera.out
+++ b/tests/result/limitera.out
@@ -5,27 +5,27 @@
 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
+7. -116 16 74
+8. -95 16 58
+9. -74 16 42
+10. -53 16 26
+11. -32 16 10
+12. -11 16 -6
+13. 10 16 10
+14. 31 16 26
+15. 52 16 42
+16. 73 16 58
+17. 94 16 74
+18. 115 16 90
+19. -121 16 74
+20. -100 16 58
+21. -79 16 42
+22. -58 16 26
+23. -37 16 10
+24. -16 16 -6
+25. 5 16 5
+26. 26 16 21
+27. 47 16 37
+28. 68 16 53
+29. 89 16 69
+30. 110 16 85
diff --git a/tests/source/gilbreath.scade b/tests/source/gilbreath.scade
new file mode 100644
index 0000000..2723f9f
--- /dev/null
+++ b/tests/source/gilbreath.scade
@@ -0,0 +1,34 @@
+node gilbreath_stream(c: bool) returns (o, probe property: bool)
+var
+  half: bool;
+let
+  activate
+    if c then
+      let
+        o = false -> not pre o;
+      tel 
+    else
+      let
+        o = true -> not pre o;
+      tel
+  returns o;
+
+  half = false -> not pre half;
+
+  property = true -> not (half and (o = pre o));
+tel
+
+node test(i: int) returns (a, b, c: int; exit: bool)
+var
+  cond: bool;
+  o, prop: bool;
+let
+  exit = i >= 20;
+  cond = i mod 3 = 0 and not (i mod 7 = 2);
+  c = if cond then 1 else 0;
+  o, prop = gilbreath_stream(cond);
+  a = if o then 1 else 0;
+  b = if prop then 1 else 0;
+tel
+
+  
diff --git a/tests/source/limiter.scade b/tests/source/limiter.scade
index ff60567..fc9fb30 100644
--- a/tests/source/limiter.scade
+++ b/tests/source/limiter.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 >= 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 1e4927e..e6db4e2 100644
--- a/tests/source/limitera.scade
+++ b/tests/source/limitera.scade
@@ -20,7 +20,7 @@ node limiter(x: int; d: int) returns (probe y: int)
 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
+        a = (i * 21 + 122) mod (2 * bound + 1) - bound;  -- not really random
         b = 16;
         c = limiter(a, b);
     tel