diff options
| -rw-r--r-- | .gitignore | 7 | ||||
| -rw-r--r-- | tests/Makefile | 4 | ||||
| -rw-r--r-- | tests/count.scade | 36 | ||||
| -rw-r--r-- | tests/limiter.scade | 21 | ||||
| -rw-r--r-- | tests/merge.scade | 22 | ||||
| -rw-r--r-- | tests/test.c | 21 | ||||
| -rw-r--r-- | tests/tests/test0.scade | 4 | ||||
| -rw-r--r-- | tests/tests/test1.scade | 5 | ||||
| -rw-r--r-- | tests/tests/test2.scade | 5 | ||||
| -rw-r--r-- | tests/tests/test3.scade | 4 | ||||
| -rw-r--r-- | tests/tests/test4.scade | 4 | ||||
| -rw-r--r-- | tests/tests/test5.scade | 7 | ||||
| -rw-r--r-- | tests/tests/test6.scade | 6 | ||||
| -rw-r--r-- | tests/tests/test7.scade | 4 | ||||
| -rw-r--r-- | tests/train.scade | 69 | ||||
| -rw-r--r-- | tests/updown.scade | 30 |
16 files changed, 248 insertions, 1 deletions
@@ -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 |