test_real_parse_02.aadl.out 6.88 KB
Newer Older
jhugues's avatar
jhugues committed
1 2 3 4
test_real_parse_02.aadl:11:03: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list.
test_real_parse_02.aadl:11:03: Warning: The value of source_language has been converted into a list.
test_real_parse_02.aadl:17:03: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list.
test_real_parse_02.aadl:17:03: Warning: The value of source_language has been converted into a list.
5 6 7 8 9 10 11







jhugues's avatar
jhugues committed
12

13 14 15 16 17 18 19 20 21 22 23 24 25
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
hugues.jerome's avatar
hugues.jerome committed
26
    applies to (process, device);
27 28

  Channel_Address : aadlinteger
hugues.jerome's avatar
hugues.jerome committed
29
    applies to (process, device);
30 31 32 33 34 35

  Protocol_Type : type enumeration (iiop, diop);

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

36
  Allowed_Execution_Platform : type enumeration (Native, Native_Compcert, bench, LEON_RTEMS, LEON_RTEMS_POSIX, LEON3_SCOC3, LEON3_XTRATUM, LEON3_XM3, LEON_ORK, LEON_GNAT, LINUX32, LINUX32_XENOMAI_NATIVE, LINUX32_XENOMAI_POSIX, LINUX64, ERC32_ORK, ARM_DSLINUX, ARM_N770, GUMSTIX_RTEMS, NDS_RTEMS, X86_RTEMS, X86_RTEMS_POSIX, X86_LINUXTASTE, MARTE_OS, WIN32, VXWORKS);
37 38

  Execution_Platform : Deployment::Allowed_Execution_Platform
hugues.jerome's avatar
hugues.jerome committed
39
    applies to ( all);
40

jhugues's avatar
jhugues committed
41 42 43 44 45 46 47 48
  Supported_Execution_Platform : list of Deployment::Allowed_Execution_Platform
    applies to (device);

  Runtime : type enumeration (PolyORB_HI_C, PolyORB_HI_Ada, POK);

  Supported_Runtime : Deployment::Runtime
    applies to ( all);

49 50 51 52 53
  Priority_Type : type aadlinteger 0 .. 255;

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

hugues.jerome's avatar
hugues.jerome committed
54 55 56 57 58 59
  Driver_Name : aadlstring
    applies to (device);

  Configuration : aadlstring
    applies to (device);

60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75
  Config : aadlstring
    applies to (device);

  ASN1_Module_Name : aadlstring
    applies to ( all);

  Help : aadlstring
    applies to ( all);

  Version : aadlstring
    applies to ( all);

  Configuration_Type : classifier (
data)
    applies to ( all);

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 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 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319
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 {**

--  set_declaration_is_bound_to

theorem set_declaration_is_bound_to
foreach e in processor_set do

proc_set(e) := { x in process_set |
is_bound_to(x, e)};

check ((cardinal(Proc_Set) = 1));
end set_declaration_is_bound_to;


--  set_declaration_is_connected_to

theorem set_declaration_is_connected_to
foreach e in process_set do

cnx_set := { x in process_set |
is_connected_to(x, e)};

check ((cardinal(Cnx_Set) >= 1));
end set_declaration_is_connected_to;


--  set_declaration_is_subcomponent_of

theorem set_declaration_is_subcomponent_of
foreach e in process_set do

threads := { x in thread_set |
is_connected_to(x, e)};

check ((cardinal(threads) >= 1));
end set_declaration_is_subcomponent_of;


--  set_declaration_is_accessed_by

theorem set_declaration_is_accessed_by
foreach e in data_set do

accessors := { t in thread_set |
is_accessed_by(e, t)};

check ((cardinal(accessors) >= 0));
end set_declaration_is_accessed_by;


--  set_declaration_is_accessing_to

theorem set_declaration_is_accessing_to
foreach e in data_set do

accessors := { t in thread_set |
is_accessing_to(t, e)};

check ((cardinal(accessors) >= 0));
end set_declaration_is_accessing_to;


--  set_declaration_is_called_by

theorem set_declaration_is_called_by
foreach e in subprogram_set do

callers(e) := { t in thread_set |
is_called_by(e, t)};

check ((cardinal(Callers) >= 0));
end set_declaration_is_called_by;


--  set_declaration_is_connecting_to

theorem set_declaration_is_connecting_to
foreach e in thread_set do

cnx_threads(e) := { t in thread_set |
is_connecting_to(e, t)};

check ((cardinal(Cnx_threads) >= 0));
end set_declaration_is_connecting_to;


--  set_declaration_compare_property_value

theorem set_declaration_compare_property_value
foreach e in processor_set do

pure_subprograms := { p in subprogram_set |
(property_exists(p, "source_language") and
(get_property_value(p, "source_language") = "ada95"))};

check ((cardinal(Pure_Subprograms) > 0));
end set_declaration_compare_property_value;


--  set_declaration_set_composition

theorem set_declaration_set_composition
foreach e in processor_set do

proc_set(e) := { x in process_set |
is_bound_to(x, e)};
new_set := { x in data_set |
is_subcomponent_of(x, Proc_Set)};

check ((cardinal(New_Set) >= 0));
end set_declaration_set_composition;


--  set_declaration_and_operator

theorem set_declaration_and_operator
foreach e in process_set do

protected_data := { x in data_set |
(is_subcomponent_of(x, e) and
(property_exists(x, "concurrency_control_protocol") and
(get_property_value(x, "concurrency_control_protocol") = "protected_access")))};

check ((cardinal(Protected_Data) >= 0));
end set_declaration_and_operator;


--  set_declaration_or_operator

theorem set_declaration_or_operator
foreach e in thread_set do

a_set := { x in data_set |
(is_subcomponent_of(x, e) or
is_accessed_by(x, e))};

check ((cardinal(a_set) >= 0));
end set_declaration_or_operator;


--  set_declaration_predefined_sets

theorem set_declaration_predefined_sets
foreach e in processor_set do

var x := 
return (cardinal(thread_set));

check ((x = 2));
end set_declaration_predefined_sets;


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