loonwerks / AGREE

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

Validation check for LiftContract does not respect refinement #54

Closed kfhoech closed 3 years ago

kfhoech commented 3 years ago

In the validation check for LiftContactStatement the check attempts to match the connections in the containing component implementation to its features and those of its contained subcomponent. However, this check fails to consider that the features might be added to the containing component's type or the subcomponent's type via a refinement of an ancestor type.

See the UAV/SW.aadl model from this commit in the CASE models for an example

kfhoech commented 3 years ago

Resolved by #57