newpcaTsmcF2_1 : CONTEXT = BEGIN cContextErrorMax: INTEGER = 1; tActivityState: TYPE = {actReady, actExecuting, actDone}; tContextErrorRange: TYPE = [0..cContextErrorMax]; tInterfaceMessage: TYPE = {SetPCADose, SetDelay, Set1HourLimit, StartBeginsRx, TreatmentAdministering, SystemOff}; tValue: TYPE = {Correct, Incorrect}; pPumpProgrammer: MODULE = BEGIN INPUT iInterfaceMessage: tInterfaceMessage INPUT iCurrentValue: tValue INPUT iPrescribedPCADose: tValue INPUT iPrescribedDelay: tValue INPUT iPrescribed1HourLimit: tValue INPUT pPumpProgrammer_Ready: BOOLEAN OUTPUT hPressStart: BOOLEAN OUTPUT hPressStop: BOOLEAN OUTPUT hPressEnter: BOOLEAN OUTPUT hPressOnOff: BOOLEAN OUTPUT hPressClear: BOOLEAN OUTPUT hPressLeft: BOOLEAN OUTPUT hPressRight: BOOLEAN OUTPUT hPressUp: BOOLEAN OUTPUT pPumpProgrammer_Submitted: BOOLEAN LOCAL pPumpProgrammer_ContextErrors: tContextErrorRange LOCAL lReviewed: BOOLEAN LOCAL aTurnOnPump: tActivityState LOCAL hPressOnOff_1: tActivityState LOCAL aTurnOffPump: tActivityState LOCAL aStopInfusing_25: tActivityState LOCAL hPressStop_5_25: tActivityState LOCAL hPressStop_6_25: tActivityState LOCAL aPressKeysToTurnOffPump: tActivityState LOCAL hPressOnOff_2: tActivityState LOCAL hPressOnOff_3: tActivityState LOCAL lReviewed_4: tActivityState LOCAL aStopInfusing: tActivityState LOCAL hPressStop_5: tActivityState LOCAL hPressStop_6: tActivityState LOCAL aSetPCADose: tActivityState LOCAL aChangePCADoseValue: tActivityState LOCAL aChangeDigit: tActivityState LOCAL hPressUp_7: tActivityState LOCAL lReviewed_8: tActivityState LOCAL aSelectNextDigit: tActivityState LOCAL hPressLeft_9: tActivityState LOCAL hPressRight_10: tActivityState LOCAL aClearValue: tActivityState LOCAL hPressClear_11: tActivityState LOCAL lReviewed_12: tActivityState LOCAL aAccept: tActivityState LOCAL hPressEnter_13: tActivityState LOCAL aSetDelay: tActivityState LOCAL aChangeDelayValue: tActivityState LOCAL aChangeDigit_14: tActivityState LOCAL hPressUp_7_14: tActivityState LOCAL lReviewed_8_14: tActivityState LOCAL aSelectNextDigit_15: tActivityState LOCAL hPressLeft_9_15: tActivityState LOCAL hPressRight_10_15: tActivityState LOCAL aClearValue_16: tActivityState LOCAL hPressClear_11_16: tActivityState LOCAL lReviewed_12_16: tActivityState LOCAL aAccept_17: tActivityState LOCAL hPressEnter_13_17: tActivityState LOCAL aSet1HourLimit: tActivityState LOCAL aChange1HourLimitValue: tActivityState LOCAL aChangeDigit_18: tActivityState LOCAL hPressUp_7_18: tActivityState LOCAL lReviewed_8_18: tActivityState LOCAL aSelectNextDigit_19: tActivityState LOCAL hPressLeft_9_19: tActivityState LOCAL hPressRight_10_19: tActivityState LOCAL aClearValue_20: tActivityState LOCAL hPressClear_11_20: tActivityState LOCAL lReviewed_12_20: tActivityState LOCAL aAccept_21: tActivityState LOCAL hPressEnter_13_21: tActivityState LOCAL aStartOrReview: tActivityState LOCAL aStartRX: tActivityState LOCAL hPressStart_22: tActivityState LOCAL aReviewRx: tActivityState LOCAL hPressEnter_23: tActivityState LOCAL lReviewed_24: tActivityState INITIALIZATION hPressStart = FALSE; hPressStop = FALSE; hPressEnter = FALSE; hPressOnOff = FALSE; hPressClear = FALSE; hPressLeft = FALSE; hPressRight = FALSE; hPressUp = FALSE; pPumpProgrammer_Submitted = FALSE; pPumpProgrammer_ContextErrors = 0; lReviewed = FALSE; aTurnOnPump = actReady; hPressOnOff_1 = actReady; aTurnOffPump = actReady; aStopInfusing_25 = actReady; hPressStop_5_25 = actReady; hPressStop_6_25 = actReady; aPressKeysToTurnOffPump = actReady; hPressOnOff_2 = actReady; hPressOnOff_3 = actReady; lReviewed_4 = actReady; aStopInfusing = actReady; hPressStop_5 = actReady; hPressStop_6 = actReady; aSetPCADose = actReady; aChangePCADoseValue = actReady; aChangeDigit = actReady; hPressUp_7 = actReady; lReviewed_8 = actReady; aSelectNextDigit = actReady; hPressLeft_9 = actReady; hPressRight_10 = actReady; aClearValue = actReady; hPressClear_11 = actReady; lReviewed_12 = actReady; aAccept = actReady; hPressEnter_13 = actReady; aSetDelay = actReady; aChangeDelayValue = actReady; aChangeDigit_14 = actReady; hPressUp_7_14 = actReady; lReviewed_8_14 = actReady; aSelectNextDigit_15 = actReady; hPressLeft_9_15 = actReady; hPressRight_10_15 = actReady; aClearValue_16 = actReady; hPressClear_11_16 = actReady; lReviewed_12_16 = actReady; aAccept_17 = actReady; hPressEnter_13_17 = actReady; aSet1HourLimit = actReady; aChange1HourLimitValue = actReady; aChangeDigit_18 = actReady; hPressUp_7_18 = actReady; lReviewed_8_18 = actReady; aSelectNextDigit_19 = actReady; hPressLeft_9_19 = actReady; hPressRight_10_19 = actReady; aClearValue_20 = actReady; hPressClear_11_20 = actReady; lReviewed_12_20 = actReady; aAccept_21 = actReady; hPressEnter_13_21 = actReady; aStartOrReview = actReady; aStartRX = actReady; hPressStart_22 = actReady; aReviewRx = actReady; hPressEnter_23 = actReady; lReviewed_24 = actReady; TRANSITION [ aTurnOnPump = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND (iInterfaceMessage = SystemOff) AND NOT (iInterfaceMessage /= SystemOff) --> aTurnOnPump' = actExecuting; []aTurnOnPump = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND NOT ((iInterfaceMessage = SystemOff) AND NOT (iInterfaceMessage /= SystemOff)) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aTurnOnPump' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aTurnOnPump = actExecuting AND hPressOnOff_1 = actDone AND (iInterfaceMessage /= SystemOff) --> aTurnOnPump' = actDone; []aTurnOnPump = actExecuting AND hPressOnOff_1 = actDone AND NOT (iInterfaceMessage /= SystemOff) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aTurnOnPump' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aTurnOnPump = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND (iInterfaceMessage /= SystemOff) --> aTurnOnPump' = actDone; []aTurnOnPump = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND NOT (iInterfaceMessage /= SystemOff) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aTurnOnPump' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aTurnOnPump = actExecuting AND hPressOnOff_1 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aTurnOnPump' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressOnOff_1' = actReady; []aTurnOnPump = actDone --> aTurnOnPump' = actReady; hPressOnOff_1' = actReady; []hPressOnOff_1 = actReady AND aTurnOnPump = actExecuting AND pPumpProgrammer_Ready --> hPressOnOff_1' = actExecuting; hPressOnOff' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aTurnOffPump = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND (iInterfaceMessage /= SystemOff) AND NOT (iInterfaceMessage = SystemOff) --> aTurnOffPump' = actExecuting; []aTurnOffPump = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND NOT ((iInterfaceMessage /= SystemOff) AND NOT (iInterfaceMessage = SystemOff)) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aTurnOffPump' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aTurnOffPump = actExecuting AND aPressKeysToTurnOffPump = actDone AND (iInterfaceMessage = SystemOff) --> aTurnOffPump' = actDone; []aTurnOffPump = actExecuting AND aPressKeysToTurnOffPump = actDone AND NOT (iInterfaceMessage = SystemOff) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aTurnOffPump' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aTurnOffPump = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND (iInterfaceMessage = SystemOff) --> aTurnOffPump' = actDone; []aTurnOffPump = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND NOT (iInterfaceMessage = SystemOff) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aTurnOffPump' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aTurnOffPump = actExecuting AND aPressKeysToTurnOffPump = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aTurnOffPump' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; aStopInfusing_25' = actReady; hPressStop_5_25' = actReady; hPressStop_6_25' = actReady; aPressKeysToTurnOffPump' = actReady; hPressOnOff_2' = actReady; hPressOnOff_3' = actReady; lReviewed_4' = actReady; []aTurnOffPump = actDone --> aTurnOffPump' = actReady; aStopInfusing_25' = actReady; hPressStop_5_25' = actReady; hPressStop_6_25' = actReady; aPressKeysToTurnOffPump' = actReady; hPressOnOff_2' = actReady; hPressOnOff_3' = actReady; lReviewed_4' = actReady; []aStopInfusing_25 = actReady AND aTurnOffPump = actExecuting AND (iInterfaceMessage = TreatmentAdministering) AND NOT (iInterfaceMessage /= TreatmentAdministering) --> aStopInfusing_25' = actExecuting; []aStopInfusing_25 = actReady AND aTurnOffPump = actExecuting AND NOT ((iInterfaceMessage = TreatmentAdministering) AND NOT (iInterfaceMessage /= TreatmentAdministering)) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aStopInfusing_25' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aStopInfusing_25 = actExecuting AND hPressStop_6_25 = actDone AND (iInterfaceMessage /= TreatmentAdministering) --> aStopInfusing_25' = actDone; []aStopInfusing_25 = actExecuting AND hPressStop_6_25 = actDone AND NOT (iInterfaceMessage /= TreatmentAdministering) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aStopInfusing_25' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aStopInfusing_25 = actReady AND aTurnOffPump = actExecuting AND (iInterfaceMessage /= TreatmentAdministering) --> aStopInfusing_25' = actDone; []aStopInfusing_25 = actReady AND aTurnOffPump = actExecuting AND NOT (iInterfaceMessage /= TreatmentAdministering) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aStopInfusing_25' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aStopInfusing_25 = actExecuting AND hPressStop_6_25 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aStopInfusing_25' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressStop_5_25' = actReady; hPressStop_6_25' = actReady; []hPressStop_5_25 = actReady AND aStopInfusing_25 = actExecuting AND pPumpProgrammer_Ready --> hPressStop_5_25' = actExecuting; hPressStop' = TRUE; pPumpProgrammer_Submitted' = TRUE; []hPressStop_6_25 = actReady AND aStopInfusing_25 = actExecuting AND hPressStop_5_25 = actDone AND pPumpProgrammer_Ready --> hPressStop_6_25' = actExecuting; hPressStop' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aPressKeysToTurnOffPump = actReady AND aTurnOffPump = actExecuting AND aStopInfusing_25 = actDone --> aPressKeysToTurnOffPump' = actExecuting; []aPressKeysToTurnOffPump = actExecuting AND lReviewed_4 = actDone --> aPressKeysToTurnOffPump' = actDone; []aPressKeysToTurnOffPump = actReady AND aTurnOffPump = actExecuting AND aStopInfusing_25 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aPressKeysToTurnOffPump' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aPressKeysToTurnOffPump = actExecuting AND lReviewed_4 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aPressKeysToTurnOffPump' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressOnOff_2' = actReady; hPressOnOff_3' = actReady; lReviewed_4' = actReady; []hPressOnOff_2 = actReady AND aPressKeysToTurnOffPump = actExecuting AND pPumpProgrammer_Ready --> hPressOnOff_2' = actExecuting; hPressOnOff' = TRUE; pPumpProgrammer_Submitted' = TRUE; []hPressOnOff_3 = actReady AND aPressKeysToTurnOffPump = actExecuting AND hPressOnOff_2 = actDone AND pPumpProgrammer_Ready --> hPressOnOff_3' = actExecuting; hPressOnOff' = TRUE; pPumpProgrammer_Submitted' = TRUE; []lReviewed_4 = actReady AND aPressKeysToTurnOffPump = actExecuting AND hPressOnOff_3 = actDone --> lReviewed_4' = actDone; lReviewed' = FALSE; []aStopInfusing = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND (iInterfaceMessage = TreatmentAdministering) AND NOT (iInterfaceMessage /= TreatmentAdministering) --> aStopInfusing' = actExecuting; []aStopInfusing = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND NOT ((iInterfaceMessage = TreatmentAdministering) AND NOT (iInterfaceMessage /= TreatmentAdministering)) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aStopInfusing' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aStopInfusing = actExecuting AND hPressStop_6 = actDone AND (iInterfaceMessage /= TreatmentAdministering) --> aStopInfusing' = actDone; []aStopInfusing = actExecuting AND hPressStop_6 = actDone AND NOT (iInterfaceMessage /= TreatmentAdministering) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aStopInfusing' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aStopInfusing = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND (iInterfaceMessage /= TreatmentAdministering) --> aStopInfusing' = actDone; []aStopInfusing = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND NOT (iInterfaceMessage /= TreatmentAdministering) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aStopInfusing' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aStopInfusing = actExecuting AND hPressStop_6 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aStopInfusing' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressStop_5' = actReady; hPressStop_6' = actReady; []aStopInfusing = actDone --> aStopInfusing' = actReady; hPressStop_5' = actReady; hPressStop_6' = actReady; []hPressStop_5 = actReady AND aStopInfusing = actExecuting AND pPumpProgrammer_Ready --> hPressStop_5' = actExecuting; hPressStop' = TRUE; pPumpProgrammer_Submitted' = TRUE; []hPressStop_6 = actReady AND aStopInfusing = actExecuting AND hPressStop_5 = actDone AND pPumpProgrammer_Ready --> hPressStop_6' = actExecuting; hPressStop' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aSetPCADose = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND (iInterfaceMessage = SetPCADose) AND NOT (iInterfaceMessage /= SetPCADose) --> aSetPCADose' = actExecuting; []aSetPCADose = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND NOT ((iInterfaceMessage = SetPCADose) AND NOT (iInterfaceMessage /= SetPCADose)) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSetPCADose' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aSetPCADose = actExecuting AND aAccept = actDone AND (iInterfaceMessage /= SetPCADose) --> aSetPCADose' = actDone; []aSetPCADose = actExecuting AND aAccept = actDone AND NOT (iInterfaceMessage /= SetPCADose) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSetPCADose' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aSetPCADose = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND (iInterfaceMessage /= SetPCADose) --> aSetPCADose' = actDone; []aSetPCADose = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND NOT (iInterfaceMessage /= SetPCADose) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSetPCADose' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aSetPCADose = actExecuting AND aAccept = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSetPCADose' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; aChangePCADoseValue' = actReady; aChangeDigit' = actReady; hPressUp_7' = actReady; lReviewed_8' = actReady; aSelectNextDigit' = actReady; hPressLeft_9' = actReady; hPressRight_10' = actReady; aClearValue' = actReady; hPressClear_11' = actReady; lReviewed_12' = actReady; aAccept' = actReady; hPressEnter_13' = actReady; []aSetPCADose = actDone --> aSetPCADose' = actReady; aChangePCADoseValue' = actReady; aChangeDigit' = actReady; hPressUp_7' = actReady; lReviewed_8' = actReady; aSelectNextDigit' = actReady; hPressLeft_9' = actReady; hPressRight_10' = actReady; aClearValue' = actReady; hPressClear_11' = actReady; lReviewed_12' = actReady; aAccept' = actReady; hPressEnter_13' = actReady; []aChangePCADoseValue = actReady AND aSetPCADose = actExecuting AND (iCurrentValue /= iPrescribedPCADose) AND NOT (iCurrentValue = iPrescribedPCADose) --> aChangePCADoseValue' = actExecuting; []aChangePCADoseValue = actReady AND aSetPCADose = actExecuting AND NOT ((iCurrentValue /= iPrescribedPCADose) AND NOT (iCurrentValue = iPrescribedPCADose)) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChangePCADoseValue' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aChangePCADoseValue = actExecuting AND aChangeDigit /= actExecuting AND aSelectNextDigit /= actExecuting AND aClearValue /= actExecuting AND (aChangeDigit = actDone OR aSelectNextDigit = actDone OR aClearValue = actDone) AND (iCurrentValue = iPrescribedPCADose) --> aChangePCADoseValue' = actDone; []aChangePCADoseValue = actExecuting AND aChangeDigit /= actExecuting AND aSelectNextDigit /= actExecuting AND aClearValue /= actExecuting AND (aChangeDigit = actDone OR aSelectNextDigit = actDone OR aClearValue = actDone) AND NOT (iCurrentValue = iPrescribedPCADose) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChangePCADoseValue' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aChangePCADoseValue = actReady AND aSetPCADose = actExecuting AND (iCurrentValue = iPrescribedPCADose) --> aChangePCADoseValue' = actDone; []aChangePCADoseValue = actReady AND aSetPCADose = actExecuting AND NOT (iCurrentValue = iPrescribedPCADose) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChangePCADoseValue' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aChangePCADoseValue = actExecuting AND aChangeDigit /= actExecuting AND aSelectNextDigit /= actExecuting AND aClearValue /= actExecuting AND (aChangeDigit = actDone OR aSelectNextDigit = actDone OR aClearValue = actDone) AND (iCurrentValue /= iPrescribedPCADose) AND NOT (iCurrentValue = iPrescribedPCADose) --> aChangePCADoseValue' = actExecuting; aChangeDigit' = actReady; hPressUp_7' = actReady; lReviewed_8' = actReady; aSelectNextDigit' = actReady; hPressLeft_9' = actReady; hPressRight_10' = actReady; aClearValue' = actReady; hPressClear_11' = actReady; lReviewed_12' = actReady; []aChangePCADoseValue = actExecuting AND aChangeDigit /= actExecuting AND aSelectNextDigit /= actExecuting AND aClearValue /= actExecuting AND (aChangeDigit = actDone OR aSelectNextDigit = actDone OR aClearValue = actDone) AND NOT ((iCurrentValue /= iPrescribedPCADose) AND NOT (iCurrentValue = iPrescribedPCADose)) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChangePCADoseValue' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; aChangeDigit' = actReady; hPressUp_7' = actReady; lReviewed_8' = actReady; aSelectNextDigit' = actReady; hPressLeft_9' = actReady; hPressRight_10' = actReady; aClearValue' = actReady; hPressClear_11' = actReady; lReviewed_12' = actReady; []aChangeDigit = actReady AND aChangePCADoseValue = actExecuting AND aChangeDigit /= actExecuting AND aSelectNextDigit /= actExecuting AND aClearValue /= actExecuting --> aChangeDigit' = actExecuting; []aChangeDigit = actExecuting AND lReviewed_8 = actDone --> aChangeDigit' = actDone; []aChangeDigit = actReady AND aChangePCADoseValue = actExecuting AND aChangeDigit /= actExecuting AND aSelectNextDigit /= actExecuting AND aClearValue /= actExecuting AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChangeDigit' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aChangeDigit = actExecuting AND lReviewed_8 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChangeDigit' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressUp_7' = actReady; lReviewed_8' = actReady; []hPressUp_7 = actReady AND aChangeDigit = actExecuting AND pPumpProgrammer_Ready --> hPressUp_7' = actExecuting; hPressUp' = TRUE; pPumpProgrammer_Submitted' = TRUE; []lReviewed_8 = actReady AND aChangeDigit = actExecuting AND hPressUp_7 = actDone --> lReviewed_8' = actDone; lReviewed' = FALSE; []aSelectNextDigit = actReady AND aChangePCADoseValue = actExecuting AND aChangeDigit /= actExecuting AND aSelectNextDigit /= actExecuting AND aClearValue /= actExecuting --> aSelectNextDigit' = actExecuting; []aSelectNextDigit = actExecuting AND hPressLeft_9 /= actExecuting AND hPressRight_10 /= actExecuting AND (hPressLeft_9 = actDone OR hPressRight_10 = actDone) --> aSelectNextDigit' = actDone; []aSelectNextDigit = actReady AND aChangePCADoseValue = actExecuting AND aChangeDigit /= actExecuting AND aSelectNextDigit /= actExecuting AND aClearValue /= actExecuting AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSelectNextDigit' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aSelectNextDigit = actExecuting AND hPressLeft_9 /= actExecuting AND hPressRight_10 /= actExecuting AND (hPressLeft_9 = actDone OR hPressRight_10 = actDone) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSelectNextDigit' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressLeft_9' = actReady; hPressRight_10' = actReady; []hPressLeft_9 = actReady AND aSelectNextDigit = actExecuting AND hPressLeft_9 = actReady AND hPressRight_10 = actReady AND pPumpProgrammer_Ready --> hPressLeft_9' = actExecuting; hPressLeft' = TRUE; pPumpProgrammer_Submitted' = TRUE; []hPressRight_10 = actReady AND aSelectNextDigit = actExecuting AND hPressLeft_9 = actReady AND hPressRight_10 = actReady AND pPumpProgrammer_Ready --> hPressRight_10' = actExecuting; hPressRight' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aClearValue = actReady AND aChangePCADoseValue = actExecuting AND aChangeDigit /= actExecuting AND aSelectNextDigit /= actExecuting AND aClearValue /= actExecuting --> aClearValue' = actExecuting; []aClearValue = actExecuting AND lReviewed_12 = actDone --> aClearValue' = actDone; []aClearValue = actReady AND aChangePCADoseValue = actExecuting AND aChangeDigit /= actExecuting AND aSelectNextDigit /= actExecuting AND aClearValue /= actExecuting AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aClearValue' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aClearValue = actExecuting AND lReviewed_12 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aClearValue' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressClear_11' = actReady; lReviewed_12' = actReady; []hPressClear_11 = actReady AND aClearValue = actExecuting AND pPumpProgrammer_Ready --> hPressClear_11' = actExecuting; hPressClear' = TRUE; pPumpProgrammer_Submitted' = TRUE; []lReviewed_12 = actReady AND aClearValue = actExecuting AND hPressClear_11 = actDone --> lReviewed_12' = actDone; lReviewed' = FALSE; []aAccept = actReady AND aSetPCADose = actExecuting AND aChangePCADoseValue = actDone --> aAccept' = actExecuting; []aAccept = actExecuting AND hPressEnter_13 = actDone --> aAccept' = actDone; []aAccept = actReady AND aSetPCADose = actExecuting AND aChangePCADoseValue = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aAccept' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aAccept = actExecuting AND hPressEnter_13 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aAccept' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressEnter_13' = actReady; []hPressEnter_13 = actReady AND aAccept = actExecuting AND pPumpProgrammer_Ready --> hPressEnter_13' = actExecuting; hPressEnter' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aSetDelay = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND (iInterfaceMessage = SetDelay) AND NOT (iInterfaceMessage /= SetDelay) --> aSetDelay' = actExecuting; []aSetDelay = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND NOT ((iInterfaceMessage = SetDelay) AND NOT (iInterfaceMessage /= SetDelay)) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSetDelay' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aSetDelay = actExecuting AND aAccept_17 = actDone AND (iInterfaceMessage /= SetDelay) --> aSetDelay' = actDone; []aSetDelay = actExecuting AND aAccept_17 = actDone AND NOT (iInterfaceMessage /= SetDelay) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSetDelay' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aSetDelay = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND (iInterfaceMessage /= SetDelay) --> aSetDelay' = actDone; []aSetDelay = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND NOT (iInterfaceMessage /= SetDelay) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSetDelay' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aSetDelay = actExecuting AND aAccept_17 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSetDelay' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; aChangeDelayValue' = actReady; aChangeDigit_14' = actReady; hPressUp_7_14' = actReady; lReviewed_8_14' = actReady; aSelectNextDigit_15' = actReady; hPressLeft_9_15' = actReady; hPressRight_10_15' = actReady; aClearValue_16' = actReady; hPressClear_11_16' = actReady; lReviewed_12_16' = actReady; aAccept_17' = actReady; hPressEnter_13_17' = actReady; []aSetDelay = actDone --> aSetDelay' = actReady; aChangeDelayValue' = actReady; aChangeDigit_14' = actReady; hPressUp_7_14' = actReady; lReviewed_8_14' = actReady; aSelectNextDigit_15' = actReady; hPressLeft_9_15' = actReady; hPressRight_10_15' = actReady; aClearValue_16' = actReady; hPressClear_11_16' = actReady; lReviewed_12_16' = actReady; aAccept_17' = actReady; hPressEnter_13_17' = actReady; []aChangeDelayValue = actReady AND aSetDelay = actExecuting AND (iCurrentValue /= iPrescribedDelay) AND NOT (iCurrentValue = iPrescribedDelay) --> aChangeDelayValue' = actExecuting; []aChangeDelayValue = actReady AND aSetDelay = actExecuting AND NOT ((iCurrentValue /= iPrescribedDelay) AND NOT (iCurrentValue = iPrescribedDelay)) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChangeDelayValue' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aChangeDelayValue = actExecuting AND aChangeDigit_14 /= actExecuting AND aSelectNextDigit_15 /= actExecuting AND aClearValue_16 /= actExecuting AND (aChangeDigit_14 = actDone OR aSelectNextDigit_15 = actDone OR aClearValue_16 = actDone) AND (iCurrentValue = iPrescribedDelay) --> aChangeDelayValue' = actDone; []aChangeDelayValue = actExecuting AND aChangeDigit_14 /= actExecuting AND aSelectNextDigit_15 /= actExecuting AND aClearValue_16 /= actExecuting AND (aChangeDigit_14 = actDone OR aSelectNextDigit_15 = actDone OR aClearValue_16 = actDone) AND NOT (iCurrentValue = iPrescribedDelay) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChangeDelayValue' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aChangeDelayValue = actReady AND aSetDelay = actExecuting AND (iCurrentValue = iPrescribedDelay) --> aChangeDelayValue' = actDone; []aChangeDelayValue = actReady AND aSetDelay = actExecuting AND NOT (iCurrentValue = iPrescribedDelay) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChangeDelayValue' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aChangeDelayValue = actExecuting AND aChangeDigit_14 /= actExecuting AND aSelectNextDigit_15 /= actExecuting AND aClearValue_16 /= actExecuting AND (aChangeDigit_14 = actDone OR aSelectNextDigit_15 = actDone OR aClearValue_16 = actDone) AND (iCurrentValue /= iPrescribedDelay) AND NOT (iCurrentValue = iPrescribedDelay) --> aChangeDelayValue' = actExecuting; aChangeDigit_14' = actReady; hPressUp_7_14' = actReady; lReviewed_8_14' = actReady; aSelectNextDigit_15' = actReady; hPressLeft_9_15' = actReady; hPressRight_10_15' = actReady; aClearValue_16' = actReady; hPressClear_11_16' = actReady; lReviewed_12_16' = actReady; []aChangeDelayValue = actExecuting AND aChangeDigit_14 /= actExecuting AND aSelectNextDigit_15 /= actExecuting AND aClearValue_16 /= actExecuting AND (aChangeDigit_14 = actDone OR aSelectNextDigit_15 = actDone OR aClearValue_16 = actDone) AND NOT ((iCurrentValue /= iPrescribedDelay) AND NOT (iCurrentValue = iPrescribedDelay)) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChangeDelayValue' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; aChangeDigit_14' = actReady; hPressUp_7_14' = actReady; lReviewed_8_14' = actReady; aSelectNextDigit_15' = actReady; hPressLeft_9_15' = actReady; hPressRight_10_15' = actReady; aClearValue_16' = actReady; hPressClear_11_16' = actReady; lReviewed_12_16' = actReady; []aChangeDigit_14 = actReady AND aChangeDelayValue = actExecuting AND aChangeDigit_14 /= actExecuting AND aSelectNextDigit_15 /= actExecuting AND aClearValue_16 /= actExecuting --> aChangeDigit_14' = actExecuting; []aChangeDigit_14 = actExecuting AND lReviewed_8_14 = actDone --> aChangeDigit_14' = actDone; []aChangeDigit_14 = actReady AND aChangeDelayValue = actExecuting AND aChangeDigit_14 /= actExecuting AND aSelectNextDigit_15 /= actExecuting AND aClearValue_16 /= actExecuting AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChangeDigit_14' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aChangeDigit_14 = actExecuting AND lReviewed_8_14 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChangeDigit_14' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressUp_7_14' = actReady; lReviewed_8_14' = actReady; []hPressUp_7_14 = actReady AND aChangeDigit_14 = actExecuting AND pPumpProgrammer_Ready --> hPressUp_7_14' = actExecuting; hPressUp' = TRUE; pPumpProgrammer_Submitted' = TRUE; []lReviewed_8_14 = actReady AND aChangeDigit_14 = actExecuting AND hPressUp_7_14 = actDone --> lReviewed_8_14' = actDone; lReviewed' = FALSE; []aSelectNextDigit_15 = actReady AND aChangeDelayValue = actExecuting AND aChangeDigit_14 /= actExecuting AND aSelectNextDigit_15 /= actExecuting AND aClearValue_16 /= actExecuting --> aSelectNextDigit_15' = actExecuting; []aSelectNextDigit_15 = actExecuting AND hPressLeft_9_15 /= actExecuting AND hPressRight_10_15 /= actExecuting AND (hPressLeft_9_15 = actDone OR hPressRight_10_15 = actDone) --> aSelectNextDigit_15' = actDone; []aSelectNextDigit_15 = actReady AND aChangeDelayValue = actExecuting AND aChangeDigit_14 /= actExecuting AND aSelectNextDigit_15 /= actExecuting AND aClearValue_16 /= actExecuting AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSelectNextDigit_15' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aSelectNextDigit_15 = actExecuting AND hPressLeft_9_15 /= actExecuting AND hPressRight_10_15 /= actExecuting AND (hPressLeft_9_15 = actDone OR hPressRight_10_15 = actDone) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSelectNextDigit_15' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressLeft_9_15' = actReady; hPressRight_10_15' = actReady; []hPressLeft_9_15 = actReady AND aSelectNextDigit_15 = actExecuting AND hPressLeft_9_15 = actReady AND hPressRight_10_15 = actReady AND pPumpProgrammer_Ready --> hPressLeft_9_15' = actExecuting; hPressLeft' = TRUE; pPumpProgrammer_Submitted' = TRUE; []hPressRight_10_15 = actReady AND aSelectNextDigit_15 = actExecuting AND hPressLeft_9_15 = actReady AND hPressRight_10_15 = actReady AND pPumpProgrammer_Ready --> hPressRight_10_15' = actExecuting; hPressRight' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aClearValue_16 = actReady AND aChangeDelayValue = actExecuting AND aChangeDigit_14 /= actExecuting AND aSelectNextDigit_15 /= actExecuting AND aClearValue_16 /= actExecuting --> aClearValue_16' = actExecuting; []aClearValue_16 = actExecuting AND lReviewed_12_16 = actDone --> aClearValue_16' = actDone; []aClearValue_16 = actReady AND aChangeDelayValue = actExecuting AND aChangeDigit_14 /= actExecuting AND aSelectNextDigit_15 /= actExecuting AND aClearValue_16 /= actExecuting AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aClearValue_16' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aClearValue_16 = actExecuting AND lReviewed_12_16 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aClearValue_16' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressClear_11_16' = actReady; lReviewed_12_16' = actReady; []hPressClear_11_16 = actReady AND aClearValue_16 = actExecuting AND pPumpProgrammer_Ready --> hPressClear_11_16' = actExecuting; hPressClear' = TRUE; pPumpProgrammer_Submitted' = TRUE; []lReviewed_12_16 = actReady AND aClearValue_16 = actExecuting AND hPressClear_11_16 = actDone --> lReviewed_12_16' = actDone; lReviewed' = FALSE; []aAccept_17 = actReady AND aSetDelay = actExecuting AND aChangeDelayValue = actDone --> aAccept_17' = actExecuting; []aAccept_17 = actExecuting AND hPressEnter_13_17 = actDone --> aAccept_17' = actDone; []aAccept_17 = actReady AND aSetDelay = actExecuting AND aChangeDelayValue = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aAccept_17' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aAccept_17 = actExecuting AND hPressEnter_13_17 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aAccept_17' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressEnter_13_17' = actReady; []hPressEnter_13_17 = actReady AND aAccept_17 = actExecuting AND pPumpProgrammer_Ready --> hPressEnter_13_17' = actExecuting; hPressEnter' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aSet1HourLimit = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND (iInterfaceMessage = Set1HourLimit) AND NOT (iInterfaceMessage /= Set1HourLimit) --> aSet1HourLimit' = actExecuting; []aSet1HourLimit = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND NOT ((iInterfaceMessage = Set1HourLimit) AND NOT (iInterfaceMessage /= Set1HourLimit)) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSet1HourLimit' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aSet1HourLimit = actExecuting AND aAccept_21 = actDone AND (iInterfaceMessage /= Set1HourLimit) --> aSet1HourLimit' = actDone; []aSet1HourLimit = actExecuting AND aAccept_21 = actDone AND NOT (iInterfaceMessage /= Set1HourLimit) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSet1HourLimit' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aSet1HourLimit = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND (iInterfaceMessage /= Set1HourLimit) --> aSet1HourLimit' = actDone; []aSet1HourLimit = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND NOT (iInterfaceMessage /= Set1HourLimit) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSet1HourLimit' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aSet1HourLimit = actExecuting AND aAccept_21 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSet1HourLimit' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; aChange1HourLimitValue' = actReady; aChangeDigit_18' = actReady; hPressUp_7_18' = actReady; lReviewed_8_18' = actReady; aSelectNextDigit_19' = actReady; hPressLeft_9_19' = actReady; hPressRight_10_19' = actReady; aClearValue_20' = actReady; hPressClear_11_20' = actReady; lReviewed_12_20' = actReady; aAccept_21' = actReady; hPressEnter_13_21' = actReady; []aSet1HourLimit = actDone --> aSet1HourLimit' = actReady; aChange1HourLimitValue' = actReady; aChangeDigit_18' = actReady; hPressUp_7_18' = actReady; lReviewed_8_18' = actReady; aSelectNextDigit_19' = actReady; hPressLeft_9_19' = actReady; hPressRight_10_19' = actReady; aClearValue_20' = actReady; hPressClear_11_20' = actReady; lReviewed_12_20' = actReady; aAccept_21' = actReady; hPressEnter_13_21' = actReady; []aChange1HourLimitValue = actReady AND aSet1HourLimit = actExecuting AND (iCurrentValue /= iPrescribed1HourLimit) AND NOT (iCurrentValue = iPrescribed1HourLimit) --> aChange1HourLimitValue' = actExecuting; []aChange1HourLimitValue = actReady AND aSet1HourLimit = actExecuting AND NOT ((iCurrentValue /= iPrescribed1HourLimit) AND NOT (iCurrentValue = iPrescribed1HourLimit)) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChange1HourLimitValue' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aChange1HourLimitValue = actExecuting AND aChangeDigit_18 /= actExecuting AND aSelectNextDigit_19 /= actExecuting AND aClearValue_20 /= actExecuting AND (aChangeDigit_18 = actDone OR aSelectNextDigit_19 = actDone OR aClearValue_20 = actDone) AND (iCurrentValue = iPrescribed1HourLimit) --> aChange1HourLimitValue' = actDone; []aChange1HourLimitValue = actExecuting AND aChangeDigit_18 /= actExecuting AND aSelectNextDigit_19 /= actExecuting AND aClearValue_20 /= actExecuting AND (aChangeDigit_18 = actDone OR aSelectNextDigit_19 = actDone OR aClearValue_20 = actDone) AND NOT (iCurrentValue = iPrescribed1HourLimit) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChange1HourLimitValue' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aChange1HourLimitValue = actReady AND aSet1HourLimit = actExecuting AND (iCurrentValue = iPrescribed1HourLimit) --> aChange1HourLimitValue' = actDone; []aChange1HourLimitValue = actReady AND aSet1HourLimit = actExecuting AND NOT (iCurrentValue = iPrescribed1HourLimit) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChange1HourLimitValue' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aChange1HourLimitValue = actExecuting AND aChangeDigit_18 /= actExecuting AND aSelectNextDigit_19 /= actExecuting AND aClearValue_20 /= actExecuting AND (aChangeDigit_18 = actDone OR aSelectNextDigit_19 = actDone OR aClearValue_20 = actDone) AND (iCurrentValue /= iPrescribed1HourLimit) AND NOT (iCurrentValue = iPrescribed1HourLimit) --> aChange1HourLimitValue' = actExecuting; aChangeDigit_18' = actReady; hPressUp_7_18' = actReady; lReviewed_8_18' = actReady; aSelectNextDigit_19' = actReady; hPressLeft_9_19' = actReady; hPressRight_10_19' = actReady; aClearValue_20' = actReady; hPressClear_11_20' = actReady; lReviewed_12_20' = actReady; []aChange1HourLimitValue = actExecuting AND aChangeDigit_18 /= actExecuting AND aSelectNextDigit_19 /= actExecuting AND aClearValue_20 /= actExecuting AND (aChangeDigit_18 = actDone OR aSelectNextDigit_19 = actDone OR aClearValue_20 = actDone) AND NOT ((iCurrentValue /= iPrescribed1HourLimit) AND NOT (iCurrentValue = iPrescribed1HourLimit)) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChange1HourLimitValue' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; aChangeDigit_18' = actReady; hPressUp_7_18' = actReady; lReviewed_8_18' = actReady; aSelectNextDigit_19' = actReady; hPressLeft_9_19' = actReady; hPressRight_10_19' = actReady; aClearValue_20' = actReady; hPressClear_11_20' = actReady; lReviewed_12_20' = actReady; []aChangeDigit_18 = actReady AND aChange1HourLimitValue = actExecuting AND aChangeDigit_18 /= actExecuting AND aSelectNextDigit_19 /= actExecuting AND aClearValue_20 /= actExecuting --> aChangeDigit_18' = actExecuting; []aChangeDigit_18 = actExecuting AND lReviewed_8_18 = actDone --> aChangeDigit_18' = actDone; []aChangeDigit_18 = actReady AND aChange1HourLimitValue = actExecuting AND aChangeDigit_18 /= actExecuting AND aSelectNextDigit_19 /= actExecuting AND aClearValue_20 /= actExecuting AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChangeDigit_18' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aChangeDigit_18 = actExecuting AND lReviewed_8_18 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aChangeDigit_18' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressUp_7_18' = actReady; lReviewed_8_18' = actReady; []hPressUp_7_18 = actReady AND aChangeDigit_18 = actExecuting AND pPumpProgrammer_Ready --> hPressUp_7_18' = actExecuting; hPressUp' = TRUE; pPumpProgrammer_Submitted' = TRUE; []lReviewed_8_18 = actReady AND aChangeDigit_18 = actExecuting AND hPressUp_7_18 = actDone --> lReviewed_8_18' = actDone; lReviewed' = FALSE; []aSelectNextDigit_19 = actReady AND aChange1HourLimitValue = actExecuting AND aChangeDigit_18 /= actExecuting AND aSelectNextDigit_19 /= actExecuting AND aClearValue_20 /= actExecuting --> aSelectNextDigit_19' = actExecuting; []aSelectNextDigit_19 = actExecuting AND hPressLeft_9_19 /= actExecuting AND hPressRight_10_19 /= actExecuting AND (hPressLeft_9_19 = actDone OR hPressRight_10_19 = actDone) --> aSelectNextDigit_19' = actDone; []aSelectNextDigit_19 = actReady AND aChange1HourLimitValue = actExecuting AND aChangeDigit_18 /= actExecuting AND aSelectNextDigit_19 /= actExecuting AND aClearValue_20 /= actExecuting AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSelectNextDigit_19' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aSelectNextDigit_19 = actExecuting AND hPressLeft_9_19 /= actExecuting AND hPressRight_10_19 /= actExecuting AND (hPressLeft_9_19 = actDone OR hPressRight_10_19 = actDone) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aSelectNextDigit_19' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressLeft_9_19' = actReady; hPressRight_10_19' = actReady; []hPressLeft_9_19 = actReady AND aSelectNextDigit_19 = actExecuting AND hPressLeft_9_19 = actReady AND hPressRight_10_19 = actReady AND pPumpProgrammer_Ready --> hPressLeft_9_19' = actExecuting; hPressLeft' = TRUE; pPumpProgrammer_Submitted' = TRUE; []hPressRight_10_19 = actReady AND aSelectNextDigit_19 = actExecuting AND hPressLeft_9_19 = actReady AND hPressRight_10_19 = actReady AND pPumpProgrammer_Ready --> hPressRight_10_19' = actExecuting; hPressRight' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aClearValue_20 = actReady AND aChange1HourLimitValue = actExecuting AND aChangeDigit_18 /= actExecuting AND aSelectNextDigit_19 /= actExecuting AND aClearValue_20 /= actExecuting --> aClearValue_20' = actExecuting; []aClearValue_20 = actExecuting AND lReviewed_12_20 = actDone --> aClearValue_20' = actDone; []aClearValue_20 = actReady AND aChange1HourLimitValue = actExecuting AND aChangeDigit_18 /= actExecuting AND aSelectNextDigit_19 /= actExecuting AND aClearValue_20 /= actExecuting AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aClearValue_20' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aClearValue_20 = actExecuting AND lReviewed_12_20 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aClearValue_20' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressClear_11_20' = actReady; lReviewed_12_20' = actReady; []hPressClear_11_20 = actReady AND aClearValue_20 = actExecuting AND pPumpProgrammer_Ready --> hPressClear_11_20' = actExecuting; hPressClear' = TRUE; pPumpProgrammer_Submitted' = TRUE; []lReviewed_12_20 = actReady AND aClearValue_20 = actExecuting AND hPressClear_11_20 = actDone --> lReviewed_12_20' = actDone; lReviewed' = FALSE; []aAccept_21 = actReady AND aSet1HourLimit = actExecuting AND aChange1HourLimitValue = actDone --> aAccept_21' = actExecuting; []aAccept_21 = actExecuting AND hPressEnter_13_21 = actDone --> aAccept_21' = actDone; []aAccept_21 = actReady AND aSet1HourLimit = actExecuting AND aChange1HourLimitValue = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aAccept_21' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aAccept_21 = actExecuting AND hPressEnter_13_21 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aAccept_21' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressEnter_13_21' = actReady; []hPressEnter_13_21 = actReady AND aAccept_21 = actExecuting AND pPumpProgrammer_Ready --> hPressEnter_13_21' = actExecuting; hPressEnter' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aStartOrReview = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND (iInterfaceMessage = StartBeginsRx) AND NOT (iInterfaceMessage /= StartBeginsRx) --> aStartOrReview' = actExecuting; []aStartOrReview = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND NOT ((iInterfaceMessage = StartBeginsRx) AND NOT (iInterfaceMessage /= StartBeginsRx)) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aStartOrReview' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aStartOrReview = actExecuting AND aStartRX /= actExecuting AND aReviewRx /= actExecuting AND (aStartRX = actDone OR aReviewRx = actDone) AND (iInterfaceMessage /= StartBeginsRx) --> aStartOrReview' = actDone; []aStartOrReview = actExecuting AND aStartRX /= actExecuting AND aReviewRx /= actExecuting AND (aStartRX = actDone OR aReviewRx = actDone) AND NOT (iInterfaceMessage /= StartBeginsRx) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aStartOrReview' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aStartOrReview = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND (iInterfaceMessage /= StartBeginsRx) --> aStartOrReview' = actDone; []aStartOrReview = actReady AND aTurnOnPump /= actExecuting AND aTurnOffPump /= actExecuting AND aStopInfusing /= actExecuting AND aSetPCADose /= actExecuting AND aSetDelay /= actExecuting AND aSet1HourLimit /= actExecuting AND aStartOrReview /= actExecuting AND NOT (iInterfaceMessage /= StartBeginsRx) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aStartOrReview' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aStartOrReview = actExecuting AND aStartRX /= actExecuting AND aReviewRx /= actExecuting AND (aStartRX = actDone OR aReviewRx = actDone) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aStartOrReview' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; aStartRX' = actReady; hPressStart_22' = actReady; aReviewRx' = actReady; hPressEnter_23' = actReady; lReviewed_24' = actReady; []aStartOrReview = actDone --> aStartOrReview' = actReady; aStartRX' = actReady; hPressStart_22' = actReady; aReviewRx' = actReady; hPressEnter_23' = actReady; lReviewed_24' = actReady; []aStartRX = actReady AND aStartOrReview = actExecuting AND aStartRX = actReady AND aReviewRx = actReady AND (lReviewed) --> aStartRX' = actExecuting; []aStartRX = actReady AND aStartOrReview = actExecuting AND aStartRX = actReady AND aReviewRx = actReady AND NOT ((lReviewed)) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aStartRX' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aStartRX = actExecuting AND hPressStart_22 = actDone --> aStartRX' = actDone; []aStartRX = actReady AND aStartOrReview = actExecuting AND aStartRX = actReady AND aReviewRx = actReady AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aStartRX' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aStartRX = actExecuting AND hPressStart_22 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aStartRX' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressStart_22' = actReady; []hPressStart_22 = actReady AND aStartRX = actExecuting AND pPumpProgrammer_Ready --> hPressStart_22' = actExecuting; hPressStart' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aReviewRx = actReady AND aStartOrReview = actExecuting AND aStartRX = actReady AND aReviewRx = actReady AND (NOT lReviewed) --> aReviewRx' = actExecuting; []aReviewRx = actReady AND aStartOrReview = actExecuting AND aStartRX = actReady AND aReviewRx = actReady AND NOT ((NOT lReviewed)) AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aReviewRx' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aReviewRx = actExecuting AND lReviewed_24 = actDone --> aReviewRx' = actDone; []aReviewRx = actReady AND aStartOrReview = actExecuting AND aStartRX = actReady AND aReviewRx = actReady AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aReviewRx' = actDone; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; []aReviewRx = actExecuting AND lReviewed_24 = actDone AND pPumpProgrammer_ContextErrors < cContextErrorMax --> aReviewRx' = actExecuting; pPumpProgrammer_ContextErrors' = pPumpProgrammer_ContextErrors + 1; hPressEnter_23' = actReady; lReviewed_24' = actReady; []hPressEnter_23 = actReady AND aReviewRx = actExecuting AND pPumpProgrammer_Ready --> hPressEnter_23' = actExecuting; hPressEnter' = TRUE; pPumpProgrammer_Submitted' = TRUE; []lReviewed_24 = actReady AND aReviewRx = actExecuting AND hPressEnter_23 = actDone --> lReviewed_24' = actDone; lReviewed' = TRUE; []pPumpProgrammer_Submitted AND NOT pPumpProgrammer_Ready --> pPumpProgrammer_Submitted' = FALSE; hPressOnOff_1' = IF hPressOnOff_1 = actExecuting THEN actDone ELSE hPressOnOff_1 ENDIF; hPressStop_5_25' = IF hPressStop_5_25 = actExecuting THEN actDone ELSE hPressStop_5_25 ENDIF; hPressStop_6_25' = IF hPressStop_6_25 = actExecuting THEN actDone ELSE hPressStop_6_25 ENDIF; hPressOnOff_2' = IF hPressOnOff_2 = actExecuting THEN actDone ELSE hPressOnOff_2 ENDIF; hPressOnOff_3' = IF hPressOnOff_3 = actExecuting THEN actDone ELSE hPressOnOff_3 ENDIF; lReviewed_4' = IF lReviewed_4 = actExecuting THEN actDone ELSE lReviewed_4 ENDIF; hPressStop_5' = IF hPressStop_5 = actExecuting THEN actDone ELSE hPressStop_5 ENDIF; hPressStop_6' = IF hPressStop_6 = actExecuting THEN actDone ELSE hPressStop_6 ENDIF; hPressUp_7' = IF hPressUp_7 = actExecuting THEN actDone ELSE hPressUp_7 ENDIF; lReviewed_8' = IF lReviewed_8 = actExecuting THEN actDone ELSE lReviewed_8 ENDIF; hPressLeft_9' = IF hPressLeft_9 = actExecuting THEN actDone ELSE hPressLeft_9 ENDIF; hPressRight_10' = IF hPressRight_10 = actExecuting THEN actDone ELSE hPressRight_10 ENDIF; hPressClear_11' = IF hPressClear_11 = actExecuting THEN actDone ELSE hPressClear_11 ENDIF; lReviewed_12' = IF lReviewed_12 = actExecuting THEN actDone ELSE lReviewed_12 ENDIF; hPressEnter_13' = IF hPressEnter_13 = actExecuting THEN actDone ELSE hPressEnter_13 ENDIF; hPressUp_7_14' = IF hPressUp_7_14 = actExecuting THEN actDone ELSE hPressUp_7_14 ENDIF; lReviewed_8_14' = IF lReviewed_8_14 = actExecuting THEN actDone ELSE lReviewed_8_14 ENDIF; hPressLeft_9_15' = IF hPressLeft_9_15 = actExecuting THEN actDone ELSE hPressLeft_9_15 ENDIF; hPressRight_10_15' = IF hPressRight_10_15 = actExecuting THEN actDone ELSE hPressRight_10_15 ENDIF; hPressClear_11_16' = IF hPressClear_11_16 = actExecuting THEN actDone ELSE hPressClear_11_16 ENDIF; lReviewed_12_16' = IF lReviewed_12_16 = actExecuting THEN actDone ELSE lReviewed_12_16 ENDIF; hPressEnter_13_17' = IF hPressEnter_13_17 = actExecuting THEN actDone ELSE hPressEnter_13_17 ENDIF; hPressUp_7_18' = IF hPressUp_7_18 = actExecuting THEN actDone ELSE hPressUp_7_18 ENDIF; lReviewed_8_18' = IF lReviewed_8_18 = actExecuting THEN actDone ELSE lReviewed_8_18 ENDIF; hPressLeft_9_19' = IF hPressLeft_9_19 = actExecuting THEN actDone ELSE hPressLeft_9_19 ENDIF; hPressRight_10_19' = IF hPressRight_10_19 = actExecuting THEN actDone ELSE hPressRight_10_19 ENDIF; hPressClear_11_20' = IF hPressClear_11_20 = actExecuting THEN actDone ELSE hPressClear_11_20 ENDIF; lReviewed_12_20' = IF lReviewed_12_20 = actExecuting THEN actDone ELSE lReviewed_12_20 ENDIF; hPressEnter_13_21' = IF hPressEnter_13_21 = actExecuting THEN actDone ELSE hPressEnter_13_21 ENDIF; hPressStart_22' = IF hPressStart_22 = actExecuting THEN actDone ELSE hPressStart_22 ENDIF; hPressEnter_23' = IF hPressEnter_23 = actExecuting THEN actDone ELSE hPressEnter_23 ENDIF; lReviewed_24' = IF lReviewed_24 = actExecuting THEN actDone ELSE lReviewed_24 ENDIF; hPressStart' = FALSE; hPressStop' = FALSE; hPressEnter' = FALSE; hPressOnOff' = FALSE; hPressClear' = FALSE; hPressLeft' = FALSE; hPressRight' = FALSE; hPressUp' = FALSE; ]; END; Mission: MODULE = BEGIN OUTPUT iPrescribedPCADose: tValue OUTPUT iPrescribedDelay: tValue OUTPUT iPrescribed1HourLimit: tValue INITIALIZATION iPrescribedPCADose = Correct; iPrescribedDelay = Correct; iPrescribed1HourLimit = Correct; END; InterfaceAndAutomation: MODULE = BEGIN INPUT hPressStart: BOOLEAN INPUT hPressStop: BOOLEAN INPUT hPressEnter: BOOLEAN INPUT hPressOnOff: BOOLEAN INPUT hPressClear: BOOLEAN INPUT hPressLeft: BOOLEAN INPUT hPressRight: BOOLEAN INPUT hPressUp: BOOLEAN INPUT pPumpProgrammer_Submitted: BOOLEAN OUTPUT iInterfaceMessage: tInterfaceMessage OUTPUT iCurrentValue: tValue OUTPUT pPumpProgrammer_Ready: BOOLEAN LOCAL lPCADose: tValue LOCAL lDelay: tValue LOCAL l1HourLimit: tValue LOCAL lStopPressedOnce: BOOLEAN LOCAL lOnOffPressedOnce: BOOLEAN %%LOCAL lUpOcclusionTested: BOOLEAN INITIALIZATION pPumpProgrammer_Ready = TRUE; iInterfaceMessage = SystemOff; iCurrentValue = Incorrect; lPCADose = Incorrect; lDelay = Incorrect; l1HourLimit = Incorrect; lStopPressedOnce = FALSE; lOnOffPressedOnce = FALSE; TRANSITION lOnOffPressedOnce' = IF iInterfaceMessage /= SystemOff and hPressOnOff and pPumpProgrammer_Ready and pPumpProgrammer_Submitted THEN not lOnOffPressedOnce ELSIF NOT hPressOnOff and pPumpProgrammer_Ready and pPumpProgrammer_Submitted THEN FALSE ELSE lOnOffPressedOnce ENDIF; lStopPressedOnce' = IF iInterfaceMessage = TreatmentAdministering and hPressStop and pPumpProgrammer_Ready and pPumpProgrammer_Submitted THEN not lOnOffPressedOnce ELSIF NOT hPressStop and pPumpProgrammer_Ready and pPumpProgrammer_Submitted THEN FALSE ELSE lStopPressedOnce ENDIF; [ %%human input handshake not (pPumpProgrammer_Ready or pPumpProgrammer_Submitted) --> pPumpProgrammer_Ready' = TRUE; %%turn the system on []iInterfaceMessage = SystemOff and hPressOnOff and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> iInterfaceMessage' = SetPCADose; pPumpProgrammer_Ready' = FALSE; %%"set pca dose" []iInterfaceMessage = SetPCADose and hPressUp and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> iCurrentValue' IN IF iCurrentValue = Correct THEN {Incorrect} ELSE {Correct, Incorrect} ENDIF;%% fLimitIncrement(iCurrentValue, iCursorPosition, cMaxPCADose); pPumpProgrammer_Ready' = FALSE; []iInterfaceMessage = SetPCADose and hPressClear and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> iCurrentValue' = Incorrect; pPumpProgrammer_Ready' = FALSE; []iInterfaceMessage = SetPCADose and hPressLeft and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> pPumpProgrammer_Ready' = FALSE; []iInterfaceMessage = SetPCADose and hPressRight and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> pPumpProgrammer_Ready' = FALSE; []iInterfaceMessage = SetPCADose and hPressEnter and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> iInterfaceMessage' = SetDelay; lPCADose' = iCurrentValue; iCurrentValue' = lDelay; pPumpProgrammer_Ready' = FALSE; %%set delay []iInterfaceMessage = SetDelay and hPressUp and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> iCurrentValue' IN IF iCurrentValue = Correct THEN {Incorrect} ELSE {Correct, Incorrect} ENDIF;%% = fLimitIncrement(iCurrentValue, iCursorPosition, cMaxDelay); pPumpProgrammer_Ready' = FALSE; []iInterfaceMessage = SetDelay and hPressClear and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> iCurrentValue' = Incorrect; pPumpProgrammer_Ready' = FALSE; []iInterfaceMessage = SetDelay and hPressLeft and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> pPumpProgrammer_Ready' = FALSE; []iInterfaceMessage = SetDelay and hPressRight and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> pPumpProgrammer_Ready' = FALSE; []iInterfaceMessage = SetDelay and hPressEnter and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> iInterfaceMessage' = Set1HourLimit; lDelay' = iCurrentValue; iCurrentValue' = l1HourLimit; pPumpProgrammer_Ready' = FALSE; %% set the 1 hour limit []iInterfaceMessage = Set1HourLimit and hPressUp and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> iCurrentValue' IN IF iCurrentValue = Correct THEN {Incorrect} ELSE {Correct, Incorrect} ENDIF;%% = fLimitIncrement(iCurrentValue, iCursorPosition, fGetMaxHourLimit(lDelay, lPCADose, lBasalRate)); pPumpProgrammer_Ready' = FALSE; []iInterfaceMessage = Set1HourLimit and hPressClear and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> iCurrentValue' = Incorrect; pPumpProgrammer_Ready' = FALSE; []iInterfaceMessage = Set1HourLimit and hPressLeft and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> pPumpProgrammer_Ready' = FALSE; []iInterfaceMessage = Set1HourLimit and hPressRight and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> pPumpProgrammer_Ready' = FALSE; []iInterfaceMessage = Set1HourLimit and hPressEnter and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> iInterfaceMessage' = StartBeginsRx; l1HourLimit' = iCurrentValue; pPumpProgrammer_Ready' = FALSE; %% press start to begin treatment, enter to review []iInterfaceMessage = StartBeginsRx and hPressEnter and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> iInterfaceMessage' = SetPCADose; pPumpProgrammer_Ready' = FALSE; []iInterfaceMessage = StartBeginsRx and hPressStart and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> iInterfaceMessage' = TreatmentAdministering; pPumpProgrammer_Ready' = FALSE; %%stoping infusion []iInterfaceMessage = TreatmentAdministering and hPressStop and lStopPressedOnce and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> iInterfaceMessage' = StartBeginsRx; pPumpProgrammer_Ready' = FALSE; %% turning the system off []iInterfaceMessage /= SystemOff and iInterfaceMessage /= TreatmentAdministering and hPressOnOff and pPumpProgrammer_Ready and pPumpProgrammer_Submitted --> iInterfaceMessage'= IF lOnOffPressedOnce THEN SystemOff ELSE iInterfaceMessage ENDIF; pPumpProgrammer_Ready' = FALSE; %% ignore superfluous user input []ELSE --> pPumpProgrammer_Ready' = IF (pPumpProgrammer_Ready and pPumpProgrammer_Submitted) THEN FALSE ELSE pPumpProgrammer_Ready ENDIF; ] END; System: module = pPumpProgrammer [] Mission [] InterfaceAndAutomation; safe1: THEOREM System |- G((iInterfaceMessage = TreatmentAdministering)=>(lPCADose = iPrescribedPCADose AND lDelay = iPrescribedDelay AND l1HourLimit = iPrescribed1HourLimit)); safe2: THEOREM System |- G(NOT(iInterfaceMessage = TreatmentAdministering)); END