Functions. R SMALLSTEPSIZE. R PumpAmountUPPERLIMIT. R PumpAmountLOWERLIMIT. /* Added Constants */ R MAXPUMP. R MINPUMP. R ENERGYCONVERSION. End. ProgramVariables. R simTime. R PumpAmount. R Switch2. R Switch3. R DrugConsumption. R EnergyConsumption. R smallStep. End. Problem. (simTime = 0.0) & (SMALLSTEPSIZE = 0.01) & (smallStep = 0.0) & /* Added Assumptions */ (MINPUMP > 0) & (MAXPUMP > MINPUMP) & (PumpAmountUPPERLIMIT < MINPUMP) & (DrugConsumption = 0.0) & (EnergyConsumption = 0.0) ->( [ { smallStep:=0.0; PumpAmount:= *; ?(( PumpAmount <= PumpAmountUPPERLIMIT) & ( PumpAmount >= PumpAmountLOWERLIMIT)); { ?(( PumpAmount > MAXPUMP) & ( PumpAmount > MINPUMP)); DrugConsumption:=MAXPUMP; ++ ?(( PumpAmount <= MAXPUMP) & ( PumpAmount > MINPUMP)); DrugConsumption:=PumpAmount; ++ ?(( 0.0 <= MAXPUMP) & ( PumpAmount <= MINPUMP)); DrugConsumption:=0.0; } { ?(( PumpAmount > MAXPUMP) & ( PumpAmount > MINPUMP)); EnergyConsumption:=(ENERGYCONVERSION*MAXPUMP); ++ ?(( PumpAmount <= MAXPUMP) & ( PumpAmount > MINPUMP)); EnergyConsumption:=(ENERGYCONVERSION*PumpAmount); ++ ?(( 0.0 <= MAXPUMP) & ( PumpAmount <= MINPUMP)); EnergyConsumption:=(ENERGYCONVERSION*0.0); } { ?(( PumpAmount > MINPUMP) & ( PumpAmount > MAXPUMP)); { simTime' = 1.0, smallStep' = 1.0 &(( PumpAmount > MINPUMP) & ( PumpAmount > MAXPUMP)) | ( smallStep <= SMALLSTEPSIZE) } ++ ?(( PumpAmount > MINPUMP) & ( PumpAmount <= MAXPUMP)); { simTime' = 1.0, smallStep' = 1.0 &(( PumpAmount > MINPUMP) & ( PumpAmount <= MAXPUMP)) | ( smallStep <= SMALLSTEPSIZE) } ++ ?(( PumpAmount <= MINPUMP) & ( 0.0 <= MAXPUMP)); { simTime' = 1.0, smallStep' = 1.0 &(( PumpAmount <= MINPUMP) & ( 0.0 <= MAXPUMP)) | ( smallStep <= SMALLSTEPSIZE) } } }* ] (DrugConsumption = 0.0) & (EnergyConsumption = 0.0) ) End.