| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/graphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 21 kB |
|
Quelle HA.vdmsl Sprache: VDM |
|||||||||
|
types
HAInputs = seq of HAInput; HAInput = Change * TargetTemp * CurrentTemp * TargetHumid * CurrentHumid; Change = bool; TargetTemp = nat inv num == num <= 100; CurrentTemp = nat inv num == num <= 100; TargetHumid = nat inv num == num <= 100; CurrentHumid = nat inv num == num <= 100; HAOut = seq of OutStep; OutStep = EnvManipulation * AbsTime; AbsTime = nat; EnvManipulation = <OpenWindow> | <CloseWindow> | <IncTemp> | <DecTemp> | <LeaveTemp>; values TempChangeDuration : nat = 2; HumidChangeDuration : nat = 4; StepLength : nat = 1; functions HomeAutomation: HAInputs -> HAOut HomeAutomation(haInputs) == HA(haInputs, [], 0); HA: HAInputs * HAOut * nat -> HAOut HA(haInputs, outputSoFar, curTime) == if haInputs = [] then outputSoFar else let mk_(change,targetTemp,currentTemp,targetHumid,currentHumid) = hd haInputs, rest = tl haInputs, nextTime = curTime + StepLength in if outputSoFar <> [] then let mk_(-,timeOfLastInput) = outputSoFar(len outputSoFar) in if curTime <= timeOfLastInput and change then let interruptedOutput = InterruptOutput(outputSoFar,curTime), newOutput = CounterOutput(interruptedOutput,curTime) in HA(rest,AddOutput(targetTemp, currentTemp, targetHumid, currentHumid, curTime, newOutput), nextTime) else ChangeHA(haInputs,outputSoFar,curTime) else ChangeHA(haInputs,outputSoFar,curTime); ChangeHA: HAInputs * HAOut * AbsTime -> HAOut ChangeHA(haInputs,outputSoFar,curTime) == let mk_(change,targetTemp,currentTemp,targetHumid,currentHumid) = hd haInputs, rest = tl haInputs, nextTime = curTime + StepLength in if change then HA(rest,AddOutput(targetTemp, currentTemp, targetHumid, currentHumid, curTime, outputSoFar), nextTime) else HA(rest,outputSoFar,nextTime); AddOutput: nat * nat * nat * nat * nat * seq of OutStep -> seq of OutStep AddOutput(targetTemp, curTemp, targetHumid, curHumid, curTime, outputSoFar) == if targetHumid <> curHumid then HumidChanged(targetTemp, curTemp, targetHumid, curHumid, curTime, outputSoFar) elseif targetTemp <> curTemp then TempChanged(targetTemp, curTemp, curTime, outputSoFar) else outputSoFar; TempChanged: nat * nat * nat * seq of OutStep -> seq of OutStep TempChanged(targetTemp, curTemp, curTime, outputSoFar) == let nextTime = curTime+(abs(curTemp-targetTemp))*TempChangeDuration, action = if curTemp > targetTemp then <DecTemp> else <IncTemp> in outputSoFar ^ [mk_(action,curTime)] ^ [mk_(<LeaveTemp>,nextTime)]; HumidChanged: nat * nat * nat * nat * nat * seq of OutStep -> seq of OutStep HumidChanged(targetTemp, curTemp, targetHumid, curHumid, curTime, outputSoFar) == let tempChanged = (curHumid-targetHumid)*HumidChangeDuration/TempChangeDuration, action = if (curTemp-tempChanged) > targetTemp then <DecTemp> else <IncTemp>, timeChange = curTime+(curHumid-targetHumid)*HumidChangeDuration in outputSoFar ^ [mk_(<OpenWindow>,curTime)] ^ if (curTemp-tempChanged) <> targetTemp then [mk_(<CloseWindow>, timeChange), mk_(action, timeChange), mk_(<LeaveTemp>, timeChange + ((abs(curTemp-targetTemp)) - tempChanged)*TempChangeDuration)] else [mk_(<CloseWindow>, timeChange)]; InterruptOutput : seq of OutStep * nat -> seq of OutStep InterruptOutput(output, curTime) == [output(i) | i in set inds output & let mk_(-,t) = output(i) in t <= curTime]; CounterOutput : seq of OutStep * nat -> seq of OutStep CounterOutput(output, curTime) == let mk_(lastOutput,-) = output(len output) in if lastOutput = <OpenWindow> then output ^ [mk_(<CloseWindow>, curTime)] elseif (lastOutput = <IncTemp> or lastOutput = <DecTemp>) then output ^ [mk_(<LeaveTemp>, curTime)] else output; ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28