heptagon/test/sdc/tracking.ept

155 lines
4.2 KiB
Text
Raw Normal View History

type level = None | Low | Normal | High | Bad
type elevel = Zero| Un | Deux | Trois | Quatre | Cinq
type wSize = NonW | Norm | Larg
node metrics(input :level) returns (st :level)
let
automaton
state Normal
do st = Normal;
unless (input = Low) then Low
| (input = High) then High
| (input = Bad) then Bad
state High
do st = High;
unless (input = Low) then Low
| (input = Normal) then Normal
| (input = Bad) then Bad
state Low
do st = Low;
unless (input = Normal) then Normal
| (input = High) then High
| (input = Bad) then Bad
state Bad
do st = Bad;
unless (input = Low) then Low
| (input = High) then High
| (input = Normal) then Normal
end
tel
node trackeur (s, c1, c2, e : bool) returns (res: int; wEx: elevel; win : wSize; running : bool)
let
automaton
state Off
do res = 0;
wEx = Zero;
win = NonW;
running = false;
unless (s & c1) then Untrackeur_nf
| (s & c2) then Untrackeur_lf
state Untrackeur_nf
do res = 1;
wEx = Cinq;
win = Norm;
running = true;
unless (e) then Off
| (not c1 & c2) then Untrackeur_lf
state Untrackeur_lf
do res = 2;
wEx = Quatre;
win = Larg;
running = true;
unless (e) then Off
| (c1 & not c2) then Untrackeur_nf
end
tel
node tracking(i_objvt, i_deadline, i_indice :level; s, e : bool)
returns (objectives:bool; st_objvt, st_deadline, st_indice :level; res: int; wEx: elevel; win : wSize; running : bool)
contract
assume true
enforce objectives
with ( c3, c1, c2 :bool)
var increase_window_size, speed_up:bool;
sst_objvt, sst_deadline : level;
winbis : wSize;
wExbis : elevel;
st_objvtbis, st_deadlinebis : level;
let
st_objvt = st_objvtbis;
st_deadline = st_deadlinebis;
sst_objvt = (None fby st_objvtbis) ;
sst_deadline = (None fby st_deadlinebis);
increase_window_size = (not (st_objvtbis = High & not ((NonW fby winbis) = NonW)) or not (winbis = Norm));
speed_up = (not (st_deadlinebis = Low & ((Zero fby wExbis) = Cinq)) or not (wExbis = Cinq)) &
(not (st_deadlinebis = Low & ((Zero fby wExbis) = Quatre)) or not (wExbis = Cinq));
objectives = (speed_up) & increase_window_size;
st_objvtbis = inlined metrics(i_objvt);
st_deadlinebis = inlined metrics(i_deadline);
st_indice = inlined metrics(i_indice);
(res, wExbis, winbis, running) = inlined trackeur (s, c1, c2, e);
win = winbis;
wEx = wExbis;
tel
2017-03-05 23:55:07 +01:00
(* CHECK main *)
node main() = (ok:bool)
var i_objvt, i_deadline, i_indice :level; s, e : bool;
objectives:bool; st_objvt, st_deadline, st_indice :level; res: int; wEx: elevel; win : wSize; running : bool;
l : int;
let
(objectives,st_objvt,st_deadline,st_indice,res,wEx,win,running) = tracking(i_objvt,i_deadline,i_indice,s,e);
i_objvt = None fby None fby High fby None fby Bad fby None fby None fby Low fby None fby Low fby None fby Normal fby None fby i_objvt;
i_deadline = None fby Normal fby None fby None fby Normal fby None fby High fby None fby Low fby None fby None fby Bad fby None fby None fby None fby High fby None fby i_deadline;
i_indice = None fby None fby None fby Normal fby High fby Low fby None fby None fby Bad fby Bad fby None fby i_indice;
l = 0 fby (if l = 17 then 0 else l + 1);
s = (l = 7);
e = (l = 17);
ok = objectives;
tel
(*
reax -s -a 'sB:d={P:D}' --triang tracking_ctrln/tracking.ctrln
./clean
clear && heptc -hepts -s tracking -target c -target ctrln tracking.ept
reax -a 'sS:d={I:D}' --triang tracking_ctrln/tracking.ctrln && ctrl2ept -n Tracking.tracking
heptc -target c tracking_controller.ept
PDW=$(pwd)
gcc -o sim -I/home/ctrl-a/.opam/4.02.3/lib/heptagon/c/ -I$PDW/tracking_c -I$PDW/tracking_controller_c -I$PDW/tracking_c tracking_c/_main.c tracking_c/tracking.c tracking_c/tracking_types.c tracking_controller_c/tracking_controller.c tracking_controller_c/tracking_controller_types.c
hepts -mod Tracking -node tracking -exec ./sim
PDW=$(pwd)
gcc -o sim -I/home/ctrl-a/.opam/4.02.3/lib/heptagon/c/ -I$PDW/tracking_c -I$PDW/tracking_c tracking_c/_main.c tracking_c/tracking.c tracking_c/tracking_types.c
hepts -mod tracking -node tracking -exec ./sim
*)