protocolNew : CONTEXT = BEGIN cComErrorMax: INTEGER = 2; tActivityState: TYPE = {actReady, actExecuting, actDone}; tHeadings: TYPE = {CorrectHeading, IncorrectHeading, IncorrectHeading2, IncorrectHeading3}; tPointableItems: TYPE = {Nothing,HeadingWindow}; humanOperators: MODULE = BEGIN % Variables for pATCo OUTPUT hATCoPressOrReleaseSwitchToTalk: BOOLEAN LOCAL sATCoTalk: tHeadings LOCAL lATCoSelectedClearance: tHeadings LOCAL lATCoHeadingHeardFromPilots: tHeadings INITIALIZATION hATCoPressOrReleaseSwitchToTalk = FALSE; lATCoSelectedClearance = CorrectHeading; lATCoHeadingHeardFromPilots = IncorrectHeading; % Variables for pPF INPUT iHeadingWindowHeading: tHeadings OUTPUT hPFPressOrReleaseSwitchToTalk: BOOLEAN OUTPUT hPFEngageHeadingSelection: BOOLEAN OUTPUT hPFPushHeadingSelectKnob: BOOLEAN OUTPUT hPFPullHeadingSelectKnob: BOOLEAN OUTPUT hPFRotateToHeading: tHeadings LOCAL lPFHeadingFromATCo: tHeadings LOCAL lPFHeadingFromPM: tHeadings LOCAL lPFItemPointedAtByPM: tPointableItems INITIALIZATION hPFPressOrReleaseSwitchToTalk = FALSE; hPFEngageHeadingSelection = FALSE; hPFPushHeadingSelectKnob = FALSE; hPFPullHeadingSelectKnob = FALSE; lPFHeadingFromATCo = IncorrectHeading; lPFHeadingFromPM = IncorrectHeading; lPFItemPointedAtByPM = Nothing; % Variables for pPM OUTPUT hPMPressOrReleaseSwitchToTalk: BOOLEAN LOCAL sPMTalk: tHeadings LOCAL sPMPoint: tPointableItems LOCAL lPMHeadingFromATCo: tHeadings LOCAL lPFHeadingFromPF: tHeadings INITIALIZATION hPMPressOrReleaseSwitchToTalk = FALSE; lPMHeadingFromATCo = IncorrectHeading; lPFHeadingFromPF = IncorrectHeading; % Variables for Shared aChangeHeading LOCAL aChangeHeading: tActivityState LOCAL aCommunicateAndConfirmHeading: tActivityState LOCAL aToggleATCoTalk: tActivityState LOCAL hATCoPressOrReleaseSwitchToTalk_1: tActivityState LOCAL aComHeading: tActivityState LOCAL sATCoTalk_2: tActivityState LOCAL lPFHeadingFromATCo_3: tActivityState LOCAL lPMHeadingFromATCo_4: tActivityState LOCAL aToggleATCoTalk_5: tActivityState LOCAL hATCoPressOrReleaseSwitchToTalk_1_5: tActivityState LOCAL aMakeTheChange: tActivityState LOCAL hPFPushHeadingSelectKnob_6: tActivityState LOCAL hPFRotateToHeading_7: tActivityState LOCAL hPFPullHeadingSelectKnob_8: tActivityState LOCAL aConfirmTheChange: tActivityState LOCAL aPointAtHeadingWindow: tActivityState LOCAL sPMPoint_9: tActivityState LOCAL lPFItemPointedAtByPM_10: tActivityState LOCAL aReadbackTheHeading: tActivityState LOCAL aTogglePMTalk: tActivityState LOCAL hPMPressOrReleaseSwitchToTalk_11: tActivityState LOCAL aComConfirmHeading: tActivityState LOCAL sPMTalk_12: tActivityState LOCAL lATCoHeadingHeardFromPilots_13: tActivityState LOCAL lPFHeadingFromPM_14: tActivityState LOCAL aTogglePMTalk_15: tActivityState LOCAL hPMPressOrReleaseSwitchToTalk_11_15: tActivityState LOCAL aUpdateTheHeading: tActivityState LOCAL aDialInUpdatedHeading: tActivityState LOCAL hPFPushHeadingSelectKnob_16: tActivityState LOCAL hPFRotateToHeading_17: tActivityState LOCAL hPFPullHeadingSelectKnob_18: tActivityState LOCAL aCorrectThePF: tActivityState LOCAL aPointAtHeadingWindow2: tActivityState LOCAL sPMPoint_19: tActivityState LOCAL lPFItemPointedAtByPM_20: tActivityState LOCAL aRepeatTheHeading: tActivityState LOCAL sPMTalk_21: tActivityState LOCAL lPFHeadingFromPM_22: tActivityState LOCAL aExecuteTheChange: tActivityState LOCAL hPFEngageHeadingSelection_23: tActivityState INITIALIZATION aChangeHeading = actReady; aCommunicateAndConfirmHeading = actReady; aToggleATCoTalk = actReady; hATCoPressOrReleaseSwitchToTalk_1 = actReady; aComHeading = actReady; sATCoTalk_2 = actReady; lPFHeadingFromATCo_3 = actReady; lPMHeadingFromATCo_4 = actReady; aToggleATCoTalk_5 = actReady; hATCoPressOrReleaseSwitchToTalk_1_5 = actReady; aMakeTheChange = actReady; hPFPushHeadingSelectKnob_6 = actReady; hPFRotateToHeading_7 = actReady; hPFPullHeadingSelectKnob_8 = actReady; aConfirmTheChange = actReady; aPointAtHeadingWindow = actReady; sPMPoint_9 = actReady; lPFItemPointedAtByPM_10 = actReady; aReadbackTheHeading = actReady; aTogglePMTalk = actReady; hPMPressOrReleaseSwitchToTalk_11 = actReady; aComConfirmHeading = actReady; sPMTalk_12 = actReady; lATCoHeadingHeardFromPilots_13 = actReady; lPFHeadingFromPM_14 = actReady; aTogglePMTalk_15 = actReady; hPMPressOrReleaseSwitchToTalk_11_15 = actReady; aUpdateTheHeading = actReady; aDialInUpdatedHeading = actReady; hPFPushHeadingSelectKnob_16 = actReady; hPFRotateToHeading_17 = actReady; hPFPullHeadingSelectKnob_18 = actReady; aCorrectThePF = actReady; aPointAtHeadingWindow2 = actReady; sPMPoint_19 = actReady; lPFItemPointedAtByPM_20 = actReady; aRepeatTheHeading = actReady; sPMTalk_21 = actReady; lPFHeadingFromPM_22 = actReady; aExecuteTheChange = actReady; hPFEngageHeadingSelection_23 = actReady; % Handshake variables INPUT ready: BOOLEAN OUTPUT submitted: BOOLEAN LOCAL lComErrorCount: [0..cComErrorMax] INITIALIZATION submitted = FALSE; lComErrorCount = 0; TRANSITION [ aChangeHeading = actReady AND (lATCoSelectedClearance = CorrectHeading) --> aChangeHeading' = actExecuting; []aChangeHeading = actExecuting AND aExecuteTheChange = actDone --> aChangeHeading' = actDone; []aChangeHeading = actDone --> aChangeHeading' = actReady; aCommunicateAndConfirmHeading' = actReady; aToggleATCoTalk' = actReady; hATCoPressOrReleaseSwitchToTalk_1' = actReady; aComHeading' = actReady; sATCoTalk_2' = actReady; lPFHeadingFromATCo_3' = actReady; lPMHeadingFromATCo_4' = actReady; aToggleATCoTalk_5' = actReady; hATCoPressOrReleaseSwitchToTalk_1_5' = actReady; aMakeTheChange' = actReady; hPFPushHeadingSelectKnob_6' = actReady; hPFRotateToHeading_7' = actReady; hPFPullHeadingSelectKnob_8' = actReady; aConfirmTheChange' = actReady; aPointAtHeadingWindow' = actReady; sPMPoint_9' = actReady; lPFItemPointedAtByPM_10' = actReady; aReadbackTheHeading' = actReady; aTogglePMTalk' = actReady; hPMPressOrReleaseSwitchToTalk_11' = actReady; aComConfirmHeading' = actReady; sPMTalk_12' = actReady; lATCoHeadingHeardFromPilots_13' = actReady; lPFHeadingFromPM_14' = actReady; aTogglePMTalk_15' = actReady; hPMPressOrReleaseSwitchToTalk_11_15' = actReady; aUpdateTheHeading' = actReady; aDialInUpdatedHeading' = actReady; hPFPushHeadingSelectKnob_16' = actReady; hPFRotateToHeading_17' = actReady; hPFPullHeadingSelectKnob_18' = actReady; aCorrectThePF' = actReady; aPointAtHeadingWindow2' = actReady; sPMPoint_19' = actReady; lPFItemPointedAtByPM_20' = actReady; aRepeatTheHeading' = actReady; sPMTalk_21' = actReady; lPFHeadingFromPM_22' = actReady; aExecuteTheChange' = actReady; hPFEngageHeadingSelection_23' = actReady; []aCommunicateAndConfirmHeading = actReady AND aChangeHeading = actExecuting AND NOT (lATCoSelectedClearance = lATCoHeadingHeardFromPilots) --> aCommunicateAndConfirmHeading' = actExecuting; []aCommunicateAndConfirmHeading = actExecuting AND aUpdateTheHeading = actDone AND (lATCoSelectedClearance = lATCoHeadingHeardFromPilots) --> aCommunicateAndConfirmHeading' = actDone; []aCommunicateAndConfirmHeading = actReady AND aChangeHeading = actExecuting AND (lATCoSelectedClearance = lATCoHeadingHeardFromPilots) --> aCommunicateAndConfirmHeading' = actDone; []aCommunicateAndConfirmHeading = actExecuting AND aUpdateTheHeading = actDone AND (lATCoSelectedClearance /= lATCoHeadingHeardFromPilots) AND NOT (lATCoSelectedClearance = lATCoHeadingHeardFromPilots) --> aCommunicateAndConfirmHeading' = actExecuting; aToggleATCoTalk' = actReady; hATCoPressOrReleaseSwitchToTalk_1' = actReady; aComHeading' = actReady; sATCoTalk_2' = actReady; lPFHeadingFromATCo_3' = actReady; lPMHeadingFromATCo_4' = actReady; aToggleATCoTalk_5' = actReady; hATCoPressOrReleaseSwitchToTalk_1_5' = actReady; aMakeTheChange' = actReady; hPFPushHeadingSelectKnob_6' = actReady; hPFRotateToHeading_7' = actReady; hPFPullHeadingSelectKnob_8' = actReady; aConfirmTheChange' = actReady; aPointAtHeadingWindow' = actReady; sPMPoint_9' = actReady; lPFItemPointedAtByPM_10' = actReady; aReadbackTheHeading' = actReady; aTogglePMTalk' = actReady; hPMPressOrReleaseSwitchToTalk_11' = actReady; aComConfirmHeading' = actReady; sPMTalk_12' = actReady; lATCoHeadingHeardFromPilots_13' = actReady; lPFHeadingFromPM_14' = actReady; aTogglePMTalk_15' = actReady; hPMPressOrReleaseSwitchToTalk_11_15' = actReady; aUpdateTheHeading' = actReady; aDialInUpdatedHeading' = actReady; hPFPushHeadingSelectKnob_16' = actReady; hPFRotateToHeading_17' = actReady; hPFPullHeadingSelectKnob_18' = actReady; aCorrectThePF' = actReady; aPointAtHeadingWindow2' = actReady; sPMPoint_19' = actReady; lPFItemPointedAtByPM_20' = actReady; aRepeatTheHeading' = actReady; sPMTalk_21' = actReady; lPFHeadingFromPM_22' = actReady; []aToggleATCoTalk = actReady AND aCommunicateAndConfirmHeading = actExecuting --> aToggleATCoTalk' = actExecuting; []aToggleATCoTalk = actExecuting AND hATCoPressOrReleaseSwitchToTalk_1 = actDone --> aToggleATCoTalk' = actDone; []hATCoPressOrReleaseSwitchToTalk_1 = actReady AND aToggleATCoTalk = actExecuting AND ready --> hATCoPressOrReleaseSwitchToTalk_1' = actExecuting; hATCoPressOrReleaseSwitchToTalk' = NOT hATCoPressOrReleaseSwitchToTalk; submitted' = TRUE; []aComHeading = actReady AND aCommunicateAndConfirmHeading = actExecuting AND aToggleATCoTalk = actDone --> aComHeading' = actExecuting; []aComHeading = actExecuting AND sATCoTalk_2 = actDone AND lPFHeadingFromATCo_3 = actDone AND lPMHeadingFromATCo_4 = actDone --> aComHeading' = actDone; []aComHeading = actExecuting AND sATCoTalk_2 = actReady AND lPFHeadingFromATCo_3 = actReady AND lPMHeadingFromATCo_4 = actReady AND ready --> sATCoTalk_2' = actDone; sATCoTalk' = lATCoSelectedClearance; lPFHeadingFromATCo_3' = actDone; lPFHeadingFromATCo' = sATCoTalk'; lPMHeadingFromATCo_4' = actDone; lPMHeadingFromATCo' = sATCoTalk'; []aComHeading = actExecuting AND sATCoTalk_2 = actReady AND lPFHeadingFromATCo_3 = actReady AND lPMHeadingFromATCo_4 = actReady AND ready AND (lComErrorCount < cComErrorMax) --> sATCoTalk_2' = actDone; sATCoTalk' IN {x: tHeadings | TRUE}; lPFHeadingFromATCo_3' = actDone; lPFHeadingFromATCo' IN {x: tHeadings | TRUE}; lPMHeadingFromATCo_4' = actDone; lPMHeadingFromATCo' IN {x: tHeadings | TRUE}; lComErrorCount' = IF (sATCoTalk' /= lATCoSelectedClearance) OR (lPFHeadingFromATCo' /= lATCoSelectedClearance) OR (lPMHeadingFromATCo' /= lATCoSelectedClearance) THEN lComErrorCount + 1 ELSE lComErrorCount ENDIF; []aToggleATCoTalk_5 = actReady AND aCommunicateAndConfirmHeading = actExecuting AND aComHeading = actDone --> aToggleATCoTalk_5' = actExecuting; []aToggleATCoTalk_5 = actExecuting AND hATCoPressOrReleaseSwitchToTalk_1_5 = actDone --> aToggleATCoTalk_5' = actDone; []hATCoPressOrReleaseSwitchToTalk_1_5 = actReady AND aToggleATCoTalk_5 = actExecuting AND ready --> hATCoPressOrReleaseSwitchToTalk_1_5' = actExecuting; hATCoPressOrReleaseSwitchToTalk' = NOT hATCoPressOrReleaseSwitchToTalk; submitted' = TRUE; []aMakeTheChange = actReady AND aCommunicateAndConfirmHeading = actExecuting AND aToggleATCoTalk_5 = actDone --> aMakeTheChange' = actExecuting; []aMakeTheChange = actExecuting AND hPFPullHeadingSelectKnob_8 = actDone --> aMakeTheChange' = actDone; []hPFPushHeadingSelectKnob_6 = actReady AND aMakeTheChange = actExecuting AND ready --> hPFPushHeadingSelectKnob_6' = actExecuting; hPFPushHeadingSelectKnob' = TRUE; submitted' = TRUE; []hPFRotateToHeading_7 = actReady AND aMakeTheChange = actExecuting AND hPFPushHeadingSelectKnob_6 = actDone AND ready --> hPFRotateToHeading_7' = actExecuting; hPFRotateToHeading' = lPFHeadingFromATCo; submitted' = TRUE; []hPFPullHeadingSelectKnob_8 = actReady AND aMakeTheChange = actExecuting AND hPFRotateToHeading_7 = actDone AND ready --> hPFPullHeadingSelectKnob_8' = actExecuting; hPFPullHeadingSelectKnob' = TRUE; submitted' = TRUE; []aConfirmTheChange = actReady AND aCommunicateAndConfirmHeading = actExecuting AND aMakeTheChange = actDone --> aConfirmTheChange' = actExecuting; []aConfirmTheChange = actExecuting AND aPointAtHeadingWindow = actDone AND aReadbackTheHeading = actDone --> aConfirmTheChange' = actDone; []aPointAtHeadingWindow = actReady AND aConfirmTheChange = actExecuting --> aPointAtHeadingWindow' = actExecuting; []aPointAtHeadingWindow = actExecuting AND sPMPoint_9 = actDone AND lPFItemPointedAtByPM_10 = actDone --> aPointAtHeadingWindow' = actDone; []aPointAtHeadingWindow = actExecuting AND sPMPoint_9 = actReady AND lPFItemPointedAtByPM_10 = actReady AND ready --> sPMPoint_9' = actDone; sPMPoint' = HeadingWindow; lPFItemPointedAtByPM_10' = actDone; lPFItemPointedAtByPM' = sPMPoint'; []aPointAtHeadingWindow = actExecuting AND sPMPoint_9 = actReady AND lPFItemPointedAtByPM_10 = actReady AND ready AND (lComErrorCount < cComErrorMax) --> sPMPoint_9' = actDone; sPMPoint' IN {x: tPointableItems | TRUE}; lPFItemPointedAtByPM_10' = actDone; lPFItemPointedAtByPM' IN {x: tPointableItems | TRUE}; lComErrorCount' = IF (sPMPoint' /= HeadingWindow) OR (lPFItemPointedAtByPM' /= HeadingWindow) THEN lComErrorCount + 1 ELSE lComErrorCount ENDIF; []aReadbackTheHeading = actReady AND aConfirmTheChange = actExecuting --> aReadbackTheHeading' = actExecuting; []aReadbackTheHeading = actExecuting AND aTogglePMTalk_15 = actDone --> aReadbackTheHeading' = actDone; []aTogglePMTalk = actReady AND aReadbackTheHeading = actExecuting --> aTogglePMTalk' = actExecuting; []aTogglePMTalk = actExecuting AND hPMPressOrReleaseSwitchToTalk_11 = actDone --> aTogglePMTalk' = actDone; []hPMPressOrReleaseSwitchToTalk_11 = actReady AND aTogglePMTalk = actExecuting AND ready --> hPMPressOrReleaseSwitchToTalk_11' = actExecuting; hPMPressOrReleaseSwitchToTalk' = NOT hPMPressOrReleaseSwitchToTalk; submitted' = TRUE; []aComConfirmHeading = actReady AND aReadbackTheHeading = actExecuting AND aTogglePMTalk = actDone --> aComConfirmHeading' = actExecuting; []aComConfirmHeading = actExecuting AND sPMTalk_12 = actDone AND lATCoHeadingHeardFromPilots_13 = actDone AND lPFHeadingFromPM_14 = actDone --> aComConfirmHeading' = actDone; []aComConfirmHeading = actExecuting AND sPMTalk_12 = actReady AND lATCoHeadingHeardFromPilots_13 = actReady AND lPFHeadingFromPM_14 = actReady AND ready --> sPMTalk_12' = actDone; sPMTalk' = lPMHeadingFromATCo; lATCoHeadingHeardFromPilots_13' = actDone; lATCoHeadingHeardFromPilots' = sPMTalk'; lPFHeadingFromPM_14' = actDone; lPFHeadingFromPM' = sPMTalk'; []aComConfirmHeading = actExecuting AND sPMTalk_12 = actReady AND lATCoHeadingHeardFromPilots_13 = actReady AND lPFHeadingFromPM_14 = actReady AND ready AND (lComErrorCount < cComErrorMax) --> sPMTalk_12' = actDone; sPMTalk' IN {x: tHeadings | TRUE}; lATCoHeadingHeardFromPilots_13' = actDone; lATCoHeadingHeardFromPilots' IN {x: tHeadings | TRUE}; lPFHeadingFromPM_14' = actDone; lPFHeadingFromPM' IN {x: tHeadings | TRUE}; lComErrorCount' = IF (sPMTalk' /= lPMHeadingFromATCo) OR (lATCoHeadingHeardFromPilots' /= lPMHeadingFromATCo) OR (lPFHeadingFromPM' /= lPMHeadingFromATCo) THEN lComErrorCount + 1 ELSE lComErrorCount ENDIF; []aTogglePMTalk_15 = actReady AND aReadbackTheHeading = actExecuting AND aComConfirmHeading = actDone --> aTogglePMTalk_15' = actExecuting; []aTogglePMTalk_15 = actExecuting AND hPMPressOrReleaseSwitchToTalk_11_15 = actDone --> aTogglePMTalk_15' = actDone; []hPMPressOrReleaseSwitchToTalk_11_15 = actReady AND aTogglePMTalk_15 = actExecuting AND ready --> hPMPressOrReleaseSwitchToTalk_11_15' = actExecuting; hPMPressOrReleaseSwitchToTalk' = NOT hPMPressOrReleaseSwitchToTalk; submitted' = TRUE; []aUpdateTheHeading = actReady AND aCommunicateAndConfirmHeading = actExecuting AND aConfirmTheChange = actDone AND NOT (lPFHeadingFromPM = iHeadingWindowHeading) --> aUpdateTheHeading' = actExecuting; []aUpdateTheHeading = actExecuting AND aCorrectThePF = actDone AND (lPFHeadingFromPM = iHeadingWindowHeading) --> aUpdateTheHeading' = actDone; []aUpdateTheHeading = actReady AND aCommunicateAndConfirmHeading = actExecuting AND aConfirmTheChange = actDone AND (lPFHeadingFromPM = iHeadingWindowHeading) --> aUpdateTheHeading' = actDone; []aUpdateTheHeading = actExecuting AND aCorrectThePF = actDone AND (iHeadingWindowHeading /= lPMHeadingFromATCo) AND NOT (lPFHeadingFromPM = iHeadingWindowHeading) --> aUpdateTheHeading' = actExecuting; aDialInUpdatedHeading' = actReady; hPFPushHeadingSelectKnob_16' = actReady; hPFRotateToHeading_17' = actReady; hPFPullHeadingSelectKnob_18' = actReady; aCorrectThePF' = actReady; aPointAtHeadingWindow2' = actReady; sPMPoint_19' = actReady; lPFItemPointedAtByPM_20' = actReady; aRepeatTheHeading' = actReady; sPMTalk_21' = actReady; lPFHeadingFromPM_22' = actReady; []aDialInUpdatedHeading = actReady AND aUpdateTheHeading = actExecuting --> aDialInUpdatedHeading' = actExecuting; []aDialInUpdatedHeading = actExecuting AND hPFPullHeadingSelectKnob_18 = actDone --> aDialInUpdatedHeading' = actDone; []hPFPushHeadingSelectKnob_16 = actReady AND aDialInUpdatedHeading = actExecuting AND ready --> hPFPushHeadingSelectKnob_16' = actExecuting; hPFPushHeadingSelectKnob' = TRUE; submitted' = TRUE; []hPFRotateToHeading_17 = actReady AND aDialInUpdatedHeading = actExecuting AND hPFPushHeadingSelectKnob_16 = actDone AND ready --> hPFRotateToHeading_17' = actExecuting; hPFRotateToHeading' = lPFHeadingFromPM; submitted' = TRUE; []hPFPullHeadingSelectKnob_18 = actReady AND aDialInUpdatedHeading = actExecuting AND hPFRotateToHeading_17 = actDone AND ready --> hPFPullHeadingSelectKnob_18' = actExecuting; hPFPullHeadingSelectKnob' = TRUE; submitted' = TRUE; []aCorrectThePF = actReady AND aUpdateTheHeading = actExecuting AND aDialInUpdatedHeading = actDone AND NOT (iHeadingWindowHeading = lPMHeadingFromATCo OR (aPointAtHeadingWindow2 = actDone AND aRepeatTheHeading = actDone)) --> aCorrectThePF' = actExecuting; []aCorrectThePF = actExecuting AND aPointAtHeadingWindow2 = actDone AND aRepeatTheHeading = actDone AND (iHeadingWindowHeading = lPMHeadingFromATCo OR (aPointAtHeadingWindow2 = actDone AND aRepeatTheHeading = actDone)) --> aCorrectThePF' = actDone; []aCorrectThePF = actReady AND aUpdateTheHeading = actExecuting AND aDialInUpdatedHeading = actDone AND (iHeadingWindowHeading = lPMHeadingFromATCo OR (aPointAtHeadingWindow2 = actDone AND aRepeatTheHeading = actDone)) --> aCorrectThePF' = actDone; []aPointAtHeadingWindow2 = actReady AND aCorrectThePF = actExecuting --> aPointAtHeadingWindow2' = actExecuting; []aPointAtHeadingWindow2 = actExecuting AND sPMPoint_19 = actDone AND lPFItemPointedAtByPM_20 = actDone --> aPointAtHeadingWindow2' = actDone; []aPointAtHeadingWindow2 = actExecuting AND sPMPoint_19 = actReady AND lPFItemPointedAtByPM_20 = actReady AND ready --> sPMPoint_19' = actDone; sPMPoint' = HeadingWindow; lPFItemPointedAtByPM_20' = actDone; lPFItemPointedAtByPM' = sPMPoint'; []aPointAtHeadingWindow2 = actExecuting AND sPMPoint_19 = actReady AND lPFItemPointedAtByPM_20 = actReady AND ready AND (lComErrorCount < cComErrorMax) --> sPMPoint_19' = actDone; sPMPoint' IN {x: tPointableItems | TRUE}; lPFItemPointedAtByPM_20' = actDone; lPFItemPointedAtByPM' IN {x: tPointableItems | TRUE}; lComErrorCount' = IF (sPMPoint' /= HeadingWindow) OR (lPFItemPointedAtByPM' /= HeadingWindow) THEN lComErrorCount + 1 ELSE lComErrorCount ENDIF; []aRepeatTheHeading = actReady AND aCorrectThePF = actExecuting --> aRepeatTheHeading' = actExecuting; []aRepeatTheHeading = actExecuting AND sPMTalk_21 = actDone AND lPFHeadingFromPM_22 = actDone --> aRepeatTheHeading' = actDone; []aRepeatTheHeading = actExecuting AND sPMTalk_21 = actReady AND lPFHeadingFromPM_22 = actReady AND ready --> sPMTalk_21' = actDone; sPMTalk' = lPMHeadingFromATCo; lPFHeadingFromPM_22' = actDone; lPFHeadingFromPM' = sPMTalk'; []aRepeatTheHeading = actExecuting AND sPMTalk_21 = actReady AND lPFHeadingFromPM_22 = actReady AND ready AND (lComErrorCount < cComErrorMax) --> sPMTalk_21' = actDone; sPMTalk' IN {x: tHeadings | TRUE}; lPFHeadingFromPM_22' = actDone; lPFHeadingFromPM' IN {x: tHeadings | TRUE}; lComErrorCount' = IF (sPMTalk' /= lPMHeadingFromATCo) OR (lPFHeadingFromPM' /= lPMHeadingFromATCo) THEN lComErrorCount + 1 ELSE lComErrorCount ENDIF; []aExecuteTheChange = actReady AND aChangeHeading = actExecuting AND aCommunicateAndConfirmHeading = actDone --> aExecuteTheChange' = actExecuting; []aExecuteTheChange = actExecuting AND hPFEngageHeadingSelection_23 = actDone --> aExecuteTheChange' = actDone; []hPFEngageHeadingSelection_23 = actReady AND aExecuteTheChange = actExecuting AND ready --> hPFEngageHeadingSelection_23' = actExecuting; hPFEngageHeadingSelection' = TRUE; submitted' = TRUE; []submitted AND NOT ready --> submitted' = FALSE; hATCoPressOrReleaseSwitchToTalk_1' = IF hATCoPressOrReleaseSwitchToTalk_1 = actExecuting THEN actDone ELSE hATCoPressOrReleaseSwitchToTalk_1 ENDIF; sATCoTalk_2' = IF sATCoTalk_2 = actExecuting THEN actDone ELSE sATCoTalk_2 ENDIF; lPFHeadingFromATCo_3' = IF lPFHeadingFromATCo_3 = actExecuting THEN actDone ELSE lPFHeadingFromATCo_3 ENDIF; lPMHeadingFromATCo_4' = IF lPMHeadingFromATCo_4 = actExecuting THEN actDone ELSE lPMHeadingFromATCo_4 ENDIF; hATCoPressOrReleaseSwitchToTalk_1_5' = IF hATCoPressOrReleaseSwitchToTalk_1_5 = actExecuting THEN actDone ELSE hATCoPressOrReleaseSwitchToTalk_1_5 ENDIF; hPFPushHeadingSelectKnob_6' = IF hPFPushHeadingSelectKnob_6 = actExecuting THEN actDone ELSE hPFPushHeadingSelectKnob_6 ENDIF; hPFRotateToHeading_7' = IF hPFRotateToHeading_7 = actExecuting THEN actDone ELSE hPFRotateToHeading_7 ENDIF; hPFPullHeadingSelectKnob_8' = IF hPFPullHeadingSelectKnob_8 = actExecuting THEN actDone ELSE hPFPullHeadingSelectKnob_8 ENDIF; sPMPoint_9' = IF sPMPoint_9 = actExecuting THEN actDone ELSE sPMPoint_9 ENDIF; lPFItemPointedAtByPM_10' = IF lPFItemPointedAtByPM_10 = actExecuting THEN actDone ELSE lPFItemPointedAtByPM_10 ENDIF; hPMPressOrReleaseSwitchToTalk_11' = IF hPMPressOrReleaseSwitchToTalk_11 = actExecuting THEN actDone ELSE hPMPressOrReleaseSwitchToTalk_11 ENDIF; sPMTalk_12' = IF sPMTalk_12 = actExecuting THEN actDone ELSE sPMTalk_12 ENDIF; lATCoHeadingHeardFromPilots_13' = IF lATCoHeadingHeardFromPilots_13 = actExecuting THEN actDone ELSE lATCoHeadingHeardFromPilots_13 ENDIF; lPFHeadingFromPM_14' = IF lPFHeadingFromPM_14 = actExecuting THEN actDone ELSE lPFHeadingFromPM_14 ENDIF; hPMPressOrReleaseSwitchToTalk_11_15' = IF hPMPressOrReleaseSwitchToTalk_11_15 = actExecuting THEN actDone ELSE hPMPressOrReleaseSwitchToTalk_11_15 ENDIF; hPFPushHeadingSelectKnob_16' = IF hPFPushHeadingSelectKnob_16 = actExecuting THEN actDone ELSE hPFPushHeadingSelectKnob_16 ENDIF; hPFRotateToHeading_17' = IF hPFRotateToHeading_17 = actExecuting THEN actDone ELSE hPFRotateToHeading_17 ENDIF; hPFPullHeadingSelectKnob_18' = IF hPFPullHeadingSelectKnob_18 = actExecuting THEN actDone ELSE hPFPullHeadingSelectKnob_18 ENDIF; sPMPoint_19' = IF sPMPoint_19 = actExecuting THEN actDone ELSE sPMPoint_19 ENDIF; lPFItemPointedAtByPM_20' = IF lPFItemPointedAtByPM_20 = actExecuting THEN actDone ELSE lPFItemPointedAtByPM_20 ENDIF; sPMTalk_21' = IF sPMTalk_21 = actExecuting THEN actDone ELSE sPMTalk_21 ENDIF; lPFHeadingFromPM_22' = IF lPFHeadingFromPM_22 = actExecuting THEN actDone ELSE lPFHeadingFromPM_22 ENDIF; hPFEngageHeadingSelection_23' = IF hPFEngageHeadingSelection_23 = actExecuting THEN actDone ELSE hPFEngageHeadingSelection_23 ENDIF; hPFEngageHeadingSelection' = FALSE; hPFPushHeadingSelectKnob' = FALSE; hPFPullHeadingSelectKnob' = FALSE; ]; END; system: MODULE = BEGIN INPUT hATCoPressOrReleaseSwitchToTalk: BOOLEAN INPUT hPFPressOrReleaseSwitchToTalk: BOOLEAN INPUT hPFEngageHeadingSelection: BOOLEAN INPUT hPFPushHeadingSelectKnob: BOOLEAN INPUT hPFPullHeadingSelectKnob: BOOLEAN INPUT hPFRotateToHeading: tHeadings INPUT hPMPressOrReleaseSwitchToTalk: BOOLEAN OUTPUT iHeadingWindowHeading: tHeadings OUTPUT ready: BOOLEAN INPUT submitted: BOOLEAN INITIALIZATION ready = FALSE; TRANSITION [ NOT (ready OR submitted) --> ready' = TRUE; []ready AND submitted --> iHeadingWindowHeading' = IF iHeadingWindowHeading /= hPFRotateToHeading THEN hPFRotateToHeading ELSE iHeadingWindowHeading ENDIF; ready' = FALSE; ]; END; model: MODULE = humanOperators [] system; Th1 : THEOREM model |- G((aChangeHeading = actDone) => (iHeadingWindowHeading = lATCoSelectedClearance)); Th2: THEOREM model |- F(aChangeHeading = actDone); END