saeaadl / emv2

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

Clarify 'all' #59

Open joeseibel opened 2 years ago

joeseibel commented 2 years ago

In section E.7.2, Semantics (10), the standard says, "The keyword all indicates that an error flow specification applies to incoming or outgoing error propagations. In the case of an error source the component is an error source for all outgoing error propagations. In the case of an error sink, the component is an error sink for all incoming error propagations. In the case of an error path, an incoming error propagation can be mapped to all outgoing error propagations, all incoming error propagations can be mapped to a single outgoing error propagation, and all incoming error propagation can be mapped to all outgoing error propagations. The latter is the default interpretation if no error flows or outgoing propagation conditions (see section E.10.1) are declared."

This describes what all means in relation to propagations, but it should also describe what all means in relation to the types on those propagations. Ideally, the standard should also contain examples of how all is logically expanded. As an example, I would expect the standard to show that this declaration:

package StandardIssue
public
  system s
    features
      f1: out feature;
      f2: out feature;
      f3: out feature;
    annex EMV2 {**
      use types ErrorLibrary;

      error propagations
        f1: out propagation {ServiceError};
        f2: out propagation {ServiceError, ItemTimingError};
        f3: out propagation {ServiceError, ConcurrencyError};
        flows
          src: error source all {ServiceError};
      end propagations;
    **};
  end s;
end StandardIssue;

is equivalent to these declarations:

package StandardIssue
public
  system s
    features
      f1: out feature;
      f2: out feature;
      f3: out feature;
    annex EMV2 {**
      use types ErrorLibrary;

      error propagations
        f1: out propagation {ServiceError};
        f2: out propagation {ServiceError, ItemTimingError};
        f3: out propagation {ServiceError, ConcurrencyError};
        flows
          src_1: error source f1 {ServiceError};
          src_2: error source f2 {ServiceError};
          src_3: error source f3 {ServiceError};
      end propagations;
    **};
  end s;
end StandardIssue;

Also, the standard should explicitly describe what happens when an error type listed in an all error flow doesn't exist for one or more propagations. Consider this example:

package StandardIssue
public
  system s
    features
      f1: out feature;
      f2: out feature;
      f3: out feature;
    annex EMV2 {**
      use types ErrorLibrary;

      error propagations
        f1: out propagation {ServiceError};
        f2: out propagation {ServiceError, ItemTimingError};
        f3: out propagation {ConcurrencyError};
        flows
          src: error source all {ServiceError};
      end propagations;
    **};
  end s;
end StandardIssue;

In this case, ServiceError is not listed for the propagation f3. Should this be legal? If it is legal, what should it mean? The standard needs to clarify this.