heptagon/test/sdc/office.ept

359 lines
7.9 KiB
Text
Raw Normal View History

(*-----------------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