Functions. R SMALLSTEPSIZE. R CAPACITY. R WarningInputUPPERLIMIT. R WarningInputLOWERLIMIT. End. ProgramVariables. R simTime. R WarningInput. R Switch1. R Warning. R smallStep. End. Problem. (simTime = 0.0) & (SMALLSTEPSIZE = 0.01) & (smallStep = 0.0) & /* Added Assumptions */ (CAPACITY > 0) & (WarningInputLOWERLIMIT > 0.01 * CAPACITY) & (Warning = 0.0) ->( [ { smallStep:=0.0; WarningInput:= *; ?((WarningInput <= WarningInputUPPERLIMIT) & (WarningInput >= WarningInputLOWERLIMIT)); { ?( WarningInput/CAPACITY > 0.01); Warning:=0.0; ++ ?( WarningInput/CAPACITY <= 0.01); Warning:=1.0; } { ?(( WarningInput/CAPACITY > 0.01)); { simTime' = 1.0, smallStep' = 1.0 &(( WarningInput/CAPACITY > 0.01)) | ( smallStep <= SMALLSTEPSIZE) } ++ ?(( WarningInput/CAPACITY <= 0.01)); { simTime' = 1.0, smallStep' = 1.0 &(( WarningInput/CAPACITY <= 0.01)) | ( smallStep <= SMALLSTEPSIZE) } } }* ] (Warning = 0.0) ) End.