diff --git a/examples/lnum/build.sh b/examples/lnum/build.sh new file mode 100755 index 0000000..623c0be --- /dev/null +++ b/examples/lnum/build.sh @@ -0,0 +1 @@ +bzreax lnum_simple.ept tasks -a sS:d={P:D} -s diff --git a/examples/lnum/lnum_simple.ept b/examples/lnum/lnum_simple.ept new file mode 100644 index 0000000..96eb6c3 --- /dev/null +++ b/examples/lnum/lnum_simple.ept @@ -0,0 +1,24 @@ +(* SDC sS:d={P:D} *) + +node f(x:int) = (y:int) + contract + assume x >= 10 + enforce y <= x + with (c:bool) +let + y = 0 -> if c then pre y + 1 else 0; +tel + + +node tasks(nb_req, ended : int) = (waiting, active : int) + contract + assume (nb_req >= 0) & (ended <= (0 fby active)) & (ended >= 0) + enforce (active <= 10) + with (act : bool) +var activated : int; +let + waiting = (0 -> pre waiting) + nb_req - activated; + activated = 0 -> if (pre waiting > 0) & act then 1 else 0; + active = (0 -> pre active) + activated - ended; +tel +