newpcaTsmc_0 : CONTEXT = BEGIN tActivityState: TYPE = {actReady, actExecuting, actDone}; 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 aTurnOnPump: tActivityState LOCAL hPressOnOff_1: tActivityState LOCAL aTurnOffPump: tActivityState LOCAL aStopInfusing_21: tActivityState LOCAL hPressStop_4_21: tActivityState LOCAL hPressStop_5_21: tActivityState LOCAL aPressKeysToTurnOffPump: tActivityState LOCAL hPressOnOff_2: tActivityState LOCAL hPressOnOff_3: tActivityState LOCAL aStopInfusing: tActivityState LOCAL hPressStop_4: tActivityState LOCAL hPressStop_5: tActivityState LOCAL aSetPCADose: tActivityState LOCAL aChangePCADoseValue: tActivityState LOCAL aChangeDigit: tActivityState LOCAL hPressUp_6: tActivityState LOCAL aSelectNextDigit: tActivityState LOCAL hPressLeft_7: tActivityState LOCAL hPressRight_8: tActivityState LOCAL aClearValue: tActivityState LOCAL hPressClear_9: tActivityState LOCAL aAccept: tActivityState LOCAL hPressEnter_10: tActivityState LOCAL aSetDelay: tActivityState LOCAL aChangeDelayValue: tActivityState LOCAL aChangeDigit_11: tActivityState LOCAL hPressUp_6_11: tActivityState LOCAL aSelectNextDigit_12: tActivityState LOCAL hPressLeft_7_12: tActivityState LOCAL hPressRight_8_12: tActivityState LOCAL aClearValue_13: tActivityState LOCAL hPressClear_9_13: tActivityState LOCAL aAccept_14: tActivityState LOCAL hPressEnter_10_14: tActivityState LOCAL aSet1HourLimit: tActivityState LOCAL aChange1HourLimitValue: tActivityState LOCAL aChangeDigit_15: tActivityState LOCAL hPressUp_6_15: tActivityState LOCAL aSelectNextDigit_16: tActivityState LOCAL hPressLeft_7_16: tActivityState LOCAL hPressRight_8_16: tActivityState LOCAL aClearValue_17: tActivityState LOCAL hPressClear_9_17: tActivityState LOCAL aAccept_18: tActivityState LOCAL hPressEnter_10_18: tActivityState LOCAL aStartOrReview: tActivityState LOCAL aStartRX: tActivityState LOCAL hPressStart_19: tActivityState LOCAL aReviewRx: tActivityState LOCAL hPressEnter_20: tActivityState INITIALIZATION hPressStart = FALSE; hPressStop = FALSE; hPressEnter = FALSE; hPressOnOff = FALSE; hPressClear = FALSE; hPressLeft = FALSE; hPressRight = FALSE; hPressUp = FALSE; pPumpProgrammer_Submitted = FALSE; aTurnOnPump = actReady; hPressOnOff_1 = actReady; aTurnOffPump = actReady; aStopInfusing_21 = actReady; hPressStop_4_21 = actReady; hPressStop_5_21 = actReady; aPressKeysToTurnOffPump = actReady; hPressOnOff_2 = actReady; hPressOnOff_3 = actReady; aStopInfusing = actReady; hPressStop_4 = actReady; hPressStop_5 = actReady; aSetPCADose = actReady; aChangePCADoseValue = actReady; aChangeDigit = actReady; hPressUp_6 = actReady; aSelectNextDigit = actReady; hPressLeft_7 = actReady; hPressRight_8 = actReady; aClearValue = actReady; hPressClear_9 = actReady; aAccept = actReady; hPressEnter_10 = actReady; aSetDelay = actReady; aChangeDelayValue = actReady; aChangeDigit_11 = actReady; hPressUp_6_11 = actReady; aSelectNextDigit_12 = actReady; hPressLeft_7_12 = actReady; hPressRight_8_12 = actReady; aClearValue_13 = actReady; hPressClear_9_13 = actReady; aAccept_14 = actReady; hPressEnter_10_14 = actReady; aSet1HourLimit = actReady; aChange1HourLimitValue = actReady; aChangeDigit_15 = actReady; hPressUp_6_15 = actReady; aSelectNextDigit_16 = actReady; hPressLeft_7_16 = actReady; hPressRight_8_16 = actReady; aClearValue_17 = actReady; hPressClear_9_17 = actReady; aAccept_18 = actReady; hPressEnter_10_18 = actReady; aStartOrReview = actReady; aStartRX = actReady; hPressStart_19 = actReady; aReviewRx = actReady; hPressEnter_20 = 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 = actExecuting AND hPressOnOff_1 = actDone 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 (iInterfaceMessage /= SystemOff) --> aTurnOnPump' = actDone; []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 = actExecuting AND aPressKeysToTurnOffPump = actDone 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 (iInterfaceMessage = SystemOff) --> aTurnOffPump' = actDone; []aTurnOffPump = actDone --> aTurnOffPump' = actReady; aStopInfusing_21' = actReady; hPressStop_4_21' = actReady; hPressStop_5_21' = actReady; aPressKeysToTurnOffPump' = actReady; hPressOnOff_2' = actReady; hPressOnOff_3' = actReady; []aStopInfusing_21 = actReady AND aTurnOffPump = actExecuting AND (iInterfaceMessage = TreatmentAdministering) AND NOT (iInterfaceMessage /= TreatmentAdministering) --> aStopInfusing_21' = actExecuting; []aStopInfusing_21 = actExecuting AND hPressStop_5_21 = actDone AND (iInterfaceMessage /= TreatmentAdministering) --> aStopInfusing_21' = actDone; []aStopInfusing_21 = actReady AND aTurnOffPump = actExecuting AND (iInterfaceMessage /= TreatmentAdministering) --> aStopInfusing_21' = actDone; []hPressStop_4_21 = actReady AND aStopInfusing_21 = actExecuting AND pPumpProgrammer_Ready --> hPressStop_4_21' = actExecuting; hPressStop' = TRUE; pPumpProgrammer_Submitted' = TRUE; []hPressStop_5_21 = actReady AND aStopInfusing_21 = actExecuting AND hPressStop_4_21 = actDone AND pPumpProgrammer_Ready --> hPressStop_5_21' = actExecuting; hPressStop' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aPressKeysToTurnOffPump = actReady AND aTurnOffPump = actExecuting AND aStopInfusing_21 = actDone --> aPressKeysToTurnOffPump' = actExecuting; []aPressKeysToTurnOffPump = actExecuting AND hPressOnOff_3 = actDone --> aPressKeysToTurnOffPump' = actDone; []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; []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 = actExecuting AND hPressStop_5 = actDone 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 (iInterfaceMessage /= TreatmentAdministering) --> aStopInfusing' = actDone; []aStopInfusing = actDone --> aStopInfusing' = actReady; hPressStop_4' = actReady; hPressStop_5' = actReady; []hPressStop_4 = actReady AND aStopInfusing = actExecuting AND pPumpProgrammer_Ready --> hPressStop_4' = actExecuting; hPressStop' = TRUE; pPumpProgrammer_Submitted' = TRUE; []hPressStop_5 = actReady AND aStopInfusing = actExecuting AND hPressStop_4 = actDone AND pPumpProgrammer_Ready --> hPressStop_5' = 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 = actExecuting AND aAccept = actDone 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 (iInterfaceMessage /= SetPCADose) --> aSetPCADose' = actDone; []aSetPCADose = actDone --> aSetPCADose' = actReady; aChangePCADoseValue' = actReady; aChangeDigit' = actReady; hPressUp_6' = actReady; aSelectNextDigit' = actReady; hPressLeft_7' = actReady; hPressRight_8' = actReady; aClearValue' = actReady; hPressClear_9' = actReady; aAccept' = actReady; hPressEnter_10' = actReady; []aChangePCADoseValue = actReady AND aSetPCADose = actExecuting AND (iCurrentValue /= iPrescribedPCADose) AND NOT (iCurrentValue = iPrescribedPCADose) --> aChangePCADoseValue' = actExecuting; []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 = actReady AND aSetPCADose = actExecuting 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 (iCurrentValue /= iPrescribedPCADose) AND NOT (iCurrentValue = iPrescribedPCADose) --> aChangePCADoseValue' = actExecuting; aChangeDigit' = actReady; hPressUp_6' = actReady; aSelectNextDigit' = actReady; hPressLeft_7' = actReady; hPressRight_8' = actReady; aClearValue' = actReady; hPressClear_9' = actReady; []aChangeDigit = actReady AND aChangePCADoseValue = actExecuting AND aChangeDigit /= actExecuting AND aSelectNextDigit /= actExecuting AND aClearValue /= actExecuting --> aChangeDigit' = actExecuting; []aChangeDigit = actExecuting AND hPressUp_6 = actDone --> aChangeDigit' = actDone; []hPressUp_6 = actReady AND aChangeDigit = actExecuting AND pPumpProgrammer_Ready --> hPressUp_6' = actExecuting; hPressUp' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aSelectNextDigit = actReady AND aChangePCADoseValue = actExecuting AND aChangeDigit /= actExecuting AND aSelectNextDigit /= actExecuting AND aClearValue /= actExecuting --> aSelectNextDigit' = actExecuting; []aSelectNextDigit = actExecuting AND hPressLeft_7 /= actExecuting AND hPressRight_8 /= actExecuting AND (hPressLeft_7 = actDone OR hPressRight_8 = actDone) --> aSelectNextDigit' = actDone; []hPressLeft_7 = actReady AND aSelectNextDigit = actExecuting AND hPressLeft_7 = actReady AND hPressRight_8 = actReady AND pPumpProgrammer_Ready --> hPressLeft_7' = actExecuting; hPressLeft' = TRUE; pPumpProgrammer_Submitted' = TRUE; []hPressRight_8 = actReady AND aSelectNextDigit = actExecuting AND hPressLeft_7 = actReady AND hPressRight_8 = actReady AND pPumpProgrammer_Ready --> hPressRight_8' = 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 hPressClear_9 = actDone --> aClearValue' = actDone; []hPressClear_9 = actReady AND aClearValue = actExecuting AND pPumpProgrammer_Ready --> hPressClear_9' = actExecuting; hPressClear' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aAccept = actReady AND aSetPCADose = actExecuting AND aChangePCADoseValue = actDone --> aAccept' = actExecuting; []aAccept = actExecuting AND hPressEnter_10 = actDone --> aAccept' = actDone; []hPressEnter_10 = actReady AND aAccept = actExecuting AND pPumpProgrammer_Ready --> hPressEnter_10' = 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 = actExecuting AND aAccept_14 = actDone 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 (iInterfaceMessage /= SetDelay) --> aSetDelay' = actDone; []aSetDelay = actDone --> aSetDelay' = actReady; aChangeDelayValue' = actReady; aChangeDigit_11' = actReady; hPressUp_6_11' = actReady; aSelectNextDigit_12' = actReady; hPressLeft_7_12' = actReady; hPressRight_8_12' = actReady; aClearValue_13' = actReady; hPressClear_9_13' = actReady; aAccept_14' = actReady; hPressEnter_10_14' = actReady; []aChangeDelayValue = actReady AND aSetDelay = actExecuting AND (iCurrentValue /= iPrescribedDelay) AND NOT (iCurrentValue = iPrescribedDelay) --> aChangeDelayValue' = actExecuting; []aChangeDelayValue = actExecuting AND aChangeDigit_11 /= actExecuting AND aSelectNextDigit_12 /= actExecuting AND aClearValue_13 /= actExecuting AND (aChangeDigit_11 = actDone OR aSelectNextDigit_12 = actDone OR aClearValue_13 = actDone) AND (iCurrentValue = iPrescribedDelay) --> aChangeDelayValue' = actDone; []aChangeDelayValue = actReady AND aSetDelay = actExecuting AND (iCurrentValue = iPrescribedDelay) --> aChangeDelayValue' = actDone; []aChangeDelayValue = actExecuting AND aChangeDigit_11 /= actExecuting AND aSelectNextDigit_12 /= actExecuting AND aClearValue_13 /= actExecuting AND (aChangeDigit_11 = actDone OR aSelectNextDigit_12 = actDone OR aClearValue_13 = actDone) AND (iCurrentValue /= iPrescribedDelay) AND NOT (iCurrentValue = iPrescribedDelay) --> aChangeDelayValue' = actExecuting; aChangeDigit_11' = actReady; hPressUp_6_11' = actReady; aSelectNextDigit_12' = actReady; hPressLeft_7_12' = actReady; hPressRight_8_12' = actReady; aClearValue_13' = actReady; hPressClear_9_13' = actReady; []aChangeDigit_11 = actReady AND aChangeDelayValue = actExecuting AND aChangeDigit_11 /= actExecuting AND aSelectNextDigit_12 /= actExecuting AND aClearValue_13 /= actExecuting --> aChangeDigit_11' = actExecuting; []aChangeDigit_11 = actExecuting AND hPressUp_6_11 = actDone --> aChangeDigit_11' = actDone; []hPressUp_6_11 = actReady AND aChangeDigit_11 = actExecuting AND pPumpProgrammer_Ready --> hPressUp_6_11' = actExecuting; hPressUp' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aSelectNextDigit_12 = actReady AND aChangeDelayValue = actExecuting AND aChangeDigit_11 /= actExecuting AND aSelectNextDigit_12 /= actExecuting AND aClearValue_13 /= actExecuting --> aSelectNextDigit_12' = actExecuting; []aSelectNextDigit_12 = actExecuting AND hPressLeft_7_12 /= actExecuting AND hPressRight_8_12 /= actExecuting AND (hPressLeft_7_12 = actDone OR hPressRight_8_12 = actDone) --> aSelectNextDigit_12' = actDone; []hPressLeft_7_12 = actReady AND aSelectNextDigit_12 = actExecuting AND hPressLeft_7_12 = actReady AND hPressRight_8_12 = actReady AND pPumpProgrammer_Ready --> hPressLeft_7_12' = actExecuting; hPressLeft' = TRUE; pPumpProgrammer_Submitted' = TRUE; []hPressRight_8_12 = actReady AND aSelectNextDigit_12 = actExecuting AND hPressLeft_7_12 = actReady AND hPressRight_8_12 = actReady AND pPumpProgrammer_Ready --> hPressRight_8_12' = actExecuting; hPressRight' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aClearValue_13 = actReady AND aChangeDelayValue = actExecuting AND aChangeDigit_11 /= actExecuting AND aSelectNextDigit_12 /= actExecuting AND aClearValue_13 /= actExecuting --> aClearValue_13' = actExecuting; []aClearValue_13 = actExecuting AND hPressClear_9_13 = actDone --> aClearValue_13' = actDone; []hPressClear_9_13 = actReady AND aClearValue_13 = actExecuting AND pPumpProgrammer_Ready --> hPressClear_9_13' = actExecuting; hPressClear' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aAccept_14 = actReady AND aSetDelay = actExecuting AND aChangeDelayValue = actDone --> aAccept_14' = actExecuting; []aAccept_14 = actExecuting AND hPressEnter_10_14 = actDone --> aAccept_14' = actDone; []hPressEnter_10_14 = actReady AND aAccept_14 = actExecuting AND pPumpProgrammer_Ready --> hPressEnter_10_14' = 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 = actExecuting AND aAccept_18 = actDone 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 (iInterfaceMessage /= Set1HourLimit) --> aSet1HourLimit' = actDone; []aSet1HourLimit = actDone --> aSet1HourLimit' = actReady; aChange1HourLimitValue' = actReady; aChangeDigit_15' = actReady; hPressUp_6_15' = actReady; aSelectNextDigit_16' = actReady; hPressLeft_7_16' = actReady; hPressRight_8_16' = actReady; aClearValue_17' = actReady; hPressClear_9_17' = actReady; aAccept_18' = actReady; hPressEnter_10_18' = actReady; []aChange1HourLimitValue = actReady AND aSet1HourLimit = actExecuting AND (iCurrentValue /= iPrescribed1HourLimit) AND NOT (iCurrentValue = iPrescribed1HourLimit) --> aChange1HourLimitValue' = actExecuting; []aChange1HourLimitValue = actExecuting AND aChangeDigit_15 /= actExecuting AND aSelectNextDigit_16 /= actExecuting AND aClearValue_17 /= actExecuting AND (aChangeDigit_15 = actDone OR aSelectNextDigit_16 = actDone OR aClearValue_17 = actDone) AND (iCurrentValue = iPrescribed1HourLimit) --> aChange1HourLimitValue' = actDone; []aChange1HourLimitValue = actReady AND aSet1HourLimit = actExecuting AND (iCurrentValue = iPrescribed1HourLimit) --> aChange1HourLimitValue' = actDone; []aChange1HourLimitValue = actExecuting AND aChangeDigit_15 /= actExecuting AND aSelectNextDigit_16 /= actExecuting AND aClearValue_17 /= actExecuting AND (aChangeDigit_15 = actDone OR aSelectNextDigit_16 = actDone OR aClearValue_17 = actDone) AND (iCurrentValue /= iPrescribed1HourLimit) AND NOT (iCurrentValue = iPrescribed1HourLimit) --> aChange1HourLimitValue' = actExecuting; aChangeDigit_15' = actReady; hPressUp_6_15' = actReady; aSelectNextDigit_16' = actReady; hPressLeft_7_16' = actReady; hPressRight_8_16' = actReady; aClearValue_17' = actReady; hPressClear_9_17' = actReady; []aChangeDigit_15 = actReady AND aChange1HourLimitValue = actExecuting AND aChangeDigit_15 /= actExecuting AND aSelectNextDigit_16 /= actExecuting AND aClearValue_17 /= actExecuting --> aChangeDigit_15' = actExecuting; []aChangeDigit_15 = actExecuting AND hPressUp_6_15 = actDone --> aChangeDigit_15' = actDone; []hPressUp_6_15 = actReady AND aChangeDigit_15 = actExecuting AND pPumpProgrammer_Ready --> hPressUp_6_15' = actExecuting; hPressUp' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aSelectNextDigit_16 = actReady AND aChange1HourLimitValue = actExecuting AND aChangeDigit_15 /= actExecuting AND aSelectNextDigit_16 /= actExecuting AND aClearValue_17 /= actExecuting --> aSelectNextDigit_16' = actExecuting; []aSelectNextDigit_16 = actExecuting AND hPressLeft_7_16 /= actExecuting AND hPressRight_8_16 /= actExecuting AND (hPressLeft_7_16 = actDone OR hPressRight_8_16 = actDone) --> aSelectNextDigit_16' = actDone; []hPressLeft_7_16 = actReady AND aSelectNextDigit_16 = actExecuting AND hPressLeft_7_16 = actReady AND hPressRight_8_16 = actReady AND pPumpProgrammer_Ready --> hPressLeft_7_16' = actExecuting; hPressLeft' = TRUE; pPumpProgrammer_Submitted' = TRUE; []hPressRight_8_16 = actReady AND aSelectNextDigit_16 = actExecuting AND hPressLeft_7_16 = actReady AND hPressRight_8_16 = actReady AND pPumpProgrammer_Ready --> hPressRight_8_16' = actExecuting; hPressRight' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aClearValue_17 = actReady AND aChange1HourLimitValue = actExecuting AND aChangeDigit_15 /= actExecuting AND aSelectNextDigit_16 /= actExecuting AND aClearValue_17 /= actExecuting --> aClearValue_17' = actExecuting; []aClearValue_17 = actExecuting AND hPressClear_9_17 = actDone --> aClearValue_17' = actDone; []hPressClear_9_17 = actReady AND aClearValue_17 = actExecuting AND pPumpProgrammer_Ready --> hPressClear_9_17' = actExecuting; hPressClear' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aAccept_18 = actReady AND aSet1HourLimit = actExecuting AND aChange1HourLimitValue = actDone --> aAccept_18' = actExecuting; []aAccept_18 = actExecuting AND hPressEnter_10_18 = actDone --> aAccept_18' = actDone; []hPressEnter_10_18 = actReady AND aAccept_18 = actExecuting AND pPumpProgrammer_Ready --> hPressEnter_10_18' = 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 = actExecuting AND aStartRX /= actExecuting AND aReviewRx /= actExecuting AND (aStartRX = actDone OR aReviewRx = actDone) 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 (iInterfaceMessage /= StartBeginsRx) --> aStartOrReview' = actDone; []aStartOrReview = actDone --> aStartOrReview' = actReady; aStartRX' = actReady; hPressStart_19' = actReady; aReviewRx' = actReady; hPressEnter_20' = actReady; []aStartRX = actReady AND aStartOrReview = actExecuting AND aStartRX = actReady AND aReviewRx = actReady --> aStartRX' = actExecuting; []aStartRX = actExecuting AND hPressStart_19 = actDone --> aStartRX' = actDone; []hPressStart_19 = actReady AND aStartRX = actExecuting AND pPumpProgrammer_Ready --> hPressStart_19' = actExecuting; hPressStart' = TRUE; pPumpProgrammer_Submitted' = TRUE; []aReviewRx = actReady AND aStartOrReview = actExecuting AND aStartRX = actReady AND aReviewRx = actReady --> aReviewRx' = actExecuting; []aReviewRx = actExecuting AND hPressEnter_20 = actDone --> aReviewRx' = actDone; []hPressEnter_20 = actReady AND aReviewRx = actExecuting AND pPumpProgrammer_Ready --> hPressEnter_20' = actExecuting; hPressEnter' = TRUE; pPumpProgrammer_Submitted' = TRUE; []pPumpProgrammer_Submitted AND NOT pPumpProgrammer_Ready --> pPumpProgrammer_Submitted' = FALSE; hPressOnOff_1' = IF hPressOnOff_1 = actExecuting THEN actDone ELSE hPressOnOff_1 ENDIF; hPressStop_4_21' = IF hPressStop_4_21 = actExecuting THEN actDone ELSE hPressStop_4_21 ENDIF; hPressStop_5_21' = IF hPressStop_5_21 = actExecuting THEN actDone ELSE hPressStop_5_21 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; hPressStop_4' = IF hPressStop_4 = actExecuting THEN actDone ELSE hPressStop_4 ENDIF; hPressStop_5' = IF hPressStop_5 = actExecuting THEN actDone ELSE hPressStop_5 ENDIF; hPressUp_6' = IF hPressUp_6 = actExecuting THEN actDone ELSE hPressUp_6 ENDIF; hPressLeft_7' = IF hPressLeft_7 = actExecuting THEN actDone ELSE hPressLeft_7 ENDIF; hPressRight_8' = IF hPressRight_8 = actExecuting THEN actDone ELSE hPressRight_8 ENDIF; hPressClear_9' = IF hPressClear_9 = actExecuting THEN actDone ELSE hPressClear_9 ENDIF; hPressEnter_10' = IF hPressEnter_10 = actExecuting THEN actDone ELSE hPressEnter_10 ENDIF; hPressUp_6_11' = IF hPressUp_6_11 = actExecuting THEN actDone ELSE hPressUp_6_11 ENDIF; hPressLeft_7_12' = IF hPressLeft_7_12 = actExecuting THEN actDone ELSE hPressLeft_7_12 ENDIF; hPressRight_8_12' = IF hPressRight_8_12 = actExecuting THEN actDone ELSE hPressRight_8_12 ENDIF; hPressClear_9_13' = IF hPressClear_9_13 = actExecuting THEN actDone ELSE hPressClear_9_13 ENDIF; hPressEnter_10_14' = IF hPressEnter_10_14 = actExecuting THEN actDone ELSE hPressEnter_10_14 ENDIF; hPressUp_6_15' = IF hPressUp_6_15 = actExecuting THEN actDone ELSE hPressUp_6_15 ENDIF; hPressLeft_7_16' = IF hPressLeft_7_16 = actExecuting THEN actDone ELSE hPressLeft_7_16 ENDIF; hPressRight_8_16' = IF hPressRight_8_16 = actExecuting THEN actDone ELSE hPressRight_8_16 ENDIF; hPressClear_9_17' = IF hPressClear_9_17 = actExecuting THEN actDone ELSE hPressClear_9_17 ENDIF; hPressEnter_10_18' = IF hPressEnter_10_18 = actExecuting THEN actDone ELSE hPressEnter_10_18 ENDIF; hPressStart_19' = IF hPressStart_19 = actExecuting THEN actDone ELSE hPressStart_19 ENDIF; hPressEnter_20' = IF hPressEnter_20 = actExecuting THEN actDone ELSE hPressEnter_20 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 AND lPCADose = iPrescribedPCADose AND lDelay = iPrescribedDelay AND l1HourLimit = iPrescribed1HourLimit)); END