featjar-formula's People

Contributors

Stargazers

Watchers

featjar-formula's Issues

FeatureIDE format: Alternative features not correctly supported

Current behaviour

In the class XMLFeatureModelFormat all alternatives are treated as atmost(1) cases. This may result an invalid number of solutions.

protected LiteralPredicate parseFeature(Literal parent, final Element e, final String nodeName, boolean and) {
//...
case ALT:
    if (parseFeatures.size() == 1) {
        constraints.add(implies(f, parseFeatures.get(0)));
    } else {
        constraints.add(new And(implies(f, parseFeatures), atMost(parseFeatures)));
    }
    break;
//...
}
protected Formula atMost(final List<Formula> parseFeatures) {
    return new AtMost(parseFeatures, 1);
}

Additionally, AtMost is not supported by JavaSMT

Exprected/proposed behaviour

protected LiteralPredicate parseFeature(Literal parent, final Element e, final String nodeName, boolean and) {
//...
case ALT:
    if (parseFeatures.size() == 1) {
        constraints.add(implies(f, parseFeatures.get(0)));
    } else {
        constraints.add(new And(implies(f, parseFeatures), alternative(f, parseFeatures)));
    }
    break;
//...
}

/**
* Creates an alternative selection using XOR.
*
* @param parent Parent feature
* @param parseFeatures All features available for selection
* @return parent implies (((f1 XOR f2) XOR ...) XOR fn)
*/
protected Formula alternative(LiteralPredicate parent, ArrayList<Formula> parseFeatures) {
List<Formula> options = new ArrayList<>();
    for (int i = 0; i < parseFeatures.size(); i++) {
	List<Formula> p = new ArrayList<>();
	for (int j = 0; j < parseFeatures.size(); j++) {
            if(i == j){
	        p.add(parseFeatures.get(j));
            } else {
	        p.add(new Not(parseFeatures.get(j)));
            }
        }
        options.add(new And(p));
    }
    return new Implies(parent, new Or(options));
}

For testing you could use the following structure:

<struct>
    <and mandatory="true" name="Webserver">
        <alt name="Datenbank">
            <feature name="MySQL"></feature>
            <feature name="PostgreSQL"></feature>
        </alt>
    </and>
</struct>