test_real_exec_02.aadl.out 9.68 KB
Newer Older
1
2
3
test_real_exec_02.aadl:81:04: warning: obj references a component type
ocarina: Total: 0 error and 1 warning
set_declaration_is_bound_to execution
4
5
6
7
-------------------------------------
Evaluating theorem set_declaration_is_bound_to

 * Iterate for variable: rma.erc32_cpu_rm
8
9
Content of set proc_set (test_real_exec_02.aadl:148:19) is 
  rma.erc32_node_a: 13 component instance test_real_exec_02.aadl:130:01
10
11
 => Result: TRUE

12
13
theorem set_declaration_is_bound_to is: TRUE

14

15
set_declaration_is_connected_to execution
16
17
18
19
-------------------------------------
Evaluating theorem set_declaration_is_connected_to

 * Iterate for variable: rma.erc32_node_a_task_1
20
Content of set cnx_set (test_real_exec_02.aadl:160:14) is 
21
22
23
 => Result: TRUE

 * Iterate for variable: rma.erc32_node_a_task_2
24
25
Content of set cnx_set (test_real_exec_02.aadl:160:14) is 
  rma.erc32_node_a_task_1: 20 component instance test_real_exec_02.aadl:44:01
26
27
28
 => Result: TRUE

 * Iterate for variable: rma.erc32_node_a_task_12
29
Content of set cnx_set (test_real_exec_02.aadl:160:14) is 
30
31
32
 => Result: TRUE

 * Iterate for variable: rma.erc32_node_a_task_22
33
34
Content of set cnx_set (test_real_exec_02.aadl:160:14) is 
  rma.erc32_node_a_task_12: 142 component instance test_real_exec_02.aadl:59:01
35
36
 => Result: TRUE

37
38
theorem set_declaration_is_connected_to is: TRUE

39

40
set_declaration_is_subcomponent_of execution
41
42
43
44
-------------------------------------
Evaluating theorem set_declaration_is_subcomponent_of

 * Iterate for variable: rma.erc32_node_a
45
46
47
48
49
Content of set threads (test_real_exec_02.aadl:172:14) is 
  rma.erc32_node_a_task_1: 20 component instance test_real_exec_02.aadl:44:01
  rma.erc32_node_a_task_2: 80 component instance test_real_exec_02.aadl:79:01
  rma.erc32_node_a_task_12: 142 component instance test_real_exec_02.aadl:59:01
  rma.erc32_node_a_task_22: 194 component instance test_real_exec_02.aadl:96:01
50
51
 => Result: TRUE

52
53
theorem set_declaration_is_subcomponent_of is: TRUE

54

55
set_declaration_is_accessed_by execution
56
57
58
59
-------------------------------------
Evaluating theorem set_declaration_is_accessed_by

 * Iterate for variable: rma.erc32_node_a_task_2_obj
60
Content of set accessors (test_real_exec_02.aadl:184:16) is 
61
62
 => Result: TRUE

63
64
theorem set_declaration_is_accessed_by is: TRUE

65

66
set_declaration_is_accessing_to execution
67
68
69
70
-------------------------------------
Evaluating theorem set_declaration_is_accessing_to

 * Iterate for variable: rma.erc32_node_a_task_2_obj
71
Content of set accessors (test_real_exec_02.aadl:196:16) is 
72
73
 => Result: TRUE

74
75
theorem set_declaration_is_accessing_to is: TRUE

76

77
set_declaration_is_called_by_1 execution
78
79
80
81
-------------------------------------
Evaluating theorem set_declaration_is_called_by_1

 * Iterate for variable: rma.erc32_node_a_task_1_mycalls_p_spg
82
83
Content of set callers (test_real_exec_02.aadl:211:19) is 
  rma.erc32_node_a_task_1: 20 component instance test_real_exec_02.aadl:44:01
84
85
86
 => Result: TRUE

 * Iterate for variable: rma.erc32_node_a_task_2_mycall_p_spg
87
88
Content of set callers (test_real_exec_02.aadl:211:19) is 
  rma.erc32_node_a_task_2: 80 component instance test_real_exec_02.aadl:79:01
89
90
91
 => Result: TRUE

 * Iterate for variable: rma.erc32_node_a_task_12_mycalls_p_spg
92
93
Content of set callers (test_real_exec_02.aadl:211:19) is 
  rma.erc32_node_a_task_12: 142 component instance test_real_exec_02.aadl:59:01
94
95
96
 => Result: TRUE

 * Iterate for variable: rma.erc32_node_a_task_22_mycall_p_spg
97
98
Content of set callers (test_real_exec_02.aadl:211:19) is 
  rma.erc32_node_a_task_22: 194 component instance test_real_exec_02.aadl:96:01
99
100
 => Result: TRUE

101
102
theorem set_declaration_is_called_by_1 is: TRUE

103

104
set_declaration_is_called_by_2 execution
105
106
107
108
-------------------------------------
Evaluating theorem set_declaration_is_called_by_2

 * Iterate for variable: test2_real_hello_spg_1
109
110
111
Content of set callers (test_real_exec_02.aadl:226:19) is 
  rma.erc32_node_a_task_1: 20 component instance test_real_exec_02.aadl:44:01
  rma.erc32_node_a_task_12: 142 component instance test_real_exec_02.aadl:59:01
112
113
114
 => Result: TRUE

 * Iterate for variable: test2_real_hello_spg_2
115
116
117
Content of set callers (test_real_exec_02.aadl:226:19) is 
  rma.erc32_node_a_task_2: 80 component instance test_real_exec_02.aadl:79:01
  rma.erc32_node_a_task_22: 194 component instance test_real_exec_02.aadl:96:01
118
119
 => Result: TRUE

120
121
theorem set_declaration_is_called_by_2 is: TRUE

122

123
set_declaration_is_connecting_to execution
124
125
126
127
-------------------------------------
Evaluating theorem set_declaration_is_connecting_to

 * Iterate for variable: rma.erc32_node_a_task_1
128
Content of set cnx_threads (test_real_exec_02.aadl:239:22) is 
129
130
131
 => Result: TRUE

 * Iterate for variable: rma.erc32_node_a_task_2
132
133
Content of set cnx_threads (test_real_exec_02.aadl:239:22) is 
  rma.erc32_node_a_task_1: 20 component instance test_real_exec_02.aadl:44:01
134
135
136
 => Result: TRUE

 * Iterate for variable: rma.erc32_node_a_task_12
137
Content of set cnx_threads (test_real_exec_02.aadl:239:22) is 
138
139
140
 => Result: TRUE

 * Iterate for variable: rma.erc32_node_a_task_22
141
142
Content of set cnx_threads (test_real_exec_02.aadl:239:22) is 
  rma.erc32_node_a_task_12: 142 component instance test_real_exec_02.aadl:59:01
143
144
 => Result: TRUE

145
146
theorem set_declaration_is_connecting_to is: TRUE

147

148
set_declaration_is_passing_through execution
149
150
151
152
-------------------------------------
Evaluating theorem set_declaration_is_passing_through

 * Iterate for variable: rma.erc32_node_a_task_1
153
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is 
154
anonymous end to end flow :3964 end to end flow spec 
155
156
157
 => Result: TRUE

 * Iterate for variable: rma.erc32_node_a_task_2
158
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is 
159
anonymous end to end flow :3964 end to end flow spec 
160
161
162
 => Result: TRUE

 * Iterate for variable: rma.erc32_node_a_task_12
jhugues's avatar
jhugues committed
163
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is 
164
anonymous end to end flow :3965 end to end flow spec 
165
166
167
 => Result: TRUE

 * Iterate for variable: rma.erc32_node_a_task_22
jhugues's avatar
jhugues committed
168
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is 
169
anonymous end to end flow :3965 end to end flow spec 
170
171
 => Result: TRUE

172
173
theorem set_declaration_is_passing_through is: TRUE

174

175
set_declaration_is_predecessor_of execution
176
177
178
179
-------------------------------------
Evaluating theorem set_declaration_is_predecessor_of

 * Iterate for variable: rma.erc32_node_a_task_1
180
181
182
Content of set pred (test_real_exec_02.aadl:264:13) is 
Content of set inv_pred (test_real_exec_02.aadl:266:17) is 
  rma.erc32_node_a_task_2: 80 component instance test_real_exec_02.aadl:79:01
183
184
185
 => Result: TRUE

 * Iterate for variable: rma.erc32_node_a_task_2
186
187
188
Content of set pred (test_real_exec_02.aadl:264:13) is 
  rma.erc32_node_a_task_1: 20 component instance test_real_exec_02.aadl:44:01
Content of set inv_pred (test_real_exec_02.aadl:266:17) is 
189
190
191
 => Result: TRUE

 * Iterate for variable: rma.erc32_node_a_task_12
192
193
194
Content of set pred (test_real_exec_02.aadl:264:13) is 
Content of set inv_pred (test_real_exec_02.aadl:266:17) is 
  rma.erc32_node_a_task_22: 194 component instance test_real_exec_02.aadl:96:01
195
196
197
 => Result: TRUE

 * Iterate for variable: rma.erc32_node_a_task_22
198
199
200
Content of set pred (test_real_exec_02.aadl:264:13) is 
  rma.erc32_node_a_task_12: 142 component instance test_real_exec_02.aadl:59:01
Content of set inv_pred (test_real_exec_02.aadl:266:17) is 
201
202
 => Result: TRUE

203
204
theorem set_declaration_is_predecessor_of is: TRUE

205

206
set_declaration_compare_property_value execution
207
208
209
210
-------------------------------------
Evaluating theorem set_declaration_compare_property_value

 * Iterate for variable: rma.erc32_cpu_rm
211
212
213
Content of set pure_subprograms (test_real_exec_02.aadl:280:24) is 
  test2_real_hello_spg_1: 41 component instance test_real_exec_02.aadl:19:01
  test2_real_hello_spg_2: 103 component instance test_real_exec_02.aadl:27:01
214
215
 => Result: TRUE

216
217
theorem set_declaration_compare_property_value is: TRUE

218

219
set_declaration_set_composition execution
220
221
222
223
-------------------------------------
Evaluating theorem set_declaration_set_composition

 * Iterate for variable: rma.erc32_cpu_rm
224
225
226
227
228
229
230
Content of set proc_set (test_real_exec_02.aadl:295:19) is 
  rma.erc32_node_a: 13 component instance test_real_exec_02.aadl:130:01
Content of set new_set (test_real_exec_02.aadl:297:15) is 
  rma.erc32_node_a_task_1: 20 component instance test_real_exec_02.aadl:44:01
  rma.erc32_node_a_task_2: 80 component instance test_real_exec_02.aadl:79:01
  rma.erc32_node_a_task_12: 142 component instance test_real_exec_02.aadl:59:01
  rma.erc32_node_a_task_22: 194 component instance test_real_exec_02.aadl:96:01
231
232
 => Result: TRUE

233
234
theorem set_declaration_set_composition is: TRUE

235

236
set_declaration_and_operator execution
237
238
239
240
-------------------------------------
Evaluating theorem set_declaration_and_operator

 * Iterate for variable: rma.erc32_node_a
241
242
Content of set protected_data (test_real_exec_02.aadl:309:21) is 
  rma.erc32_node_a_task_2_obj: 92 component instance test_real_exec_02.aadl:10:01
243
244
 => Result: TRUE

245
246
theorem set_declaration_and_operator is: TRUE

247

248
set_declaration_or_operator execution
249
250
251
252
-------------------------------------
Evaluating theorem set_declaration_or_operator

 * Iterate for variable: rma.erc32_node_a
253
254
255
256
257
Content of set a_set (test_real_exec_02.aadl:325:14) is 
  rma.erc32_node_a_task_1: 20 component instance test_real_exec_02.aadl:44:01
  rma.erc32_node_a_task_2: 80 component instance test_real_exec_02.aadl:79:01
  rma.erc32_node_a_task_12: 142 component instance test_real_exec_02.aadl:59:01
  rma.erc32_node_a_task_22: 194 component instance test_real_exec_02.aadl:96:01
258
259
 => Result: TRUE

260
261
theorem set_declaration_or_operator is: TRUE

262

263
set_declaration_predefined_sets execution
264
265
266
267
-------------------------------------
Evaluating theorem set_declaration_predefined_sets

 * Iterate for variable: rma.erc32_cpu_rm
hugues.jerome's avatar
hugues.jerome committed
268
     -> value for x is 4
269
270
 => Result: TRUE

271
272
theorem set_declaration_predefined_sets is: TRUE

273