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

3 files changed, 36 insertions, 1 deletions

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