aircraftTORDeX : CONTEXT = BEGIN cCapture: INTEGER = 0; cOneDot: INTEGER = 1; cTwoDots: INTEGER = 2; cAlive: INTEGER = 3; cInactive: INTEGER = 4; cStartPosition: INTEGER = 0; cAlivePosition: INTEGER = cStartPosition + 1; cTwoDotPosition: INTEGER = cAlivePosition + 5; cOneDotPosition: INTEGER = cTwoDotPosition + 5; cCapturePosition: INTEGER = cOneDotPosition + 6; cEndPosition: INTEGER = cCapturePosition + 1; cGearDoorsClosed: INTEGER = 0; cGearDoorsOpen: INTEGER = 10; tActivityState: TYPE = {actReady, actExecuting, actDone}; tLight: TYPE = {On, Off}; tLever: TYPE = {Unpulled, Pulled}; tFlapsDegrees: TYPE = {Flaps0, Flaps25, Flaps40}; tGSPosition: TYPE = [cCapture..cInactive]; tSpoiler: TYPE = {Unarmed, Armed, Deployed}; tPosition: TYPE = [cStartPosition..cEndPosition]; tLandingGear: TYPE = {Up, Down}; tGearDoorPosition: TYPE = [cGearDoorsClosed..cGearDoorsOpen]; tSwitch: TYPE = {Switched, Unswitched}; pPilot: MODULE = BEGIN INPUT iSpoilerIndicator: tLight INPUT iSpoilerLever: tLever INPUT iGearDoorLight: tLight INPUT iThreeGearLights: tLight INPUT iGearLever: tLever INPUT iFlapsGauge: tFlapsDegrees INPUT iGSIndicator: tGSPosition INPUT iIgnitionLight: tLight INPUT iIgnitionSwitch: tSwitch INPUT pPilot_Ready: BOOLEAN OUTPUT hArmSpoiler: BOOLEAN OUTPUT hSetFlaps25: BOOLEAN OUTPUT hSetFlaps40: BOOLEAN OUTPUT hPullGearLever: BOOLEAN OUTPUT hFlipIgnitionSwitch: BOOLEAN OUTPUT pPilot_Submitted: BOOLEAN LOCAL aPrepareForLanding: tActivityState LOCAL aOverrideIgnition: tActivityState LOCAL hFlipIgnitionSwitch_1: tActivityState LOCAL aDeployLandingGear: tActivityState LOCAL hPullGearLever_2: tActivityState LOCAL aSetFlaps25: tActivityState LOCAL hSetFlaps25_3: tActivityState LOCAL aSetSpoliers: tActivityState LOCAL hArmSpoiler_4: tActivityState LOCAL aSetFlaps40: tActivityState LOCAL hSetFlaps40_5: tActivityState INITIALIZATION hArmSpoiler = FALSE; hSetFlaps25 = FALSE; hSetFlaps40 = FALSE; hPullGearLever = FALSE; hFlipIgnitionSwitch = FALSE; pPilot_Submitted = FALSE; aPrepareForLanding = actReady; aOverrideIgnition = actReady; hFlipIgnitionSwitch_1 = actReady; aDeployLandingGear = actReady; hPullGearLever_2 = actReady; aSetFlaps25 = actReady; hSetFlaps25_3 = actReady; aSetSpoliers = actReady; hArmSpoiler_4 = actReady; aSetFlaps40 = actReady; hSetFlaps40_5 = actReady; TRANSITION [ aPrepareForLanding = actReady AND (iGSIndicator <= cInactive) --> aPrepareForLanding' = actExecuting; []aPrepareForLanding = actExecuting AND aSetFlaps40 = actDone --> aPrepareForLanding' = actDone; %[]aPrepareForLanding = actDone --> % aPrepareForLanding' = actReady; % aOverrideIgnition' = actReady; % hFlipIgnitionSwitch_1' = actReady; % aDeployLandingGear' = actReady; % hPullGearLever_2' = actReady; % aSetFlaps25' = actReady; % hSetFlaps25_3' = actReady; % aSetSpoliers' = actReady; % hArmSpoiler_4' = actReady; % aSetFlaps40' = actReady; % hSetFlaps40_5' = actReady; []aOverrideIgnition = actReady AND aPrepareForLanding = actExecuting AND (iGSIndicator <= cInactive AND iIgnitionLight = Off) AND NOT (iIgnitionLight = On) --> aOverrideIgnition' = actExecuting; []aOverrideIgnition = actExecuting AND hFlipIgnitionSwitch_1 = actDone AND (iIgnitionLight = On) --> aOverrideIgnition' = actDone; []aOverrideIgnition = actReady AND aPrepareForLanding = actExecuting AND (iIgnitionLight = On) --> aOverrideIgnition' = actDone; []hFlipIgnitionSwitch_1 = actReady AND aOverrideIgnition = actExecuting AND pPilot_Ready --> hFlipIgnitionSwitch_1' = actExecuting; hFlipIgnitionSwitch' = TRUE; pPilot_Submitted' = TRUE; []aDeployLandingGear = actReady AND aPrepareForLanding = actExecuting AND aOverrideIgnition = actDone AND (iGSIndicator <= cAlive AND iThreeGearLights = Off) AND NOT (iThreeGearLights = On) --> aDeployLandingGear' = actExecuting; []aDeployLandingGear = actExecuting AND hPullGearLever_2 = actDone AND (iThreeGearLights = On) --> aDeployLandingGear' = actDone; []aDeployLandingGear = actReady AND aPrepareForLanding = actExecuting AND aOverrideIgnition = actDone AND (iThreeGearLights = On) --> aDeployLandingGear' = actDone; []hPullGearLever_2 = actReady AND aDeployLandingGear = actExecuting AND pPilot_Ready --> hPullGearLever_2' = actExecuting; hPullGearLever' = TRUE; pPilot_Submitted' = TRUE; []aSetFlaps25 = actReady AND aPrepareForLanding = actExecuting AND aDeployLandingGear = actDone AND (iGSIndicator <= cOneDot AND iGSIndicator > cCapture AND iFlapsGauge /= Flaps25) AND NOT (iFlapsGauge = Flaps25 OR iGSIndicator = cCapture) --> aSetFlaps25' = actExecuting; []aSetFlaps25 = actExecuting AND hSetFlaps25_3 = actDone AND (iFlapsGauge = Flaps25 OR iGSIndicator = cCapture) --> aSetFlaps25' = actDone; []aSetFlaps25 = actReady AND aPrepareForLanding = actExecuting AND aDeployLandingGear = actDone AND (iFlapsGauge = Flaps25 OR iGSIndicator = cCapture) --> aSetFlaps25' = actDone; []hSetFlaps25_3 = actReady AND aSetFlaps25 = actExecuting AND pPilot_Ready --> hSetFlaps25_3' = actExecuting; hSetFlaps25' = TRUE; pPilot_Submitted' = TRUE; []aSetSpoliers = actReady AND aPrepareForLanding = actExecuting AND aSetFlaps25 = actDone AND (iGearDoorLight = Off AND iSpoilerIndicator = Off AND iThreeGearLights = On) AND NOT (iSpoilerIndicator = On) --> aSetSpoliers' = actExecuting; []aSetSpoliers = actExecuting AND hArmSpoiler_4 = actDone AND (iSpoilerIndicator = On) --> aSetSpoliers' = actDone; []aSetSpoliers = actReady AND aPrepareForLanding = actExecuting AND aSetFlaps25 = actDone AND (iSpoilerIndicator = On) --> aSetSpoliers' = actDone; []hArmSpoiler_4 = actReady AND aSetSpoliers = actExecuting AND pPilot_Ready --> hArmSpoiler_4' = actExecuting; hArmSpoiler' = TRUE; pPilot_Submitted' = TRUE; []aSetFlaps40 = actReady AND aPrepareForLanding = actExecuting AND aSetSpoliers = actDone AND (iGSIndicator <= cCapture AND iFlapsGauge /= Flaps40) AND NOT (iFlapsGauge = Flaps40) --> aSetFlaps40' = actExecuting; []aSetFlaps40 = actExecuting AND hSetFlaps40_5 = actDone AND (iFlapsGauge = Flaps40) --> aSetFlaps40' = actDone; []aSetFlaps40 = actReady AND aPrepareForLanding = actExecuting AND aSetSpoliers = actDone AND (iFlapsGauge = Flaps40) --> aSetFlaps40' = actDone; []hSetFlaps40_5 = actReady AND aSetFlaps40 = actExecuting AND pPilot_Ready --> hSetFlaps40_5' = actExecuting; hSetFlaps40' = TRUE; pPilot_Submitted' = TRUE; []pPilot_Submitted AND NOT pPilot_Ready --> pPilot_Submitted' = FALSE; hFlipIgnitionSwitch_1' = IF hFlipIgnitionSwitch_1 = actExecuting THEN actDone ELSE hFlipIgnitionSwitch_1 ENDIF; hPullGearLever_2' = IF hPullGearLever_2 = actExecuting THEN actDone ELSE hPullGearLever_2 ENDIF; hSetFlaps25_3' = IF hSetFlaps25_3 = actExecuting THEN actDone ELSE hSetFlaps25_3 ENDIF; hArmSpoiler_4' = IF hArmSpoiler_4 = actExecuting THEN actDone ELSE hArmSpoiler_4 ENDIF; hSetFlaps40_5' = IF hSetFlaps40_5 = actExecuting THEN actDone ELSE hSetFlaps40_5 ENDIF; hArmSpoiler' = FALSE; hSetFlaps25' = FALSE; hSetFlaps40' = FALSE; hPullGearLever' = FALSE; hFlipIgnitionSwitch' = FALSE; [] NOT (aPrepareForLanding = actReady AND (iGSIndicator <= cInactive) ) AND NOT (aPrepareForLanding = actExecuting AND aSetFlaps40 = actDone ) AND NOT (aOverrideIgnition = actReady AND aPrepareForLanding = actExecuting AND (iGSIndicator <= cInactive AND iIgnitionLight = Off) AND NOT (iIgnitionLight = On) ) AND NOT (aOverrideIgnition = actExecuting AND hFlipIgnitionSwitch_1 = actDone AND (iIgnitionLight = On) ) AND NOT (aOverrideIgnition = actReady AND aPrepareForLanding = actExecuting AND (iIgnitionLight = On) ) AND NOT (hFlipIgnitionSwitch_1 = actReady AND aOverrideIgnition = actExecuting AND pPilot_Ready ) AND NOT (aDeployLandingGear = actReady AND aPrepareForLanding = actExecuting AND aOverrideIgnition = actDone AND (iGSIndicator <= cAlive AND iThreeGearLights = Off) AND NOT (iThreeGearLights = On) ) AND NOT (aDeployLandingGear = actExecuting AND hPullGearLever_2 = actDone AND (iThreeGearLights = On) ) AND NOT (aDeployLandingGear = actReady AND aPrepareForLanding = actExecuting AND aOverrideIgnition = actDone AND (iThreeGearLights = On) ) AND NOT (hPullGearLever_2 = actReady AND aDeployLandingGear = actExecuting AND pPilot_Ready ) AND NOT (aSetFlaps25 = actReady AND aPrepareForLanding = actExecuting AND aDeployLandingGear = actDone AND (iGSIndicator <= cOneDot AND iGSIndicator > cCapture AND iFlapsGauge /= Flaps25) AND NOT (iFlapsGauge = Flaps25 OR iGSIndicator = cCapture) ) AND NOT (aSetFlaps25 = actExecuting AND hSetFlaps25_3 = actDone AND (iFlapsGauge = Flaps25 OR iGSIndicator = cCapture) ) AND NOT (aSetFlaps25 = actReady AND aPrepareForLanding = actExecuting AND aDeployLandingGear = actDone AND (iFlapsGauge = Flaps25 OR iGSIndicator = cCapture) ) AND NOT (hSetFlaps25_3 = actReady AND aSetFlaps25 = actExecuting AND pPilot_Ready ) AND NOT (aSetSpoliers = actReady AND aPrepareForLanding = actExecuting AND aSetFlaps25 = actDone AND (iGearDoorLight = Off AND iSpoilerIndicator = Off AND iThreeGearLights = On) AND NOT (iSpoilerIndicator = On) ) AND NOT (aSetSpoliers = actExecuting AND hArmSpoiler_4 = actDone AND (iSpoilerIndicator = On) ) AND NOT (aSetSpoliers = actReady AND aPrepareForLanding = actExecuting AND aSetFlaps25 = actDone AND (iSpoilerIndicator = On) ) AND NOT (hArmSpoiler_4 = actReady AND aSetSpoliers = actExecuting AND pPilot_Ready ) AND NOT (aSetFlaps40 = actReady AND aPrepareForLanding = actExecuting AND aSetSpoliers = actDone AND (iGSIndicator <= cCapture AND iFlapsGauge /= Flaps40) AND NOT (iFlapsGauge = Flaps40) ) AND NOT (aSetFlaps40 = actExecuting AND hSetFlaps40_5 = actDone AND (iFlapsGauge = Flaps40) ) AND NOT (aSetFlaps40 = actReady AND aPrepareForLanding = actExecuting AND aSetSpoliers = actDone AND (iFlapsGauge = Flaps40) ) AND NOT (hSetFlaps40_5 = actReady AND aSetFlaps40 = actExecuting AND pPilot_Ready ) AND NOT (pPilot_Submitted AND NOT pPilot_Ready ) AND (NOT pPilot_Submitted AND pPilot_Ready)--> pPilot_Submitted' = TRUE; ]; END; tGearTime: TYPE = [0..8]; Stuff: MODULE = BEGIN INPUT pPilot_Submitted: BOOLEAN OUTPUT pPilot_Ready: BOOLEAN INPUT hArmSpoiler: BOOLEAN INPUT hSetFlaps25: BOOLEAN INPUT hSetFlaps40: BOOLEAN INPUT hPullGearLever: BOOLEAN INPUT hFlipIgnitionSwitch: BOOLEAN LOCAL lPosition: tPosition LOCAL lLandingGear: tLandingGear LOCAL lSpoilers: tSpoiler LOCAL lGearDoors: tGearDoorPosition LOCAL lFlaps: tFlapsDegrees LOCAL lExtraGearTime: tGearTime OUTPUT iSpoilerIndicator:tLight %%Inidcates if spoilers are armed OUTPUT iSpoilerLever: tLever %%Arms spoilers when pulled OUTPUT iGearDoorLight: tLight %%off until lower gear, then on till gear is raised OUTPUT iThreeGearLights: tLight %%on when gear is down OUTPUT iGearLever: tLever %%pulled to deploy gear OUTPUT iFlapsGauge: tFlapsDegrees %%flaps position in degrees OUTPUT iGSIndicator: tGSPosition %%Glide Slop Indicator OUTPUT iIgnitionLight: tLight %%ignition indicator light OUTPUT iIgnitionSwitch: tSwitch %%ignition indicator light INITIALIZATION lPosition = cStartPosition; iSpoilerIndicator = Off; iSpoilerLever = Unpulled; iGearDoorLight = Off; iThreeGearLights = Off; iGearLever = Unpulled; iFlapsGauge = Flaps0; iGSIndicator = cInactive; iIgnitionLight = Off; iIgnitionSwitch = Unswitched; lLandingGear = Up; lSpoilers = Unarmed; lGearDoors = cGearDoorsClosed; lFlaps = Flaps0; TRANSITION [ %%transition to being ready for inpur NOT (pPilot_Ready OR pPilot_Submitted) --> pPilot_Ready' = TRUE; []lPosition < cEndPosition AND pPilot_Submitted AND pPilot_Ready --> pPilot_Ready' = FALSE; %%Environment lPosition' = lPosition + 1; %%Automation lLandingGear' = IF hPullGearLever THEN Down ELSE lLandingGear ENDIF; lSpoilers' = IF hArmSpoiler THEN Armed ELSE lSpoilers ENDIF; lGearDoors' = IF (hPullGearLever AND lGearDoors = cGearDoorsClosed OR lGearDoors /= cGearDoorsClosed AND lGearDoors /= cGearDoorsOpen AND lExtraGearTime = 0) THEN lGearDoors + 1 ELSE lGearDoors ENDIF; lExtraGearTime' = IF (lGearDoors /= cGearDoorsClosed AND lGearDoors /= cGearDoorsOpen AND lExtraGearTime /= 0) THEN lExtraGearTime - 1 ELSE lExtraGearTime ENDIF; lFlaps' = IF hSetFlaps25 THEN Flaps25 ELSIF hSetFlaps40 THEN Flaps40 ELSE iFlapsGauge ENDIF; %%HDI iSpoilerIndicator' = IF lSpoilers' = Armed THEN On ELSE Off ENDIF; iSpoilerLever' = IF hArmSpoiler THEN Pulled ELSE iSpoilerLever ENDIF; iGearDoorLight' = IF (lGearDoors' /= cGearDoorsClosed AND lGearDoors' /= cGearDoorsOpen) THEN On ELSE Off ENDIF; iThreeGearLights' = IF lLandingGear' = Down THEN On ELSE Off ENDIF; iGearLever' = IF hPullGearLever THEN Pulled ELSE iGearLever ENDIF; iFlapsGauge' = lFlaps'; iGSIndicator' = IF lPosition' = cAlivePosition THEN cAlive ELSIF lPosition' = cTwoDotPosition THEN cTwoDots ELSIF lPosition' = cOneDotPosition THEN cOneDot ELSIF lPosition' = cCapturePosition THEN cCapture ELSE iGSIndicator ENDIF; iIgnitionSwitch' = IF (hFlipIgnitionSwitch AND iIgnitionSwitch = Switched) THEN Unswitched ELSIF (hFlipIgnitionSwitch AND iIgnitionSwitch = Unswitched) THEN Switched ELSE iIgnitionSwitch ENDIF; iIgnitionLight' = IF iIgnitionSwitch' = Switched THEN On ELSE Off ENDIF; []lPosition = cEndPosition AND pPilot_Submitted AND pPilot_Ready --> pPilot_Ready' = FALSE; lPosition' = lPosition; ]; END; main: MODULE = pPilot [] Stuff; aPrepareForLanding_Execuability : THEOREM main |- G(NOT(aPrepareForLanding = actExecuting)); aPrepareForLanding_InevitableCompletability : THEOREM main |- G(NOT(aPrepareForLanding = actDone)); aPrepareForLanding_InevitableCompletability : THEOREM main |- G((aPrepareForLanding = actExecuting) => F(aPrepareForLanding /= actExecuting)); aOverrideIgnition_Execuability : THEOREM main |- G(NOT(aOverrideIgnition = actExecuting)); aOverrideIgnition_Completability : THEOREM main |- G(NOT(aOverrideIgnition = actDone)); aOverrideIgnition_InevitableCompletability : THEOREM main |- G((aOverrideIgnition = actExecuting) => F(aOverrideIgnition /= actExecuting)); hFlipIgnitionSwitch_1_Execuability : THEOREM main |- G(NOT(hFlipIgnitionSwitch_1 = actExecuting)); hFlipIgnitionSwitch_1_Completability : THEOREM main |- G(NOT(hFlipIgnitionSwitch_1 = actDone)); hFlipIgnitionSwitch_1_InevitableCompletability : THEOREM main |- G((hFlipIgnitionSwitch_1 = actExecuting) => F(hFlipIgnitionSwitch_1 /= actExecuting)); aDeployLandingGear_Execuability : THEOREM main |- G(NOT(aDeployLandingGear = actExecuting)); aDeployLandingGear_Completability : THEOREM main |- G(NOT(aDeployLandingGear = actDone)); aDeployLandingGear_InevitableCompletability : THEOREM main |- G((aDeployLandingGear = actExecuting) => F(aDeployLandingGear /= actExecuting)); hPullGearLever_2_Execuability : THEOREM main |- G(NOT(hPullGearLever_2 = actExecuting)); hPullGearLever_2_Completability : THEOREM main |- G(NOT(hPullGearLever_2 = actDone)); hPullGearLever_2_InevitableCompletability : THEOREM main |- G((hPullGearLever_2 = actExecuting) => F(hPullGearLever_2 /= actExecuting)); aSetFlaps25_Execuability : THEOREM main |- G(NOT(aSetFlaps25 = actExecuting)); aSetFlaps25_Completability : THEOREM main |- G(NOT(aSetFlaps25 = actDone)); aSetFlaps25_InevitableCompletability : THEOREM main |- G((aSetFlaps25 = actExecuting) => F(aSetFlaps25 /= actExecuting)); hSetFlaps25_3_Execuability : THEOREM main |- G(NOT(hSetFlaps25_3 = actExecuting)); hSetFlaps25_3_Completability : THEOREM main |- G(NOT(hSetFlaps25_3 = actDone)); hSetFlaps25_3_InevitableCompletability : THEOREM main |- G((hSetFlaps25_3 = actExecuting) => F(hSetFlaps25_3 /= actExecuting)); aSetSpoliers_Execuability : THEOREM main |- G(NOT(aSetSpoliers = actExecuting)); aSetSpoliers_Completability : THEOREM main |- G(NOT(aSetSpoliers = actDone)); aSetSpoliers_InevitableCompletability : THEOREM main |- G((aSetSpoliers = actExecuting) => F(aSetSpoliers /= actExecuting)); hArmSpoiler_4_Execuability : THEOREM main |- G(NOT(hArmSpoiler_4 = actExecuting)); hArmSpoiler_4_Completability : THEOREM main |- G(NOT(hArmSpoiler_4 = actDone)); hArmSpoiler_4_InevitableCompletability : THEOREM main |- G((hArmSpoiler_4 = actExecuting) => F(hArmSpoiler_4 /= actExecuting)); aSetFlaps40_Execuability : THEOREM main |- G(NOT(aSetFlaps40 = actExecuting)); aSetFlaps40_Completability : THEOREM main |- G(NOT(aSetFlaps40 = actDone)); aSetFlaps40_Blocking : THEOREM main |- G((aSetFlaps40 = actExecuting) => F(aSetFlaps40 /= actExecuting)); hSetFlaps40_5_Execuability : THEOREM main |- G(NOT(hSetFlaps40_5 = actExecuting)); hSetFlaps40_5_Completability : THEOREM main |- G(NOT(hSetFlaps40_5 = actDone)); hSetFlaps40_5_InevitableCompletability : THEOREM main |- G((hSetFlaps40_5 = actExecuting) => F(hSetFlaps40_5 /= actExecuting)); pPilot_TaskLiveness : THEOREM main |- G(NOT(F(G(aPrepareForLanding /= actExecuting)))); revised_pPilot_TaskLiveness : THEOREM main |- (G(NOT(F(G(aPrepareForLanding /= actExecuting))))) => (NOT(lPosition = cEndPosition)); END