From fd027ca593bdfb2d2db811730521b4f5d52c8593 Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ansys.com>
Date: Fri, 11 Jul 2014 14:50:18 +0200
Subject: Acceptable heuristic.

---
 tests/source/cdrom.scade | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 tests/source/cdrom.scade

(limited to 'tests/source/cdrom.scade')

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
-- 
cgit v1.2.3