summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/source/jeannet.scade16
1 files changed, 16 insertions, 0 deletions
diff --git a/tests/source/jeannet.scade b/tests/source/jeannet.scade
new file mode 100644
index 0000000..9fca060
--- /dev/null
+++ b/tests/source/jeannet.scade
@@ -0,0 +1,16 @@
+node test() returns(x, y, probe z: int; a, b: bool)
+var px, py: int;
+let
+ a = false -> pre b;
+ b = true -> not pre a;
+
+ px = pre x;
+ py = pre y;
+
+ x = 0 -> (if a = b then px + 1 else px);
+ y = 0 -> (if a = b then py else py + 1);
+
+ z = x - y;
+
+ guarantee g1: x >= y;
+tel