loonwerks / AGREE

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

AGREE Same Name In AGREE Annex and Subcomponent Validator Check Not Catching All Cases #130

Open aaurandt opened 1 year ago

aaurandt commented 1 year ago

Validator check in question (lines 1939-1948 specifically):

https://github.com/loonwerks/AGREE/blob/8d101f31460c3f539bb06d6ed123fdcb4226ee96/com.rockwellcollins.atc.agree/src/com/rockwellcollins/atc/agree/validation/AgreeValidator.java#L1899-L1951

The error is flagged with this code:

package TestPackage
public

system sys
end sys;

system implementation sys.impl
    subcomponents
        test : device TestSensor;
    annex agree {**
        eq test : int = 100;
    **};
end sys.impl;

device TestSensor
end TestSensor;

end TestPackage;

But it is not triggered with the following code:

package TestPackage
public

system sys
    annex agree {**
        eq test : int = 100;
    **};
end sys;

system implementation sys.impl
    subcomponents
        test : device TestSensor;
end sys.impl;

device TestSensor
end TestSensor;

end TestPackage;