diff options
author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-08 18:03:14 +0200 |
---|---|---|
committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-08 18:03:14 +0200 |
commit | 4ecc11528b3490df5e2b8ea2c602d291b19c6bf0 (patch) | |
tree | eba009eb4d6023b4a19af0a43298aae98e03dfb7 /tests/source | |
parent | d6db8e934346d3a4ff2bb1470a9512462419bf03 (diff) | |
download | scade-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.scade | 28 |
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 + |