Wrong validation for type products in transitions

[joeseibel]

When a transition refers to a typed state with a type product, the validator does not properly check that the type product listed in the transition is also listed in the state. In some cases, the validator reports errors when there shouldn't be any and in other cases the validator doesn't report errors when there should be. In the following example, transition1 should be valid and transition2 shouldn't be valid:

package missing_validation
public
  annex EMV2 {**
    error behavior machine1
      use types ErrorLibrary;
      events
        error1: error event;
      states
        state1: initial state {ConcurrencyError * ReplicationError};
        state2: state {ConcurrencyError * ReplicationError};
        state3: state {ConcurrencyError};
        state4: state {ReplicationError};
      transitions
        transition1: state1 {ConcurrencyError * ReplicationError} -[error1]->
          state2 {ReplicationError * ConcurrencyError};
        transition2: state3 {ConcurrencyError * ReplicationError} -[error1]->
          state4 {ConcurrencyError * ReplicationError};
    end behavior;
  **};
end missing_validation;

The validator currently reports two errors for transition1:

• Source type {ConcurrencyError * ReplicationError} is not contained in type set of error behavior state 'state1'
• Target type {ReplicationError * ConcurrencyError} is not contained in type set of error behavior state 'state2'

These errors should not be there since the type product is in the type set of state1 and state2. Note that I have swapped the order of the types in the product of the target just to show that order doesn't matter when checking a type product.

The validator currently does not report any errors for transition2, but it should. The type product ConcurrencyError * ReplicationError is not in the type set of state3 or state4.

Also, when the validator report errors, the error should be on the type product and not on the whole transition. The errors that are currently reported on transition1 are reported on the whole transition.