search

loonwerks / AGREE

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

AGREE Lustre ASE Builder attempted to add multiple nodes of name '_TOP_A' #24

Closed bcbrusse closed 4 years ago

bcbrusse commented 4 years ago

I'm having issues running agree when I refine a subcomponent type that extends another component. See the attachment for 4 simple models that clarify my issue.

refinement_test.zip

kfhoech commented 4 years ago

Confirmed.

This appears to be due to a change in the semantics of AADL instance model traversal where in the current version we encounter the connections and subcomponents possibly multiple times.

Solution is to guard addition of new connections or subcomponents by checking that a elements with the same model reference have not already been added.

kfhoech commented 4 years ago

Fixed by #26

kfhoech commented 4 years ago

This is deeper than first appears. When traversing the OSATE declarative model the methods that get the connections always return the base connection regardless if they're called in context of the refined component. Thus, we miss the refinements and do not generate all of the necessary connective assertions. The only way I've found to get the refinements is by traversing the instance model. Need to redesign the means of generating the connection assertions using the instance model.

kfhoech commented 4 years ago

Fixed by #29.