Skip to content

CIF/BDD custom variable order parser may fail if parentheses are used in the option value

Running the following ToolDef script:

from "lib:cif" import *;

writefile("test.cif", [
"plant a:",
"  location:",
"    initial;",
"    marked;",
"end",
]);

cifdatasynth(
    "test.cif",
    "--var-order=(a;b)",
);

results in:

[Exception]
java.util.regex.PatternSyntaxException: Unclosed group near index 4
^(a$
	at java.base/java.util.regex.Pattern.error(Pattern.java:2204)
	at java.base/java.util.regex.Pattern.accept(Pattern.java:2054)
	at java.base/java.util.regex.Pattern.group0(Pattern.java:3232)
	at java.base/java.util.regex.Pattern.sequence(Pattern.java:2300)
	at java.base/java.util.regex.Pattern.expr(Pattern.java:2245)
	at java.base/java.util.regex.Pattern.compile(Pattern.java:1945)
	at java.base/java.util.regex.Pattern.<init>(Pattern.java:1576)
	at java.base/java.util.regex.Pattern.compile(Pattern.java:1101)
	at org.eclipse.escet.cif.bdd.varorder.parser.CustomVarOrderParser.parse(CustomVarOrderParser.java:71)
	at org.eclipse.escet.cif.bdd.varorder.parser.VarOrdererTypeChecker.getBasicConfiguredInitialOrderer(VarOrdererTypeChecker.java:269)
	at org.eclipse.escet.cif.bdd.varorder.parser.VarOrdererTypeChecker.getBasicConfiguredOrderer(VarOrdererTypeChecker.java:219)
	at org.eclipse.escet.cif.bdd.varorder.parser.VarOrdererTypeChecker.checkBasicOrderer(VarOrdererTypeChecker.java:189)
	at org.eclipse.escet.cif.bdd.varorder.parser.VarOrdererTypeChecker.checkVarOrderer(VarOrdererTypeChecker.java:129)
	at org.eclipse.escet.cif.bdd.varorder.parser.VarOrdererTypeChecker.checkVarOrderers(VarOrdererTypeChecker.java:103)
	at org.eclipse.escet.cif.bdd.varorder.parser.VarOrdererTypeChecker.transRoot(VarOrdererTypeChecker.java:88)
	at org.eclipse.escet.cif.bdd.varorder.parser.VarOrdererTypeChecker.transRoot(VarOrdererTypeChecker.java:1)
	at org.eclipse.escet.common.typechecker.TypeChecker.typeCheck(TypeChecker.java:201)
	at org.eclipse.escet.cif.bdd.conversion.CifToBddConverter.orderVars(CifToBddConverter.java:709)
	at org.eclipse.escet.cif.bdd.conversion.CifToBddConverter.convert(CifToBddConverter.java:443)
	at org.eclipse.escet.cif.datasynth.CifDataSynthesis.computeControlledSystem(CifDataSynthesis.java:189)
	at org.eclipse.escet.cif.datasynth.CifDataSynthesis.doSynthesisOnSpec(CifDataSynthesis.java:106)
	at org.eclipse.escet.cif.datasynth.CifDataSynthesisApp.doSynthesis(CifDataSynthesisApp.java:207)
	at org.eclipse.escet.cif.datasynth.CifDataSynthesisApp.runInternal(CifDataSynthesisApp.java:172)
	at org.eclipse.escet.common.app.framework.Application.runApplication(Application.java:316)
	at org.eclipse.escet.common.app.framework.ChildAppStarter$1.run(ChildAppStarter.java:285)
	at java.base/java.lang.Thread.run(Thread.java:1583)

The . and * are treated specially in the regex that is created, but any other characters that have a special meaning in regexes may still be interpreted.