Move a lot of things.

14 files changed, 234 insertions, 0 deletions

diff --git a/tests/source/limiter.scade b/tests/source/limiter.scade
new file mode 100644
index 0000000..a611d98
--- /dev/null
+++ b/tests/source/limiter.scade
@@ -0,0 +1,21 @@
+const bound: int = 128;
+
+node limiter(x: int; d: int) returns (probe y: int)
+    var s, r: int;
+    let
+        assume in_bounded: x >= -bound and x <= bound;
+        guarantee out_bounded: y >= -bound and y <= bound;
+        s = 0 -> pre y;
+        r = x - s;
+        y = if r <= -d then s - d
+            else if r >= d then s + d
+            else x;
+    tel
+
+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
+        b = 16;
+        c = limiter(a, b);
+    tel
diff --git a/tests/source/limitera.scade b/tests/source/limitera.scade
new file mode 100644
index 0000000..1e4927e
--- /dev/null
+++ b/tests/source/limitera.scade
@@ -0,0 +1,26 @@
+const bound: int = 128;
+
+node limiter(x: int; d: int) returns (probe y: int)
+    var s, r: int;
+    let
+        assume in_bounded: x >= -bound and x <= bound;
+        guarantee out_bounded: y >= -bound and y <= bound;
+        s = 0 -> pre y;
+        r = x - s;
+        activate
+          if r <= -d then
+            let y = s - d; tel
+          else if r >= d then
+            let y = s + d; tel
+          else 
+            let y = x; tel
+        returns y;
+    tel
+
+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
+        b = 16;
+        c = limiter(a, b);
+    tel
diff --git a/tests/source/locals.scade b/tests/source/locals.scade
new file mode 100644
index 0000000..379cbde
--- /dev/null
+++ b/tests/source/locals.scade
@@ -0,0 +1,20 @@
+node test(i: int) returns(a, b, c: int; exit: bool)
+let
+  activate
+    if i mod 5 = 0 then
+      var x: int;
+      let
+        x = i;
+        a = x;
+      tel
+    else
+      var x: int;
+      let
+        x = (0 -> pre i);
+        a = x;
+      tel
+  returns a;
+  b = 0;
+  c = 0;
+  exit = i >= 12;
+tel
diff --git a/tests/source/test0.scade b/tests/source/test0.scade
new file mode 100644
index 0000000..65a5331
--- /dev/null
+++ b/tests/source/test0.scade
@@ -0,0 +1,7 @@
+function test(i: int) returns(probe a, b, c: int; exit: bool)
+let
+    exit = i >= 5;
+    a = i;
+    b = 0;
+    c = 0;
+tel
diff --git a/tests/source/test1.scade b/tests/source/test1.scade
new file mode 100644
index 0000000..f247a57
--- /dev/null
+++ b/tests/source/test1.scade
@@ -0,0 +1,8 @@
+function test(i: int) returns(probe a, b, c: int; exit: bool)
+let
+    assume i_pos : i >= 0;
+    exit = i >= 5;
+    a = i;
+    b = 0;
+    c = 0;
+tel
diff --git a/tests/source/test2.scade b/tests/source/test2.scade
new file mode 100644
index 0000000..28a3e2d
--- /dev/null
+++ b/tests/source/test2.scade
@@ -0,0 +1,8 @@
+function test(i: int) returns(probe a, b, c: int; exit: bool)
+let
+    assume i_pos : i >= 0;
+    exit = i >= 5;
+    a = if i < 0 then 42 else 12;
+    b = 0;
+    c = 0;
+tel
diff --git a/tests/source/test3.scade b/tests/source/test3.scade
new file mode 100644
index 0000000..541b9f5
--- /dev/null
+++ b/tests/source/test3.scade
@@ -0,0 +1,7 @@
+function test(i: int) returns(probe a, b, c: int; exit: bool)
+let
+    exit = i >= 5;
+    a = if i < 0 then -i else i;
+    b = 0;
+    c = 0;
+tel
diff --git a/tests/source/test4.scade b/tests/source/test4.scade
new file mode 100644
index 0000000..c66a56f
--- /dev/null
+++ b/tests/source/test4.scade
@@ -0,0 +1,7 @@
+node test(i: int) returns(probe a, b, c: int; exit: bool)
+let
+    exit = i >= 5;
+    a = 0 -> (if pre a > 10 then 0 else pre a + 1);
+    b = 0 -> pre i;
+    c = 0;
+tel
diff --git a/tests/source/test5.scade b/tests/source/test5.scade
new file mode 100644
index 0000000..1de390d
--- /dev/null
+++ b/tests/source/test5.scade
@@ -0,0 +1,8 @@
+node test(i: int) returns(probe a, b, c: int; exit: bool)
+let
+    b = 0 -> pre a;
+    a = if b > 4 then 0 else b + 1;
+    c = 0;   
+    exit = i >= 10;
+tel
+
diff --git a/tests/source/test6.scade b/tests/source/test6.scade
new file mode 100644
index 0000000..e3257cc
--- /dev/null
+++ b/tests/source/test6.scade
@@ -0,0 +1,9 @@
+function test(probe i: int) returns(probe a, b, c: int; exit: bool)
+let
+    assume i_bounded : i >= -10 and i <= 10;
+    a = i;
+    guarantee a_eq_i : a = i;
+    b = 0;
+    c = 0;
+    exit = i >= 5;
+tel
diff --git a/tests/source/test7.scade b/tests/source/test7.scade
new file mode 100644
index 0000000..c756a9e
--- /dev/null
+++ b/tests/source/test7.scade
@@ -0,0 +1,7 @@
+node test(i: int) returns(a, b, probe c: int; exit: bool)
+let
+    a = 0;
+    b = 0;
+    c = 0 -> (pre c + 1);
+    exit = i >= 5;
+tel
diff --git a/tests/source/testc.scade b/tests/source/testc.scade
new file mode 100644
index 0000000..40a04d3
--- /dev/null
+++ b/tests/source/testc.scade
@@ -0,0 +1,11 @@
+const x : int = 12;
+const y : int = z + 3;
+const z : int = x * 2;
+
+function test(i: int) returns (a, b, c: int; exit: bool)
+let
+  exit = i >= 0;
+  a = x;
+  b = y;
+  c = z;
+tel
diff --git a/tests/source/train.scade b/tests/source/train.scade
new file mode 100644
index 0000000..c51971e
--- /dev/null
+++ b/tests/source/train.scade
@@ -0,0 +1,69 @@
+-- Cet exemple est clairement trop compliqué.
+
+
+node diff(incr, decr: bool) returns (diff: int)
+let
+    diff = (0 -> pre diff) +
+        (if incr and not decr then 1
+        else if not incr and decr then -1
+        else 0);
+tel
+
+node train(beacon, second: bool) returns (early, late: bool)
+var probe advance: int;
+let
+    advance = diff(beacon, second);
+
+    automaton
+        initial state NotEarly
+        let early = false; tel
+        until if advance >= 10 resume Early;
+
+        state Early
+        let early = true; tel
+        until if advance = 0 resume NotEarly;
+    returns early;
+
+    automaton
+        initial state NotLate
+        let late = false; tel
+        until if advance <= -10 resume Late;
+
+        state Late
+        let late = true; tel
+        until if advance = 0 resume NotLate;
+    returns late;
+tel
+
+node observer(early, late: bool) returns (alarm: bool)
+var ontime: bool;
+let
+    ontime = not (late or early);
+    automaton
+        initial state Ok
+        let alarm = false; tel
+        until if early resume Early;
+
+        state Early
+        let alarm = late and not early; tel
+        until if ontime resume Ok;
+    returns alarm;
+tel
+
+node train_check(beacon, second: bool) returns (early, late, alarm: bool)
+let
+    early, late = train(beacon, second);
+    alarm = observer(early, late);
+    guarantee ok : not alarm;
+tel
+
+node test(i: int) returns(a, b, c: int; exit: bool)
+var early, late, alarm: bool;
+let
+    exit = i >= 100;
+    early, late, alarm = train_check((i+1) mod 2 = 0, i mod 3 = 0);
+    c = if alarm then 1 else 0;
+    a = if early then 1 else 0;
+    b = if late then 1 else 0;
+tel
+
diff --git a/tests/source/updown.scade b/tests/source/updown.scade
new file mode 100644
index 0000000..089293a
--- /dev/null
+++ b/tests/source/updown.scade
@@ -0,0 +1,26 @@
+const bound: int = 7;
+
+node updown() returns(probe x: int)
+var last_x: int;
+let
+    last_x = 0 -> pre x;
+    guarantee x_bounded: x >= -bound and x <= bound;
+    automaton
+        initial state UP
+        let x = last_x + 1; tel
+        until if x >= bound resume DOWN;
+
+        state DOWN
+        let x = last_x - 1; tel
+        until if x <= -bound resume UP;
+
+    returns x;
+tel
+
+node test(i: int) returns(a, b, c: int; exit: bool)
+let
+    exit = i >= 30;
+    a = updown();
+    b = 0;
+    c = 0;
+tel