Skip to content

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

@AaronGreenhouse

Description

@AaronGreenhouse

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 d11d16 the errors are correct: d13 and d15 are not erroneous.
  • For detections d1d6 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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions