property set ARINC653 is
  Module_Major_Frame : Time
    applies to (processor, virtual processor);

  Sampling_Refresh_Period : Time
    applies to (data port);

  Supported_Error_Code : type enumeration (Module_Config, Module_Init, Module_Scheduling, Partition_Scheduling, Partition_Config, Partition_Handler, Partition_Init, Deadline_Miss, Application_Error, Numeric_Error, Illegal_Request, Stack_Overflow, Memory_Violation, Hardware_Fault, Power_Fail);

  Supported_Memory_Type : type enumeration (Data_Memory, Code_Memory, IO_Memory);

  Memory_Type : list of ARINC653::Supported_Memory_Type
    applies to (memory);

  Timeout : Time
    applies to (port, access connections);

  Supported_DAL_Type : type enumeration (LEVEL_A, LEVEL_B, LEVEL_C, LEVEL_D, LEVEL_E);

  DAL : ARINC653::Supported_DAL_Type
    applies to (virtual processor, system, abstract);

  Module_Version : aadlstring
    applies to (processor);

  Module_Identifier : aadlstring
    applies to (processor);

  Partition_Identifier : aadlinteger
    applies to (virtual processor);

  Partition_Name : aadlstring
    applies to (virtual processor);

  System_Partition : aadlboolean
    applies to (virtual processor);

  Error_Handling : reference (
thread)
    applies to (virtual processor);

  Error_Level_Type : type enumeration (Module_Level, Partition_Level, Process_Level);

  HM_Error_ID_Level_Type : type record (ErrorIdentifier : aadlinteger; Description : aadlstring; ErrorLevel : ARINC653::Error_Level_Type; ErrorCode : ARINC653::Supported_Error_Code;);

  HM_Error_ID_Levels : list of ARINC653::HM_Error_ID_Level_Type
    applies to (processor);

  HM_Error_ID_Action_Type : type record (ErrorIdentifier : aadlinteger; Description : aadlstring; Action : aadlstring;);

  HM_Error_ID_Actions : list of ARINC653::HM_Error_ID_Action_Type
    applies to (processor, virtual processor, thread);

  State_Information_Type : type record (Identifier : aadlinteger; Description : aadlstring;);

  State_Information : ARINC653::State_Information_Type
    applies to (mode);

  Queueing_Discipline_Type : type enumeration (Fifo, By_Priority);

  Queueing_Discipline : ARINC653::Queueing_Discipline_Type
    applies to (port, data access);

  Schedule_Window : type record (Partition : reference (
virtual processor, processor); Duration : time; Periodic_Processing_Start : aadlboolean;);

  Module_Schedule : list of ARINC653::Schedule_Window
    applies to (processor, virtual processor);

  Time_Capacity : Time
    applies to (thread);

  Deadline_Type : enumeration (soft, hard)
    applies to (thread);

end ARINC653;

package PartitionedSystemExample
public
  with ARINC653;

  data integer
  end integer;

  data ordercmd
  end ordercmd;

  data protected_data
  properties
    Concurrency_Control_Protocol => Protected_Access;

  end protected_data;

  virtual processor partition1_rt
  properties
    Scheduling_Protocol => (EARLIEST_DEADLINE_FIRST_PROTOCOL);

  end partition1_rt;

  virtual processor implementation partition1_rt.impl
  end partition1_rt.impl;

  virtual processor partition2_rt
  properties
    Scheduling_Protocol => (RATE_MONOTONIC_PROTOCOL);

  end partition2_rt;

  virtual processor implementation partition2_rt.impl
  end partition2_rt.impl;

  subprogram sensor_temperature_spg
  end sensor_temperature_spg;

  subprogram sensor_receiveinput_spg
  end sensor_receiveinput_spg;

  subprogram commandboard_receiveinput_spg
  end commandboard_receiveinput_spg;

  subprogram commandboard_printinfos_spg
  end commandboard_printinfos_spg;

  thread sensor_temperature_thread
  features
    tempout : out data port integer;
    order : in event data port ordercmd;

  properties
    Initialize_Entrypoint => classifier (PartitionedSystemExample::sensor_temperature_spg);
    Priority => 42;
    Source_Stack_Size => 100 Kbyte;
    Period => 20 ms;
    Compute_Execution_Time => 10 ms .. 12 ms;
    Deadline => 40 ms;

  end sensor_temperature_thread;

  thread implementation sensor_temperature_thread.impl
  end sensor_temperature_thread.impl;

  thread sensor_receiveinput_thread
  features
    commandin : in event data port integer;
    order : out event data port ordercmd;

  properties
    Initialize_Entrypoint => classifier (PartitionedSystemExample::sensor_receiveinput_spg);
    Priority => 10;
    Source_Stack_Size => 100 Kbyte;
    Period => 20 ms;
    Compute_Execution_Time => 8 ms .. 10 ms;
    Deadline => 40 ms;

  end sensor_receiveinput_thread;

  thread implementation sensor_receiveinput_thread.impl
  end sensor_receiveinput_thread.impl;

  thread commandboard_receiveinput_thread
  features
    temp : in data port integer;
    tempavg : requires data access integer;
    newavg : out event port;
    need_semaphore : requires data access protected_data;

  properties
    Initialize_Entrypoint => classifier (PartitionedSystemExample::commandboard_receiveinput_spg);
    Priority => 42;
    Source_Stack_Size => 100 Kbyte;
    Period => 20 ms;
    Compute_Execution_Time => 5 ms .. 7 ms;
    Deadline => 40 ms;

  end commandboard_receiveinput_thread;

  thread commandboard_printinfos_thread
  features
    ordersensor : out event data port integer;
    tempavg : requires data access integer;
    newavg : in event port;
    need_semaphore : requires data access protected_data;

  properties
    Initialize_Entrypoint => classifier (PartitionedSystemExample::commandboard_printinfos_spg);
    Priority => 43;
    Source_Stack_Size => 100 Kbyte;
    Period => 20 ms;
    Compute_Execution_Time => 2 ms .. 6 ms;
    Deadline => 40 ms;

  end commandboard_printinfos_thread;

  process partition1_process
  features
    queueingin : in event data port integer
      {Queue_Size => 4;};
    samplingout : out data port integer;

  end partition1_process;

  process implementation partition1_process.impl
  subcomponents
    temperature : thread sensor_temperature_thread.impl;
    order : thread sensor_receiveinput_thread.impl;

  connections
    bufferconnectionexample : port order.order -> temperature.order;
    port queueingin -> order.commandin;
    port temperature.tempout -> samplingout;

  end partition1_process.impl;

  process partition2_process
  features
    queueingout : out event data port integer;
    samplingin : in data port integer
      {ARINC653::Sampling_Refresh_Period => 10 ms;};

  end partition2_process;

  process implementation partition2_process.impl
  subcomponents
    receiver : thread commandboard_receiveinput_thread;
    printer : thread commandboard_printinfos_thread;
    sem : data protected_data;
    blackboard : data integer;

  connections
    blackboardconnection1 : data access blackboard -> printer.tempavg;
    blackboardconnection2 : data access blackboard -> receiver.tempavg;
    eventconnectionexample : port receiver.newavg -> printer.newavg;
    port printer.ordersensor -> queueingout;
    port samplingin -> receiver.temp;
    data access sem -> receiver.need_semaphore;
    data access sem -> printer.need_semaphore;

  end partition2_process.impl;

  processor powerpc
  end powerpc;

  processor implementation powerpc.impl
  subcomponents
    part1 : virtual processor partition1_rt.impl;
    part2 : virtual processor partition2_rt.impl;

  properties
    ARINC653::Module_Major_Frame => 50 ms;

  end powerpc.impl;

  memory partition1_memory
  properties
    Base_Address => 0;

  end partition1_memory;

  memory partition2_memory
  properties
    Base_Address => 100;

  end partition2_memory;

  memory main_memory
  end main_memory;

  memory implementation main_memory.impl
  subcomponents
    part1mem : memory partition1_memory;
    part2mem : memory partition2_memory;

  end main_memory.impl;

  system arincsystem
  end arincsystem;

  system implementation arincsystem.impl
  subcomponents
    mem : memory main_memory.impl;
    cpu : processor powerpc.impl;
    partition1_pr : process partition1_process.impl;
    partition2_pr : process partition2_process.impl;

  connections
    samplingconnection : port partition1_pr.samplingout -> partition2_pr.samplingin;
    queueingconnection : port partition2_pr.queueingout -> partition1_pr.queueingin;

  properties
    Actual_Processor_Binding => (reference ( cpu.part1 ))
      applies to partition1_pr;
    Actual_Processor_Binding => (reference ( cpu.part2 ))
      applies to partition2_pr;
    Actual_Memory_Binding => (reference ( mem.part1mem ))
      applies to partition1_pr;
    Actual_Memory_Binding => (reference ( mem.part2mem ))
      applies to partition2_pr;

  end arincsystem.impl;

end PartitionedSystemExample;