diff options
Diffstat (limited to 'tests')
-rw-r--r-- | tests/source/jeannet.scade | 16 |
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 |