/*LighInspectionV5.alt */
/* Date : May 23, 2018 */
/* DataFlow format */
/* Copyright ONERA */

domain Quality_Statement_OStSf = {ok, stuck_false, stuck_true};

node Operator_Bool_and2
  flow
    icone:[1,2]:private;
    O:bool:out;
    I1:bool:in;
    I2:bool:in;
  assert
    icone = case {
      (I1 and I2) : 1,
      else 2
    },
    O = (I1 and I2);
edon

node Operator_Bool_and4
  flow
    icone:[1,2]:private;
    O:bool:out;
    I1:bool:in;
    I2:bool:in;
    I3:bool:in;
    I4:bool:in;
  assert
    icone = case {
      (((I1 and I2) and I3) and I4) : 1,
      else 2
    },
    O = (((I1 and I2) and I3) and I4);
edon

node Operator_Bool_neg
  flow
    icone:[1,2]:private;
    O:bool:out;
    I:bool:in;
  assert
    icone = case {
      (not I) : 1,
      else 2
    },
    O = (not I);
edon

node Operation_Task_alone_perfo_ExternalCondition
  flow
    icone:[1,2]:private;
    Out_cond:bool:out;
  state
    cond:bool;
  event
    is_false;
  trans
    (cond = true) |- is_false -> cond := false;
  assert
    icone = case {
      cond : 1,
      else 2
    },
    Out_cond = cond;
  init
    cond := true;
  extern
    law <event is_false> = exponential(0.001);
    attribute DassaultSpecialCtrlPeriod(<event is_false>) = 9.877E8;
edon

node Operator_Bool_and3
  flow
    icone:[1,2]:private;
    O:bool:out;
    I1:bool:in;
    I2:bool:in;
    I3:bool:in;
  assert
    icone = case {
      ((I1 and I2) and I3) : 1,
      else 2
    },
    O = ((I1 and I2) and I3);
edon

node Block_Bool_funcO
  flow
    icone:[1,2]:private;
    O:bool:out;
  state
    ok:bool;
  event
    fail;
  trans
    ok |- fail -> ok := false;
  assert
    icone = case {
      ok : 1,
      else 2
    },
    O = ok;
  init
    ok := true;
  extern
    law <event fail> = constant(1.6E-4);
edon

node Block_Bool_obsI
  flow
    icone:[1,4]:private;
    I:bool:in;
    O:bool:out;
  state
    S:Quality_Statement_OStSf;
  event
    stuck_on_true,
    stuck_on_false;
  trans
    (S = ok) |- stuck_on_true -> S := stuck_true;
    (S = ok) |- stuck_on_false -> S := stuck_false;
  assert
    icone = case {
      ((S = ok) and I) : 1,
      ((S = ok) and (not I)) : 2,
      (S = stuck_true) : 3,
      else 4
    },
    O = case {
      (S = ok) : I,
      (S = stuck_true) : true,
      else false
    };
  init
    S := ok;
  extern
    law <event stuck_on_true> = constant(1.0E-4);
    law <event stuck_on_false> = constant(1.0E-5);
edon

node Operator_Bool_or2
  flow
    icone:[1,2]:private;
    O:bool:out;
    I1:bool:in;
    I2:bool:in;
  assert
    icone = case {
      (I1 or I2) : 1,
      else 2
    },
    O = (I1 or I2);
edon

node eq_RobotLightInspection_MissionPhases_EnvironmentV5
  flow
    RobotSafe:bool:out;
    SupervisionSafe:bool:out;
    RunwayClear:bool:out;
    RunwayClosed:bool:out;
  sub
    SupervisionSafe:Operation_Task_alone_perfo_ExternalCondition;
    RunWayClosed:Operation_Task_alone_perfo_ExternalCondition;
    RobotSafe:Operation_Task_alone_perfo_ExternalCondition;
    RunWayClear:Operation_Task_alone_perfo_ExternalCondition;
  assert
    RobotSafe = RobotSafe.Out_cond,
    SupervisionSafe = SupervisionSafe.Out_cond,
    RunwayClear = RunWayClear.Out_cond,
    RunwayClosed = RunWayClosed.Out_cond;
edon

node eq_RobotLightInspection_MissionPhases_ActionV5
  flow
    D_REmergencyStop:bool:in;
    D_RRunWayExit:bool:in;
    OutRobotRunwayExit:bool:out;
    OutRobotEmergencyStop:bool:out;
    OutRobotlNormalMove:bool:out;
  sub
    NormalMove:Operator_Bool_and3;
    NoStop:Operator_Bool_neg;
    EmergencyStop:Operator_Bool_and2;
    StopMove:Block_Bool_funcO;
    ExitRunway:Block_Bool_funcO;
    MoveNormal:Block_Bool_funcO;
    RunwayExit:Operator_Bool_and2;
    NoExit:Operator_Bool_neg;
  assert
    OutRobotRunwayExit = RunwayExit.O,
    OutRobotEmergencyStop = EmergencyStop.O,
    OutRobotlNormalMove = NormalMove.O,
    NormalMove.I1 = NoStop.O,
    NormalMove.I2 = MoveNormal.O,
    NormalMove.I3 = NoExit.O,
    NoStop.I = D_REmergencyStop,
    EmergencyStop.I1 = StopMove.O,
    EmergencyStop.I2 = D_REmergencyStop,
    RunwayExit.I1 = D_RRunWayExit,
    RunwayExit.I2 = ExitRunway.O,
    NoExit.I = D_RRunWayExit;
edon

node eq_RobotLightInspection_MissionPhases_ControlV5
  flow
    K_ATC_RunwayClosed:bool:in;
    K_Supervisor_RunwayClosed:bool:in;
    K_ATC_SupervisionSafe:bool:in;
    K_Supervisor_SupervisionSafe:bool:in;
    K_Robot_SupervisionSafe:bool:in;
    K_Supervisor_RobotSafe:bool:in;
    K_Robot_RobotSafe:bool:in;
    K_Supervisor_RunwayClear:bool:in;
    K_Robot_RunwayClear:bool:in;
    D_ATC_RunwayClose:bool:out;
    D_Robot_EmergencyStop:bool:out;
    D_Robot_RunwayExit:bool:out;
    D_Supervisor_EmergencyStop:bool:out;
    D_Supervisor_RunwayExit:bool:out;
  sub
    D_Robot_RunwayExit:Operator_Bool_and2;
    ATCDecideRunwayClosure:Block_Bool_obsI;
    SupervisorDecideEmergencyStop:Block_Bool_obsI;
    RobotDecideEmergencyStop:Block_Bool_obsI;
    SupervisorDecideRunwayExit:Block_Bool_obsI;
    RobotReceiveEmergencyStop:Block_Bool_obsI;
    SupervisorSendEmergencyStop:Block_Bool_obsI;
    K_ATC_Operationsafe:Operator_Bool_or2;
    K_ATC_OperationUnsafe:Operator_Bool_neg;
    K_Supervisor_OperationSafe:Operator_Bool_and3;
    K_Supervisor_RunwayExitNoNeeded:Operator_Bool_or2;
    K_SupervisorRunwayExitNeeded:Operator_Bool_neg;
    K_Supervisor_OperationUnsafe:Operator_Bool_neg;
    K_Robot_OperationSafe:Operator_Bool_and3;
    K_Robot_OperationUnsafe:Operator_Bool_neg;
    K_Robot_EmergencyStopNeeded:Operator_Bool_or2;
    RobotReceiveRunwayExit:Block_Bool_obsI;
    SupervisorSendRunwayExit:Block_Bool_obsI;
    K_RobotEmergencyStopNotNeeded:Operator_Bool_neg;
    RobotDecideRunwayExit:Block_Bool_obsI;
  assert
    D_ATC_RunwayClose = ATCDecideRunwayClosure.O,
    D_Robot_EmergencyStop = RobotDecideEmergencyStop.O,
    D_Robot_RunwayExit = RobotDecideRunwayExit.O,
    D_Supervisor_EmergencyStop = SupervisorDecideEmergencyStop.O,
    D_Supervisor_RunwayExit = SupervisorDecideRunwayExit.O,
    D_Robot_RunwayExit.I1 = RobotReceiveRunwayExit.O,
    D_Robot_RunwayExit.I2 = K_RobotEmergencyStopNotNeeded.O,
    ATCDecideRunwayClosure.I = K_ATC_OperationUnsafe.O,
    SupervisorDecideEmergencyStop.I = K_Supervisor_OperationUnsafe.O,
    RobotDecideEmergencyStop.I = K_Robot_EmergencyStopNeeded.O,
    SupervisorDecideRunwayExit.I = K_SupervisorRunwayExitNeeded.O,
    RobotReceiveEmergencyStop.I = SupervisorSendEmergencyStop.O,
    SupervisorSendEmergencyStop.I = SupervisorDecideEmergencyStop.O,
    K_ATC_Operationsafe.I1 = K_ATC_RunwayClosed,
    K_ATC_Operationsafe.I2 = K_ATC_SupervisionSafe,
    K_ATC_OperationUnsafe.I = K_ATC_Operationsafe.O,
    K_Supervisor_OperationSafe.I1 = K_Supervisor_SupervisionSafe,
    K_Supervisor_OperationSafe.I2 = K_Supervisor_RobotSafe,
    K_Supervisor_OperationSafe.I3 = K_Supervisor_RunwayClear,
    K_Supervisor_RunwayExitNoNeeded.I1 = K_Supervisor_RunwayClosed,
    K_Supervisor_RunwayExitNoNeeded.I2 = SupervisorDecideEmergencyStop.O,
    K_SupervisorRunwayExitNeeded.I = K_Supervisor_RunwayExitNoNeeded.O,
    K_Supervisor_OperationUnsafe.I = K_Supervisor_OperationSafe.O,
    K_Robot_OperationSafe.I1 = K_Robot_SupervisionSafe,
    K_Robot_OperationSafe.I2 = K_Robot_RobotSafe,
    K_Robot_OperationSafe.I3 = K_Robot_RunwayClear,
    K_Robot_OperationUnsafe.I = K_Robot_OperationSafe.O,
    K_Robot_EmergencyStopNeeded.I1 = RobotReceiveEmergencyStop.O,
    K_Robot_EmergencyStopNeeded.I2 = K_Robot_OperationUnsafe.O,
    RobotReceiveRunwayExit.I = SupervisorSendRunwayExit.O,
    SupervisorSendRunwayExit.I = SupervisorDecideRunwayExit.O,
    K_RobotEmergencyStopNotNeeded.I = RobotDecideEmergencyStop.O,
    RobotDecideRunwayExit.I = D_Robot_RunwayExit.O;
edon

node eq_RobotLightInspection_MissionPhases_MonitoringV5
  flow
    RobotSafe:bool:in;
    SupervisionSafe:bool:in;
    RunwayClear:bool:in;
    RunwayClosed:bool:in;
    K_ATC_RunwayClosed:bool:out;
    K_S_RunwayClosed:bool:out;
    K_ATC_SupervisionSafe:bool:out;
    K_S_SupervisionSafe:bool:out;
    K_R_SupervisionSafe:bool:out;
    K_S_RobotSafe:bool:out;
    K_R_RobotSafe:bool:out;
    K_S_RunwayClear:bool:out;
    K_R_RunwayClear:bool:out;
  sub
    SupervisorAnalyseRobotStatus:Block_Bool_obsI;
    SupervisorReceiveRobotStatus:Block_Bool_obsI;
    SupervisorSelfAnalyse:Block_Bool_obsI;
    SupervisorAnalyseRunwayStatus:Block_Bool_obsI;
    SupervisorReceiveRunwayStatus:Block_Bool_obsI;
    SupervisorAnalyseObstacleStatus:Block_Bool_obsI;
    SupervisorReceiveObstacleStatus:Block_Bool_obsI;
    ATCAnalyseRunWay:Block_Bool_obsI;
    ATCSendRunWayStatus:Block_Bool_obsI;
    SupervisorSendSelfStatus:Block_Bool_obsI;
    ATCReceiceSupervisorStatus:Block_Bool_obsI;
    ATCAnalyseSupervisorStatus:Block_Bool_obsI;
    RobotSendSelfStatus:Block_Bool_obsI;
    RobotSelfAnalyse:Block_Bool_obsI;
    RobotAnalyseObstacle:Block_Bool_obsI;
    RobotSendObstacleStatus:Block_Bool_obsI;
    RobotReceiveSupervisorStatus:Block_Bool_obsI;
    RobotAnalyseSupervisorStatus:Block_Bool_obsI;
  assert
    K_ATC_RunwayClosed = ATCAnalyseRunWay.O,
    K_S_RunwayClosed = SupervisorAnalyseRunwayStatus.O,
    K_ATC_SupervisionSafe = ATCAnalyseSupervisorStatus.O,
    K_S_SupervisionSafe = SupervisorSelfAnalyse.O,
    K_R_SupervisionSafe = RobotAnalyseSupervisorStatus.O,
    K_S_RobotSafe = SupervisorAnalyseRobotStatus.O,
    K_R_RobotSafe = RobotSelfAnalyse.O,
    K_S_RunwayClear = SupervisorAnalyseObstacleStatus.O,
    K_R_RunwayClear = RobotAnalyseObstacle.O,
    SupervisorAnalyseRobotStatus.I = SupervisorReceiveRobotStatus.O,
    SupervisorReceiveRobotStatus.I = RobotSendSelfStatus.O,
    SupervisorSelfAnalyse.I = SupervisionSafe,
    SupervisorAnalyseRunwayStatus.I = SupervisorReceiveRunwayStatus.O,
    SupervisorReceiveRunwayStatus.I = ATCSendRunWayStatus.O,
    SupervisorAnalyseObstacleStatus.I = SupervisorReceiveObstacleStatus.O,
    SupervisorReceiveObstacleStatus.I = RobotSendObstacleStatus.O,
    ATCAnalyseRunWay.I = RunwayClosed,
    ATCSendRunWayStatus.I = ATCAnalyseRunWay.O,
    SupervisorSendSelfStatus.I = SupervisorSelfAnalyse.O,
    ATCReceiceSupervisorStatus.I = SupervisorSendSelfStatus.O,
    ATCAnalyseSupervisorStatus.I = ATCReceiceSupervisorStatus.O,
    RobotSendSelfStatus.I = RobotSelfAnalyse.O,
    RobotSelfAnalyse.I = RobotSafe,
    RobotAnalyseObstacle.I = RunwayClear,
    RobotSendObstacleStatus.I = RobotAnalyseObstacle.O,
    RobotReceiveSupervisorStatus.I = SupervisorSendSelfStatus.O,
    RobotAnalyseSupervisorStatus.I = RobotReceiveSupervisorStatus.O;
edon

node main
  sub
    CollisionWithObstacle:Operator_Bool_and2;
    SituationOK:Operator_Bool_and4;
    DebrisOnRunway:Operator_Bool_neg;
    RealWorld:eq_RobotLightInspection_MissionPhases_EnvironmentV5;
    RobotAction:eq_RobotLightInspection_MissionPhases_ActionV5;
    OperationControl:eq_RobotLightInspection_MissionPhases_ControlV5;
    OperationMonitoring:eq_RobotLightInspection_MissionPhases_MonitoringV5;
    OpenRunway:Operator_Bool_neg;
    SupervisionKO:Operator_Bool_neg;
    RobotKO:Operator_Bool_neg;
    EmergencyStopKO:Operator_Bool_neg;
    RunwayExitKO:Operator_Bool_neg;
    NormalMoveKO:Operator_Bool_neg;
    CollisionWithAircraft:Operator_Bool_and2;
    DegradedSupervisionOperation:Operator_Bool_and2;
    DegradedRobotOperation:Operator_Bool_and2;
    IntempestiveNormalMissionStop:Operator_Bool_and2;
  assert
    CollisionWithObstacle.I1 = DebrisOnRunway.O,
    CollisionWithObstacle.I2 = EmergencyStopKO.O,
    SituationOK.I1 = RealWorld.RunwayClosed,
    SituationOK.I2 = RealWorld.RunwayClear,
    SituationOK.I3 = RealWorld.SupervisionSafe,
    SituationOK.I4 = RealWorld.RobotSafe,
    DebrisOnRunway.I = RealWorld.RunwayClear,
    RobotAction.D_REmergencyStop = OperationControl.D_Robot_EmergencyStop,
    RobotAction.D_RRunWayExit = OperationControl.D_Robot_RunwayExit,
    OperationControl.K_ATC_RunwayClosed = OperationMonitoring.K_ATC_RunwayClosed,
    OperationControl.K_Supervisor_RunwayClosed = OperationMonitoring.K_S_RunwayClosed,
    OperationControl.K_ATC_SupervisionSafe = OperationMonitoring.K_ATC_SupervisionSafe,
    OperationControl.K_Supervisor_SupervisionSafe = OperationMonitoring.K_S_SupervisionSafe,
    OperationControl.K_Robot_SupervisionSafe = OperationMonitoring.K_R_SupervisionSafe,
    OperationControl.K_Supervisor_RobotSafe = OperationMonitoring.K_S_RobotSafe,
    OperationControl.K_Robot_RobotSafe = OperationMonitoring.K_R_RobotSafe,
    OperationControl.K_Supervisor_RunwayClear = OperationMonitoring.K_S_RunwayClear,
    OperationControl.K_Robot_RunwayClear = OperationMonitoring.K_R_RunwayClear,
    OperationMonitoring.RobotSafe = RealWorld.RobotSafe,
    OperationMonitoring.SupervisionSafe = RealWorld.SupervisionSafe,
    OperationMonitoring.RunwayClear = RealWorld.RunwayClear,
    OperationMonitoring.RunwayClosed = RealWorld.RunwayClosed,
    OpenRunway.I = RealWorld.RunwayClosed,
    SupervisionKO.I = RealWorld.SupervisionSafe,
    RobotKO.I = RealWorld.RobotSafe,
    EmergencyStopKO.I = RobotAction.OutRobotEmergencyStop,
    RunwayExitKO.I = RobotAction.OutRobotRunwayExit,
    NormalMoveKO.I = RobotAction.OutRobotlNormalMove,
    CollisionWithAircraft.I1 = OpenRunway.O,
    CollisionWithAircraft.I2 = RunwayExitKO.O,
    DegradedSupervisionOperation.I1 = SupervisionKO.O,
    DegradedSupervisionOperation.I2 = EmergencyStopKO.O,
    DegradedRobotOperation.I1 = RobotKO.O,
    DegradedRobotOperation.I2 = EmergencyStopKO.O,
    IntempestiveNormalMissionStop.I1 = SituationOK.O,
    IntempestiveNormalMissionStop.I2 = NormalMoveKO.O;
  extern
    nodeproperty <global projectName> = "OpMod/GlobalOperation/LightInspectionV5";
    nodeproperty <global projectVersion> = "1";
    nodeproperty <global projectConfig> = "default";
    nodeproperty <global currentDate> = "2018-05-23 9:17:51";
edon