OpenAADL / ocarina

AADL model processor: mappings to code (C, Ada); Petri Nets; scheduling tools (MAST, Cheddar); WCET; REAL
http://www.openaadl.org
Other
65 stars 29 forks source link

REAL "Connection Instances" do not represent semantic connections? #3

Closed philip-alldredge closed 9 years ago

philip-alldredge commented 11 years ago

It appears that REAL's connection instances do not represent semantic connections or Ocarina is instantiating models differently than I expect.

In the below model, I expected the constraint to fail with six connection instances(1 for each ultimate destination/source pair). According to the output there are only 2 connection instances.

Thoughts?

test_case.aadl

package Test
public

bus TestBus
end TestBus;

bus implementation TestBus.Impl
end TestBus.Impl;

system C
features
    ba1 : requires bus access TestBus.Impl;
end C;

system implementation C.Impl
subcomponents
    c1 : system C.Impl2;
    c2 : system C.Impl2;
    c3 : system C.Impl2;

connections
    con1_1 : bus access ba1 -> c1.ba1;
    con1_2 : bus access ba1 -> c2.ba1;
    con1_3 : bus access ba1 -> c3.ba1;
end C.Impl;

system implementation C.Impl2
end C.Impl2;

system A
end A;

system implementation A.impl
subcomponents
    b1 : bus TestBus.Impl;
    c1 : system C.Impl;
    c2 : system C.Impl;

connections
    con1_1 : bus access b1 -> c1.ba1;
    con1_2 : bus access b1 -> c2.ba1;

annex real_specification {**
    theorem constraints
    foreach b in Bus_Set do
        connections := {c in Connection_Set | Is_Accessed_By (b, c)};
        check(size(list(connections)) <= 2);
    end;
**};
end A.impl;

end Test;

Output:

 * Iterate for variable: a.impl_b1
Content of set connections (test-case.aadl:47:18) is 
  a.impl_con1_1: 172 connection instance test-case.aadl:41:02
  a.impl_con1_2: 183 connection instance test-case.aadl:42:02
 => Result: TRUE
yoogx commented 11 years ago

Actually, connections are there Content of set connections_2 (test.aadl:48:26) is a.impl_con1_1: 172 connection instance test.aadl:41:05 a.impl_con1_2: 183 connection instance test.aadl:42:05 a.impl_c1_con1_1: 63 connection instance test.aadl:22:05 a.impl_c1_con1_2: 74 connection instance test.aadl:23:05 a.impl_c1_con1_3: 85 connection instance test.aadl:24:05 a.impl_c2_con1_1: 138 connection instance test.aadl:22:05 a.impl_c2_con1_2: 149 connection instance test.aadl:23:05 a.impl_c2_con1_3: 160 connection instance test.aadl:24:05

But the way Ocarina instances connections is by keeping hierarchy, hence source and destination are the one of the enclosing component. In your case, there are two direct connections to the bus (to respect the provides/requires bus access), and each connection is actually an alias to three connections internal to the system implementation (requires/actual).

hence an interesting question, part of the discussion we should have about standardizing this language: shall we keep this level of indirection, or shall we have resolution, so that instead of 2 + 2 x 3 = 8 connections, we keep only the 6 actual connections you expect.

I guess we need at least an accessor so that you can resolve the connections served by the provided access when you do this con1_2 : bus access b1 -> c2.ba1;

i.e. an accessor to resolve entities connected to ba1

philip-alldredge commented 11 years ago

Interesting. I believe this is something that should be standardized so it can be treated consistently between tools. My interpretation of the standard: 9(2) leads me to believe that the intent is to have connection instances only represent the entire semantic connection and point between leaf nodes. However, I'll leave that discussion for you and the other language gurus.

yoogx commented 11 years ago

Indeed. I just asked Peter, he was next to me. There should be 6 connexions at the instance level, from the 8 defined in the declarative model.

yoogx commented 9 years ago

Closing, this question will be handled in the Constraint sublanguage we defined as part of AS2-C