test_real_exec_env_01.aadl 3.29 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
package Test_01
public

-----------------
-- Subprograms --
-----------------

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;

-------------
-- Threads --
-------------

thread Task
end Task;

thread implementation Task.impl_1
calls
   MyCalls : {
      P_Spg : subprogram Hello_Spg_1;
   };
properties
   Dispatch_Protocol                  => periodic;
   Period                             => 1000ms;
   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                             => 500ms;
   Compute_Execution_time             => 0 ms .. 3 ms;
   Deadline                           => 500 ms;
   Source_Stack_Size                  => 13952 Bytes;
end Task.impl_2;

---------------
-- Processor --
---------------

processor cpurm
end cpurm;

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

---------------
-- Processes --
---------------

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 {**

--  test extern subprogram calls in variable declaration

theorem test_env_subtheorem_call_no_parameter

foreach e in Processor_Set do

  var x := compute sub_theorem_1;

  check (x = 2.0);
end;

--  test literal parameter passing in sub-theorems

theorem test_env_subtheorem_call_one_parameter
foreach e in Processor_Set do
  var x := compute sub_theorem_2 (e, 2);
  check (x = 2.0);
end;

--  test multiple literal parameters passing in sub-theorems

theorem test_env_subtheorem_call_multiple_parameters
foreach e in Processor_Set do
  a_set := {p in Process_Set | Is_Bound_To (p, e)};
  var y := 3;
  var x := compute sub_theorem_3 (a_set, y, 1);
  check (x = 4.0);
end;

--  test domain passing in sub-theorems

theorem  test_env_subtheorem_call_with_domain
foreach e in Process_Set do
  a_set := {t in Thread_Set | (1 = 1)};
  var y := 1;
  var x := compute sub_theorem_4 (a_set, y);
115
  check (x = 1000000000.0);
116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160
end;

--  test global variable declaration and access

theorem test_env_subtheorem_call_global_variable
foreach e in Processor_Set do
  a_set := {p in Process_Set | Is_Bound_To (p, e)};
  global y := 1;
  var x := compute sub_theorem_5 (a_set);
  check (x = 1.0);
end;

--  test sub-theorems with empty domain

theorem  test_env_subtheorem_call_with_empty_domain
foreach e in Process_Set do

  a_set := {t in Thread_Set | (1 = 0)};

  var x := compute sub_theorem_6 (a_set);

  check (x = 0.0);
end test_env_subtheorem_call_with_empty_domain;


**};

end node_a.impl;

------------
-- System --
------------

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 Test_01;