Examples with contracts and sdc for tests
This commit is contained in:
Gwenaël Delaval
parent
ace152e096
commit
7bc5e4c115
3 changed files with 537 additions and 0 deletions
39
test/sdc/modular.ept
Normal file
39
test/sdc/modular.ept
Normal file
|
|
@ -0,0 +1,39 @@
|
|||
type t = Haut | Bas
|
||||
|
||||
node f(x:bool;r:t) = (y:bool)
|
||||
contract
|
||||
enforce (y)
|
||||
with (c:bool)
|
||||
|
||||
let
|
||||
|
||||
automaton
|
||||
state Haut
|
||||
do
|
||||
y = true;
|
||||
unless (r=Bas) & c then Bas
|
||||
|
|
||||
state Bas
|
||||
do
|
||||
y = false
|
||||
unless (r=Haut) or c then Haut
|
||||
end;
|
||||
y =
|
||||
tel
|
||||
|
||||
node g(u,v:bool;m :t) = (z:bool)
|
||||
contract
|
||||
enforce z
|
||||
with (c,d:bool)
|
||||
let
|
||||
z = f(u & c, m)
|
||||
tel
|
||||
|
||||
node main() = (ok:bool)
|
||||
var u : bool;
|
||||
m : t;
|
||||
let
|
||||
u = false fby true fby true fby u;
|
||||
m = Haut fby Bas fby m;
|
||||
ok = g(u,u,m);
|
||||
tel
|
||||
358
test/sdc/office.ept
Normal file
358
test/sdc/office.ept
Normal file
|
|
@ -0,0 +1,358 @@
|
|||
(*-----------------TYPES DECLARATION ------------------*)
|
||||
|
||||
type command = Open|Close|SwitchOn|SwitchOff|Cool|Heat|SwitchMode1|SwitchMode2|Nothing
|
||||
type deviceState = On|Off|Closed|Opened|HalfOpened|Cooling|Heating|Mode1|Mode2
|
||||
|
||||
|
||||
|
||||
(*-----------------SHUTTER AUTOMATON ------------------*)
|
||||
|
||||
|
||||
node shutter(copen:bool;outdoorlum:int) returns (cmd:command;shutterlum:int;air:bool;shutterstate:deviceState)
|
||||
|
||||
let
|
||||
|
||||
automaton
|
||||
|
||||
state Closed
|
||||
do
|
||||
cmd = Close -> Nothing;
|
||||
shutterlum = 0;
|
||||
air = false;
|
||||
shutterstate = Closed;
|
||||
unless not copen then Opened
|
||||
|
||||
|
||||
state Opened
|
||||
do
|
||||
cmd = Open -> Nothing;
|
||||
shutterlum = outdoorlum;
|
||||
air = true;
|
||||
shutterstate = Opened;
|
||||
unless not copen then Closed
|
||||
|
||||
end
|
||||
|
||||
tel
|
||||
|
||||
|
||||
|
||||
(*-----------------LAMP AUTOMATON ---------------------*)
|
||||
|
||||
|
||||
node lamp(coff:bool) returns (cmd:command;lumlamp:int;lampstate:deviceState)
|
||||
|
||||
let
|
||||
|
||||
automaton
|
||||
|
||||
state Off
|
||||
|
||||
do
|
||||
cmd = SwitchOff -> Nothing;
|
||||
lumlamp = 0;
|
||||
lampstate = Off;
|
||||
unless not coff then On
|
||||
|
||||
state On
|
||||
|
||||
do
|
||||
cmd = SwitchOn -> Nothing;
|
||||
lumlamp = 500;
|
||||
lampstate = On;
|
||||
unless coff then Off
|
||||
|
||||
end
|
||||
|
||||
tel
|
||||
|
||||
|
||||
(*-----------------WINDOW AUTOMATON ------------------*)
|
||||
|
||||
|
||||
node window(copen:bool;iCO2,itemp,oCO2,otemp,onoise,opollen:int;air:bool) returns (cmd:command;ventil,heat,cool,poll:bool;winoise:int;wistate:deviceState)
|
||||
|
||||
let
|
||||
|
||||
automaton
|
||||
|
||||
state Closed
|
||||
do
|
||||
cmd = Close -> Nothing;
|
||||
ventil = false;
|
||||
heat = false;
|
||||
cool = false;
|
||||
poll = false;
|
||||
winoise = 0;
|
||||
wistate = Closed;
|
||||
unless not copen then Opened
|
||||
|
||||
state Opened
|
||||
do
|
||||
cmd = Open -> Nothing;
|
||||
if air & itemp > otemp & not poll then ventil = true else ventil = false end;
|
||||
if air & otemp > itemp then heat = true else heat = false end;
|
||||
if air & otemp < itemp then cool = true else cool = false end;
|
||||
if air & oCO2 > iCO2 or opollen > 80 then poll = true else poll = false end;
|
||||
winoise = onoise;
|
||||
wistate = Opened;
|
||||
unless not copen then Closed
|
||||
|
||||
end
|
||||
|
||||
tel
|
||||
|
||||
|
||||
(*-----------------RAC AUTOMATON ------------------*)
|
||||
|
||||
|
||||
node rac(coff,cheat,ccool:bool) returns (cmd:command;cool,heat:bool;racstate:deviceState)
|
||||
|
||||
let
|
||||
|
||||
automaton
|
||||
|
||||
state Off
|
||||
|
||||
do
|
||||
cmd = SwitchOff -> Nothing;
|
||||
cool = false;
|
||||
heat = false;
|
||||
racstate = Off;
|
||||
|
||||
unless not ccool then Cooling
|
||||
|not cheat then Heating
|
||||
|
||||
state Cooling
|
||||
|
||||
do
|
||||
cmd = Cool -> Nothing;
|
||||
cool = true;
|
||||
heat = false;
|
||||
racstate = Cooling;
|
||||
|
||||
unless coff then Off
|
||||
|not cheat then Heating
|
||||
|
||||
|
||||
state Heating
|
||||
|
||||
do
|
||||
cmd = Heat -> Nothing;
|
||||
cool = false;
|
||||
heat = true;
|
||||
racstate = Heating;
|
||||
|
||||
unless coff then Off
|
||||
|not ccool then Cooling
|
||||
|
||||
end
|
||||
tel
|
||||
|
||||
(*-----------------VMC AUTOMATON ------------------*)
|
||||
|
||||
|
||||
node vmc(coff,cmode1,cmode2:bool) returns (cmd:command;ventil,quick:bool;vmcstate:deviceState)
|
||||
|
||||
let
|
||||
|
||||
automaton
|
||||
|
||||
state Off
|
||||
|
||||
do
|
||||
cmd = SwitchOff -> Nothing;
|
||||
ventil = false;
|
||||
quick = false;
|
||||
vmcstate = Off;
|
||||
unless not cmode1 then Mode1
|
||||
|not cmode2 then Mode2
|
||||
|
||||
state Mode1
|
||||
|
||||
do
|
||||
cmd = SwitchMode1 -> Nothing;
|
||||
ventil = true;
|
||||
quick = false;
|
||||
vmcstate = Mode1;
|
||||
unless coff then Off
|
||||
|not cmode2 then Mode2
|
||||
|
||||
state Mode2
|
||||
|
||||
do
|
||||
cmd = SwitchMode2 -> Nothing;
|
||||
ventil = true;
|
||||
quick = true;
|
||||
vmcstate = Mode2;
|
||||
unless coff then Off
|
||||
|not cmode1 then Mode1
|
||||
|
||||
end
|
||||
tel
|
||||
|
||||
|
||||
|
||||
(*-----------------DOOR AUTOMATON ------------------*)
|
||||
|
||||
|
||||
node door(cclose:bool;cnoise:int) returns (cmd:command;noise:int;doorstate:deviceState)
|
||||
|
||||
let
|
||||
|
||||
automaton
|
||||
|
||||
state Closed
|
||||
do
|
||||
cmd = Close -> Nothing;
|
||||
noise = 0;
|
||||
doorstate = Closed;
|
||||
unless not cclose then Opened
|
||||
|
||||
state Opened
|
||||
do
|
||||
cmd = Open -> Nothing;
|
||||
noise = cnoise;
|
||||
doorstate = Opened;
|
||||
unless cclose then Closed
|
||||
|
||||
end
|
||||
|
||||
tel
|
||||
|
||||
|
||||
(*-----------------Agenda AUTOMATON ------------------*)
|
||||
|
||||
|
||||
|
||||
node agenda(begin:bool;nextmeetingtime:int) returns (between2meetings:bool)
|
||||
|
||||
let
|
||||
|
||||
automaton
|
||||
state NoMeeting
|
||||
do
|
||||
between2meetings = false;
|
||||
unless begin then Meeting
|
||||
|
||||
state Meeting
|
||||
do
|
||||
between2meetings = false;
|
||||
unless not begin & nextmeetingtime > 30 then NoMeeting
|
||||
| not begin & nextmeetingtime <= 30 then Between2Meetings
|
||||
|
||||
state Between2Meetings
|
||||
do
|
||||
between2meetings = true;
|
||||
unless begin then Meeting
|
||||
|
||||
end
|
||||
|
||||
tel
|
||||
|
||||
(*-----------------LUMINOSITY NODE ---------------------*)
|
||||
|
||||
|
||||
node luminosity(presence:bool;olum:int;cconfidential:bool) returns (shutterCmd,lampCmd:command;shutterair,shutterclosed,proplumin:bool)
|
||||
|
||||
contract
|
||||
var propconf:bool;
|
||||
let
|
||||
propconf = (false fby not cconfidential) or shutterclosed;
|
||||
tel
|
||||
assume true
|
||||
enforce proplumin & propconf
|
||||
with (copen_shutter,coff_lamp:bool)
|
||||
|
||||
var shutterlum,lamplum,lum:int;
|
||||
shutterst,lampst:deviceState;
|
||||
proplum,propconfmeeting:bool;
|
||||
|
||||
let
|
||||
lum = shutterlum + lamplum;
|
||||
shutterclosed = (shutterst = Closed);
|
||||
|
||||
(shutterCmd,shutterlum,shutterair,shutterst) = inlined shutter(copen_shutter,olum);
|
||||
(lampCmd,lamplum,lampst) = inlined lamp(coff_lamp);
|
||||
proplum = not presence or (lum >= 500 & lum <= 600);
|
||||
propconfmeeting = not cconfidential or (shutterst = Closed);
|
||||
proplumin = proplum & propconfmeeting;
|
||||
|
||||
tel
|
||||
|
||||
|
||||
|
||||
(*----------------- TEMPERATURE AIR QUALITY AND NOISE NODE-------------------*)
|
||||
|
||||
|
||||
node tempairnoise(presence:bool;itemp,iCO2,otemp,oCO2,onoise,opollen,cnoise:int;shutterair,startmeeting:bool;nextmeetingtime:int;cconfidential:bool) returns (windowCmd,doorCmd,vmcCmd,racCmd:command;windoorclosed,prop:bool)
|
||||
|
||||
contract
|
||||
var propconfmeeting:bool;
|
||||
let
|
||||
propconfmeeting = (false fby not cconfidential) or windoorclosed;
|
||||
tel
|
||||
assume true
|
||||
enforce prop & propconfmeeting
|
||||
with (copen_window,coff_rac, ccool, cheat, coff_vmc, cmode1, cmode2, cclose_door:bool)
|
||||
|
||||
var windownoise,doornoise:int;
|
||||
wincool,winheat,winventil,pollution:bool;
|
||||
raccool,racheat,vmcventil,quickventil:bool;
|
||||
heat,cool,ventilation:bool;
|
||||
between2meetings:bool;
|
||||
windowst,vmcst,racst,doorst:deviceState;
|
||||
propCO2,propnoise,proppoll,proptemp:bool;
|
||||
proptemp1,proptemp2:bool;
|
||||
propbetween2meetings,propconf,propmeeting:bool;
|
||||
|
||||
let
|
||||
|
||||
heat = winheat or racheat;
|
||||
cool = wincool or raccool;
|
||||
ventilation = winventil or vmcventil;
|
||||
windoorclosed = (windowst = Closed & doorst = Closed);
|
||||
|
||||
(windowCmd,winventil,winheat,wincool,pollution,windownoise,windowst) = inlined window(copen_window,iCO2,itemp,oCO2,otemp,onoise,opollen,shutterair);
|
||||
|
||||
(racCmd,raccool,racheat,racst) = inlined rac(coff_rac,cheat,ccool);
|
||||
|
||||
(vmcCmd,vmcventil,quickventil,vmcst) = inlined vmc(coff_vmc,cmode1,cmode2);
|
||||
|
||||
(doorCmd,doornoise,doorst) = inlined door(cclose_door,cnoise);
|
||||
|
||||
between2meetings = inlined agenda(startmeeting,nextmeetingtime);
|
||||
|
||||
prop = propCO2 & propnoise & proppoll & proptemp & propmeeting;
|
||||
|
||||
propCO2 = not (presence & iCO2 >= 800) or ventilation = true;
|
||||
propnoise = not presence or (not (windownoise >=80 or doornoise >=80));
|
||||
proppoll = pollution = false;
|
||||
proptemp = proptemp1 & proptemp2;
|
||||
proptemp1 = not (presence & itemp >= 24) or cool = true;
|
||||
proptemp2 = not (presence & itemp <= 21) or heat = true;
|
||||
propbetween2meetings = not between2meetings or quickventil = true;
|
||||
propconf = not cconfidential or (windowst = Closed & doorst = Closed);
|
||||
propmeeting = propbetween2meetings & propconf;
|
||||
|
||||
tel
|
||||
|
||||
|
||||
(*-------------------OFFICE NODE------------------------------------*)
|
||||
|
||||
|
||||
node office(presence:bool;itemp,iCO2,otemp,oCO2,olum,onoise,opollen,cnoise:int;begin,confidential:bool;nextmtime:int) returns(shutterCmd,windowCmd,doorCmd,lampCmd,vmcCmd,racCmd:command;prop:bool)
|
||||
|
||||
contract
|
||||
assume true
|
||||
enforce prop
|
||||
with (cconfwd,cconfs:bool)
|
||||
|
||||
var wdclosed,sclosed,sh_air:bool;
|
||||
proplumi, proptan:bool;
|
||||
|
||||
let
|
||||
(shutterCmd,lampCmd,sh_air,sclosed,proplumi) = luminosity(presence,olum,cconfs);
|
||||
(windowCmd,doorCmd,vmcCmd,racCmd,wdclosed,proptan) = tempairnoise(presence,itemp,iCO2,otemp,oCO2,onoise,opollen,cnoise,sh_air,begin,nextmtime,cconfwd);
|
||||
prop = not (begin & confidential) or (wdclosed & sclosed);
|
||||
tel
|
||||
140
test/sdc/tracking.ept
Normal file
140
test/sdc/tracking.ept
Normal file
|
|
@ -0,0 +1,140 @@
|
|||
|
||||
|
||||
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
|
||||
|
||||
|
||||
|
||||
|
||||
(*
|
||||
|
||||
|
||||
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
|
||||
|
||||
*)
|
||||
|
||||
|
||||
Loading…
Reference in a new issue