diff options
| author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-09 15:32:28 +0200 |
|---|---|---|
| committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-09 15:32:28 +0200 |
| commit | bc9ad2280839677bb46acfd846ff05bb37719b6e (patch) | |
| tree | 238de281268baef8399d52c7315eb618b7e120d9 /tests/source | |
| parent | 52a7d356a1c1c1bf0d1881d0cf6e13bb94dbc1a4 (diff) | |
| download | scade-analyzer-bc9ad2280839677bb46acfd846ff05bb37719b6e.tar.gz scade-analyzer-bc9ad2280839677bb46acfd846ff05bb37719b6e.zip | |
Begin dynamic partitionning ; CORRECT BUG IN unpass_cycle !!
Diffstat (limited to 'tests/source')
| -rw-r--r-- | tests/source/two_counters.scade | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/tests/source/two_counters.scade b/tests/source/two_counters.scade index 7970aab..6468523 100644 --- a/tests/source/two_counters.scade +++ b/tests/source/two_counters.scade @@ -1,5 +1,5 @@ -const n1: int = 10; -const n2: int = 6; +const n1: int = 100; +const n2: int = 60; node top(a,b,c : bool) returns (ok, r1, r2 : bool) @@ -7,12 +7,12 @@ var x, y, pre_x, pre_y: int; o1, o2: bool; - m: bool; + m, n, lb: 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; + 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; @@ -20,6 +20,8 @@ let pre_y = 0 -> pre(y); m = true -> pre o2; + n = true -> pre o1; + lb = true -> pre b; guarantee g1: ok; guarantee g2: r1; |