From b1cdf90995c8f70e4a450b3319a136f0d50515d0 Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ansys.com>
Date: Fri, 4 Jul 2014 16:21:45 +0200
Subject: New example ; minor fixes.

---
 tests/source/NestedControl.scade |  8 ++++----
 tests/source/counters.scade      | 38 ++++++++++++++++++++++++++++++++++++++
 tests/source/test5.scade         |  4 ++--
 3 files changed, 44 insertions(+), 6 deletions(-)
 create mode 100644 tests/source/counters.scade

(limited to 'tests')

diff --git a/tests/source/NestedControl.scade b/tests/source/NestedControl.scade
index 2551eb6..af4fdab 100644
--- a/tests/source/NestedControl.scade
+++ b/tests/source/NestedControl.scade
@@ -1,13 +1,13 @@
 node root(In : int; C : bool) returns (Out, Out1 : int)
 var last_Out, last_Out1: int;
-    isp, isn: bool;
+    disj, disj2: bool;
 let
   last_Out = 0 -> pre Out;
   last_Out1 = 0 -> pre Out1;
 
-  isp = In > 0;
-  isn = In < 0;
-  assume C_in_not_null: (not C) or isp or isn;
+  disj = In > 0;
+  disj2 = In < 0;
+  assume C_in_not_null: (not C) or disj or disj2;
 
   automaton SM1
     initial state State1
diff --git a/tests/source/counters.scade b/tests/source/counters.scade
new file mode 100644
index 0000000..334bca1
--- /dev/null
+++ b/tests/source/counters.scade
@@ -0,0 +1,38 @@
+/*
+   x = 10 | 9 | 8 | 7 | 6 | 5 | ... | 0  | 1 | 2 | ... | 10 | ...
+   y =  0 | 1 | 2 | 3 | 4 | 5 | ... | 10 | 9 | 8 | ... | 0  | ...
+
+   b1 = t | f | f | f | f | f | ... | f  | f | f | ... |  t | ...
+   b2 = t | f | f | f | f | f | ... | f  | f | f | ... |  t | ...
+
+   eq* = t | t | t | t | t | t | ... | t  | t | t | ... |  t | ...
+*/
+
+
+-- type t2 = subrange [0,10] of int;
+
+const bound: int = 1000;
+
+node counters(z: bool) returns (eq_nind : bool ; probe x, probe y : int)
+var
+  b1, b2 : bool;
+  a, b : bool;
+let
+
+  a = false -> (if pre a then pre x < bound else pre x <= 0);
+  --a = false -> pre(if a then x < bound else x <= 0);
+  x = bound -> (if a then pre x + 1 else pre x - 1);
+
+  b = true -> (if pre b then pre y < bound else pre y <= 0);
+  --b = true -> pre(if b then y < bound else y <= 0);
+  y = 0 -> (if b then pre y + 1 else pre y - 1);
+
+  b1 = x=bound;
+  b2 = y=0;
+
+
+  guarantee xy : x+y = bound;
+  guarantee bb : b1 = b2;
+  guarantee rp : -bound <= (x-y) and (x-y) <= bound;
+
+tel
diff --git a/tests/source/test5.scade b/tests/source/test5.scade
index 1de390d..566acf0 100644
--- a/tests/source/test5.scade
+++ b/tests/source/test5.scade
@@ -1,8 +1,8 @@
-node test(i: int) returns(probe a, b, c: int; exit: bool)
+node test(i: int) returns(probe a, probe b, probe c: int; exit: bool)
 let
     b = 0 -> pre a;
     a = if b > 4 then 0 else b + 1;
-    c = 0;   
+    c = i;   
     exit = i >= 10;
 tel
 
-- 
cgit v1.2.3