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.