jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Logico-numerical DCS example

Browse source
This commit is contained in:
Gwenaël Delaval 2017-03-16 11:59:47 +01:00
parent f284ff2872
commit 5440bb3129
2 changed files with 25 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
examples/lnum/build.sh Executable file
View file

@ -0,0 +1 @@
bzreax lnum_simple.ept tasks -a sS:d={P:D} -s

24
examples/lnum/lnum_simple.ept Normal file
View file

@ -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