Add some tests

16 files changed, 248 insertions, 1 deletions

diff --git a/.gitignore b/.gitignore
index ac48673..e6c5390 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,7 +2,12 @@
 *.swp
 *~
 
-# Build products
+# Tests : KCG & C build products
+tests/kcg
+*.log
+*.test
+
+# OCaml build products
 _build
 analyze
 
diff --git a/tests/Makefile b/tests/Makefile
new file mode 100644
index 0000000..4073cad
--- /dev/null
+++ b/tests/Makefile
@@ -0,0 +1,4 @@
+%.test: %.scade test.c
+	rm kcg/*
+	kcg64 -target C -node test $<
+	gcc -o $@ test.c kcg/*.c -I./kcg
diff --git a/tests/count.scade b/tests/count.scade
new file mode 100644
index 0000000..c5ce47d
--- /dev/null
+++ b/tests/count.scade
@@ -0,0 +1,36 @@
+node count() returns (c: int)
+let
+	c = 0 -> (1 + pre c);
+tel
+
+node resettable_count (r: bool) returns (c: int)
+let
+    c = (restart count every r)();
+tel
+
+node nat() returns (s: int) s = 1 -> (1 + pre s);
+
+node rst_clk(rst: bool; clock h: bool)
+    returns (s: int; t: int)
+let
+    s = (restart nat every rst) ();
+    t = merge(h; ((restart nat every rst) (() when h)); 0 when not h);
+tel
+
+node even_times(c: bool; i: int) returns (o: int)
+let
+    automaton
+        initial state EVEN
+        unless if c resume ODD;
+        let
+            o = i+1;
+        tel
+
+        state ODD
+        unless if c resume EVEN;
+        let
+            o = -2 * i;
+        tel
+    returns o;
+tel
+    
diff --git a/tests/limiter.scade b/tests/limiter.scade
new file mode 100644
index 0000000..a611d98
--- /dev/null
+++ b/tests/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/merge.scade b/tests/merge.scade
new file mode 100644
index 0000000..9e666a1
--- /dev/null
+++ b/tests/merge.scade
@@ -0,0 +1,22 @@
+type t1 = enum { True, False, Error };
+
+node #pragma kcg expand #end
+  mm(clock clk: t1; v: int when (clk match True)) returns(r: int)
+var lr: int;
+let
+  lr = 0 -> pre r;
+  r = merge(clk;
+        v;
+        lr when (clk match False);
+        -1 when (clk match Error));
+tel
+
+node test(i: int) returns (a, b, c: int; exit: bool)
+var clock clk: t1;
+let
+  exit = i >= 30;
+  clk = if i mod 5 = 0 then True else if i mod 9 = 8 then Error else False;
+  a = mm(clk, i when (clk match True));
+  b = if clk = True then 1 else 0;
+  c = if clk = Error then 1 else 0;
+tel
diff --git a/tests/test.c b/tests/test.c
new file mode 100644
index 0000000..11c3557
--- /dev/null
+++ b/tests/test.c
@@ -0,0 +1,21 @@
+#include <stdio.h>
+
+#include "test.h"
+
+int main() {
+    inC_test inC;
+    outC_test outC;
+
+    test_reset(&outC);
+
+    int i = 0;
+    while(1) {
+        inC.i = i++;
+
+        test(&inC, &outC);
+
+        printf("%d. %d %d %d\n", inC.i, outC.a, outC.b, outC.c);
+
+        if (outC.exit) return 0;
+    }
+}
diff --git a/tests/tests/test0.scade b/tests/tests/test0.scade
new file mode 100644
index 0000000..a8dddf7
--- /dev/null
+++ b/tests/tests/test0.scade
@@ -0,0 +1,4 @@
+node test0(i: int) returns(probe j: int)
+let
+    j = i;
+tel
diff --git a/tests/tests/test1.scade b/tests/tests/test1.scade
new file mode 100644
index 0000000..db1d6bc
--- /dev/null
+++ b/tests/tests/test1.scade
@@ -0,0 +1,5 @@
+node test1(i: int) returns(probe j: int)
+let
+    assume i_pos : i >= 0;
+    j = i;
+tel
diff --git a/tests/tests/test2.scade b/tests/tests/test2.scade
new file mode 100644
index 0000000..2db6cf5
--- /dev/null
+++ b/tests/tests/test2.scade
@@ -0,0 +1,5 @@
+node test2(i: int) returns(probe j: int)
+let
+    assume i_pos : i >= 0;
+    j = if i < 0 then 42 else 12;
+tel
diff --git a/tests/tests/test3.scade b/tests/tests/test3.scade
new file mode 100644
index 0000000..d133be7
--- /dev/null
+++ b/tests/tests/test3.scade
@@ -0,0 +1,4 @@
+node test3(i: int) returns(probe j: int)
+let
+    j = if i < 0 then -i else i;
+tel
diff --git a/tests/tests/test4.scade b/tests/tests/test4.scade
new file mode 100644
index 0000000..8c5bf2d
--- /dev/null
+++ b/tests/tests/test4.scade
@@ -0,0 +1,4 @@
+node test4() returns(probe j: int)
+let
+    j = 0 -> (if pre j > 10 then 0 else pre j + 1);
+tel
diff --git a/tests/tests/test5.scade b/tests/tests/test5.scade
new file mode 100644
index 0000000..403a069
--- /dev/null
+++ b/tests/tests/test5.scade
@@ -0,0 +1,7 @@
+node test5() returns(probe j: int)
+var p: int;
+let
+    p = 0 -> pre j;
+    j = if p > 10 then 0 else p + 1;
+tel
+
diff --git a/tests/tests/test6.scade b/tests/tests/test6.scade
new file mode 100644
index 0000000..a8d6cfe
--- /dev/null
+++ b/tests/tests/test6.scade
@@ -0,0 +1,6 @@
+node test6(probe i: int) returns(probe j: int)
+let
+    assume i_bounded : i >= -10 and i <= 10;
+    j = i;
+    guarantee j_eq_i : j = i;
+tel
diff --git a/tests/tests/test7.scade b/tests/tests/test7.scade
new file mode 100644
index 0000000..4bd49b9
--- /dev/null
+++ b/tests/tests/test7.scade
@@ -0,0 +1,4 @@
+node test7() returns(probe c: int)
+let
+    c = 0 -> (pre c + 1);
+tel
diff --git a/tests/train.scade b/tests/train.scade
new file mode 100644
index 0000000..d91df01
--- /dev/null
+++ b/tests/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
+        unless if advance > 10 resume Early;
+        let early = false; tel
+
+        state Early
+        unless if advance = 0 resume NotEarly;
+        let early = true; tel
+    returns early;
+
+    automaton
+        initial state NotLate
+        unless if advance < -10 resume Late;
+        let late = false; tel
+
+        state Late
+        unless if advance = 0 resume NotLate;
+        let late = true; tel
+    returns late;
+tel
+
+node observer(early, late: bool) returns (alarm: bool)
+var ontime: bool;
+let
+    ontime = not (late or early);
+    automaton
+        initial state Ok
+        unless if early resume Early;
+        let alarm = false; tel
+
+        state Early
+        unless if ontime resume Ok;
+        let alarm = late; tel
+    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/updown.scade b/tests/updown.scade
new file mode 100644
index 0000000..02e2029
--- /dev/null
+++ b/tests/updown.scade
@@ -0,0 +1,30 @@
+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
+            do guarantee x_up : x = bound;
+            resume DOWN;
+
+        state DOWN
+        let x = last_x - 1; tel
+        until if x <= -bound
+            do guarantee x_down : 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