Functions. R SMALLSTEPSIZE. R HeatOnUPPERLIMIT. R HeatOnLOWERLIMIT. R HeatOffUPPERLIMIT. R HeatOffLOWERLIMIT. /* changed concrete value for desired temperature to parameter */ R DESIREDTEMP. End. ProgramVariables. R simTime. R HeatOn. R HeatOff. R Tout. R Relay. R Switch. R Integrator. R smallStep. End. Problem. ( simTime = 0.0) & ( SMALLSTEPSIZE = 0.01) & ( smallStep = 0.0) & /* added Assumptions */ /* Bounds for heating and cooling */ (HeatOnUPPERLIMIT = 10) & (HeatOnLOWERLIMIT = 0) & (HeatOffUPPERLIMIT = 0) & (HeatOffLOWERLIMIT = -10) & /* intially guarantee is fulfilled */ (Integrator >= DESIREDTEMP - 2.0) & (Integrator <= DESIREDTEMP + 2.0) & (Tout = Integrator) -> ( [ { smallStep:=0.0; HeatOff:= *; ?(( HeatOff <= HeatOffUPPERLIMIT) & ( HeatOff >= HeatOffLOWERLIMIT)); HeatOn:= *; ?(( HeatOn <= HeatOnUPPERLIMIT) & ( HeatOn >= HeatOnLOWERLIMIT)); Tout:=Integrator; { ?( (DESIREDTEMP-Integrator) >= 0.5); Relay:=1.0; ++ ?( (DESIREDTEMP-Integrator) <= (-0.5)); Relay:=0.0; ++ ?(( (DESIREDTEMP-Integrator) < 0.5) & ( (DESIREDTEMP-Integrator) > (-0.5))); } { ?(( (DESIREDTEMP-Integrator) >= 0.5) & ( Relay > 0.0)); { simTime' = 1.0, Integrator' = HeatOn, smallStep' = 1.0 &(( (DESIREDTEMP-Integrator) >= 0.5)) | ( smallStep <= SMALLSTEPSIZE) } ++ ?(( (DESIREDTEMP-Integrator) >= 0.5) & ( Relay <= 0.0)); { simTime' = 1.0, Integrator' = HeatOff, smallStep' = 1.0 &(( (DESIREDTEMP-Integrator) >= 0.5)) | ( smallStep <= SMALLSTEPSIZE) } ++ ?(( (DESIREDTEMP-Integrator) <= (-0.5)) & ( Relay > 0.0)); { simTime' = 1.0, Integrator' = HeatOn, smallStep' = 1.0 &(( (DESIREDTEMP-Integrator) <= (-0.5))) | ( smallStep <= SMALLSTEPSIZE) } ++ ?(( (DESIREDTEMP-Integrator) <= (-0.5)) & ( Relay <= 0.0)); { simTime' = 1.0, Integrator' = HeatOff, smallStep' = 1.0 &(( (DESIREDTEMP-Integrator) <= (-0.5))) | ( smallStep <= SMALLSTEPSIZE) } ++ ?(( (DESIREDTEMP-Integrator) < 0.5) & ( (DESIREDTEMP-Integrator) > (-0.5)) & ( Relay > 0.0)); { simTime' = 1.0, Integrator' = HeatOn, smallStep' = 1.0 &(( (DESIREDTEMP-Integrator) < 0.5) & ( (DESIREDTEMP-Integrator) > (-0.5))) | ( smallStep <= SMALLSTEPSIZE) } ++ ?(( (DESIREDTEMP-Integrator) < 0.5) & ( (DESIREDTEMP-Integrator) > (-0.5)) & ( Relay <= 0.0)); { simTime' = 1.0, Integrator' = HeatOff, smallStep' = 1.0 &(( (DESIREDTEMP-Integrator) < 0.5) & ( (DESIREDTEMP-Integrator) > (-0.5))) | ( smallStep <= SMALLSTEPSIZE) } } }* ] /* Guarantee */ ( (Integrator >= DESIREDTEMP - 2.0) & (Integrator <= DESIREDTEMP + 2.0) ) ) End.