/* Date : Jul 23, 2022 */ /* DataFlow format */ domain ARP4761_AppendixQ_CTRL = {Braking, Braking_With_AS, Not_Braking}; domain ARP4761_Flow_Bus_Color = {Ctrl_Pressure, Full_Pressure, Mixed_Pressure, No_Pressure}; domain ARP4761_Flow_CMD = {Off, On}; domain ARP4761_Flow_Elec = {Degraded_Power, No_Power, Power}; domain ARP4761_Flow_Hyd = {Ctrl_Pressure, Full_Pressure, No_Pressure}; domain ARP4761_Flow_Sel_Pos = {Alternate, Middle, Normal}; node ARP4761_BSCU_Command flow icone:[1,9]:private; Power_Input:ARP4761_Flow_Elec:in; Pos2:ARP4761_AppendixQ_CTRL:in; Pos1:ARP4761_AppendixQ_CTRL:in; Enable:ARP4761_Flow_CMD:out; Normal:ARP4761_AppendixQ_CTRL:out; Alt_Emer:ARP4761_AppendixQ_CTRL:out; o_isBraking:bool:out; isBraking:bool:in; Validity:bool:out; BrakingSt:bool:private; state States:{CMD_Incorrect, CMD_Loss, Nominal}; event Incorrect_Behavior, Loss; trans (States = Nominal) |- Loss -> States := CMD_Loss; (States = Nominal) |- Incorrect_Behavior -> States := CMD_Incorrect; assert icone = (if (States = Nominal) then (if (Power_Input = Power) then 1 else (if (Power_Input = Degraded_Power) then 7 else 4)) else (if (States = CMD_Loss) then (if (Power_Input = Power) then 2 else (if (Power_Input = No_Power) then 5 else 8)) else (if (Power_Input = Power) then 3 else (if (Power_Input = Degraded_Power) then 9 else 6)))), BrakingSt = isBraking, Enable = (if (States = Nominal) then (if (Power_Input = Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then (if BrakingSt then On else Off) else (if BrakingSt then Off else On)) else (if (Power_Input = Degraded_Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then On else On) else Off)) else (if (States = CMD_Loss) then Off else (if (Power_Input = Power) then On else (if (Power_Input = Degraded_Power) then On else Off)))), Normal = (if (States = Nominal) then (if (Power_Input = Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then (if BrakingSt then Braking_With_AS else Not_Braking) else (if BrakingSt then Not_Braking else Not_Braking)) else (if (Power_Input = Degraded_Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then Not_Braking else Braking) else Not_Braking)) else (if (States = CMD_Loss) then Not_Braking else (if (Power_Input = Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then Not_Braking else Braking) else (if (Power_Input = Degraded_Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then Not_Braking else Braking) else Not_Braking)))), Alt_Emer = (if (States = Nominal) then (if (Power_Input = Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then (if BrakingSt then Not_Braking else Braking_With_AS) else (if BrakingSt then Not_Braking else Not_Braking)) else (if (Power_Input = Degraded_Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then Not_Braking else Not_Braking) else Not_Braking)) else (if (States = CMD_Loss) then Not_Braking else (if (Power_Input = Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then Not_Braking else Braking) else (if (Power_Input = Degraded_Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then Not_Braking else Braking) else Not_Braking)))), o_isBraking = isBraking, Validity = (if (States = Nominal) then (if (Power_Input = Power) then true else (Power_Input = Degraded_Power)) else (if (States = CMD_Loss) then false else (if (Power_Input = Power) then true else (Power_Input = Degraded_Power)))); init States := Nominal; extern law = exponential(1.0E-6); law = exponential(5.0E-6); edon node ARP4761_BSCU_InternalPower flow icone:[1,3]:private; Pwr_Input:ARP4761_Flow_Elec:in; Pwr_Output:ARP4761_Flow_Elec:out; state States:{Nominal, Pwr_Degraded, Pwr_Loss}; event Degraded, Loss; trans (States = Nominal) |- Loss -> States := Pwr_Loss; (States = Nominal) |- Degraded -> States := Pwr_Degraded; assert icone = (if (States = Nominal) then (if (Pwr_Input = No_Power) then 2 else (if (Pwr_Input = Degraded_Power) then 3 else 1)) else (if (States = Pwr_Loss) then 2 else (if (Pwr_Input = No_Power) then 2 else 3))), Pwr_Output = (if (States = Nominal) then (if (Pwr_Input = No_Power) then No_Power else (if (Pwr_Input = Degraded_Power) then Degraded_Power else Power)) else (if (States = Pwr_Loss) then No_Power else (if (Pwr_Input = No_Power) then No_Power else Degraded_Power))); init States := Nominal; extern law = exponential(1.06E-5); law = exponential(2.0E-5); edon node ARP4761_BSCU_Monitor flow icone:[1,9]:private; Power_Input:ARP4761_Flow_Elec:in; Pos2:ARP4761_AppendixQ_CTRL:in; Pos1:ARP4761_AppendixQ_CTRL:in; Enable_Cmd:ARP4761_Flow_CMD:in; Enable:ARP4761_Flow_CMD:private; Normal_Cmd:ARP4761_AppendixQ_CTRL:in; Normal:ARP4761_AppendixQ_CTRL:private; Alt_Emer_Cmd:ARP4761_AppendixQ_CTRL:in; Alt_Emer:ARP4761_AppendixQ_CTRL:private; isBraking:bool:in; Validity:bool:out; BrakingSt:bool:private; state States:{MON_Incorrect, MON_Loss, Nominal}; event Incorrect_Behavior, Loss; trans (States = Nominal) |- Loss -> States := MON_Loss; (States = Nominal) |- Incorrect_Behavior -> States := MON_Incorrect; assert icone = (if (States = Nominal) then (if (Power_Input = Power) then 1 else (if (Power_Input = Degraded_Power) then 7 else 4)) else (if (States = MON_Loss) then (if (Power_Input = Power) then 2 else (if (Power_Input = No_Power) then 5 else 8)) else (if (Power_Input = Power) then 3 else (if (Power_Input = Degraded_Power) then 9 else 6)))), BrakingSt = isBraking, Enable = (if (States = Nominal) then (if (Power_Input = Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then (if BrakingSt then On else Off) else (if BrakingSt then Off else On)) else (if (Power_Input = Degraded_Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then On else On) else Off)) else (if (States = MON_Loss) then Off else (if (Power_Input = Power) then On else (if (Power_Input = Degraded_Power) then On else Off)))), Normal = (if (States = Nominal) then (if (Power_Input = Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then (if BrakingSt then Braking_With_AS else Not_Braking) else (if BrakingSt then Not_Braking else Not_Braking)) else (if (Power_Input = Degraded_Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then Not_Braking else Braking) else Not_Braking)) else (if (States = MON_Loss) then Not_Braking else (if (Power_Input = Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then Not_Braking else Braking) else (if (Power_Input = Degraded_Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then Not_Braking else Braking) else Not_Braking)))), Alt_Emer = (if (States = Nominal) then (if (Power_Input = Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then (if BrakingSt then Not_Braking else Braking_With_AS) else (if BrakingSt then Not_Braking else Not_Braking)) else (if (Power_Input = Degraded_Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then Not_Braking else Not_Braking) else Not_Braking)) else (if (States = MON_Loss) then Not_Braking else (if (Power_Input = Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then Not_Braking else Braking) else (if (Power_Input = Degraded_Power) then (if ((Pos1 = Braking) and (Pos2 = Braking)) then Not_Braking else Braking) else Not_Braking)))), Validity = (if (States = Nominal) then (if (Power_Input = Power) then (((Enable = Enable_Cmd) and (Normal = Normal_Cmd)) and (Alt_Emer = Alt_Emer_Cmd)) else (Power_Input = Degraded_Power)) else (if (States = MON_Loss) then false else (if (Power_Input = Power) then true else (Power_Input = Degraded_Power)))); init States := Nominal; extern law = exponential(6.0E-6); remark = "covers Incorrect and Loss undetected"; attribute DassaultSpecialRemark() = "covers Incorrect and Loss undetected"; law = exponential(5.0E-6); attribute DassaultSpecialLawModifier() = "inspected(100.0)"; edon node ARP4761_BSCU_PowerMonitor flow icone:[1,3]:private; Pwr_Input:ARP4761_Flow_Elec:in; Pwr_Validity:bool:out; state States:{MON_Incorrect, MON_Loss, Nominal}; event Loss, Incorrect; trans (States = Nominal) |- Loss -> States := MON_Loss; (States = Nominal) |- Incorrect -> States := MON_Incorrect; assert icone = (if (States = Nominal) then 1 else (if (States = MON_Incorrect) then 3 else 2)), Pwr_Validity = (if (States = Nominal) then (Pwr_Input = Power) else (if (States = MON_Incorrect) then (not (Pwr_Input = Power)) else false)); init States := Nominal; extern law = exponential(1.429E-7); attribute DassaultSpecialLawModifier() = "inspected(100.0)"; law = exponential(2.0E-7); edon node ARP4761_BSCU_SelectionManagement flow icone:[1,6]:private; Channel1:bool:out; Channel2:bool:out; Channel1_Validity:bool:in; Channel2_Validity:bool:in; Enable1:ARP4761_Flow_CMD:in; Enable2:ARP4761_Flow_CMD:in; Enable:ARP4761_Flow_CMD:out; Normal1:ARP4761_AppendixQ_CTRL:in; Normal2:ARP4761_AppendixQ_CTRL:in; Normal:ARP4761_AppendixQ_CTRL:out; Alt_Emer1:ARP4761_AppendixQ_CTRL:in; Alt_Emer2:ARP4761_AppendixQ_CTRL:in; Alt_Emer:ARP4761_AppendixQ_CTRL:out; state States:{Loss, Nominal, Unt_Sel_Cmd1, Unt_Sel_Cmd2}; event Cmd1_Untimely_sel, Cmd2_Untimely_sel, Loss; trans (States = Nominal) |- Cmd1_Untimely_sel -> States := Unt_Sel_Cmd1; (States = Nominal) |- Cmd2_Untimely_sel -> States := Unt_Sel_Cmd2; (States = Nominal) |- Loss -> States := Loss; assert icone = case { ((States = Nominal) and ((not Channel1_Validity) and (not Channel2_Validity))) : 5, ((States = Nominal) and (not ((not Channel1_Validity) and (not Channel2_Validity))) and Channel1_Validity) : 1, ((States = Nominal) and (not ((not Channel1_Validity) and (not Channel2_Validity))) and (not Channel1_Validity) and Channel2_Validity) : 2, ((States # Nominal) and (States = Unt_Sel_Cmd1)) : 3, ((States # Nominal) and (States # Unt_Sel_Cmd1) and (States = Unt_Sel_Cmd2)) : 4, else 6 }, Channel1 = case { ((States = Nominal) and ((not Channel1_Validity) and (not Channel2_Validity))) : false, ((States = Nominal) and (not ((not Channel1_Validity) and (not Channel2_Validity))) and Channel1_Validity) : true, ((States = Nominal) and (not ((not Channel1_Validity) and (not Channel2_Validity))) and (not Channel1_Validity) and Channel2_Validity) : false, ((States # Nominal) and (States = Unt_Sel_Cmd1)) : true, ((States # Nominal) and (States # Unt_Sel_Cmd1) and (States = Unt_Sel_Cmd2)) : false, else false }, Channel2 = case { ((States = Nominal) and ((not Channel1_Validity) and (not Channel2_Validity))) : false, ((States = Nominal) and (not ((not Channel1_Validity) and (not Channel2_Validity))) and Channel1_Validity) : false, ((States = Nominal) and (not ((not Channel1_Validity) and (not Channel2_Validity))) and (not Channel1_Validity) and Channel2_Validity) : true, ((States # Nominal) and (States = Unt_Sel_Cmd1)) : false, ((States # Nominal) and (States # Unt_Sel_Cmd1) and (States = Unt_Sel_Cmd2)) : true, else false }, Enable = case { ((States = Nominal) and ((not Channel1_Validity) and (not Channel2_Validity))) : Off, ((States = Nominal) and (not ((not Channel1_Validity) and (not Channel2_Validity))) and Channel1_Validity) : Enable1, ((States = Nominal) and (not ((not Channel1_Validity) and (not Channel2_Validity))) and (not Channel1_Validity) and Channel2_Validity) : Enable2, ((States # Nominal) and (States = Unt_Sel_Cmd1)) : Enable1, ((States # Nominal) and (States # Unt_Sel_Cmd1) and (States = Unt_Sel_Cmd2)) : Enable2, else Off }, Normal = case { ((States = Nominal) and ((not Channel1_Validity) and (not Channel2_Validity))) : Not_Braking, ((States = Nominal) and (not ((not Channel1_Validity) and (not Channel2_Validity))) and Channel1_Validity) : Normal1, ((States = Nominal) and (not ((not Channel1_Validity) and (not Channel2_Validity))) and (not Channel1_Validity) and Channel2_Validity) : Normal2, ((States # Nominal) and (States = Unt_Sel_Cmd1)) : Normal1, ((States # Nominal) and (States # Unt_Sel_Cmd1) and (States = Unt_Sel_Cmd2)) : Normal2, else Not_Braking }, Alt_Emer = case { ((States = Nominal) and ((not Channel1_Validity) and (not Channel2_Validity))) : Braking, ((States = Nominal) and (not ((not Channel1_Validity) and (not Channel2_Validity))) and Channel1_Validity) : Alt_Emer1, ((States = Nominal) and (not ((not Channel1_Validity) and (not Channel2_Validity))) and (not Channel1_Validity) and Channel2_Validity) : Alt_Emer2, ((States # Nominal) and (States = Unt_Sel_Cmd1)) : Alt_Emer1, ((States # Nominal) and (States # Unt_Sel_Cmd1) and (States = Unt_Sel_Cmd2)) : Alt_Emer2, else Braking }; init States := Nominal; extern law = exponential(1.0E-6); attribute DassaultSpecialLawModifier() = "inspected(100.0)"; law = exponential(1.0E-6); law = exponential(1.0E-6); attribute DassaultSpecialLawModifier() = "inspected(100.0)"; edon node ARP4761_ElectricalPower_Electrical_Power flow icone:[1,3]:private; Power_Output:ARP4761_Flow_Elec:out; state States:{PowerDegraded, PowerOff, PowerOn}; event Degraded, Loss; trans (States = PowerOn) |- Loss -> States := PowerOff; (States = PowerOn) |- Degraded -> States := PowerDegraded; assert icone = (if (States = PowerOn) then 1 else (if (States = PowerOff) then 2 else 3)), Power_Output = (if (States = PowerOn) then Power else (if (States = PowerOff) then No_Power else Degraded_Power)); init States := PowerOn; extern law = exponential(1.0E-5); law = exponential(1.0E-4); edon node ARP4761_Hydraulic_Alt_Emer_Meter_Valve flow icone:[1,4]:private; CMD:ARP4761_AppendixQ_CTRL:in; Hyd_Input:ARP4761_Flow_Hyd:in; Hyd_Output:ARP4761_Flow_Hyd:out; state States:{Failed_Off, Failed_On, Nominal}; event Untimely_Off, Untimely_On; trans (States = Nominal) |- Untimely_On -> States := Failed_On; (States = Nominal) |- Untimely_Off -> States := Failed_Off; assert icone = (if (States = Nominal) then (if (CMD = Braking) then 1 else 2) else (if (States = Failed_On) then 3 else 4)), Hyd_Output = (if (States = Nominal) then (if (CMD = Braking) then Hyd_Input else No_Pressure) else (if (States = Failed_On) then Hyd_Input else No_Pressure)); init States := Nominal; extern law = exponential(2.0E-6); law = exponential(1.0E-6); edon node ARP4761_Hydraulic_AntiSkidValve flow icone:[1,4]:private; Hyd_Input:ARP4761_Flow_Hyd:in; Hyd_Output:ARP4761_Flow_Hyd:out; CMD:ARP4761_AppendixQ_CTRL:in; state States:{Failed_Off, Failed_On, Nominal}; event Untimely_On, Untimely_Off; trans (States = Nominal) |- Untimely_On -> States := Failed_On; (States = Nominal) |- Untimely_Off -> States := Failed_Off; assert icone = (if (States = Nominal) then (if (Hyd_Input = No_Pressure) then 2 else (if (CMD = Braking) then 1 else (if (CMD = Braking_With_AS) then 1 else 2))) else (if (States = Failed_On) then 3 else 4)), Hyd_Output = (if (States = Nominal) then (if (Hyd_Input = No_Pressure) then No_Pressure else (if (CMD = Braking) then Full_Pressure else (if (CMD = Braking_With_AS) then Ctrl_Pressure else No_Pressure))) else (if (States = Failed_On) then Hyd_Input else No_Pressure)); init States := Nominal; extern law = exponential(1.0E-6); law = exponential(1.0E-6); edon node ARP4761_Hydraulic_EmergencyAccumulator flow icone:[1,2]:private; Isol:bool:in; HydOut:ARP4761_Flow_Hyd:out; HydIn:ARP4761_Flow_Hyd:in; Sel_Pos:ARP4761_Flow_Sel_Pos:in; state States:{Failed, Nominal}; HydActive:bool; event Failure, FirstTrans; trans (States = Nominal) |- Failure -> States := Failed; ((Sel_Pos = Alternate) and HydActive) |- FirstTrans -> HydActive := false; assert icone = (if (States = Nominal) then (if (((HydIn = No_Pressure) and (Isol = false)) and (Sel_Pos = Alternate)) then 2 else 1) else 2), HydOut = (if (States = Nominal) then (if (((HydIn = No_Pressure) and (Isol = false)) and (Sel_Pos = Alternate)) then No_Pressure else Full_Pressure) else No_Pressure); init States := Nominal, HydActive := true; extern law = exponential(1.0E-5); attribute DassaultSpecialLawModifier() = "inspected(100.0)"; law = Dirac(0.0); edon node ARP4761_Hydraulic_Hyd_Or flow HydOut:ARP4761_Flow_Hyd:out; HydAccuIn:ARP4761_Flow_Hyd:in; HydIn:ARP4761_Flow_Hyd:in; assert HydOut = (if ((HydIn = No_Pressure) and (HydAccuIn = No_Pressure)) then No_Pressure else Full_Pressure); edon node ARP4761_Hydraulic_Hydraulic_Power flow icone:[1,2]:private; Hyd_Output:ARP4761_Flow_Hyd:out; state States:{SwitchOff, SwitchOn}; event Loss; trans (States = SwitchOn) |- Loss -> States := SwitchOff; assert icone = (if (States = SwitchOn) then 1 else 2), Hyd_Output = (if (States = SwitchOn) then Full_Pressure else No_Pressure); init States := SwitchOn; extern law = exponential(6.6E-6); edon node ARP4761_Hydraulic_Isolation_Valve flow icone:[1,4]:private; Isol:bool:out; Hyd_Input:ARP4761_Flow_Hyd:in; Hyd_Output:ARP4761_Flow_Hyd:out; state States:{Failed_Off, Failed_On, Nominal}; event Always_Off, Always_On; trans (States = Nominal) |- Always_On -> States := Failed_On; (States = Nominal) |- Always_Off -> States := Failed_Off; assert icone = case { ((States = Nominal) and (Hyd_Input = Full_Pressure)) : 1, ((States = Nominal) and (Hyd_Input # Full_Pressure)) : 2, (States = Failed_On) : 4, else 3 }, Isol = case { ((States = Nominal) and (Hyd_Input = Full_Pressure)) : false, ((States = Nominal) and (Hyd_Input # Full_Pressure)) : true, (States = Failed_On) : false, else true }, Hyd_Output = case { ((States = Nominal) and (Hyd_Input = Full_Pressure)) : Full_Pressure, ((States = Nominal) and (Hyd_Input # Full_Pressure)) : No_Pressure, (States = Failed_On) : Hyd_Input, else No_Pressure }; init States := Nominal; extern law = exponential(5.0E-9); law = exponential(1.0E-7); attribute DassaultSpecialLawModifier() = "inspected(100.0)"; edon node ARP4761_Hydraulic_NormalValve flow icone:[1,4]:private; Hyd_Input:ARP4761_Flow_Hyd:in; Hyd_Output:ARP4761_Flow_Hyd:out; CMD:ARP4761_AppendixQ_CTRL:in; state States:{Failed_Off, Failed_On, Nominal}; event Untimely_On, Untimely_Off; trans (States = Nominal) |- Untimely_On -> States := Failed_On; (States = Nominal) |- Untimely_Off -> States := Failed_Off; assert icone = (if (States = Nominal) then (if (Hyd_Input = No_Pressure) then 1 else (if (CMD = Braking) then 1 else (if (CMD = Braking_With_AS) then 1 else 2))) else (if (States = Failed_On) then 3 else 4)), Hyd_Output = (if (States = Nominal) then (if (Hyd_Input = No_Pressure) then No_Pressure else (if (CMD = Braking) then Full_Pressure else (if (CMD = Braking_With_AS) then Ctrl_Pressure else No_Pressure))) else (if (States = Failed_On) then Hyd_Input else No_Pressure)); init States := Nominal; extern law = exponential(2.0E-7); law = exponential(5.0E-6); edon node ARP4761_Hydraulic_SelectorValve flow icone:[1,5]:private; Hyd_Input1:ARP4761_Flow_Hyd:in; Hyd_Input2:ARP4761_Flow_Hyd:in; Hyd_Output1:ARP4761_Flow_Hyd:out; Hyd_Output2:ARP4761_Flow_Hyd:out; Sel_Pos:ARP4761_Flow_Sel_Pos:out; state States:{Nominal, Stuck_Alternate_State, Stuck_Middle_State, Stuck_Normal_State}; event Stuck_Normal, Stuck_Alternate, Stuck_Middle; trans (States = Nominal) |- Stuck_Normal -> States := Stuck_Normal_State; (States = Nominal) |- Stuck_Alternate -> States := Stuck_Alternate_State; (States = Nominal) |- Stuck_Middle -> States := Stuck_Middle_State; assert icone = (if (States = Nominal) then (if (Hyd_Input1 = Full_Pressure) then 1 else 2) else (if (States = Stuck_Alternate_State) then 5 else (if (States = Stuck_Middle_State) then 4 else 3))), Hyd_Output1 = (if (States = Nominal) then (if (Hyd_Input1 = Full_Pressure) then Full_Pressure else No_Pressure) else (if (States = Stuck_Alternate_State) then No_Pressure else (if (States = Stuck_Middle_State) then No_Pressure else Hyd_Input1))), Hyd_Output2 = (if (States = Nominal) then (if (Hyd_Input1 = Full_Pressure) then No_Pressure else Hyd_Input2) else (if (States = Stuck_Alternate_State) then Hyd_Input2 else (if (States = Stuck_Middle_State) then No_Pressure else No_Pressure))), Sel_Pos = (if (States = Nominal) then (if (Hyd_Input1 = Full_Pressure) then Normal else Alternate) else (if (States = Stuck_Alternate_State) then Alternate else (if (States = Stuck_Middle_State) then Middle else Normal))); init States := Nominal; extern law = exponential(1.0E-6); law = exponential(1.0E-6); law = exponential(1.0E-8); edon node ARP4761_Hydraulic_ShutOffValve flow icone:[1,4]:private; CMD:ARP4761_Flow_CMD:in; Hyd_Input:ARP4761_Flow_Hyd:in; Hyd_Output:ARP4761_Flow_Hyd:out; state States:{Failed_Off, Failed_On, Nominal}; event Untimely_Off, Untimely_On; trans (States = Nominal) |- Untimely_On -> States := Failed_On; (States = Nominal) |- Untimely_Off -> States := Failed_Off; assert icone = (if (States = Nominal) then (if (CMD = On) then 1 else 2) else (if (States = Failed_On) then 3 else 4)), Hyd_Output = (if (States = Nominal) then (if (CMD = On) then Hyd_Input else No_Pressure) else (if (States = Failed_On) then Hyd_Input else No_Pressure)); init States := Nominal; extern law = exponential(1.0E-6); law = exponential(5.0E-6); edon node ARP4761_PilotCtrl_ElectricalBrakeUnit flow icone:[1,3]:private; CMD_Input:ARP4761_AppendixQ_CTRL:in; CMD_Output1:ARP4761_AppendixQ_CTRL:out; CMD_Output2:ARP4761_AppendixQ_CTRL:out; CMD_Output3:ARP4761_AppendixQ_CTRL:out; state States:{Nominal, Not_Braking, Untimely_Braking}; event Intempestive_Braking, Not_Braking; trans (States = Nominal) |- Intempestive_Braking -> States := Untimely_Braking; (States = Nominal) |- Not_Braking -> States := Not_Braking; assert icone = (if (States = Nominal) then 1 else (if (States = Untimely_Braking) then 2 else 3)), CMD_Output1 = (if (States = Nominal) then CMD_Input else (if (States = Untimely_Braking) then Braking else Not_Braking)), CMD_Output2 = (if (States = Nominal) then CMD_Input else (if (States = Untimely_Braking) then Braking else Not_Braking)), CMD_Output3 = (if (States = Nominal) then CMD_Input else (if (States = Untimely_Braking) then Braking else Not_Braking)); init States := Nominal; extern law = exponential(1.0E-6); law = exponential(1.0E-6); edon node ARP4761_PilotCtrl_Pilot flow icone:[1,2]:private; CMD_Output:ARP4761_AppendixQ_CTRL:out; state States:{Braking, Not_Braking}; assert icone = (if (States = Braking) then 1 else 2), CMD_Output = (if (States = Braking) then Braking else Not_Braking); init States := Braking; edon node ARP4761_miscelaneous_AND_3 flow Out:bool:out; Input1:bool:in; Input2:bool:in; Input3:bool:in; assert Out = ((Input1 and Input2) and Input3); edon node ARP4761_miscelaneous_Counter flow O8by8:bool:out; O7by8:bool:out; O6by8:bool:out; O5by8:bool:out; O4by8:bool:out; O3by8:bool:out; O2by8:bool:out; O1by8:bool:out; e8:bool:in; e7:bool:in; e6:bool:in; e5:bool:in; e4:bool:in; e3:bool:in; e2:bool:in; e1:bool:in; Compteur:[0,8]:private; assert Compteur = #(e1, e2, e3, e4, e5, e6, e7, e8), O8by8 = (Compteur >= 8), O7by8 = (Compteur >= 7), O6by8 = (Compteur >= 6), O5by8 = (Compteur >= 5), O4by8 = (Compteur >= 4), O3by8 = (Compteur >= 3), O2by8 = (Compteur >= 2), O1by8 = (Compteur >= 1); edon node ARP4761_miscelaneous_FC_Braking_loss flow icone:[1,2]:private; WheelBrakingStatus:bool:in; BrakingCMD:ARP4761_AppendixQ_CTRL:in; assert icone = (if (BrakingCMD = Braking) then (if WheelBrakingStatus then 1 else 2) else 1); edon node ARP4761_miscelaneous_FC_Untimely_Braking flow icone:[1,2]:private; FullBrakingStatus:bool:in; BrakingCMD:ARP4761_AppendixQ_CTRL:in; assert icone = (if (BrakingCMD = Not_Braking) then (if FullBrakingStatus then 2 else 1) else 1); edon node ARP4761_miscelaneous_OR_2 flow Out:bool:out; Input1:bool:in; Input2:bool:in; assert Out = (Input1 or Input2); edon node ARP4761_miscelaneous_Stub1 flow iElecPedalPos2:ARP4761_AppendixQ_CTRL:in; iElecPedalPos1:ARP4761_AppendixQ_CTRL:in; oElecPedalPos2:ARP4761_AppendixQ_CTRL:out; oElecPedalPos1:ARP4761_AppendixQ_CTRL:out; assert oElecPedalPos2 = iElecPedalPos2, oElecPedalPos1 = iElecPedalPos1; edon node ARP4761_miscelaneous_Wheel flow Wheel_Braking_Status_hyd1:bool:out; Wheel_Braking_Status:bool:out; Wheel_Status:ARP4761_AppendixQ_CTRL:out; Hyd_Input2:ARP4761_Flow_Hyd:in; Hyd_Input1:ARP4761_Flow_Hyd:in; state States:{AlwaysBraking, NeverBraking, Nominal}; assert Wheel_Braking_Status_hyd1 = (if (States = Nominal) then ((Hyd_Input1 = Full_Pressure) or (Hyd_Input1 = Ctrl_Pressure)) else (States = AlwaysBraking)), Wheel_Braking_Status = (if (States = Nominal) then (if ((Hyd_Input1 = Full_Pressure) or (Hyd_Input2 = Full_Pressure)) then true else ((Hyd_Input1 = Ctrl_Pressure) or (Hyd_Input2 = Ctrl_Pressure))) else (States = AlwaysBraking)), Wheel_Status = (if (States = Nominal) then (if ((Hyd_Input1 = Full_Pressure) or (Hyd_Input2 = Full_Pressure)) then Braking else (if ((Hyd_Input1 = Ctrl_Pressure) or (Hyd_Input2 = Ctrl_Pressure)) then Braking_With_AS else Not_Braking)) else (if (States = AlwaysBraking) then Braking else Not_Braking)); init States := Nominal; edon node ARP4761_miscelaneous_antiskid flow Wheel_status8:ARP4761_AppendixQ_CTRL:in; Wheel_status7:ARP4761_AppendixQ_CTRL:in; Wheel_status6:ARP4761_AppendixQ_CTRL:in; Wheel_status5:ARP4761_AppendixQ_CTRL:in; Wheel_status4:ARP4761_AppendixQ_CTRL:in; Wheel_status3:ARP4761_AppendixQ_CTRL:in; Wheel_status2:ARP4761_AppendixQ_CTRL:in; Wheel_status1:ARP4761_AppendixQ_CTRL:in; Antiskid_status:bool:out; assert Antiskid_status = (not ((((((((Wheel_status1 = Braking) or (Wheel_status2 = Braking)) or (Wheel_status3 = Braking)) or (Wheel_status4 = Braking)) or (Wheel_status5 = Braking)) or (Wheel_status6 = Braking)) or (Wheel_status7 = Braking)) or (Wheel_status8 = Braking))); edon node ARP4761_miscelaneous_computer_in_control flow icone:[1,3]:private; Channel1:bool:in; Channel2:bool:in; assert icone = (if (Channel1 = true) then 1 else (if (Channel2 = true) then 2 else 3)); edon node ARP4761_miscelaneous_control_mode flow icone:[1,6]:private; Alt_Emer:ARP4761_AppendixQ_CTRL:in; Normal:ARP4761_AppendixQ_CTRL:in; Hyd2:ARP4761_Flow_Hyd:in; Accu:ARP4761_Flow_Hyd:in; assert icone = (if (Normal = Braking_With_AS) then 1 else (if (Normal = Braking) then 2 else (if (Alt_Emer = Braking_With_AS) then 3 else (if ((Alt_Emer = Braking) and (Hyd2 # No_Pressure)) then 4 else (if ((Alt_Emer = Braking) and (Accu # No_Pressure)) then 5 else 6))))); edon node ARP4761_miscelaneous_delay4 flow Out:bool:out; In:bool:in; Braking_val:ARP4761_AppendixQ_CTRL:in; state stat1:bool; stat2:bool; event Ev; trans (((In = false) and (Braking_val = Braking)) and (stat1 = true)) |- Ev -> stat1 := false; (((In = true) and (Braking_val = Not_Braking)) and (stat2 = false)) |- Ev -> stat2 := true; assert Out = (if (Braking_val = Braking) then stat1 else stat2); init stat1 := true, stat2 := false; extern law = Dirac(0.0); edon node ARP4761_miscelaneous_delay5 flow Out:bool:out; In:bool:in; Braking_val:ARP4761_AppendixQ_CTRL:in; assert Out = (if In then (Braking_val = Braking) else In); edon node ARP4761_miscelaneous_effect_on_wheels flow icone:[1,5]:private; Full_braking_status:bool:in; Wheels_braking_status:bool:in; Wheels_antiskid_status:bool:in; assert icone = (if ((Full_braking_status = true) and (Wheels_antiskid_status = true)) then 1 else (if ((Full_braking_status = true) and (Wheels_antiskid_status = false)) then 2 else (if ((Wheels_braking_status = true) and (Wheels_antiskid_status = true)) then 3 else (if ((Wheels_braking_status = true) and (Wheels_antiskid_status = false)) then 4 else 5)))); edon node ARP4761_miscelaneous_hyd1 flow v8:ARP4761_Flow_Hyd:in; v7:ARP4761_Flow_Hyd:in; v6:ARP4761_Flow_Hyd:in; v5:ARP4761_Flow_Hyd:in; v4:ARP4761_Flow_Hyd:in; v3:ARP4761_Flow_Hyd:in; v2:ARP4761_Flow_Hyd:in; v1:ARP4761_Flow_Hyd:in; hyd1:bool:out; assert hyd1 = ((((((((v1 # No_Pressure) or (v2 # No_Pressure)) or (v3 # No_Pressure)) or (v4 # No_Pressure)) or (v5 # No_Pressure)) or (v6 # No_Pressure)) or (v7 # No_Pressure)) or (v8 # No_Pressure)); edon node ARP4761_miscelaneous_hydraulic_path flow icone:[1,4]:private; accu:ARP4761_Flow_Hyd:in; hyd2i:ARP4761_Flow_Hyd:in; hyd2g:bool:in; hyd1:bool:in; assert icone = (if (hyd1 = true) then 1 else (if ((hyd2g = true) and (hyd2i # No_Pressure)) then 2 else (if ((hyd2g = true) and (accu # No_Pressure)) then 3 else 4))); edon node ARP4761_miscelaneous_inhib flow O:bool:out; I:bool:in; state inhib_state:{inhib, normal}; assert O = (if (inhib_state = normal) then I else true); init inhib_state := normal; edon node ARP4761_miscelaneous_inv flow O:bool:out; I:bool:in; assert O = (not I); edon node ARP4761_miscelaneous_speed_sensor flow Out:bool:out; In:bool:in; state Status:{consistent, unconsistent}; event failure; trans (Status = consistent) |- failure -> Status := unconsistent; assert Out = (if (Status = consistent) then In else (not In)); init Status := consistent; extern law = exponential(1.0E-7); edon node eq_ARP4761_Hydraulic_AntiSkid_Valve flow icone:[1,6]:private; Hyd_Output^Bus_Color:ARP4761_Flow_Bus_Color:out; Hyd_Output^Hyd_Output1:ARP4761_Flow_Hyd:out; Hyd_Output^Hyd_Output2:ARP4761_Flow_Hyd:out; Hyd_Output^Hyd_Output3:ARP4761_Flow_Hyd:out; Hyd_Output^Hyd_Output4:ARP4761_Flow_Hyd:out; Hyd_Output^Hyd_Output5:ARP4761_Flow_Hyd:out; Hyd_Output^Hyd_Output6:ARP4761_Flow_Hyd:out; Hyd_Output^Hyd_Output7:ARP4761_Flow_Hyd:out; Hyd_Output^Hyd_Output8:ARP4761_Flow_Hyd:out; Ctrl:ARP4761_AppendixQ_CTRL:in; Hyd_Input1:ARP4761_Flow_Hyd:in; Hyd_Input2:ARP4761_Flow_Hyd:in; hyd:bool:out; sub Valve1:ARP4761_Hydraulic_AntiSkidValve; Valve2:ARP4761_Hydraulic_AntiSkidValve; Valve3:ARP4761_Hydraulic_AntiSkidValve; Valve4:ARP4761_Hydraulic_AntiSkidValve; Valve5:ARP4761_Hydraulic_AntiSkidValve; Valve6:ARP4761_Hydraulic_AntiSkidValve; Valve7:ARP4761_Hydraulic_AntiSkidValve; Valve8:ARP4761_Hydraulic_AntiSkidValve; hydraulic:ARP4761_miscelaneous_hyd1; assert icone = (if (((((((((Valve1.States = Nominal) and (Valve2.States = Nominal)) and (Valve3.States = Nominal)) and (Valve4.States = Nominal)) and (Valve5.States = Nominal)) and (Valve6.States = Nominal)) and (Valve7.States = Nominal)) and (Valve8.States = Nominal)) and ((Hyd_Input1 = No_Pressure) and (Hyd_Input1 = No_Pressure))) then 2 else (if (((((((((Valve1.States = Failed_On) and (Valve2.States = Failed_On)) and (Valve3.States = Failed_On)) and (Valve4.States = Failed_On)) and (Valve5.States = Failed_On)) and (Valve6.States = Failed_On)) and (Valve7.States = Failed_On)) and (Valve8.States = Failed_On)) and ((Hyd_Input1 = No_Pressure) and (Hyd_Input1 = No_Pressure))) then 4 else (if (((((((((Valve1.States = Nominal) and (Valve2.States = Nominal)) and (Valve3.States = Nominal)) and (Valve4.States = Nominal)) and (Valve5.States = Nominal)) and (Valve6.States = Nominal)) and (Valve7.States = Nominal)) and (Valve8.States = Nominal)) and (Ctrl # Not_Braking)) then 1 else (if (((((((((Valve1.States = Nominal) and (Valve2.States = Nominal)) and (Valve3.States = Nominal)) and (Valve4.States = Nominal)) and (Valve5.States = Nominal)) and (Valve6.States = Nominal)) and (Valve7.States = Nominal)) and (Valve8.States = Nominal)) and (Ctrl = Not_Braking)) then 2 else (if ((((((((Valve1.States = Failed_On) and (Valve2.States = Failed_On)) and (Valve3.States = Failed_On)) and (Valve4.States = Failed_On)) and (Valve5.States = Failed_On)) and (Valve6.States = Failed_On)) and (Valve7.States = Failed_On)) and (Valve8.States = Failed_On)) then 3 else (if ((((((((Valve1.States = Failed_Off) and (Valve2.States = Failed_Off)) and (Valve3.States = Failed_Off)) and (Valve4.States = Failed_Off)) and (Valve5.States = Failed_Off)) and (Valve6.States = Failed_Off)) and (Valve7.States = Failed_Off)) and (Valve8.States = Failed_Off)) then 4 else (if (Ctrl = Not_Braking) then 6 else 5))))))), Hyd_Output^Bus_Color = (if (((((((((Valve1.States = Nominal) and (Valve2.States = Nominal)) and (Valve3.States = Nominal)) and (Valve4.States = Nominal)) and (Valve5.States = Nominal)) and (Valve6.States = Nominal)) and (Valve7.States = Nominal)) and (Valve8.States = Nominal)) and ((Hyd_Input1 = No_Pressure) and (Hyd_Input1 = No_Pressure))) then No_Pressure else (if (((((((((Valve1.States = Failed_On) and (Valve2.States = Failed_On)) and (Valve3.States = Failed_On)) and (Valve4.States = Failed_On)) and (Valve5.States = Failed_On)) and (Valve6.States = Failed_On)) and (Valve7.States = Failed_On)) and (Valve8.States = Failed_On)) and ((Hyd_Input1 = No_Pressure) and (Hyd_Input1 = No_Pressure))) then No_Pressure else (if (((((((((Valve1.States = Nominal) and (Valve2.States = Nominal)) and (Valve3.States = Nominal)) and (Valve4.States = Nominal)) and (Valve5.States = Nominal)) and (Valve6.States = Nominal)) and (Valve7.States = Nominal)) and (Valve8.States = Nominal)) and (Ctrl # Not_Braking)) then (if (Valve1.Hyd_Output = Full_Pressure) then Full_Pressure else Ctrl_Pressure) else (if (((((((((Valve1.States = Nominal) and (Valve2.States = Nominal)) and (Valve3.States = Nominal)) and (Valve4.States = Nominal)) and (Valve5.States = Nominal)) and (Valve6.States = Nominal)) and (Valve7.States = Nominal)) and (Valve8.States = Nominal)) and (Ctrl = Not_Braking)) then No_Pressure else (if ((((((((Valve1.States = Failed_On) and (Valve2.States = Failed_On)) and (Valve3.States = Failed_On)) and (Valve4.States = Failed_On)) and (Valve5.States = Failed_On)) and (Valve6.States = Failed_On)) and (Valve7.States = Failed_On)) and (Valve8.States = Failed_On)) then Full_Pressure else (if ((((((((Valve1.States = Failed_Off) and (Valve2.States = Failed_Off)) and (Valve3.States = Failed_Off)) and (Valve4.States = Failed_Off)) and (Valve5.States = Failed_Off)) and (Valve6.States = Failed_Off)) and (Valve7.States = Failed_Off)) and (Valve8.States = Failed_Off)) then No_Pressure else (if (Ctrl = Not_Braking) then Mixed_Pressure else Mixed_Pressure))))))), Hyd_Output^Hyd_Output1 = Valve1.Hyd_Output, Hyd_Output^Hyd_Output2 = Valve2.Hyd_Output, Hyd_Output^Hyd_Output3 = Valve3.Hyd_Output, Hyd_Output^Hyd_Output4 = Valve4.Hyd_Output, Hyd_Output^Hyd_Output5 = Valve5.Hyd_Output, Hyd_Output^Hyd_Output6 = Valve6.Hyd_Output, Hyd_Output^Hyd_Output7 = Valve7.Hyd_Output, Hyd_Output^Hyd_Output8 = Valve8.Hyd_Output, hyd = hydraulic.hyd1, Valve1.Hyd_Input = Hyd_Input1, Valve1.CMD = Ctrl, Valve2.Hyd_Input = Hyd_Input1, Valve2.CMD = Ctrl, Valve3.Hyd_Input = Hyd_Input1, Valve3.CMD = Ctrl, Valve4.Hyd_Input = Hyd_Input1, Valve4.CMD = Ctrl, Valve5.Hyd_Input = Hyd_Input2, Valve5.CMD = Ctrl, Valve6.Hyd_Input = Hyd_Input2, Valve6.CMD = Ctrl, Valve7.Hyd_Input = Hyd_Input2, Valve7.CMD = Ctrl, Valve8.Hyd_Input = Hyd_Input2, Valve8.CMD = Ctrl, hydraulic.v8 = Valve8.Hyd_Output, hydraulic.v7 = Valve7.Hyd_Output, hydraulic.v6 = Valve6.Hyd_Output, hydraulic.v5 = Valve5.Hyd_Output, hydraulic.v4 = Valve4.Hyd_Output, hydraulic.v3 = Valve3.Hyd_Output, hydraulic.v2 = Valve2.Hyd_Output, hydraulic.v1 = Valve1.Hyd_Output; edon node eq_ARP4761_Hydraulic_Normal_Valve flow icone:[1,6]:private; Hyd_Output^Bus_Color:ARP4761_Flow_Bus_Color:out; Hyd_Output^Hyd_Output1:ARP4761_Flow_Hyd:out; Hyd_Output^Hyd_Output2:ARP4761_Flow_Hyd:out; Hyd_Output^Hyd_Output3:ARP4761_Flow_Hyd:out; Hyd_Output^Hyd_Output4:ARP4761_Flow_Hyd:out; Hyd_Output^Hyd_Output5:ARP4761_Flow_Hyd:out; Hyd_Output^Hyd_Output6:ARP4761_Flow_Hyd:out; Hyd_Output^Hyd_Output7:ARP4761_Flow_Hyd:out; Hyd_Output^Hyd_Output8:ARP4761_Flow_Hyd:out; Ctrl:ARP4761_AppendixQ_CTRL:in; Hyd_Input1:ARP4761_Flow_Hyd:in; Hyd_Input2:ARP4761_Flow_Hyd:in; hyd:bool:out; sub Valve1:ARP4761_Hydraulic_NormalValve; Valve2:ARP4761_Hydraulic_NormalValve; Valve3:ARP4761_Hydraulic_NormalValve; Valve4:ARP4761_Hydraulic_NormalValve; Valve5:ARP4761_Hydraulic_NormalValve; Valve6:ARP4761_Hydraulic_NormalValve; Valve7:ARP4761_Hydraulic_NormalValve; Valve8:ARP4761_Hydraulic_NormalValve; hydraulic:ARP4761_miscelaneous_hyd1; assert icone = (if (((((((((Valve1.States = Nominal) and (Valve2.States = Nominal)) and (Valve3.States = Nominal)) and (Valve4.States = Nominal)) and (Valve5.States = Nominal)) and (Valve6.States = Nominal)) and (Valve7.States = Nominal)) and (Valve8.States = Nominal)) and (Ctrl # Not_Braking)) then 1 else (if ((((((((Valve1.States = Nominal) and (Valve2.States = Nominal)) and (Valve3.States = Nominal)) and (Valve4.States = Nominal)) and (Valve5.States = Nominal)) and (Valve6.States = Nominal)) and (Valve7.States = Nominal)) and (Valve8.States = Nominal)) then 2 else (if ((((((((Valve1.States = Failed_On) and (Valve2.States = Failed_On)) and (Valve3.States = Failed_On)) and (Valve4.States = Failed_On)) and (Valve5.States = Failed_On)) and (Valve6.States = Failed_On)) and (Valve7.States = Failed_On)) and (Valve8.States = Failed_On)) then 3 else (if ((((((((Valve1.States = Failed_Off) and (Valve2.States = Failed_Off)) and (Valve3.States = Failed_Off)) and (Valve4.States = Failed_Off)) and (Valve5.States = Failed_Off)) and (Valve6.States = Failed_Off)) and (Valve7.States = Failed_Off)) and (Valve8.States = Failed_Off)) then 4 else (if (Ctrl = Not_Braking) then 6 else 5))))), Hyd_Output^Bus_Color = (if (((((((((Valve1.States = Nominal) and (Valve2.States = Nominal)) and (Valve3.States = Nominal)) and (Valve4.States = Nominal)) and (Valve5.States = Nominal)) and (Valve6.States = Nominal)) and (Valve7.States = Nominal)) and (Valve8.States = Nominal)) and (Ctrl # Not_Braking)) then (if (Valve1.Hyd_Output = Full_Pressure) then Full_Pressure else Ctrl_Pressure) else (if ((((((((Valve1.States = Nominal) and (Valve2.States = Nominal)) and (Valve3.States = Nominal)) and (Valve4.States = Nominal)) and (Valve5.States = Nominal)) and (Valve6.States = Nominal)) and (Valve7.States = Nominal)) and (Valve8.States = Nominal)) then No_Pressure else (if ((((((((Valve1.States = Failed_On) and (Valve2.States = Failed_On)) and (Valve3.States = Failed_On)) and (Valve4.States = Failed_On)) and (Valve5.States = Failed_On)) and (Valve6.States = Failed_On)) and (Valve7.States = Failed_On)) and (Valve8.States = Failed_On)) then Full_Pressure else (if ((((((((Valve1.States = Failed_Off) and (Valve2.States = Failed_Off)) and (Valve3.States = Failed_Off)) and (Valve4.States = Failed_Off)) and (Valve5.States = Failed_Off)) and (Valve6.States = Failed_Off)) and (Valve7.States = Failed_Off)) and (Valve8.States = Failed_Off)) then No_Pressure else (if (Ctrl = Not_Braking) then Mixed_Pressure else Mixed_Pressure))))), Hyd_Output^Hyd_Output1 = Valve1.Hyd_Output, Hyd_Output^Hyd_Output2 = Valve2.Hyd_Output, Hyd_Output^Hyd_Output3 = Valve3.Hyd_Output, Hyd_Output^Hyd_Output4 = Valve4.Hyd_Output, Hyd_Output^Hyd_Output5 = Valve5.Hyd_Output, Hyd_Output^Hyd_Output6 = Valve6.Hyd_Output, Hyd_Output^Hyd_Output7 = Valve7.Hyd_Output, Hyd_Output^Hyd_Output8 = Valve8.Hyd_Output, hyd = hydraulic.hyd1, Valve1.Hyd_Input = Hyd_Input1, Valve1.CMD = Ctrl, Valve2.Hyd_Input = Hyd_Input1, Valve2.CMD = Ctrl, Valve3.Hyd_Input = Hyd_Input1, Valve3.CMD = Ctrl, Valve4.Hyd_Input = Hyd_Input1, Valve4.CMD = Ctrl, Valve5.Hyd_Input = Hyd_Input2, Valve5.CMD = Ctrl, Valve6.Hyd_Input = Hyd_Input2, Valve6.CMD = Ctrl, Valve7.Hyd_Input = Hyd_Input2, Valve7.CMD = Ctrl, Valve8.Hyd_Input = Hyd_Input2, Valve8.CMD = Ctrl, hydraulic.v8 = Valve8.Hyd_Output, hydraulic.v7 = Valve7.Hyd_Output, hydraulic.v6 = Valve6.Hyd_Output, hydraulic.v5 = Valve5.Hyd_Output, hydraulic.v4 = Valve4.Hyd_Output, hydraulic.v3 = Valve3.Hyd_Output, hydraulic.v2 = Valve2.Hyd_Output, hydraulic.v1 = Valve1.Hyd_Output; edon node eq_ARP4761_Misceleneaous_Wheels flow icone:[1,9]:private; Hyd_Input2^Bus_Color:ARP4761_Flow_Bus_Color:in; Hyd_Input2^Hyd_Output1:ARP4761_Flow_Hyd:in; Hyd_Input2^Hyd_Output2:ARP4761_Flow_Hyd:in; Hyd_Input2^Hyd_Output3:ARP4761_Flow_Hyd:in; Hyd_Input2^Hyd_Output4:ARP4761_Flow_Hyd:in; Hyd_Input2^Hyd_Output5:ARP4761_Flow_Hyd:in; Hyd_Input2^Hyd_Output6:ARP4761_Flow_Hyd:in; Hyd_Input2^Hyd_Output7:ARP4761_Flow_Hyd:in; Hyd_Input2^Hyd_Output8:ARP4761_Flow_Hyd:in; Hyd_Input1^Bus_Color:ARP4761_Flow_Bus_Color:in; Hyd_Input1^Hyd_Output1:ARP4761_Flow_Hyd:in; Hyd_Input1^Hyd_Output2:ARP4761_Flow_Hyd:in; Hyd_Input1^Hyd_Output3:ARP4761_Flow_Hyd:in; Hyd_Input1^Hyd_Output4:ARP4761_Flow_Hyd:in; Hyd_Input1^Hyd_Output5:ARP4761_Flow_Hyd:in; Hyd_Input1^Hyd_Output6:ARP4761_Flow_Hyd:in; Hyd_Input1^Hyd_Output7:ARP4761_Flow_Hyd:in; Hyd_Input1^Hyd_Output8:ARP4761_Flow_Hyd:in; Sensors_Braking_Status:bool:out; Full_Braking_Status:bool:out; Wheels_Braking_Status:bool:out; Wheels_Antiskid_Status:bool:out; sub Wheel_1:ARP4761_miscelaneous_Wheel; Wheel_2:ARP4761_miscelaneous_Wheel; Wheel_3:ARP4761_miscelaneous_Wheel; Wheel_4:ARP4761_miscelaneous_Wheel; Wheel_5:ARP4761_miscelaneous_Wheel; Wheel_6:ARP4761_miscelaneous_Wheel; Wheel_7:ARP4761_miscelaneous_Wheel; Wheel_8:ARP4761_miscelaneous_Wheel; Counter1:ARP4761_miscelaneous_Counter; Counter2:ARP4761_miscelaneous_Counter; sensor1:ARP4761_miscelaneous_speed_sensor; sensor2:ARP4761_miscelaneous_speed_sensor; sensor3:ARP4761_miscelaneous_speed_sensor; sensor4:ARP4761_miscelaneous_speed_sensor; sensor5:ARP4761_miscelaneous_speed_sensor; sensor6:ARP4761_miscelaneous_speed_sensor; sensor7:ARP4761_miscelaneous_speed_sensor; sensor8:ARP4761_miscelaneous_speed_sensor; antiskid1:ARP4761_miscelaneous_antiskid; assert icone = (if (Counter1.O8by8 = true) then 8 else (if (Counter1.O7by8 = true) then 7 else (if (Counter1.O6by8 = true) then 6 else (if (Counter1.O5by8 = true) then 5 else (if (Counter1.O4by8 = true) then 4 else (if (Counter1.O3by8 = true) then 3 else (if (Counter1.O2by8 = true) then 2 else (if (Counter1.O1by8 = true) then 1 else 9)))))))), Sensors_Braking_Status = Counter2.O6by8, Full_Braking_Status = Counter1.O7by8, Wheels_Braking_Status = Counter1.O2by8, Wheels_Antiskid_Status = antiskid1.Antiskid_status, Wheel_1.Hyd_Input2 = Hyd_Input2^Hyd_Output1, Wheel_1.Hyd_Input1 = Hyd_Input1^Hyd_Output1, Wheel_2.Hyd_Input2 = Hyd_Input2^Hyd_Output2, Wheel_2.Hyd_Input1 = Hyd_Input1^Hyd_Output2, Wheel_3.Hyd_Input2 = Hyd_Input2^Hyd_Output3, Wheel_3.Hyd_Input1 = Hyd_Input1^Hyd_Output3, Wheel_4.Hyd_Input2 = Hyd_Input2^Hyd_Output4, Wheel_4.Hyd_Input1 = Hyd_Input1^Hyd_Output4, Wheel_5.Hyd_Input2 = Hyd_Input2^Hyd_Output5, Wheel_5.Hyd_Input1 = Hyd_Input1^Hyd_Output5, Wheel_6.Hyd_Input2 = Hyd_Input2^Hyd_Output6, Wheel_6.Hyd_Input1 = Hyd_Input1^Hyd_Output6, Wheel_7.Hyd_Input2 = Hyd_Input2^Hyd_Output7, Wheel_7.Hyd_Input1 = Hyd_Input1^Hyd_Output7, Wheel_8.Hyd_Input2 = Hyd_Input2^Hyd_Output8, Wheel_8.Hyd_Input1 = Hyd_Input1^Hyd_Output8, Counter1.e8 = Wheel_8.Wheel_Braking_Status, Counter1.e7 = Wheel_7.Wheel_Braking_Status, Counter1.e6 = Wheel_6.Wheel_Braking_Status, Counter1.e5 = Wheel_5.Wheel_Braking_Status, Counter1.e4 = Wheel_4.Wheel_Braking_Status, Counter1.e3 = Wheel_3.Wheel_Braking_Status, Counter1.e2 = Wheel_2.Wheel_Braking_Status, Counter1.e1 = Wheel_1.Wheel_Braking_Status, Counter2.e8 = sensor8.Out, Counter2.e7 = sensor7.Out, Counter2.e6 = sensor6.Out, Counter2.e5 = sensor5.Out, Counter2.e4 = sensor4.Out, Counter2.e3 = sensor3.Out, Counter2.e2 = sensor2.Out, Counter2.e1 = sensor1.Out, sensor1.In = Wheel_1.Wheel_Braking_Status_hyd1, sensor2.In = Wheel_2.Wheel_Braking_Status_hyd1, sensor3.In = Wheel_3.Wheel_Braking_Status_hyd1, sensor4.In = Wheel_4.Wheel_Braking_Status_hyd1, sensor5.In = Wheel_5.Wheel_Braking_Status_hyd1, sensor6.In = Wheel_6.Wheel_Braking_Status_hyd1, sensor7.In = Wheel_7.Wheel_Braking_Status_hyd1, sensor8.In = Wheel_8.Wheel_Braking_Status_hyd1, antiskid1.Wheel_status8 = Wheel_8.Wheel_Status, antiskid1.Wheel_status7 = Wheel_7.Wheel_Status, antiskid1.Wheel_status6 = Wheel_6.Wheel_Status, antiskid1.Wheel_status5 = Wheel_5.Wheel_Status, antiskid1.Wheel_status4 = Wheel_4.Wheel_Status, antiskid1.Wheel_status3 = Wheel_3.Wheel_Status, antiskid1.Wheel_status2 = Wheel_2.Wheel_Status, antiskid1.Wheel_status1 = Wheel_1.Wheel_Status; edon node main event CCF_HW_COM_MON_Incorrect, CCF_HW_COM_MON_Loss, CCF_SW_COM_Incorrect, CCF_SW_COM_Loss, CCF_SW_MON_Incorrect, CCF_SW_MON_Loss; sub Monitor1:ARP4761_BSCU_Monitor; Pilot:ARP4761_PilotCtrl_Pilot; ElectricalBrakeUnit:ARP4761_PilotCtrl_ElectricalBrakeUnit; delay1:ARP4761_miscelaneous_delay4; PWR1:ARP4761_ElectricalPower_Electrical_Power; PWR2:ARP4761_ElectricalPower_Electrical_Power; HYD1:ARP4761_Hydraulic_Hydraulic_Power; HYD2:ARP4761_Hydraulic_Hydraulic_Power; IsolationValve1:ARP4761_Hydraulic_Isolation_Valve; IsolationValve2:ARP4761_Hydraulic_Isolation_Valve; NormalMeterValves:eq_ARP4761_Hydraulic_Normal_Valve; ShutOff_AntiSkidValves:eq_ARP4761_Hydraulic_AntiSkid_Valve; SelectorValve:ARP4761_Hydraulic_SelectorValve; ShutOff_Valve:ARP4761_Hydraulic_ShutOffValve; Alt_EmerMeterValve_L:ARP4761_Hydraulic_Alt_Emer_Meter_Valve; Accumulator:ARP4761_Hydraulic_EmergencyAccumulator; InternalPower1:ARP4761_BSCU_InternalPower; InternalPower2:ARP4761_BSCU_InternalPower; PowerMonitor1:ARP4761_BSCU_PowerMonitor; PowerMonitor2:ARP4761_BSCU_PowerMonitor; Command1:ARP4761_BSCU_Command; Command2:ARP4761_BSCU_Command; Monitor2:ARP4761_BSCU_Monitor; Selection_Mgt:ARP4761_BSCU_SelectionManagement; AND1:ARP4761_miscelaneous_AND_3; AND2:ARP4761_miscelaneous_AND_3; Hyd_Or:ARP4761_Hydraulic_Hyd_Or; Alt_EmerMeterValve_R:ARP4761_Hydraulic_Alt_Emer_Meter_Valve; Wheels:eq_ARP4761_Misceleneaous_Wheels; FromEBU_1:ARP4761_miscelaneous_Stub1; FromEBU_2:ARP4761_miscelaneous_Stub1; ToBSCU:ARP4761_miscelaneous_Stub1; inhib1:ARP4761_miscelaneous_inhib; inhib2:ARP4761_miscelaneous_inhib; inhib3:ARP4761_miscelaneous_inhib; inhib4:ARP4761_miscelaneous_inhib; delay2:ARP4761_miscelaneous_delay5; OR:ARP4761_miscelaneous_OR_2; inv:ARP4761_miscelaneous_inv; FC_Loss_of_Braking:ARP4761_miscelaneous_FC_Braking_loss; FC_Untimely_Braking:ARP4761_miscelaneous_FC_Untimely_Braking; hydraulic_path:ARP4761_miscelaneous_hydraulic_path; computer_in_control:ARP4761_miscelaneous_computer_in_control; effect_on_wheels:ARP4761_miscelaneous_effect_on_wheels; computer_control_mode:ARP4761_miscelaneous_control_mode; assert Monitor1.Power_Input = InternalPower1.Pwr_Output, Monitor1.Pos2 = FromEBU_1.oElecPedalPos2, Monitor1.Pos1 = FromEBU_1.oElecPedalPos1, Monitor1.Enable_Cmd = Command1.Enable, Monitor1.Normal_Cmd = Command1.Normal, Monitor1.Alt_Emer_Cmd = Command1.Alt_Emer, Monitor1.isBraking = Command1.o_isBraking, ElectricalBrakeUnit.CMD_Input = Pilot.CMD_Output, delay1.In = Wheels.Sensors_Braking_Status, delay1.Braking_val = Pilot.CMD_Output, IsolationValve1.Hyd_Input = HYD1.Hyd_Output, IsolationValve2.Hyd_Input = HYD2.Hyd_Output, NormalMeterValves.Ctrl = Selection_Mgt.Normal, NormalMeterValves.Hyd_Input1 = SelectorValve.Hyd_Output1, NormalMeterValves.Hyd_Input2 = SelectorValve.Hyd_Output1, ShutOff_AntiSkidValves.Ctrl = Selection_Mgt.Alt_Emer, ShutOff_AntiSkidValves.Hyd_Input1 = Alt_EmerMeterValve_L.Hyd_Output, ShutOff_AntiSkidValves.Hyd_Input2 = Alt_EmerMeterValve_R.Hyd_Output, SelectorValve.Hyd_Input1 = ShutOff_Valve.Hyd_Output, SelectorValve.Hyd_Input2 = IsolationValve2.Hyd_Output, ShutOff_Valve.CMD = Selection_Mgt.Enable, ShutOff_Valve.Hyd_Input = IsolationValve1.Hyd_Output, Alt_EmerMeterValve_L.CMD = ElectricalBrakeUnit.CMD_Output3, Alt_EmerMeterValve_L.Hyd_Input = Hyd_Or.HydOut, Accumulator.Isol = IsolationValve2.Isol, Accumulator.HydIn = SelectorValve.Hyd_Output2, Accumulator.Sel_Pos = SelectorValve.Sel_Pos, InternalPower1.Pwr_Input = PWR1.Power_Output, InternalPower2.Pwr_Input = PWR2.Power_Output, PowerMonitor1.Pwr_Input = InternalPower1.Pwr_Output, PowerMonitor2.Pwr_Input = InternalPower2.Pwr_Output, Command1.Power_Input = InternalPower1.Pwr_Output, Command1.Pos2 = FromEBU_1.oElecPedalPos2, Command1.Pos1 = FromEBU_1.oElecPedalPos1, Command1.isBraking = delay1.Out, Command2.Power_Input = InternalPower2.Pwr_Output, Command2.Pos2 = FromEBU_2.oElecPedalPos2, Command2.Pos1 = FromEBU_2.oElecPedalPos1, Command2.isBraking = OR.Out, Monitor2.Power_Input = InternalPower2.Pwr_Output, Monitor2.Pos2 = FromEBU_2.oElecPedalPos2, Monitor2.Pos1 = FromEBU_2.oElecPedalPos1, Monitor2.Enable_Cmd = Command2.Enable, Monitor2.Normal_Cmd = Command2.Normal, Monitor2.Alt_Emer_Cmd = Command2.Alt_Emer, Monitor2.isBraking = Command2.o_isBraking, Selection_Mgt.Channel1_Validity = AND1.Out, Selection_Mgt.Channel2_Validity = AND2.Out, Selection_Mgt.Enable1 = Command1.Enable, Selection_Mgt.Enable2 = Command2.Enable, Selection_Mgt.Normal1 = Command1.Normal, Selection_Mgt.Normal2 = Command2.Normal, Selection_Mgt.Alt_Emer1 = Command1.Alt_Emer, Selection_Mgt.Alt_Emer2 = Command2.Alt_Emer, AND1.Input1 = inhib1.O, AND1.Input2 = inhib3.O, AND1.Input3 = Command1.Validity, AND2.Input1 = inhib2.O, AND2.Input2 = inhib4.O, AND2.Input3 = Command2.Validity, Hyd_Or.HydAccuIn = Accumulator.HydOut, Hyd_Or.HydIn = SelectorValve.Hyd_Output2, Alt_EmerMeterValve_R.CMD = ElectricalBrakeUnit.CMD_Output3, Alt_EmerMeterValve_R.Hyd_Input = Hyd_Or.HydOut, Wheels.Hyd_Input2^Bus_Color = ShutOff_AntiSkidValves.Hyd_Output^Bus_Color, Wheels.Hyd_Input2^Hyd_Output1 = ShutOff_AntiSkidValves.Hyd_Output^Hyd_Output1, Wheels.Hyd_Input2^Hyd_Output2 = ShutOff_AntiSkidValves.Hyd_Output^Hyd_Output2, Wheels.Hyd_Input2^Hyd_Output3 = ShutOff_AntiSkidValves.Hyd_Output^Hyd_Output3, Wheels.Hyd_Input2^Hyd_Output4 = ShutOff_AntiSkidValves.Hyd_Output^Hyd_Output4, Wheels.Hyd_Input2^Hyd_Output5 = ShutOff_AntiSkidValves.Hyd_Output^Hyd_Output5, Wheels.Hyd_Input2^Hyd_Output6 = ShutOff_AntiSkidValves.Hyd_Output^Hyd_Output6, Wheels.Hyd_Input2^Hyd_Output7 = ShutOff_AntiSkidValves.Hyd_Output^Hyd_Output7, Wheels.Hyd_Input2^Hyd_Output8 = ShutOff_AntiSkidValves.Hyd_Output^Hyd_Output8, Wheels.Hyd_Input1^Bus_Color = NormalMeterValves.Hyd_Output^Bus_Color, Wheels.Hyd_Input1^Hyd_Output1 = NormalMeterValves.Hyd_Output^Hyd_Output1, Wheels.Hyd_Input1^Hyd_Output2 = NormalMeterValves.Hyd_Output^Hyd_Output2, Wheels.Hyd_Input1^Hyd_Output3 = NormalMeterValves.Hyd_Output^Hyd_Output3, Wheels.Hyd_Input1^Hyd_Output4 = NormalMeterValves.Hyd_Output^Hyd_Output4, Wheels.Hyd_Input1^Hyd_Output5 = NormalMeterValves.Hyd_Output^Hyd_Output5, Wheels.Hyd_Input1^Hyd_Output6 = NormalMeterValves.Hyd_Output^Hyd_Output6, Wheels.Hyd_Input1^Hyd_Output7 = NormalMeterValves.Hyd_Output^Hyd_Output7, Wheels.Hyd_Input1^Hyd_Output8 = NormalMeterValves.Hyd_Output^Hyd_Output8, FromEBU_1.iElecPedalPos2 = ToBSCU.oElecPedalPos2, FromEBU_1.iElecPedalPos1 = ToBSCU.oElecPedalPos1, FromEBU_2.iElecPedalPos2 = ToBSCU.oElecPedalPos2, FromEBU_2.iElecPedalPos1 = ToBSCU.oElecPedalPos1, ToBSCU.iElecPedalPos2 = ElectricalBrakeUnit.CMD_Output2, ToBSCU.iElecPedalPos1 = ElectricalBrakeUnit.CMD_Output1, inhib1.I = PowerMonitor1.Pwr_Validity, inhib2.I = PowerMonitor2.Pwr_Validity, inhib3.I = Monitor1.Validity, inhib4.I = Monitor2.Validity, delay2.In = inv.O, delay2.Braking_val = Pilot.CMD_Output, OR.Input1 = delay2.Out, OR.Input2 = Wheels.Sensors_Braking_Status, inv.I = Selection_Mgt.Channel2, FC_Loss_of_Braking.WheelBrakingStatus = Wheels.Wheels_Braking_Status, FC_Loss_of_Braking.BrakingCMD = Pilot.CMD_Output, FC_Untimely_Braking.FullBrakingStatus = Wheels.Full_Braking_Status, FC_Untimely_Braking.BrakingCMD = Pilot.CMD_Output, hydraulic_path.accu = Accumulator.HydOut, hydraulic_path.hyd2i = SelectorValve.Hyd_Output2, hydraulic_path.hyd2g = ShutOff_AntiSkidValves.hyd, hydraulic_path.hyd1 = NormalMeterValves.hyd, computer_in_control.Channel1 = Selection_Mgt.Channel1, computer_in_control.Channel2 = Selection_Mgt.Channel2, effect_on_wheels.Full_braking_status = Wheels.Full_Braking_Status, effect_on_wheels.Wheels_braking_status = Wheels.Wheels_Braking_Status, effect_on_wheels.Wheels_antiskid_status = Wheels.Wheels_Antiskid_Status, computer_control_mode.Alt_Emer = Selection_Mgt.Alt_Emer, computer_control_mode.Normal = Selection_Mgt.Normal, computer_control_mode.Hyd2 = SelectorValve.Hyd_Output2, computer_control_mode.Accu = Accumulator.HydOut; sync , , , , , , , , , , , , , ; init Monitor1.States := MON_Loss, Monitor2.States := MON_Loss, Pilot.States := Braking, PowerMonitor1.States := MON_Loss, PowerMonitor2.States := MON_Loss, inhib1.inhib_state := inhib, inhib2.inhib_state := inhib, inhib3.inhib_state := inhib, inhib4.inhib_state := inhib; extern law = exponential(1.0E-15); attribute 'Safety/DAL;1'() = ; law = exponential(1.0E-15); attribute 'Safety/DAL;1'() = ; law = exponential(1.0E-15); attribute 'Safety/DAL;1'() = ; law = exponential(1.0E-15); attribute 'Safety/DAL;1'() = ; law = exponential(1.0E-15); attribute 'Safety/DAL;1'() = ; law = exponential(1.0E-15); attribute 'Safety/DAL;1'() = ; nodeproperty = "ARP_V21"; nodeproperty = "1"; nodeproperty = "Braking_withoutMON"; nodeproperty = "2022-07-23 00:51:04"; ccf = true; withCCF = {, }; withCCF = {, }; withCCF = {, }; withCCF = {, }; ccf = true; withCCF = {, }; withCCF = {, }; withCCF = {, }; withCCF = {, }; ccf = true; ccf = true; ccf = true; ccf = true; edon