diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/source/cdrom.scade | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/tests/source/cdrom.scade b/tests/source/cdrom.scade new file mode 100644 index 0000000..92438c3 --- /dev/null +++ b/tests/source/cdrom.scade @@ -0,0 +1,19 @@ +node cdrom(speed: int) returns (plus, minus, error: bool) +var ps, count: int; +let + ps = 0 -> pre speed; + + assume h1 : speed - ps <= 4 and speed - ps >= -4; + assume h2 : if (false -> pre plus) then (speed - ps > 0) + else if (false -> pre minus) then (speed - ps < 0) + else true; + + plus = (ps <= 9); + minus = (ps >= 11); + + 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); +tel |