From dedc98b0c14262c53e8573d7fe1dcaa370e43fb5 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Fri, 13 Jun 2014 14:17:22 +0200 Subject: Move a lot of things. --- tests/source/limiter.scade | 21 ++++++++++++++ tests/source/limitera.scade | 26 +++++++++++++++++ tests/source/locals.scade | 20 +++++++++++++ tests/source/test0.scade | 7 +++++ tests/source/test1.scade | 8 ++++++ tests/source/test2.scade | 8 ++++++ tests/source/test3.scade | 7 +++++ tests/source/test4.scade | 7 +++++ tests/source/test5.scade | 8 ++++++ tests/source/test6.scade | 9 ++++++ tests/source/test7.scade | 7 +++++ tests/source/testc.scade | 11 ++++++++ tests/source/train.scade | 69 +++++++++++++++++++++++++++++++++++++++++++++ tests/source/updown.scade | 26 +++++++++++++++++ 14 files changed, 234 insertions(+) create mode 100644 tests/source/limiter.scade create mode 100644 tests/source/limitera.scade create mode 100644 tests/source/locals.scade create mode 100644 tests/source/test0.scade create mode 100644 tests/source/test1.scade create mode 100644 tests/source/test2.scade create mode 100644 tests/source/test3.scade create mode 100644 tests/source/test4.scade create mode 100644 tests/source/test5.scade create mode 100644 tests/source/test6.scade create mode 100644 tests/source/test7.scade create mode 100644 tests/source/testc.scade create mode 100644 tests/source/train.scade create mode 100644 tests/source/updown.scade (limited to 'tests/source') 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 -- cgit v1.2.3