property set Deployment is
  Allowed_Transport_APIs : type enumeration (BSD_Sockets, SpaceWire);

  Transport_API : Deployment::Allowed_Transport_APIs
    applies to (bus);

  Location : aadlstring
    applies to (processor, device);

  Port_Number : aadlinteger
    applies to (process, device);

  Process_ID : aadlinteger
    applies to (process, device);

  Channel_Address : aadlinteger
    applies to (process, device);

  Protocol_Type : type enumeration (iiop, diop);

  Protocol : Deployment::Protocol_Type
    applies to (system);

  Allowed_Execution_Platform : type enumeration (Native, Native_Compcert, LEON_RTEMS, LEON_ORK, LEON_GNAT, LINUX32, LINUX64, ERC32_ORK, ARM_DSLINUX, ARM_N770, X86_RTEMS, X86_LINUXTASTE, MARTE_OS, VXWORKS);

  Execution_Platform : Deployment::Allowed_Execution_Platform
    applies to (processor);

  Priority_Type : type aadlinteger 0 .. 255;

  Priority : Deployment::Priority_Type
    applies to (data, thread);

  Driver_Name : aadlstring
    applies to (device);

  Configuration : aadlstring
    applies to (device);

end Deployment;

package RMAAadl
public
  with Deployment;

  subprogram Hello_Spg_1
  properties
    source_language => Ada95;
    source_name => "Hello.Hello_Spg_1";

  end Hello_Spg_1;

  subprogram Hello_Spg_2
  properties
    source_language => Ada95;
    source_name => "Hello.Hello_Spg_2";

  end Hello_Spg_2;

  thread Task
  end Task;

  thread implementation Task.impl_1
  calls
    MyCalls :
    {P_Spg : subprogram Hello_Spg_1;}
;

  properties
    Dispatch_Protocol => periodic;
    Period => 1000 ms;
    Compute_Execution_time => 0 ms .. 3 ms;
    Deadline => 1000 ms;
    Source_Stack_Size => 13952 Bytes;

  end Task.impl_1;

  thread implementation Task.impl_2
  calls
    MyCall :
    {P_Spg : subprogram Hello_Spg_2;}
;

  properties
    Dispatch_Protocol => periodic;
    Period => 500 ms;
    Compute_Execution_time => 0 ms .. 3 ms;
    Deadline => 500 ms;
    Source_Stack_Size => 13952 Bytes;

  end Task.impl_2;

  processor cpurm
  properties
    Deployment::Execution_Platform => ERC32_ORK;

  end cpurm;

  processor implementation cpurm.impl
  properties
    Scheduling_Protocol => (Posix_1003_Highest_Priority_First_Protocol);

  end cpurm.impl;

  process node_a
  end node_a;

  process implementation node_a.impl
  subcomponents
    Task1 : thread Task.impl_1;
    Task2 : thread Task.impl_2;

    annex real_specification {**

--  variables_basis

theorem variables_basis
foreach e in processor_set do

var bla := 
return (2);

check ((bla = 2));
end variables_basis;


--  variables_with_expression

theorem variables_with_expression
foreach e in processor_set do

var bla := 
return ((2 + 1));

check ((bla = 3));
end variables_with_expression;


--  variables_dependant

theorem variables_dependant
foreach e in processor_set do

var x1 := 
return (1);
var x2 := 
return ((2 + x1));

check ((x2 = 3));
end variables_dependant;


--  variables_set_dependants

theorem variables_set_dependants
foreach e in processor_set do

a_set := { x in process_set |
is_bound_to(x, e)};
var x2 := 
return ((2 + cardinal(a_set)));

check ((x2 = 3));
end variables_set_dependants;


--  variables_iterative_expressions

theorem variables_iterative_expressions
foreach e in processor_set do

proc_set(e) := { x in process_set |
is_bound_to(x, e)};
threads := { x in thread_set |
is_subcomponent_of(x, Proc_Set)};
var y := 
return (max(expr(Threads, t, (2 * first(get_property_value(t, "compute_execution_time"))))));

check ((y = 3.0));
end variables_iterative_expressions;


--  variables_imbricated_iterative_expressions

theorem variables_imbricated_iterative_expressions
foreach e in processor_set do

proc_set(e) := { x in process_set |
is_bound_to(x, e)};
threads := { x in thread_set |
is_subcomponent_of(x, Proc_Set)};
var y := 
return (max(expr(Threads, t, ((2 * max(expr(proc_set, p, last(get_property_value(p, "load_time"))))) + last(get_property_value(t, "compute_execution_time"))))));

check (((y = 6.0) or
(y = 8.0)));
end variables_imbricated_iterative_expressions;


    **};
  end node_a.impl;

  system rma
  end rma;

  system implementation rma.ERC32
  subcomponents
    node_a : process node_a.impl;
    cpu_rm : processor cpurm.impl;

  properties
    Actual_Processor_Binding => (reference ( cpu_rm ))
      applies to node_a;

  end rma.ERC32;

end RMAAadl;