summaryrefslogtreecommitdiff
path: root/tests/source
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-08 18:03:14 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-08 18:03:14 +0200
commit4ecc11528b3490df5e2b8ea2c602d291b19c6bf0 (patch)
treeeba009eb4d6023b4a19af0a43298aae98e03dfb7 /tests/source
parentd6db8e934346d3a4ff2bb1470a9512462419bf03 (diff)
downloadscade-analyzer-4ecc11528b3490df5e2b8ea2c602d291b19c6bf0.tar.gz
scade-analyzer-4ecc11528b3490df5e2b8ea2c602d291b19c6bf0.zip
Correct some bugs on clocks.
Diffstat (limited to 'tests/source')
-rw-r--r--tests/source/two_counters.scade28
1 files changed, 28 insertions, 0 deletions
diff --git a/tests/source/two_counters.scade b/tests/source/two_counters.scade
new file mode 100644
index 0000000..7970aab
--- /dev/null
+++ b/tests/source/two_counters.scade
@@ -0,0 +1,28 @@
+const n1: int = 10;
+const n2: int = 6;
+
+
+node top(a,b,c : bool) returns (ok, r1, r2 : bool)
+var
+ x, y, pre_x, pre_y: int;
+ o1, o2: bool;
+
+ m: bool;
+let
+ x = if (b or c) then 0 else (if (a and pre_x < n1) then pre_x + 1 else pre_x);
+ y = if (c) then 0 else (if (a and pre_y < n2) then pre_y + 1 else pre_y);
+ o1= x = n1;
+ o2= y = n2;
+ ok= if o1 then o2 else true;
+ r1 = 0<=x and x<=n1;
+ r2 = 0<=y and y<=n2;
+ pre_x = 0 -> pre(x);
+ pre_y = 0 -> pre(y);
+
+ m = true -> pre o2;
+
+ guarantee g1: ok;
+ guarantee g2: r1;
+ guarantee g3: r2;
+tel
+