CIF multilevel splitter partial spec builder crashes when inserting multiple new input variables
For a student, I quickly created a new plug-in to expose the partial specification builder, as part of multilevel synthesis, to end-users. (In case you're interested, see https://gitlab.eclipse.org/mgoorden7u4/escet/-/tree/expose-sub-specification?ref_type=heads.) Using this, I found the following bug where a list of new input variables are not properly inserted in the partial specification, hence causing a crash of the pretty printer. This bug is never triggered in the current implementation of multi-level splitter due to the most-refined product system preprocessing step (making proper plant and requirement groups).
Consider the following CIF specification:
plant A:
controllable a;
location l1:
initial;
edge a goto l2;
location l2:
edge a goto l1;
end
plant B:
controllable b;
location:
initial;
edge b when A.l1 or A.l2;
end
If we want to keep only plant B, the expected result is
group A:
input bool l1;
input bool l2;
end
plant B:
controllable b;
location:
initial;
edge b when A.l1 or A.l2;
end
Yet, the partial spec builder only adds one of the two new input variables to group A.
The problem lies in https://gitlab.eclipse.org/eclipse/escet/escet/-/blob/develop/cif/org.eclipse.escet.cif.multilevel/src/org/eclipse/escet/cif/multilevel/partialspecs/PartialSpecManager.java#L270 of the method insertObject(EList<T> origList, EList<T> partialList, U newPartialObject), where origlist is the list of declarations of the original parent (in this example plant A), partialList is the list of declarations of the corresponding new parent in the partial specification (in this example group A), and newPartialObject is the new input variable that needs to be added to partialList of the new parent respecting the order of declarations already present in the original parent's list origList.
If partialList is empty (which is the case in this example when adding the first input variable), a special case simply adds the newPartialObject to partialList. When this method is called for the second new input variable, partialList is no longer empty, so the main body of the function is considered. But this main body is only looping over elements of origList, which is in this example empty as plant A did not contain any declarations. Therefore, nothing is done with the second new input variable, and thus this one is not correctly assign group A as a parent.