diff options
| author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-11 16:59:13 +0200 |
|---|---|---|
| committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-11 16:59:13 +0200 |
| commit | 29e7daea2d613f1a3b375934446f7f9b6c489021 (patch) | |
| tree | 83c58b001d35d91a05afe563952f4d4dc6b612aa /tests | |
| parent | fd027ca593bdfb2d2db811730521b4f5d52c8593 (diff) | |
| download | scade-analyzer-29e7daea2d613f1a3b375934446f7f9b6c489021.tar.gz scade-analyzer-29e7daea2d613f1a3b375934446f7f9b6c489021.zip | |
DOES NOT WORK AT ALL
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/source/cdrom.scade | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/tests/source/cdrom.scade b/tests/source/cdrom.scade index 92438c3..03501d5 100644 --- a/tests/source/cdrom.scade +++ b/tests/source/cdrom.scade @@ -1,5 +1,6 @@ -node cdrom(speed: int) returns (plus, minus, error: bool) +node cdrom(probe speed: int) returns (plus, minus, error: bool) var ps, count: int; + _a, _b, _la, _lb: bool; let ps = 0 -> pre speed; @@ -11,9 +12,14 @@ let plus = (ps <= 9); minus = (ps >= 11); + _a = speed < 8; + _b = speed > 12; + _la = true -> pre _a; + _lb = false -> pre _b; + count = if speed < 8 or speed > 12 then (0 -> pre count) + 1 else 0; error = (count >= 15); - guarantee g: not error and (true -> not pre error); + guarantee g: not error; tel |