You cannot select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
359 lines
7.9 KiB
Plaintext
359 lines
7.9 KiB
Plaintext
(*-----------------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
|