summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-11 14:50:18 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-11 14:50:18 +0200
commitfd027ca593bdfb2d2db811730521b4f5d52c8593 (patch)
tree94982e74c74a480e9bafd235101d1934a330439e /tests
parent9ca8bcb35eb0385c8f9852045bb282c445bd6901 (diff)
downloadscade-analyzer-fd027ca593bdfb2d2db811730521b4f5d52c8593.tar.gz
scade-analyzer-fd027ca593bdfb2d2db811730521b4f5d52c8593.zip
Acceptable heuristic.
Diffstat (limited to 'tests')
-rw-r--r--tests/source/cdrom.scade19
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