Wrong validation of end to end flow across data access

[AaronGreenhouse]

The example from Issue #643 has 2 errors on the declarative model that seem overly strict and should probably be removed. We need check what exactly are the rules in the spec and what exactly the verifier thinks it is verifying.

package issue643
public
    system top

    end top;

    system implementation top.i
        subcomponents
            p: system S;
            c: system S;
            d: data;
        connections
            c0: data access p.a <-> d;
            c1: data access d <-> c.a;
        flows
            e2e: end to end flow p -> c0 -> d -> c1 -> c;
    end top.i;

    system S
        features
            a: requires data access;
    end S;

end issue643;

On c0 in the flow spec we have the error

The destination of connection 'c0' does not match the succeeding subcomponent or in flow spec feature 'd'

On c1 in the flow spec we have the error

The source of connection 'c1' does not match the preceding subcomponent or out flow spec feature 'd'

[AaronGreenhouse]

There are even MORE errors if you switch around the end points of the bidirectional connections, see top.i2, which has 7 errors, compared to the 4 errors of top.i.

package issue643
public
    system top

    end top;

    system implementation top.i
        subcomponents
            p: system S;
            c: system S;
            d: data;
        connections
            c0: data access p.a <-> d;
            c1: data access d <-> c.a;
        flows
            e2e_1: end to end flow p -> c0 -> d -> c1 -> c;
            
            e2e_2: end to end flow p.start -> c0 -> d -> c1 -> c.finish;
    end top.i;

    system implementation top.i2
        subcomponents
            p: system S;
            c: system S;
            d: data;
        connections
            c0: data access d <-> p.a;
            c1: data access c.a <-> d;
        flows
            e2e_1: end to end flow p -> c0 -> d -> c1 -> c;
            
            e2e_2: end to end flow p.start -> c0 -> d -> c1 -> c.finish;
    end top.i2;


    system S
        features
            a: requires data access;
    	flows
    		start: flow source a;
    		finish: flow sink a;
    end S;
end issue643;

[AaronGreenhouse]

I think this has to do with an interaction between bidirectional connections and the flow path checking.

I should create an example that uses regular ports instead of access connections and see how it behaves.

[AaronGreenhouse]

Definitely a problem with the bidirectional connections. I made an example that uses ports instead of data access, and it is easier to understand the problem there:

package ports
public
    system top

    end top;

    system implementation top.i
        subcomponents
            p: system S;
            c: system S;
            m: system S;
        connections
            c0: port p.x <-> m.x;
            c1: port m.x <-> c.x;
        flows
            e2e_1a: end to end flow p -> c0 -> m -> c1 -> c;            
            e2e_1b: end to end flow p.start -> c0 -> m.through -> c1 -> c.finish;
            
            e2e_2a: end to end flow c -> c1 -> m -> c0 -> p;
            e2e_3b: end to end flow c.start -> c1 -> m.through -> c0 -> p.finish;
    end top.i;

    system implementation top.i2
        subcomponents
            p: system S;
            c: system S;
            m: system S;
        connections
            c0: port m.x <-> p.x;
            c1: port c.x <-> m.x;
        flows
            e2e_1a: end to end flow p -> c0 -> m -> c1 -> c;            
            e2e_1b: end to end flow p.start -> c0 -> m.through -> c1 -> c.finish;
            
            e2e_2a: end to end flow c -> c1 -> m -> c0 -> p;
            e2e_3b: end to end flow c.start -> c1 -> m.through -> c0 -> p.finish;
    end top.i2;


    system S
    	features
    		x: in out event port;
    	flows
    		start: flow source x;
    		finish: flow sink x;
    		through: flow path x -> x;
    end S;
end ports;

It definitely seems like the checking on the flow elements is only considering the literal connection source and destination elements and ignoring the bidirectionally of the connection. You can see this by the fact that in top.i the errors on the connections in the second group of flows, and in top.i2 the errors are on the connections in the first group of flows. In both cases the errors are on the flows that go opposite the the direction in which the connections are declared.

[AaronGreenhouse]

Error messages come from Aadl2JavaValidator.checkFlowConnectionEnds(). I do see checks in that method for whether the connection is bidirectional.

[AaronGreenhouse]

Being looking through Aadl2JavaValidator.checkFlowConnectionEnds() and I see several problems:

• when checking the connection and the previous flow element is a flow specification, the method isMatchingConnectionPoint() is used. Even when the direction of the connection wrong, this method returns true which prevents the method from moving to the case where it checks if the connection is bidirectional and then reverses direction.
• when checking the connection and the previous flow element is a plain subcomponent, the method seems to correctly get to point where it checks if the connection is bidirectional, but then it does the wrong thing: it gets the source of the connection again instead of getting the destination.
• checking of the endpoint of the connection doesn't seem to be complete. It never checks if the connection is bidirectional at all, and possibly overlooks some other things.

[AaronGreenhouse]

Fixed the second bullet, above.

Looking at isMatchingConnectionPoint(). Seems that in this case it is not comparing the context of the connection against the context of the flow because FlowEnd.getContext() is null. Need to figure out more about what this really means and should be. It's not right that the contexts are not being compared. In this case, they are declared to "match" because the feature is the same, even though the subcomponents involved are not the same.

[AaronGreenhouse]

Also, need to create separate test where I use connections that really only do match on one endpoint.

[AaronGreenhouse]

The problem is not isMatchingConnectionPoint(). The problem is that when it detects that the features match, but the contexts do not match, it doesn't try to flip the connection around. If it detects that the features do not match, it does try to flip the connection around.

[AaronGreenhouse]

Did a substantial rewrite of checkFlowConnectionEnds(). It seems to fix the problems with port connections, but doesn't work with access connections yet, not sure why.

Going to

1. fix this
2. set up unit tests
3. refactor the guts of the method further so that it is easier to understand and maintain. (lots of duplicate code right now)

[AaronGreenhouse]

Data access connections do not work because the connection references the data subcomponent as the "connection end" not the "context". We need a special case to check for this.

I was worried that I need to test endpoints of the form "sub.fg.f", but this is not the case because end to end flows deal with components that are all siblings, so we cannot reach into the feature group in the connections.