loonwerks / AGREE

Assume-Guarantee REasoning Environment
BSD 3-Clause "New" or "Revised" License
12 stars 5 forks source link

AGREE validator overzealous on specification statement id duplication #105

Closed kfhoech closed 2 years ago

kfhoech commented 2 years ago

The AgreeValidator flags an error when a specification statement id is duplicated within the collection of packages it depends upon (including itself). This is not an AGREE error per se. However, use of a duplicate id within an namespace should be regarded as an error.

Since specification statement ids are intended to map to ids in a requirements management tool such as DOORS, it is helpful that the AGREE validator issue an informational statement or warning if such ids are not unique across the collection of packages upon which it depends.

Three changes should be made:

  1. Change the level of the present error to an informational message.
  2. Improve the message to include a list names it duplicates in qualified name form.
  3. Add a check for nonduplication within a namespace. This might already be handled by the standard NamesAreUniqueValidator.