test_real_exec_01.aadl 2.37 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 115 116 117 118 119 120 121 122
package Test1_REAL
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 {**

--  Tests power, equal, plus, minus, multipliate, divide, 
--  and greater or equals operators on integers

theorem integer_and_binaries_operators

  foreach e in Processor_Set do

  check ((((2**2) = 4) and
         ((2 + 4) =  (2 * 3)))
         or ((2 - 1) >= (4/2)));

end integer_and_binaries_operators;

--  Tests the modulo operator on integers

theorem modulo_operator

  foreach e in Processor_Set do

  check (((10 mod 5) = 0) and
         ((10 mod 4) = 2) and
         ((2 mod 5) = 2));

end modulo_operator;

**};
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 Test1_REAL;