Generating metaproduct for family-based verification does not encode feature model correctly

[ekuiter]

If I use the FeatureIDE > FeatureHouse > Generate Meta Product menu option, the generated code seems to contain errors in the feature model encoding in the JML contracts.
For example, generating a metaproduct for the example project IntList-FH-JML, the following JML specification is generated:

I am pretty sure that this should be (i.e. referencing the FeatureModel class):

@ requires (FM.FeatureModel.root) && (FM.FeatureModel.root || !FM.FeatureModel.base) && (FM.FeatureModel.root || !FM.FeatureModel.cons) && 

KeY also cannot load this metaproduct:

Am I missing something? If this is a bug, is it due to FeatureIDE or FeatureHouse (or wherever metaproduct generation is implemented?)

[tthuem]

Looks like a bug indeed. The missing prefix is most likely handled in the FeatureHouse code.

[rahelsundermann]

The regex in the replace function (for replacing "feature" with "FM.FeatureModel.feature" when creating the expression) only checks for a " "or a "(" infront of a feature, not for a "!".