saeaadl / emv2

AADL Error Model V2 annex language
0 stars 0 forks source link

Legality rules for "all" expressions #90

Open AaronGreenhouse opened 1 year ago

AaronGreenhouse commented 1 year ago

Section E.8 Legality Rules does not cover "all" expressions. In particular, the value of the numeric literal needs to be bounded. Most certainly should not be greater than the number of error condition triggers in the following sequence. Should definitely be greater than 0. Should it be allowed to equal the number of elements, or must be it strictly less than the number of elements?

In any case, the following example is currently legal, but is problematic:

The current OSATE implementation doesn't flag these because there is no guidance from the EMV2 standard.

package AllButExample
public
    annex EMV2 {**
        error types
            Fired: type;
        end types;

        error behavior TestBehavior
        events
            A: error event;
            B: error event;
            C: error event;
            D: error event;
            E: error event;
            F: error event;
            G: error event;
            H: error event;
            I: error event;
        states
            TheState: initial state;
        end behavior;
    **};

    system Test
        features
            output1: out event port;
            output2: out event port;
            output3: out event port;
            output4: out event port;
    end Test;

    system implementation Test.i
        annex EMV2 {**
            use behavior AllButExample::TestBehavior;

            error propagations
                output1: out propagation{CountExpressions::Fired};
                output2: out propagation{CountExpressions::Fired};
                output3: out propagation{CountExpressions::Fired};
                output4: out propagation{CountExpressions::Fired};
            end propagations;

            component error behavior
            propagations
                p1: TheState -[all -2 (A, B, C, D)]-> output3{CountExpressions::Fired};
                p2: TheState -[all -3 (E, F, G, H, I)]-> output4{CountExpressions::Fired};
                p3: TheState -[all -5 (E, F, G, H, I)]-> output4{CountExpressions::Fired};
                p4: TheState -[all -15 (E, F, G, H, I)]-> output4{CountExpressions::Fired};
            end component;
        **};
    end Test.i;
end AllButExample;
brlarson commented 1 year ago

Certainly, p4 should have an error. A legality rule that the 'all' quantity should not exceed the number of propagation points should be added. I think p3 is okay.