EMV2 checking of typesets in propagations and error conditions is incomplete.

Summary The checking of typesets on outgoing propagation conditions vs. the declared out propagations is not correct. It misses cases.

I'm looking at the rule (C12) in E.10 on page 112 of the latest draft:

(C12) For each outgoing propagation in a component there must be at least one outgoing propagation condition. All error types in the outgoing propagation type set must be contained in at least one outgoing propagation condition target type set.

I also think this rule is backwards: It should be that the typeset of the OPC is contained in the typeset of the declared out propagation.

There is the same sort of the problem when checking the typesets of error_condition_trigger expressions as well. The relevant rule here is This bug comes into play in the checking of in propagations in error_condition_trigger expressions as well. The relevant rule is (L25) on page 101:

The optional error_type_set of a transition condition element must be contained in the error_type_set declared for the referenced error event or incoming error propagation.

Expected behavior Any OPC whose typeset is not contained in the typeset of the relevant out propagation should be marked with an error.

Any error_condition_trigger expression whose typeset is not contained in the typeset of the relevant propagation declaration should be marked with an error.

Actual behavior I believe the current implementation is trying to check the above (OPC contained in the declared), but there are problems handling the subtype relationships. The same problems are observed when checking error conditions.

Steps To Reproduce

Open the example packages below in OSATE. For package q,

p1 should have an error, but does not
p2 and p3 should not have errors, and do not
p4 should have an error and does

For package OPC_Test,

For detections d11–d16 the errors are correct: d13 and d15 are not erroneous.
For detections d1–d6 the errors are not correct: d1 should have an error but does not.

package q
public
    annex EMV2 {**
        error types
            A: type;
            B: type extends A;
            C: type extends B;
            X: type;
        end types;

        error behavior Simple
        events
            E1: error event;
            E2: error event;
            E3: error event;
            E4: error event;
        states
            A: initial state;
        end behavior;
    **};

    system s
        features
            o1: out data port;
            o2: out data port;
            o3: out data port;
            o4: out data port;
        annex EMV2 {**
            use behavior q::Simple;

            error propagations
                o1: out propagation{q::B};
                o2: out propagation{q::B};
                o3: out propagation{q::B};
                o4: out propagation{q::B};
            end propagations;

            component error behavior
            propagations
                p1: A -[E1]-> o1{ q::A }; -- Should be an error, but is not flagged
                p2: A -[E2]-> o2{ q::B }; -- No error, should not be flagged
                p3: A -[E3]-> o3{ q::C }; -- No error, should not be flagged
                p4: A -[E4]-> o4{ q::X }; -- Error, is correctly flagged already
            end component;
        **};
    end s;

    system t
        features
            i1: in data port;
            i2: in data port;
            i3: in data port;
            i4: in data port;
        annex EMV2 {**
            use behavior q::Simple;

            error propagations
                i1: in propagation{q::B};
                i2: in propagation{q::B};
                i3: in propagation{q::B};
                i4: in propagation{q::B};
            end propagations;
        **};        
    end t;

    system x
    end x;

    system implementation x.i
        subcomponents
            s1: system s;
            s2: system t;
        connections
            c1: port s1.o2 -> s2.i1;
            c2: port s1.o2 -> s2.i2;
            c3: port s1.o2 -> s2.i3;
            c4: port s1.o2 -> s2.i4;
    end x.i;
end q;

package OPC_Test
public
    annex EMV2 {**
        error types
            R: type;
            A: type extends R;
            B: type extends A;
            C: type extends A;
            D: type extends A;
            X: type;
        end types;

        error behavior Simple
        events
            E1: error event;
            E2: error event;
            E3: error event;
            E4: error event;
        states
            S1: initial state;
        end behavior;
    **};

    system X2 
        features 
            input1: in data port;
            input2: in data port;
            error_flag: out event data port;
        annex EMV2 {**
            use behavior OPC_Test::Simple;

            error propagations
                input1: in propagation{OPC_Test::A};
                input2: in propagation{OPC_Test::B, OPC_Test::D};
            end propagations;

            component error behavior
            detections
                d1: S1 -[input1{OPC_Test::R}]-> error_flag!(1); -- Should have error, but doesn't
                d2: S1 -[input1{OPC_Test::A}]-> error_flag!(2); -- Okay, no error reported
                d3: S1 -[input1{OPC_Test::B}]-> error_flag!(3); -- Okay, no error reported
                d4: S1 -[input1{OPC_Test::C}]-> error_flag!(4); -- Okay, no error reported
                d5: S1 -[input1{OPC_Test::D}]-> error_flag!(5); -- Okay, no error reported
                d6: S1 -[input1{OPC_Test::X}]-> error_flag!(6); -- Erroneous and error is reported

                d11: S1 -[input2{OPC_Test::R}]-> error_flag!(11); -- Erroneous and error is reported
                d12: S1 -[input2{OPC_Test::A}]-> error_flag!(12); -- Erroneous and error is reported
                d13: S1 -[input2{OPC_Test::B}]-> error_flag!(13); -- Okay, no error reported
                d14: S1 -[input2{OPC_Test::C}]-> error_flag!(14); -- Erroneous and error is reported
                d15: S1 -[input2{OPC_Test::D}]-> error_flag!(15); -- Okay, no error reported
                d16: S1 -[input2{OPC_Test::X}]-> error_flag!(16); -- Erroneous and error is reported
            end component;
        **};
    end X2;
end OPC_Test;

Screenshots If applicable, add screenshots to help explain your problem.

Desktop (please complete the following information):

OSATE Version:
Operating System:

Additional context Add any other context about the problem here.

osate / osate2

EMV2 checking of typesets in propagations and error conditions is incomplete. #2855