osate / osate2

Open Source AADL2 Tool Environment
http://osate.org
Eclipse Public License 2.0
35 stars 8 forks source link

The Slicer should support models where propagations are not described in flows #2879

Open sprocter opened 11 months ago

sprocter commented 11 months ago

Please describe the problem your proposed feature would address

Currently, the Slicer crashes when building the reachability graph for a model that has propagations which are not covered by flows. This example will cause a crash (stack trace below) as-is, but the reachability graph will be generated without problems if lines 49 and 50 are uncommented.

package ErrorPropagationsWithoutFlows
public

    system sys
    end sys;

    system implementation sys.impl
        subcomponents
            a : abstract Thing.one;
            b : abstract Thing.two;
            c : abstract Thing.three;
        connections
            aToB1 : feature a.o1 -> b.i1;
            aToB2 : feature a.o2 -> b.i2;
            aToB3 : feature a.o3 -> b.i3;
            bToC1 : feature b.o1 -> c.i1;
            bToC2 : feature b.o2 -> c.i2;
            bToC3 : feature b.o3 -> c.i3;
        annex EMV2 {** **};
    end sys.impl;

    abstract Thing
        features
            i1 : in feature;
            i2 : in feature;
            i3 : in feature;
            o1 : out feature;
            o2 : out feature;
            o3 : out feature;
    end Thing;

    abstract implementation Thing.one
        annex EMV2 {**
            use types ErrorLibrary;
            error propagations
                o1 : out propagation {ItemTimingError};
                flows
                    o1TimingSrc : error source o1 {ItemTimingError};
            end propagations;
        **};
    end Thing.one;

    abstract implementation Thing.two
        annex EMV2 {**
            use types ErrorLibrary;
            error propagations
                i1 : in propagation {ItemTimingError};
                o3 : out propagation {ItemTimingError};
--              flows
--                  i1ToO3 : error path i1 {ItemTimingError} -> o3 {ItemTimingError};
            end propagations;
        **};
    end Thing.two;

    abstract implementation Thing.three
        annex EMV2 {**
            use types ErrorLibrary;
            error propagations
                i3 : in propagation {ItemTimingError};
                flows
                    i3TimingSink : error sink i3 {ItemTimingError};
            end propagations;
        **};
    end Thing.three;

end ErrorPropagationsWithoutFlows;

This is the error and stack trace generated:

Can't add edge, vertex sys_impl_Instance.b.i1.ItemTimingError doesn't exist!

!ENTRY org.osate.ui 4 0 2023-07-31 10:19:39.040
!MESSAGE Internal error
!SUBENTRY 1 org.osate.ui 4 0 2023-07-31 10:19:39.041
!MESSAGE NullPointerException
!STACK 0
java.lang.NullPointerException
    at org.jgrapht.graph.AbstractGraph.assertVertexExist(AbstractGraph.java:129)
    at org.jgrapht.graph.AbstractBaseGraph.addEdge(AbstractBaseGraph.java:232)
    at org.osate.slicer.SlicerRepresentation.addEdge(SlicerRepresentation.java:248)
    at org.osate.slicer.SlicerRepresentation.calculateFixpoint(SlicerRepresentation.java:693)
    at org.osate.slicer.SlicerRepresentation.buildGraph(SlicerRepresentation.java:166)
    at org.osate.modelstats.ComponentCounter.countComponents(ComponentCounter.java:46)
    at org.osate.modelstats.ui.CountComponentsHandler.doAaxlAction(CountComponentsHandler.java:58)
    at org.osate.ui.handlers.AbstractAaxlHandler.processAaxlAction(AbstractAaxlHandler.java:472)
    at org.osate.ui.handlers.AbstractAaxlHandler.actionBody(AbstractAaxlHandler.java:181)
    at org.osate.ui.handlers.AaxlReadOnlyHandlerAsJob$ActionAsJob.runInWorkspace(AaxlReadOnlyHandlerAsJob.java:115)
    at org.eclipse.core.internal.resources.InternalWorkspaceJob.run(InternalWorkspaceJob.java:43)
    at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)

What is the impact of the problem?

Models that are syntactically valid (though they do violate consistency rules, see Additional Context section below) are not Sliceable. This means they have to be modified before being analyzed by any Slicer-backed analysis, which is a pain.

Describe the solution you'd like

The models should be parsed / the reachability graph generated without errors. Without deeply investigating, it seems like the easiest way to do that would be to create vertices for each propagation so they're accessible to the fixpoint calculation method, i.e., adding something like this to org.osate.slicer.SlicerRepresentation.Emv2SlicerSwitch:

@Override
public Void caseErrorPropagationInstance(ErrorPropagationInstance epi) {
    if (epi instanceof FeaturePropagation) {
        // add vertex here...
    } else if (epi instanceof AccessPropagation) {
        // and here...
    } else if (epi instanceof BindingPropagation) {
        // and here...
    } else if (epi instanceof PointPropagation) {
        // and here.
    } else {
        // This shouldn't happen. If it does, a new subtype has been added to ErrorPropagationInstance
    }
    return null;
}

Describe alternatives you've considered

As a workaround, models can be updated to include flows that cover all propagations. This is better from an accuracy standpoint, in that we don't have to make worst-case assumptions or guess at modeler intent. But, it requires more work from modelers and doesn't align with the standard.

Additional context

The relevant part of the EMV2 standard is E.7.2 "Error Flow Declarations." In particular, note consistency rules C2 and C3 and semantics rule 2.