Nice view of guarantees ; add half test, proved.

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;