module JoystickDrv:

 type orcStrlPtr ;
input 
   EmergencyStopE,
   EndOKE,
   PbMotorE,
   InitOK_PhRCycab,
   JoystickDrv_Start:orcStrlPtr,
   START_JoystickDrv,
   FinTransite_PhRCycab,
   Abort_Local_JoystickDrv;

output 
T2_PbMotorE,
   STARTED_JoystickDrv,
   GoodEnd_JoystickDrv,
   ActivateJoystickDrv_PhRCycab:orcStrlPtr,
   T2_JoystickDrv,
   JoystickDrvTransite : orcStrlPtr,
   Abort_JoystickDrv:orcStrlPtr,
   BF_JoystickDrv,
   T3_JoystickDrv,
   StartTransite_PhRCycab,
   Prev_rt_PhRCycab:orcStrlPtr, 
   ReadyToStart_PhRCycab;

relation 
   EmergencyStopE#
   EndOKE#
   PbMotorE#
   InitOK_PhRCycab#
   START_JoystickDrv#
   Abort_Local_JoystickDrv#
   FinTransite_PhRCycab;

trap T3 in 
 loop   await immediate START_JoystickDrv;
  emit STARTED_JoystickDrv;

  trap Abort in 
  do 
  [ 
   await InitOK_PhRCycab
  ]
  watching Abort_Local_JoystickDrv
   timeout emit Abort_JoystickDrv(?JoystickDrv_Start); exit Abort;
  end;

  do 
  [ 
   emit ReadyToStart_PhRCycab;
   await immediate FinTransite_PhRCycab;
   emit ActivateJoystickDrv_PhRCycab(?JoystickDrv_Start);
   emit Prev_rt_PhRCycab(?JoystickDrv_Start);
  ]
  watching Abort_Local_JoystickDrv
   timeout emit StartTransite_PhRCycab;
           emit JoystickDrvTransite(?JoystickDrv_Start); exit Abort
  end;

  trap T2 in 
   trap BF in

   [ 
    await Abort_Local_JoystickDrv;
    emit StartTransite_PhRCycab;
    emit JoystickDrvTransite(?JoystickDrv_Start);
    exit Abort; 
   ]
  ||
   await PbMotorE; emit T2_PbMotorE; exit T2
  || 
   await EmergencyStopE; exit T3
  || 
  [[
  [ 
   await EndOKE
  ]
 ]; exit BF; ]

   handle BF do 
    emit JoystickDrvTransite(?JoystickDrv_Start);
    emit BF_JoystickDrv; emit GoodEnd_JoystickDrv; 
    emit StartTransite_PhRCycab;
   end trap 

  handle T2 do 
   emit T2_JoystickDrv; 
   emit StartTransite_PhRCycab; 
   emit JoystickDrvTransite(?JoystickDrv_Start);
  end trap
 end trap

end loop

handle T3 do emit T3_JoystickDrv
end trap


end module