summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-04 16:21:45 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-04 16:21:45 +0200
commitb1cdf90995c8f70e4a450b3319a136f0d50515d0 (patch)
tree9074c54967f384fac8d41359a503774158081ac9 /tests
parent1445a2be1e1bd81efa552230a0f11672aa20a92c (diff)
downloadscade-analyzer-b1cdf90995c8f70e4a450b3319a136f0d50515d0.tar.gz
scade-analyzer-b1cdf90995c8f70e4a450b3319a136f0d50515d0.zip
New example ; minor fixes.
Diffstat (limited to 'tests')
-rw-r--r--tests/source/NestedControl.scade8
-rw-r--r--tests/source/counters.scade38
-rw-r--r--tests/source/test5.scade4
3 files changed, 44 insertions, 6 deletions
diff --git a/tests/source/NestedControl.scade b/tests/source/NestedControl.scade
index 2551eb6..af4fdab 100644
--- a/tests/source/NestedControl.scade
+++ b/tests/source/NestedControl.scade
@@ -1,13 +1,13 @@
node root(In : int; C : bool) returns (Out, Out1 : int)
var last_Out, last_Out1: int;
- isp, isn: bool;
+ disj, disj2: bool;
let
last_Out = 0 -> pre Out;
last_Out1 = 0 -> pre Out1;
- isp = In > 0;
- isn = In < 0;
- assume C_in_not_null: (not C) or isp or isn;
+ disj = In > 0;
+ disj2 = In < 0;
+ assume C_in_not_null: (not C) or disj or disj2;
automaton SM1
initial state State1
diff --git a/tests/source/counters.scade b/tests/source/counters.scade
new file mode 100644
index 0000000..334bca1
--- /dev/null
+++ b/tests/source/counters.scade
@@ -0,0 +1,38 @@
+/*
+ x = 10 | 9 | 8 | 7 | 6 | 5 | ... | 0 | 1 | 2 | ... | 10 | ...
+ y = 0 | 1 | 2 | 3 | 4 | 5 | ... | 10 | 9 | 8 | ... | 0 | ...
+
+ b1 = t | f | f | f | f | f | ... | f | f | f | ... | t | ...
+ b2 = t | f | f | f | f | f | ... | f | f | f | ... | t | ...
+
+ eq* = t | t | t | t | t | t | ... | t | t | t | ... | t | ...
+*/
+
+
+-- type t2 = subrange [0,10] of int;
+
+const bound: int = 1000;
+
+node counters(z: bool) returns (eq_nind : bool ; probe x, probe y : int)
+var
+ b1, b2 : bool;
+ a, b : bool;
+let
+
+ a = false -> (if pre a then pre x < bound else pre x <= 0);
+ --a = false -> pre(if a then x < bound else x <= 0);
+ x = bound -> (if a then pre x + 1 else pre x - 1);
+
+ b = true -> (if pre b then pre y < bound else pre y <= 0);
+ --b = true -> pre(if b then y < bound else y <= 0);
+ y = 0 -> (if b then pre y + 1 else pre y - 1);
+
+ b1 = x=bound;
+ b2 = y=0;
+
+
+ guarantee xy : x+y = bound;
+ guarantee bb : b1 = b2;
+ guarantee rp : -bound <= (x-y) and (x-y) <= bound;
+
+tel
diff --git a/tests/source/test5.scade b/tests/source/test5.scade
index 1de390d..566acf0 100644
--- a/tests/source/test5.scade
+++ b/tests/source/test5.scade
@@ -1,8 +1,8 @@
-node test(i: int) returns(probe a, b, c: int; exit: bool)
+node test(i: int) returns(probe a, probe b, probe c: int; exit: bool)
let
b = 0 -> pre a;
a = if b > 4 then 0 else b + 1;
- c = 0;
+ c = i;
exit = i >= 10;
tel