From 7bc5e4c115f120fbee46aef4787392a727f4fbc7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= Date: Mon, 6 Feb 2017 15:32:44 +0100 Subject: [PATCH] Examples with contracts and sdc for tests --- test/sdc/modular.ept | 39 +++++ test/sdc/office.ept | 358 ++++++++++++++++++++++++++++++++++++++++++ test/sdc/tracking.ept | 140 +++++++++++++++++ 3 files changed, 537 insertions(+) create mode 100644 test/sdc/modular.ept create mode 100644 test/sdc/office.ept create mode 100644 test/sdc/tracking.ept diff --git a/test/sdc/modular.ept b/test/sdc/modular.ept new file mode 100644 index 0000000..bb4fff6 --- /dev/null +++ b/test/sdc/modular.ept @@ -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 diff --git a/test/sdc/office.ept b/test/sdc/office.ept new file mode 100644 index 0000000..c272fc3 --- /dev/null +++ b/test/sdc/office.ept @@ -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 diff --git a/test/sdc/tracking.ept b/test/sdc/tracking.ept new file mode 100644 index 0000000..0bbf147 --- /dev/null +++ b/test/sdc/tracking.ept @@ -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 + +*) + +