From 68fef7a9612cf42ba42d9ca1cc2423556f66b461 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Thu, 12 Jun 2014 16:42:25 +0200 Subject: Working prototype for an interpret ! But very messy. --- tests/tests/test0.scade | 7 +++++-- tests/tests/test1.scade | 7 +++++-- tests/tests/test2.scade | 7 +++++-- tests/tests/test3.scade | 7 +++++-- tests/tests/test4.scade | 7 +++++-- tests/tests/test5.scade | 9 +++++---- tests/tests/test6.scade | 9 ++++++--- tests/tests/test7.scade | 5 ++++- tests/tests/testc.scade | 11 +++++++++++ tests/updown.scade | 10 +++------- 10 files changed, 54 insertions(+), 25 deletions(-) create mode 100644 tests/tests/testc.scade (limited to 'tests') diff --git a/tests/tests/test0.scade b/tests/tests/test0.scade index a8dddf7..3d03be5 100644 --- a/tests/tests/test0.scade +++ b/tests/tests/test0.scade @@ -1,4 +1,7 @@ -node test0(i: int) returns(probe j: int) +node test(i: int) returns(probe a, b, c: int; exit: bool) let - j = i; + exit = i >= 5; + a = i; + b = 0; + c = 0; tel diff --git a/tests/tests/test1.scade b/tests/tests/test1.scade index db1d6bc..350b920 100644 --- a/tests/tests/test1.scade +++ b/tests/tests/test1.scade @@ -1,5 +1,8 @@ -node test1(i: int) returns(probe j: int) +node test(i: int) returns(probe a, b, c: int; exit: bool) let assume i_pos : i >= 0; - j = i; + exit = i >= 5; + a = i; + b = 0; + c = 0; tel diff --git a/tests/tests/test2.scade b/tests/tests/test2.scade index 2db6cf5..1777689 100644 --- a/tests/tests/test2.scade +++ b/tests/tests/test2.scade @@ -1,5 +1,8 @@ -node test2(i: int) returns(probe j: int) +node test(i: int) returns(probe a, b, c: int; exit: bool) let assume i_pos : i >= 0; - j = if i < 0 then 42 else 12; + exit = i >= 5; + a = if i < 0 then 42 else 12; + b = 0; + c = 0; tel diff --git a/tests/tests/test3.scade b/tests/tests/test3.scade index d133be7..9380a49 100644 --- a/tests/tests/test3.scade +++ b/tests/tests/test3.scade @@ -1,4 +1,7 @@ -node test3(i: int) returns(probe j: int) +node test(i: int) returns(probe a, b, c: int; exit: bool) let - j = if i < 0 then -i else i; + exit = i >= 5; + a = if i < 0 then -i else i; + b = 0; + c = 0; tel diff --git a/tests/tests/test4.scade b/tests/tests/test4.scade index 8c5bf2d..c66a56f 100644 --- a/tests/tests/test4.scade +++ b/tests/tests/test4.scade @@ -1,4 +1,7 @@ -node test4() returns(probe j: int) +node test(i: int) returns(probe a, b, c: int; exit: bool) let - j = 0 -> (if pre j > 10 then 0 else pre j + 1); + 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/tests/test5.scade b/tests/tests/test5.scade index 403a069..1de390d 100644 --- a/tests/tests/test5.scade +++ b/tests/tests/test5.scade @@ -1,7 +1,8 @@ -node test5() returns(probe j: int) -var p: int; +node test(i: int) returns(probe a, b, c: int; exit: bool) let - p = 0 -> pre j; - j = if p > 10 then 0 else p + 1; + b = 0 -> pre a; + a = if b > 4 then 0 else b + 1; + c = 0; + exit = i >= 10; tel diff --git a/tests/tests/test6.scade b/tests/tests/test6.scade index a8d6cfe..574e271 100644 --- a/tests/tests/test6.scade +++ b/tests/tests/test6.scade @@ -1,6 +1,9 @@ -node test6(probe i: int) returns(probe j: int) +node test(probe i: int) returns(probe a, b, c: int; exit: bool) let assume i_bounded : i >= -10 and i <= 10; - j = i; - guarantee j_eq_i : j = i; + a = i; + guarantee a_eq_i : a = i; + b = 0; + c = 0; + exit = i >= 5; tel diff --git a/tests/tests/test7.scade b/tests/tests/test7.scade index 4bd49b9..c756a9e 100644 --- a/tests/tests/test7.scade +++ b/tests/tests/test7.scade @@ -1,4 +1,7 @@ -node test7() returns(probe c: int) +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/tests/testc.scade b/tests/tests/testc.scade new file mode 100644 index 0000000..7c99b32 --- /dev/null +++ b/tests/tests/testc.scade @@ -0,0 +1,11 @@ +const x : int = 12; +const y : int = z + 3; +const z : int = x * 2; + +node test(i: int) returns (a, b, c: int; exit: bool) +let + exit = true; + a = x; + b = y; + c = z; +tel diff --git a/tests/updown.scade b/tests/updown.scade index 02e2029..089293a 100644 --- a/tests/updown.scade +++ b/tests/updown.scade @@ -4,19 +4,15 @@ node updown() returns(probe x: int) var last_x: int; let last_x = 0 -> pre x; - guarantee x_bounded : x >= -bound and x <= bound; + 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; + until if x >= bound resume DOWN; state DOWN let x = last_x - 1; tel - until if x <= -bound - do guarantee x_down : x = -bound; - resume UP; + until if x <= -bound resume UP; returns x; tel -- cgit v1.2.3