Missing validation for emv2PropagationKind in EMV2PathElement

[joeseibel]

When referencing a propagation that is named with a keyword (processor, memory, connection, binding, bindings, access), the validator does not check to see if that propagation exists. The validator should check if these propagations exist and report errors when they don't. Consider the following example:

package missing_validation
public
  system s
    features
      fg1: feature group;
  end s;

  system implementation s.i
    subcomponents
      sub1: abstract a;
    annex EMV2 {**
      use types ErrorLibrary;
      use behavior missing_validation::machine1;

      error propagations
        processor: in propagation {ServiceError};
      end propagations;

      component error behavior
        transitions
          --The following two transitions are ok since the propagations "processor" and "sub1.processor" do
          --exist.
          state1 -[processor]-> state2;
          state1 -[sub1.processor]-> state2;

          --There should be errors on these transitions because there is no propagation "memory" or
          --"sub1.memory".
          state1 -[memory]-> state2;
          state1 -[sub1.memory]-> state2;

          --There should be errors on these transitions because it is not possible to have a keyword-named
          --propagation in a feature group.
          state1 -[fg1.memory]-> state2;
          state1 -[sub1.fg2.memory]-> state2;
      end component;
    **};
  end s.i;

  abstract a
    features
      fg2: feature group;
    annex EMV2 {**
      use types ErrorLibrary;

      error propagations
        processor: out propagation {ServiceError};
      end propagations;
    **};
  end a;

  annex EMV2 {**
    error behavior machine1
      states
        state1: initial state;
        state2: state;
    end behavior;
  **};
end missing_validation;

The above example shows two kinds of problems that should be reported:

1. When a keyword-named propagation is referenced in a dot expression after a feature group (fg1.memory and sub1.fg2.memory), there should always be an error since it is not possible to have a keyword-named propagation in a feature group.
2. When a keyword-named propagation is referenced directly or after a subcomponent in a dot expression, the validator should check if that propagation actually exists. In the example above, the references to processor and sub1.processor are fine since those propagations do exist. There should be errors on the references to memory and sub1.memory since those propagations do not exist.

The example showed this problem in the condition of transitions, but I would expect that the problem would occur in other EMV2 elements that contain EMV2PathElement.