package Crazyflie_System
public

  with Crazyflie_Hardware;
  with Crazyflie_Software;
  with Cheddar_Transformation_Properties;
  with Cheddar_Parameters_Properties;

  system Crazyflie_System extends Crazyflie_Hardware::Crazyflie
  end Crazyflie_System;

  system implementation Crazyflie_System.impl
     extends Crazyflie_Hardware::Crazyflie.impl
  subcomponents
    nRF51822_Firmware : process Crazyflie_Software::nRF51822_Firmware;
    STM32F405_Firmware : process Crazyflie_Software::STM32F405_Firmware.impl;

  connections
    C10 : port nRF51822_Firmware.Syslink_Packet_TX
      -> STM32F405_Firmware.Syslink_Packet_Rx;
    C10b : port STM32F405_Firmware.Syslink_Packet_TX
      -> nRF51822_Firmware.Syslink_Packet_Rx;
      
    C11 : port MPU9250.DOF6 -> STM32F405_Firmware.DOFs;
    C12 : port STM32F405_Firmware.Rate_1 -> M1.rate;
    C13 : port STM32F405_Firmware.Rate_2 -> M2.rate;
    C14 : port STM32F405_Firmware.Rate_3 -> M3.rate;
    C15 : port STM32F405_Firmware.Rate_4 -> M4.rate;

  flows
    -- etef1 represents the functional chain from MPU9250 IMU to STM32
    -- firmware to one of the propeller.

    etef1 : end to end flow MPU9250.f1 -> C11 -> STM32F405_Firmware.f2
       -> C12 -> M1.f1 { latency => 0 ms .. 2 ms;};

    -- etef2 represents the functional chain from command
    -- (received from nRF51822) to STM32 firmware to one of the
    -- propeller.

    etef2 : end to end flow nRF51822_Firmware.f1 -> C10 -> STM32F405_Firmware.f1
      -> C12 -> M1.f1 { latency => 0 ms .. 2 ms;};

  	properties
  	
  	Cheddar_Transformation_Properties::Exported_Attribute_Time_Units => MicroSecond;
	Cheddar_Parameters_Properties::Scheduling_Feasibility_Interval => 10000;
	Cheddar_Parameters_Properties::Response_Time_From_Scheduling_Simulation => true;
	
    Actual_Processor_Binding => (reference (STM32F405)) applies to STM32F405_Firmware;
    Actual_Processor_Binding => (reference (nRF51822)) applies to nRF51822_Firmware;

    Actual_Connection_Binding => (reference (UART)) applies to C10;
    Actual_Connection_Binding => (reference (I2C)) applies to C11;
    
  annex EMV2 {**
    use types Crazyflie_Errors;
    use behavior Crazyflie_Errors::simple;
    composite error behavior
    states
      [ MPU9250.Operational and STM32F405.Operational]-> Operational;   
      [ MPU9250.Failed or STM32F405.Failed]-> Failed;       
    end composite;  
        
    connection error
       C10_err : error source C10{ValueErroneous}; 
    end connection;
  **};
  end Crazyflie_System.impl;

end Crazyflie_System;