Acceptable heuristic.

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