test_real_exec_02.aadl.out 6.3 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
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
6
7
8
theorem set_declaration_is_bound_to is: TRUE

set_declaration_is_connected_to execution
9
10
11
12
13
14
Content of set cnx_set (test_real_exec_02.aadl:160:14) is 
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
Content of set cnx_set (test_real_exec_02.aadl:160:14) is 
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
15
16
17
theorem set_declaration_is_connected_to is: TRUE

set_declaration_is_subcomponent_of execution
18
19
20
21
22
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
23
24
25
theorem set_declaration_is_subcomponent_of is: TRUE

set_declaration_is_accessed_by execution
26
Content of set accessors (test_real_exec_02.aadl:184:16) is 
27
28
29
theorem set_declaration_is_accessed_by is: TRUE

set_declaration_is_accessing_to execution
30
Content of set accessors (test_real_exec_02.aadl:196:16) is 
31
32
33
theorem set_declaration_is_accessing_to is: TRUE

set_declaration_is_called_by_1 execution
34
35
36
37
38
39
40
41
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
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
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
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
42
43
44
theorem set_declaration_is_called_by_1 is: TRUE

set_declaration_is_called_by_2 execution
45
46
47
48
49
50
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
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
51
52
53
theorem set_declaration_is_called_by_2 is: TRUE

set_declaration_is_connecting_to execution
54
55
56
57
58
59
Content of set cnx_threads (test_real_exec_02.aadl:239:22) is 
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
Content of set cnx_threads (test_real_exec_02.aadl:239:22) is 
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
60
61
62
theorem set_declaration_is_connecting_to is: TRUE

set_declaration_is_passing_through execution
63
64
65
66
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is 
anonymous end to end flow :3449 end to end flow spec 
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is 
anonymous end to end flow :3449 end to end flow spec 
jhugues's avatar
jhugues committed
67
68
69
70
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is 
anonymous end to end flow :3450 end to end flow spec 
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is 
anonymous end to end flow :3450 end to end flow spec 
71
72
73
theorem set_declaration_is_passing_through is: TRUE

set_declaration_is_predecessor_of execution
74
75
76
77
78
79
80
81
82
83
84
85
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
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 
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
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 
86
87
88
theorem set_declaration_is_predecessor_of is: TRUE

set_declaration_compare_property_value execution
89
90
91
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
92
93
94
theorem set_declaration_compare_property_value is: TRUE

set_declaration_set_composition execution
95
96
97
98
99
100
101
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
102
103
104
theorem set_declaration_set_composition is: TRUE

set_declaration_and_operator execution
105
106
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
107
108
109
theorem set_declaration_and_operator is: TRUE

set_declaration_or_operator execution
110
111
112
113
114
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
115
116
117
theorem set_declaration_or_operator is: TRUE

set_declaration_predefined_sets execution
hugues.jerome's avatar
hugues.jerome committed
118
     -> value for x is 4
119
120
theorem set_declaration_predefined_sets is: TRUE