Nice view of guarantees ; add half test, proved.

4 files changed, 33 insertions, 1 deletions

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;