diff --git a/prism-tests/functionality/verify/dtmcs/hoa/GFa_and_FGb_parity.hoa b/prism-tests/functionality/verify/dtmcs/hoa/GFa_and_FGb_parity.hoa new file mode 100644 index 0000000000..f99954c8ff --- /dev/null +++ b/prism-tests/functionality/verify/dtmcs/hoa/GFa_and_FGb_parity.hoa @@ -0,0 +1,31 @@ +HOA: v1 +name: "G(Fa & FGb)" +States: 4 +Start: 0 +AP: 2 "a" "b" +acc-name: parity max even 2 +Acceptance: 2 Fin(1) & Inf(0) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic stutter-invariant +--BODY-- +State: 0 {0 1} +[0&!1] 0 +[0&1] 1 +[!0&!1] 2 +[!0&1] 3 +State: 1 {0} +[0&!1] 0 +[0&1] 1 +[!0&!1] 2 +[!0&1] 3 +State: 2 {1} +[0&!1] 0 +[0&1] 1 +[!0&!1] 2 +[!0&1] 3 +State: 3 +[0&!1] 0 +[0&1] 1 +[!0&!1] 2 +[!0&1] 3 +--END-- diff --git a/prism-tests/functionality/verify/dtmcs/hoa/Xa_buchi.hoa b/prism-tests/functionality/verify/dtmcs/hoa/Xa_buchi.hoa new file mode 100644 index 0000000000..00cea47b7c --- /dev/null +++ b/prism-tests/functionality/verify/dtmcs/hoa/Xa_buchi.hoa @@ -0,0 +1,20 @@ +HOA: v1 +name: "Xa" +States: 4 +Start: 1 +AP: 1 "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic terminal +--BODY-- +State: 0 +[0] 2 +[!0] 3 +State: 1 +[t] 0 +State: 2 {0} +[t] 2 +State: 3 +[t] 3 +--END-- diff --git a/prism-tests/functionality/verify/dtmcs/hoa/lec15dtmc.pm b/prism-tests/functionality/verify/dtmcs/hoa/lec15dtmc.pm new file mode 100644 index 0000000000..d908e46902 --- /dev/null +++ b/prism-tests/functionality/verify/dtmcs/hoa/lec15dtmc.pm @@ -0,0 +1,16 @@ +// Simple DTMC from Lec 15 of Probabilistic Model Checking + +dtmc + +module M + +s:[0..5]; + +[] s=0 -> 0.5:(s'=1) + 0.5:(s'=3); +[] s=1 -> 0.5:(s'=0) + 0.25:(s'=2) + 0.25:(s'=4); +[] s=2 -> 1:(s'=5); +[] s=3 -> 1:(s'=3); +[] s=4 -> 1:(s'=4); +[] s=5 -> 1:(s'=2); + +endmodule diff --git a/prism-tests/functionality/verify/dtmcs/hoa/lec15dtmc.pm.hoa.props b/prism-tests/functionality/verify/dtmcs/hoa/lec15dtmc.pm.hoa.props new file mode 100644 index 0000000000..b847c0b8c7 --- /dev/null +++ b/prism-tests/functionality/verify/dtmcs/hoa/lec15dtmc.pm.hoa.props @@ -0,0 +1,47 @@ +// explicitly resolve path via $PROPERTY_DIR +// RESULT: 1/6 +P=?[ HOA: { "$PROPERTY_DIR/GFa_and_FGb_parity.hoa", "a" <- s=2, "b" <- s=2|s=5} ] + +// explicitly resolve path via $MODEL_DIR +// RESULT: 1/6 +P=?[ HOA: { "$MODEL_DIR/GFa_and_FGb_parity.hoa", "a" <- s=2, "b" <- s=2|s=5} ] + +// from now on, implicitly resolve via property dir + +// RESULT: 1/6 +P=?[ HOA: { "GFa_and_FGb_parity.hoa", "a" <- s=2, "b" <- s=2|s=5} ] +// RESULT: 1/6 +P=?[ (G F s=2) & (F G (s=2|s=5)) ] + +// RESULT: 5/6 +P=?[ ! HOA: { "GFa_and_FGb_parity.hoa", "a" <- s=2, "b" <- s=2|s=5} ] +// RESULT: 5/6 +P=?[ !((G F s=2) & (F G (s=2|s=5))) ] + + +// RESULT: 5/6 +P=?[ HOA: { "GFa_and_FGb_parity.hoa", "a" <- s>=2, "b" <- s>=3} ] +// RESULT: 5/6 +P=?[ (G F s>=2) & (F G s>=3) ] +// RESULT: 1/6 +P=?[ ! HOA: { "GFa_and_FGb_parity.hoa", "a" <- s>=2, "b" <- s>=3} ] +// RESULT: 1/6 +P=?[ !((G F s>=2) & (F G s>=3)) ] + +// use labels directly as APs for the automaton +label "a" = s>=2; +label "b" = s>=3; +// RESULT: 5/6 +P=?[ HOA: { "GFa_and_FGb_parity.hoa" } ] +// RESULT: 1/6 +P=?[ ! HOA: { "GFa_and_FGb_parity.hoa" } ] + +// RESULT: 1/2 +P=?[ HOA: {"Xa_buchi.hoa"} ] +// RESULT: 1/2 +P=?[ X "a" ] + +// RESULT: 1/2 +P=?[ ! HOA: {"Xa_buchi.hoa"} ] +// RESULT: 1/2 +P=?[ ! (X "a") ] \ No newline at end of file diff --git a/prism-tests/functionality/verify/mdps/hoa/GFa_and_FGb.hoa b/prism-tests/functionality/verify/mdps/hoa/GFa_and_FGb.hoa new file mode 100644 index 0000000000..f99954c8ff --- /dev/null +++ b/prism-tests/functionality/verify/mdps/hoa/GFa_and_FGb.hoa @@ -0,0 +1,31 @@ +HOA: v1 +name: "G(Fa & FGb)" +States: 4 +Start: 0 +AP: 2 "a" "b" +acc-name: parity max even 2 +Acceptance: 2 Fin(1) & Inf(0) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic stutter-invariant +--BODY-- +State: 0 {0 1} +[0&!1] 0 +[0&1] 1 +[!0&!1] 2 +[!0&1] 3 +State: 1 {0} +[0&!1] 0 +[0&1] 1 +[!0&!1] 2 +[!0&1] 3 +State: 2 {1} +[0&!1] 0 +[0&1] 1 +[!0&!1] 2 +[!0&1] 3 +State: 3 +[0&!1] 0 +[0&1] 1 +[!0&!1] 2 +[!0&1] 3 +--END-- diff --git a/prism-tests/functionality/verify/mdps/hoa/GFa_and_FGb_rabin.hoa b/prism-tests/functionality/verify/mdps/hoa/GFa_and_FGb_rabin.hoa new file mode 100644 index 0000000000..b6f18b100b --- /dev/null +++ b/prism-tests/functionality/verify/mdps/hoa/GFa_and_FGb_rabin.hoa @@ -0,0 +1,33 @@ +HOA: v1 +name: "G(Fa & FGb)" +States: 6 +Start: 0 +AP: 2 "a" "b" +acc-name: Rabin 1 +Acceptance: 2 Fin(0) & Inf(1) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic stutter-invariant +--BODY-- +State: 0 {0} +[!0 | !1] 1 +[0&1] 2 +State: 1 +[!0 | !1] 1 +[0&1] 2 +State: 2 +[!1] 0 +[0&1] 3 +[!0&1] 4 +State: 3 {1} +[!1] 0 +[0&1] 3 +[!0&1] 4 +State: 4 {1} +[!1] 0 +[0&1] 3 +[!0&1] 5 +State: 5 +[!1] 0 +[0&1] 3 +[!0&1] 5 +--END-- diff --git a/prism-tests/functionality/verify/mdps/hoa/Xa_buchi.hoa b/prism-tests/functionality/verify/mdps/hoa/Xa_buchi.hoa new file mode 100644 index 0000000000..00cea47b7c --- /dev/null +++ b/prism-tests/functionality/verify/mdps/hoa/Xa_buchi.hoa @@ -0,0 +1,20 @@ +HOA: v1 +name: "Xa" +States: 4 +Start: 1 +AP: 1 "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic terminal +--BODY-- +State: 0 +[0] 2 +[!0] 3 +State: 1 +[t] 0 +State: 2 {0} +[t] 2 +State: 3 +[t] 3 +--END-- diff --git a/prism-tests/functionality/verify/mdps/hoa/lec15mdp.nm b/prism-tests/functionality/verify/mdps/hoa/lec15mdp.nm new file mode 100644 index 0000000000..d29b3a3411 --- /dev/null +++ b/prism-tests/functionality/verify/mdps/hoa/lec15mdp.nm @@ -0,0 +1,22 @@ +// Simple MDP from Lec 15 of Probabilistic Model Checking + +mdp + +module M + +s:[0..8]; + +[] s=0 -> 1:(s'=2); +[] s=0 -> 0.6:(s'=0) + 0.3:(s'=1) + 0.1:(s'=2); +[] s=1 -> 0.3:(s'=3) + 0.7:(s'=4); +[] s=3 -> 1:(s'=4); +[] s=4 -> 1:(s'=1); +[] s=4 -> 1:(s'=3); +[] s=4 -> 1:(s'=6); +[] s=6 -> 1:(s'=6); +[] s=2 -> 1:(s'=5); +[] s=5 -> 0.9:(s'=7) + 0.1:(s'=8); +[] s=7 -> 1:(s'=5); +[] s=8 -> 1:(s'=5); + +endmodule diff --git a/prism-tests/functionality/verify/mdps/hoa/lec15mdp.nm.hoa.props b/prism-tests/functionality/verify/mdps/hoa/lec15mdp.nm.hoa.props new file mode 100644 index 0000000000..c627f280e6 --- /dev/null +++ b/prism-tests/functionality/verify/mdps/hoa/lec15mdp.nm.hoa.props @@ -0,0 +1,33 @@ +// RESULT: 3/4 +Pmax=?[ HOA: { "GFa_and_FGb_rabin.hoa", "a" <- s>=3, "b" <- s<=4} ] +// RESULT: 3/4 +Pmax=?[ (G F s>=3) & (F G (s<=4)) ] + +// RESULT: 0 +Pmin=?[ HOA: { "GFa_and_FGb_rabin.hoa", "a" <- s>=3, "b" <- s<=4} ] +// RESULT: 0 +Pmin=?[ (G F s>=3) & (F G (s<=4)) ] + +// RESULT: 0 +1 - Pmax=?[ ! HOA: { "GFa_and_FGb_rabin.hoa", "a" <- s>=3, "b" <- s<=4} ] +// RESULT: 0 +1 - Pmax=?[ !((G F s>=3) & (F G (s<=4))) ] + +// use labels directly as APs for the automaton +label "a" = s>=3; +label "b" = s<=4; +// RESULT: 3/4 +Pmax=?[ HOA: { "GFa_and_FGb_rabin.hoa" } ] + + +// RESULT: 0.3 +Pmax=?[ HOA: { "Xa_buchi.hoa", "a" <- s=1 } ] +// RESULT: 0.3 +Pmax=?[ X s=1 ] + +// RESULT: 0 +Pmin=?[ HOA: { "Xa_buchi.hoa", "a" <- s=1 } ] +// RESULT: 0 +Pmin=?[ X s=1 ] + + diff --git a/prism/src/automata/LTL2DA.java b/prism/src/automata/LTL2DA.java index 92718f3efd..8638b01820 100644 --- a/prism/src/automata/LTL2DA.java +++ b/prism/src/automata/LTL2DA.java @@ -33,9 +33,11 @@ import java.io.IOException; import java.io.InputStream; import java.io.PrintStream; +import java.nio.file.Path; import java.util.ArrayList; import java.util.BitSet; import java.util.List; +import java.util.Vector; import jhoafparser.consumer.HOAIntermediateStoreAndManipulate; import jhoafparser.parser.HOAFParser; @@ -47,9 +49,14 @@ import jltl2dstar.LTL2Rabin; import parser.Values; import parser.ast.Expression; +import parser.ast.ExpressionHOA; +import parser.ast.ExpressionLabel; +import parser.ast.ExpressionUnaryOp; +import prism.Pair; import prism.PrismComponent; import prism.PrismException; import prism.PrismNotSupportedException; +import prism.PrismPaths; import prism.PrismSettings; import acceptance.AcceptanceOmega; import acceptance.AcceptanceRabin; @@ -320,6 +327,120 @@ public DA convertLTLFormulaToDRA(Expression ltl, Values } } + /** + * Reads a HOA automaton from the given file and returns the parsed automaton. + * Throws a PrismException if the automaton does not have one of the allowed acceptance conditions. + */ + public DA readHOA(String filename, AcceptanceType... allowedAcceptance) throws PrismException + { + DA result; + try { + try { + HOAF2DA consumerDA = new HOAF2DA(); + + mainLog.println("Reading HOA automaton from "+filename+"..."); + InputStream input = new FileInputStream(filename); + HOAFParser.parseHOA(input, consumerDA); + result = consumerDA.getDA(); + } catch (HOAF2DA.TransitionBasedAcceptanceException e) { + // try again, this time transforming to state acceptance + getLog().println("Automaton with transition-based acceptance, automatically converting to state-based acceptance..."); + HOAF2DA consumerDA = new HOAF2DA(); + HOAIntermediateStoreAndManipulate consumerTransform = new HOAIntermediateStoreAndManipulate(consumerDA, new ToStateAcceptance()); + + InputStream input = new FileInputStream(filename); + HOAFParser.parseHOA(input, consumerTransform); + result = consumerDA.getDA(); + } + + if (result == null) { + throw new PrismException("Could not construct DA"); + } + } catch (ParseException e) { + throw new PrismException("Reading from " + filename + ", parse error: "+e.getMessage()); + } catch (PrismException e) { + throw new PrismException("Reading from " + filename + ", " + e.getMessage()); + } catch (IOException e) { + throw new PrismException("I/O error: " + e.getMessage()); + } + + if (!getSettings().getBoolean(PrismSettings.PRISM_NO_DA_SIMPLIFY)) { + result = DASimplifyAcceptance.simplifyAcceptance(this, result, allowedAcceptance); + } + + AcceptanceOmega acceptance = result.getAcceptance(); + if (AcceptanceType.contains(allowedAcceptance, acceptance.getType())) { + return result; + } else if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) { + // The specific acceptance type is not allowed, but GENERIC is allowed + // -> transform to generic acceptance and switch acceptance condition + DA.switchAcceptance(result, acceptance.toAcceptanceGeneric()); + return result; + } else { + throw new PrismNotSupportedException("HOA automaton has acceptance "+acceptance.getType()+", which is not yet supported for model checking this model / property"); + } + } + + /** + * Handles a ExpressionHOA expression, possibly negated. + * Reads the HOA automaton from the specified file and returns the parsed automaton. + * + * If the expression is of the form "! HOA: {....}" will attempt to negate the automaton + * via an appropriate switch of the acceptance condition. + * + * Throws a PrismException if the automaton does not have one of the allowed acceptance conditions. + * @param expr the expression + * @param paths path information for relative locations + * @param allowed acceptance + */ + public DA fromExpressionHOA(Expression expr, PrismPaths paths, Vector apExpressions, AcceptanceType... allowedAcceptance) throws PrismException + { + boolean negate = false; + while (Expression.isNot(expr) || Expression.isParenth(expr)) { + if (Expression.isNot(expr)) { + negate = !negate; + expr = ((ExpressionUnaryOp)expr).getOperand(); + } else if (Expression.isParenth(expr)) { + expr = ((ExpressionUnaryOp)expr).getOperand(); + } else { + throw new PrismException("implementation error"); + } + } + if (!(expr instanceof ExpressionHOA)) { + throw new PrismException("Expected HOA path automaton expression, found "+expr); + } + ExpressionHOA exprHOA = (ExpressionHOA) expr; + + Path automatonFile = paths.resolvePropertyResource(mainLog, exprHOA.getAutomatonFile().getText(), "HOA automaton file"); + + DA da = readHOA(automatonFile.toString(), allowedAcceptance); + + assert(apExpressions.size() == 0); + for (String ap : da.getAPList()) { + // default: ap corresponds to label expression + apExpressions.add(new ExpressionLabel(ap)); + } + + // handle renames + for (Pair rename : exprHOA.getRenames()) { + int i = da.getAPList().indexOf(rename.getKey()); + if (i == -1) { + throw new PrismException("Can not rename label \"" + rename.getKey() +"\", not an atomic proposition of the automaton"); + } else { + apExpressions.set(i, rename.getValue()); + } + } + + if (negate) { + String before = da.getAutomataType(); + AcceptanceOmega negated = da.getAcceptance().complement(da.size(), allowedAcceptance); + DA.switchAcceptance(da, negated); + mainLog.println("Switch to complement automaton, it is now a " + da.getAutomataType() + ", was a " +before + "."); + } + + return da; + } + /** Check whether we should use an external LTL->DA tool */ private boolean useExternal() { diff --git a/prism/src/common/PathUtil.java b/prism/src/common/PathUtil.java new file mode 100644 index 0000000000..83fc57729b --- /dev/null +++ b/prism/src/common/PathUtil.java @@ -0,0 +1,102 @@ +//============================================================================== +// +// Copyright (c) 2016- +// Authors: +// * Joachim Klein (formerly TU Dresden) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package common; + +import java.io.File; +import java.io.IOException; +import java.nio.file.Path; + +import parser.ast.ModulesFile; +import parser.ast.PropertiesFile; + +/** + * Static helpers for dealing with paths. + */ +public class PathUtil +{ + /** + * Returns the absolute path for the directory containing + * the argument file. Returns {@code null} on error, e.g., + * if the file does not exist. + */ + public static File getDirectoryFromFile(File file) + { + return getDirectoryFromFile(file.toPath()).toFile(); + } + + /** + * Returns the absolute path for the directory containing + * the argument file. Returns {@code null} on error, e.g., + * if the file does not exist. + */ + public static Path getDirectoryFromFile(Path filePath) + { + try { + return filePath.toRealPath().getParent(); + } catch (IOException e) { + // E.g., file does not exist + return null; + } + } + + /** + * Returns the path for the directory that is used for loading + * resources (e.g. a HOA automata file) in a property, + * extracting locations from the ModulesFile and PropertiesFile. + *
+ * The location of the properties file is preferred, then the location + * of the modules file. If there is no location, {@code null} is returned + * and should be treated as "current working directory". + */ + public static Path getDirectoryForRelativePropertyResource(ModulesFile mf, PropertiesFile pf) + { + if (pf != null && pf.getLocation() != null) { + return getDirectoryFromFile(pf.getLocation()); + } + + if (mf != null && mf.getLocation() != null) { + return getDirectoryFromFile(mf.getLocation()); + } + + return null; + } + + /** + * Resolves path2 relative to path1 (which has to point to a directory). + * If path2 is absolute, path1 is ignored. + * If path1 is {@code null}, resolution happens relative + * to the current working directory. + */ + public static Path resolvePath(Path path1, Path path2) + { + if (path1 == null) { + path1 = new File(".").toPath(); + } + return path1.resolve(path2); + } + +} diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index eb3961421e..34fb299458 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -55,6 +55,7 @@ import prism.PrismException; import prism.PrismLangException; import prism.PrismNotSupportedException; +import prism.PrismPaths; import prism.PrismUtils; import acceptance.AcceptanceBuchi; import acceptance.AcceptanceGenRabin; @@ -129,6 +130,7 @@ public static boolean isSupportedLTLFormula(ModelType modelType, Expression expr if (!expr.isPathFormula(true)) { return false; } + if (Expression.containsTemporalTimeBounds(expr)) { if (modelType.continuousTime()) { // Only support temporal bounds for discrete time models @@ -140,6 +142,10 @@ public static boolean isSupportedLTLFormula(ModelType modelType, Expression expr return false; } } + + if (Expression.isHOA(expr)) + return true; + return true; } @@ -236,14 +242,33 @@ public DA constructDAForLTLFormula(ProbModelCh } } - // Model check maximal state formulas - ltl = checkMaximalStateFormulas(mc, model, expr.deepCopy(), labelBS); + if (Expression.isHOA(expr)) { + LTL2DA ltl2da = new LTL2DA(this); + time = System.currentTimeMillis(); + mainLog.println("Parsing and constructing HOA automaton for "+expr); + PrismPaths paths = new PrismPaths(mc.getModulesFile(), + mc.getPropertiesFile()); + Vector apExpressions = new Vector(); + da = ltl2da.fromExpressionHOA(expr, paths, apExpressions, allowedAcceptance); + + mainLog.println("Determining states satisfying atomic proposition labels of the automaton..."); + for (int i=0; i labels, List labelNam } } } + + /** Get the optionally stored ModulesFile (may be {@code null}) */ + public ModulesFile getModulesFile() + { + return modulesFile; + } + + /** Get the optionally stored ModulesFile (may be {@code null}) */ + public PropertiesFile getPropertiesFile() + { + return propertiesFile; + } + } diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index 51c18ffe55..e7c031e02e 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -533,10 +533,10 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case DLBRACKET: case DLT: case MINUS: - case DQUOTE: case REG_INT: case REG_DOUBLE: - case REG_IDENT:{ + case REG_IDENT: + case REG_QUOTED_IDENT:{ ; break; } @@ -565,10 +565,10 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case DLBRACKET: case DLT: case MINUS: - case DQUOTE: case REG_INT: case REG_DOUBLE: - case REG_IDENT:{ + case REG_IDENT: + case REG_QUOTED_IDENT:{ prop = Property(); pf.addProperty(prop); label_3: @@ -640,10 +640,10 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case DLBRACKET: case DLT: case MINUS: - case DQUOTE: case REG_INT: case REG_DOUBLE: - case REG_IDENT:{ + case REG_IDENT: + case REG_QUOTED_IDENT:{ ; break; } @@ -672,10 +672,10 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case DLBRACKET: case DLT: case MINUS: - case DQUOTE: case REG_INT: case REG_DOUBLE: - case REG_IDENT:{ + case REG_IDENT: + case REG_QUOTED_IDENT:{ prop = Property(); label_5: while (true) { @@ -722,9 +722,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression Token begin = null; begin = getToken(1); if (jj_2_2(2147483647)) { - jj_consume_token(DQUOTE); - name = Identifier(); - jj_consume_token(DQUOTE); + name = QuotedIdentifier(); jj_consume_token(COLON); } else { ; @@ -850,9 +848,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression Expression expr = null; if (jj_2_3(2147483647)) { jj_consume_token(LABEL); - jj_consume_token(DQUOTE); - name = IdentifierExpression(); - jj_consume_token(DQUOTE); + name = QuotedIdentifierExpression(); jj_consume_token(EQ); expr = Expression(false, false); jj_consume_token(SEMICOLON); @@ -1147,10 +1143,10 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case DLBRACKET: case DLT: case MINUS: - case DQUOTE: case REG_INT: case REG_DOUBLE: - case REG_IDENT:{ + case REG_IDENT: + case REG_QUOTED_IDENT:{ prob = Expression(false, false); jj_consume_token(COLON); update = Update(); @@ -1278,9 +1274,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression Token begin = null, begin2 = null; begin = jj_consume_token(REWARDS); if (jj_2_6(2147483647)) { - jj_consume_token(DQUOTE); - name = Identifier(); - jj_consume_token(DQUOTE); + name = QuotedIdentifier(); rs.setName(name); } else { ; @@ -1312,10 +1306,10 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case DLBRACKET: case DLT: case MINUS: - case DQUOTE: case REG_INT: case REG_DOUBLE: - case REG_IDENT:{ + case REG_IDENT: + case REG_QUOTED_IDENT:{ ; break; } @@ -1371,9 +1365,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression SystemDefn sysdef; jj_consume_token(SYSTEM); if (jj_2_7(2147483647)) { - jj_consume_token(DQUOTE); - name = Identifier(); - jj_consume_token(DQUOTE); + name = QuotedIdentifier(); } else { ; } @@ -1594,10 +1586,8 @@ static class ExpressionPair { public Expression expr1 = null; public Expression sys = new SystemModule(name); break; } - case DQUOTE:{ - jj_consume_token(DQUOTE); - name = Identifier(); - jj_consume_token(DQUOTE); + case REG_QUOTED_IDENT:{ + name = QuotedIdentifier(); sys = new SystemReference(name); break; } @@ -1778,10 +1768,10 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case DLBRACKET: case DLT: case MINUS: - case DQUOTE: case REG_INT: case REG_DOUBLE: - case REG_IDENT:{ + case REG_IDENT: + case REG_QUOTED_IDENT:{ ret = ExpressionITE(prop, pathprop); break; } @@ -1828,10 +1818,10 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case DLBRACKET: case DLT: case MINUS: - case DQUOTE: case REG_INT: case REG_DOUBLE: - case REG_IDENT:{ + case REG_IDENT: + case REG_QUOTED_IDENT:{ uBound = Expression(false, false); break; } @@ -1873,10 +1863,10 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case DLBRACKET: case DLT: case MINUS: - case DQUOTE: case REG_INT: case REG_DOUBLE: - case REG_IDENT:{ + case REG_IDENT: + case REG_QUOTED_IDENT:{ uBound = Expression(false, false); break; } @@ -1918,10 +1908,10 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case DLBRACKET: case DLT: case MINUS: - case DQUOTE: case REG_INT: case REG_DOUBLE: - case REG_IDENT:{ + case REG_IDENT: + case REG_QUOTED_IDENT:{ lBound = Expression(false, false); break; } @@ -1963,10 +1953,10 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case DLBRACKET: case DLT: case MINUS: - case DQUOTE: case REG_INT: case REG_DOUBLE: - case REG_IDENT:{ + case REG_IDENT: + case REG_QUOTED_IDENT:{ lBound = Expression(false, false); break; } @@ -2154,10 +2144,10 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case DLBRACKET: case DLT: case MINUS: - case DQUOTE: case REG_INT: case REG_DOUBLE: - case REG_IDENT:{ + case REG_IDENT: + case REG_QUOTED_IDENT:{ ret = ExpressionEquality(prop, pathprop); break; } @@ -2346,10 +2336,10 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case LPARENTH: case DLBRACKET: case DLT: - case DQUOTE: case REG_INT: case REG_DOUBLE: - case REG_IDENT:{ + case REG_IDENT: + case REG_QUOTED_IDENT:{ ret = ExpressionBasic(prop, pathprop); break; } @@ -2420,7 +2410,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression ret = ExpressionStrategy(prop, pathprop); break; } - case DQUOTE:{ + case REG_QUOTED_IDENT:{ ret = ExpressionLabel(prop, pathprop); break; } @@ -2703,7 +2693,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression throw new ParseException(); } jj_consume_token(LBRACKET); - expr = Expression(prop, true); + expr = PathSpecification(prop); switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { case LBRACE:{ filter = Filter(); @@ -2732,6 +2722,123 @@ static class ExpressionPair { public Expression expr1 = null; public Expression throw new Error("Missing return statement in function"); } +// A path specification: +// Currently, can be +// - an LTL formula, i.e., Expression() +// - a (possibly negated) HOA: ... automaton specification + static final public Expression PathSpecification(boolean prop) throws ParseException {Expression result; + ExpressionIdent kind = null; + if (jj_2_15(1)) { + if (getToken(1).kind==REG_IDENT + && getToken(1).image.equals("HOA") + && getToken(2).kind==COLON) { + + } else { + jj_consume_token(-1); + throw new ParseException(); + } + kind = IdentifierExpression(); + jj_consume_token(COLON); + jj_consume_token(LBRACE); + result = PathSpecificationHOA(prop); + jj_consume_token(RBRACE); + } else if (jj_2_16(1)) { + if (getToken(1).kind==NOT + && getToken(2).kind==REG_IDENT + && getToken(2).image.equals("HOA") + && getToken(3).kind==COLON) { + + } else { + jj_consume_token(-1); + throw new ParseException(); + } + jj_consume_token(NOT); + kind = IdentifierExpression(); + jj_consume_token(COLON); + jj_consume_token(LBRACE); + result = PathSpecificationHOA(prop); + jj_consume_token(RBRACE); +result = Expression.Not(result); + } else if (jj_2_17(1)) { + if (getToken(1).kind==REG_IDENT + && getToken(2).kind==COLON) { + + } else { + jj_consume_token(-1); + throw new ParseException(); + } + kind = IdentifierExpression(); +{if (true) throw new ParseException("Unknown path type '"+kind.getName()+"'");} + } else { + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { + case A: + case E: + case FALSE: + case FILTER: + case FUNC: + case F: + case G: + case MAX: + case MIN: + case X: + case PMAX: + case PMIN: + case P: + case RMAX: + case RMIN: + case R: + case S: + case TRUE: + case NOT: + case LPARENTH: + case DLBRACKET: + case DLT: + case MINUS: + case REG_INT: + case REG_DOUBLE: + case REG_IDENT: + case REG_QUOTED_IDENT:{ + result = Expression(prop, true); + break; + } + default: + jj_la1[72] = jj_gen; + jj_consume_token(-1); + throw new ParseException(); + } + } +{if ("" != null) return result;} + throw new Error("Missing return statement in function"); + } + +// The inner part of a HOA: { "automatonfile", "ap" <- state-expression, ... } specification + static final public ExpressionHOA PathSpecificationHOA(boolean prop) throws ParseException {QuotedString hoaAutomatonFile; + ExpressionHOA result = null; + Expression stateExpression = null; + String ap, label; + hoaAutomatonFile = QuotedString(); +result = new ExpressionHOA(hoaAutomatonFile); + label_27: + while (true) { + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { + case COMMA:{ + ; + break; + } + default: + jj_la1[73] = jj_gen; + break label_27; + } + jj_consume_token(COMMA); + ap = QuotedIdentifier(); + jj_consume_token(RENAME); + stateExpression = Expression(prop, false); +result.addRename(ap, stateExpression); + } +{if ("" != null) return result;} + throw new Error("Missing return statement in function"); + } + // Filter for a P/S/R operator static final public Filter Filter() throws ParseException {Filter filter; @@ -2741,7 +2848,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression expr = Expression(true, false); filter = new Filter(expr); jj_consume_token(RBRACE); - label_27: + label_28: while (true) { switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { case LBRACE:{ @@ -2749,8 +2856,8 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[72] = jj_gen; - break label_27; + jj_la1[74] = jj_gen; + break label_28; } jj_consume_token(LBRACE); switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { @@ -2765,7 +2872,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[73] = jj_gen; + jj_la1[75] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2803,7 +2910,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[74] = jj_gen; + jj_la1[76] = jj_gen; ; } r = LtGt(); @@ -2818,7 +2925,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[75] = jj_gen; + jj_la1[77] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2830,7 +2937,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[76] = jj_gen; + jj_la1[78] = jj_gen; ; } jj_consume_token(RBRACKET); @@ -2875,7 +2982,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[77] = jj_gen; + jj_la1[79] = jj_gen; ; } switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { @@ -2884,7 +2991,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[78] = jj_gen; + jj_la1[80] = jj_gen; ; } switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { @@ -2918,7 +3025,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[79] = jj_gen; + jj_la1[81] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2939,7 +3046,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[80] = jj_gen; + jj_la1[82] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2951,7 +3058,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[81] = jj_gen; + jj_la1[83] = jj_gen; ; } jj_consume_token(RBRACKET); @@ -2978,10 +3085,8 @@ static class ExpressionPair { public Expression expr1 = null; public Expression void RewardIndex(ExpressionReward exprRew) throws ParseException {Object index = null; Object indexDiv = null; jj_consume_token(LBRACE); - if (jj_2_15(2147483647)) { - jj_consume_token(DQUOTE); - index = Identifier(); - jj_consume_token(DQUOTE); + if (jj_2_18(2147483647)) { + index = QuotedIdentifier(); } else { switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { case A: @@ -3007,15 +3112,15 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case DLBRACKET: case DLT: case MINUS: - case DQUOTE: case REG_INT: case REG_DOUBLE: - case REG_IDENT:{ + case REG_IDENT: + case REG_QUOTED_IDENT:{ index = Expression(false, false); break; } default: - jj_la1[82] = jj_gen; + jj_la1[84] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3025,10 +3130,8 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case DIVIDE:{ jj_consume_token(DIVIDE); jj_consume_token(LBRACE); - if (jj_2_16(2147483647)) { - jj_consume_token(DQUOTE); - indexDiv = Identifier(); - jj_consume_token(DQUOTE); + if (jj_2_19(2147483647)) { + indexDiv = QuotedIdentifier(); } else { switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { case A: @@ -3054,15 +3157,15 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case DLBRACKET: case DLT: case MINUS: - case DQUOTE: case REG_INT: case REG_DOUBLE: - case REG_IDENT:{ + case REG_IDENT: + case REG_QUOTED_IDENT:{ indexDiv = Expression(false, false); break; } default: - jj_la1[83] = jj_gen; + jj_la1[85] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3071,7 +3174,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[84] = jj_gen; + jj_la1[86] = jj_gen; ; } exprRew.setRewardStructIndex(index); @@ -3091,7 +3194,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression Expression ret = null; Token begin; begin = getToken(1); - if (jj_2_17(2147483647)) { + if (jj_2_20(2147483647)) { expr = ExpressionSS(prop, true); ret = expr; } else { @@ -3102,8 +3205,8 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[85] = jj_gen; - if (jj_2_18(2147483647)) { + jj_la1[87] = jj_gen; + if (jj_2_21(2147483647)) { begin = jj_consume_token(C); jj_consume_token(LE); expr = Expression(false, false); @@ -3145,16 +3248,16 @@ static class ExpressionPair { public Expression expr1 = null; public Expression case DLBRACKET: case DLT: case MINUS: - case DQUOTE: case REG_INT: case REG_DOUBLE: - case REG_IDENT:{ + case REG_IDENT: + case REG_QUOTED_IDENT:{ expr = Expression(prop, true); ret = expr; break; } default: - jj_la1[86] = jj_gen; + jj_la1[88] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3219,7 +3322,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[87] = jj_gen; + jj_la1[89] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3244,7 +3347,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[88] = jj_gen; + jj_la1[90] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3257,7 +3360,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[89] = jj_gen; + jj_la1[91] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3277,13 +3380,13 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[92] = jj_gen; + jj_la1[94] = jj_gen; switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { case REG_INT: case REG_IDENT:{ s = ExpressionStrategyCoalitionPlayer(); coalition.add(s); - label_28: + label_29: while (true) { switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { case COMMA:{ @@ -3291,8 +3394,8 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[90] = jj_gen; - break label_28; + jj_la1[92] = jj_gen; + break label_29; } jj_consume_token(COMMA); s = ExpressionStrategyCoalitionPlayer(); @@ -3301,7 +3404,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[91] = jj_gen; + jj_la1[93] = jj_gen; ; } exprStrat.setCoalition(coalition); @@ -3321,7 +3424,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[93] = jj_gen; + jj_la1[95] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3332,28 +3435,13 @@ static class ExpressionPair { public Expression expr1 = null; public Expression // (Property) expression: label (including "init") static final public -Expression ExpressionLabel(boolean prop, boolean pathprop) throws ParseException {String s; +Expression ExpressionLabel(boolean prop, boolean pathprop) throws ParseException {ExpressionIdent qi; ExpressionLabel ret = null; Token begin; if (!prop) {if (true) throw generateParseException();} - begin = jj_consume_token(DQUOTE); - switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { - case REG_IDENT:{ - s = Identifier(); - break; - } - case INIT:{ - jj_consume_token(INIT); -s = "init"; - break; - } - default: - jj_la1[94] = jj_gen; - jj_consume_token(-1); - throw new ParseException(); - } - jj_consume_token(DQUOTE); -ret = new ExpressionLabel(s); ret.setPosition(begin, getToken(0)); {if ("" != null) return ret;} + // Label can be arbitary quoted identifier + qi = QuotedIdentifierExpression(); +ret = new ExpressionLabel(qi.getName()); ret.setPosition(qi,qi); {if ("" != null) return ret;} throw new Error("Missing return statement in function"); } @@ -3399,7 +3487,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[95] = jj_gen; + jj_la1[96] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3412,7 +3500,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[96] = jj_gen; + jj_la1[97] = jj_gen; ; } jj_consume_token(RPARENTH); @@ -3432,6 +3520,14 @@ String Identifier() throws ParseException { throw new Error("Missing return statement in function"); } + static final public String QuotedIdentifier() throws ParseException { + jj_consume_token(REG_QUOTED_IDENT); +String s = getToken(0).image; + // remove " + {if ("" != null) return s.substring(1,s.length()-1);} + throw new Error("Missing return statement in function"); + } + // Identifier (returns ExpressionIdent, storing position info) static final public ExpressionIdent IdentifierExpression() throws ParseException {String ident; @@ -3441,6 +3537,45 @@ String Identifier() throws ParseException { throw new Error("Missing return statement in function"); } +// QuotedIdentifier (returns ExpressionIdent, storing position info) + static final public +ExpressionIdent QuotedIdentifierExpression() throws ParseException {String ident; + ExpressionIdent ret; + Token begin; +begin = getToken(1); + ident = QuotedIdentifier(); +ret = new ExpressionIdent(ident); ret.setPosition(begin, getToken(0)); {if ("" != null) return ret;} + throw new Error("Missing return statement in function"); + } + +// A quoted string ("text"), returns the unquoted text + static final public QuotedString QuotedString() throws ParseException {String s; + Token begin; +begin = getToken(1); + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { + case REG_QUOTED_IDENT:{ + jj_consume_token(REG_QUOTED_IDENT); +s = getToken(0).image; + break; + } + case REG_QUOTED_STRING:{ + jj_consume_token(REG_QUOTED_STRING); +s = getToken(0).image; + break; + } + default: + jj_la1[98] = jj_gen; + jj_consume_token(-1); + throw new ParseException(); + } +try { + {if ("" != null) return QuotedString.fromQuoted(s);} + } catch (PrismLangException e) { + {if (true) throw new ParseException(e.getMessage() + ", at line " + begin.next.beginLine + ", column " + begin.next.beginColumn +".");} + } + throw new Error("Missing return statement in function"); + } + // Identifier or min/max keyword (returns ExpressionIdent, storing position info) static final public ExpressionIdent IdentifierExpressionMinMax() throws ParseException {String ident; @@ -3461,7 +3596,7 @@ String Identifier() throws ParseException { break; } default: - jj_la1[97] = jj_gen; + jj_la1[99] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3498,7 +3633,7 @@ int EqNeq() throws ParseException { break; } default: - jj_la1[98] = jj_gen; + jj_la1[100] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3530,7 +3665,7 @@ int LtGt() throws ParseException { break; } default: - jj_la1[99] = jj_gen; + jj_la1[101] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3556,7 +3691,7 @@ int LtGt() throws ParseException { break; } default: - jj_la1[100] = jj_gen; + jj_la1[102] = jj_gen; ; } jj_consume_token(0); @@ -3713,271 +3848,278 @@ static private boolean jj_2_18(int xla) finally { jj_save(17, xla); } } - static private boolean jj_3R_164() + static private boolean jj_2_19(int xla) { - if (jj_3R_29()) return true; - return false; + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return !jj_3_19(); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(18, xla); } } - static private boolean jj_3R_46() + static private boolean jj_2_20(int xla) { - if (jj_3R_55()) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_56()) jj_scanpos = xsp; - return false; + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return !jj_3_20(); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(19, xla); } } - static private boolean jj_3R_184() + static private boolean jj_2_21(int xla) { - if (jj_scan_token(OR)) return true; - return false; + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return !jj_3_21(); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(20, xla); } } - static private boolean jj_3R_90() + static private boolean jj_3R_96() { if (jj_scan_token(COMMA)) return true; - if (jj_3R_29()) return true; + if (jj_3R_30()) return true; return false; } - static private boolean jj_3R_146() + static private boolean jj_3R_152() { if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_38()) return true; + if (jj_3R_44()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_32() + static private boolean jj_3R_158() { - if (jj_3R_29()) return true; + if (jj_3R_32()) return true; return false; } - static private boolean jj_3R_163() + static private boolean jj_3R_213() + { + if (jj_3R_154()) return true; + return false; + } + + static private boolean jj_3R_169() { if (jj_scan_token(MAX)) return true; return false; } - static private boolean jj_3R_157() + static private boolean jj_3R_163() { if (jj_scan_token(FALSE)) return true; return false; } - static private boolean jj_3R_156() + static private boolean jj_3R_162() { if (jj_scan_token(TRUE)) return true; return false; } - static private boolean jj_3R_183() + static private boolean jj_3R_228() { - if (jj_scan_token(AND)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_scan_token(85)) { + jj_scanpos = xsp; + if (jj_scan_token(88)) return true; + } return false; } - static private boolean jj_3R_181() + static private boolean jj_3R_44() { - if (jj_scan_token(MAX)) return true; + if (jj_3R_52()) return true; return false; } - static private boolean jj_3R_38() + static private boolean jj_3_4() { - if (jj_3R_46()) return true; + if (jj_scan_token(LABEL)) return true; return false; } - static private boolean jj_3R_29() + static private boolean jj_3R_161() { - if (jj_scan_token(REG_IDENT)) return true; + if (jj_scan_token(REG_DOUBLE)) return true; return false; } - static private boolean jj_3_4() + static private boolean jj_3_3() { if (jj_scan_token(LABEL)) return true; + if (jj_3R_32()) return true; return false; } - static private boolean jj_3R_179() + static private boolean jj_3R_229() { - if (jj_scan_token(INIT)) return true; + if (jj_scan_token(COMMA)) return true; + if (jj_3R_228()) return true; return false; } - static private boolean jj_3R_155() + static private boolean jj_3R_223() { - if (jj_scan_token(REG_DOUBLE)) return true; + if (jj_3R_228()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_229()) { jj_scanpos = xsp; break; } + } return false; } - static private boolean jj_3_3() + static private boolean jj_3R_217() { - if (jj_scan_token(LABEL)) return true; - if (jj_scan_token(DQUOTE)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_223()) jj_scanpos = xsp; return false; } - static private boolean jj_3R_186() + static private boolean jj_3R_216() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_38()) return true; + if (jj_scan_token(TIMES)) return true; return false; } - static private boolean jj_3R_162() + static private boolean jj_3R_211() + { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_216()) { + jj_scanpos = xsp; + if (jj_3R_217()) return true; + } + return false; + } + + static private boolean jj_3R_168() { if (jj_scan_token(MIN)) return true; return false; } - static private boolean jj_3R_79() + static private boolean jj_3R_85() { if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_31()) return true; + if (jj_3R_34()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_185() + static private boolean jj_3R_160() { - if (jj_3R_29()) return true; + if (jj_scan_token(REG_INT)) return true; return false; } - static private boolean jj_3R_182() + static private boolean jj_3R_84() { - if (jj_scan_token(PLUS)) return true; + if (jj_3R_31()) return true; return false; } - static private boolean jj_3R_154() - { - if (jj_scan_token(REG_INT)) return true; - return false; - } - - static private boolean jj_3R_78() - { - if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_29()) return true; - if (jj_scan_token(DQUOTE)) return true; - return false; - } - - static private boolean jj_3R_180() - { - if (jj_scan_token(MIN)) return true; - return false; - } - - static private boolean jj_3R_142() + static private boolean jj_3R_148() { Token xsp; xsp = jj_scanpos; - if (jj_3R_154()) { + if (jj_3R_160()) { jj_scanpos = xsp; - if (jj_3R_155()) { + if (jj_3R_161()) { jj_scanpos = xsp; - if (jj_3R_156()) { + if (jj_3R_162()) { jj_scanpos = xsp; - if (jj_3R_157()) return true; + if (jj_3R_163()) return true; } } } return false; } - static private boolean jj_3R_178() - { - if (jj_3R_29()) return true; - return false; - } - - static private boolean jj_3R_77() + static private boolean jj_3R_76() { - if (jj_3R_29()) return true; + if (jj_scan_token(COMMA)) return true; + if (jj_3R_30()) return true; return false; } - static private boolean jj_3R_70() + static private boolean jj_3R_83() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_29()) return true; + if (jj_3R_30()) return true; return false; } - static private boolean jj_3R_160() + static private boolean jj_3R_166() { if (jj_scan_token(MAX)) return true; return false; } - static private boolean jj_3R_68() + static private boolean jj_3R_74() { Token xsp; xsp = jj_scanpos; - if (jj_3R_77()) { + if (jj_3R_83()) { jj_scanpos = xsp; - if (jj_3R_78()) { + if (jj_3R_84()) { jj_scanpos = xsp; - if (jj_3R_79()) return true; + if (jj_3R_85()) return true; } } return false; } - static private boolean jj_3R_153() + static private boolean jj_3R_184() { - if (jj_scan_token(FILTER)) return true; - if (jj_scan_token(LPARENTH)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_180()) { - jj_scanpos = xsp; - if (jj_3R_181()) { - jj_scanpos = xsp; - if (jj_3R_182()) { - jj_scanpos = xsp; - if (jj_3R_183()) { - jj_scanpos = xsp; - if (jj_3R_184()) { - jj_scanpos = xsp; - if (jj_3R_185()) return true; - } - } - } - } - } - if (jj_scan_token(COMMA)) return true; - if (jj_3R_38()) return true; - xsp = jj_scanpos; - if (jj_3R_186()) jj_scanpos = xsp; - if (jj_scan_token(RPARENTH)) return true; + if (jj_3R_152()) return true; return false; } - static private boolean jj_3R_161() + static private boolean jj_3R_212() { - if (jj_3R_38()) return true; + if (jj_3R_153()) return true; + return false; + } + + static private boolean jj_3R_167() + { + if (jj_3R_44()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_187()) { jj_scanpos = xsp; break; } + if (jj_3R_192()) { jj_scanpos = xsp; break; } } return false; } - static private boolean jj_3R_91() + static private boolean jj_3R_183() + { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_212()) { + jj_scanpos = xsp; + if (jj_3R_213()) return true; + } + return false; + } + + static private boolean jj_3R_97() { if (jj_scan_token(COMMA)) return true; - if (jj_3R_29()) return true; + if (jj_3R_30()) return true; if (jj_scan_token(RENAME)) return true; - if (jj_3R_29()) return true; + if (jj_3R_30()) return true; + return false; + } + + static private boolean jj_3R_182() + { + if (jj_scan_token(DLBRACKET)) return true; + if (jj_3R_211()) return true; + if (jj_scan_token(DRBRACKET)) return true; return false; } @@ -3989,105 +4131,122 @@ static private boolean jj_3_9() return false; } - static private boolean jj_3R_81() + static private boolean jj_3R_181() + { + if (jj_scan_token(DLT)) return true; + if (jj_3R_211()) return true; + if (jj_scan_token(DGT)) return true; + return false; + } + + static private boolean jj_3R_227() + { + if (jj_3R_44()) return true; + return false; + } + + static private boolean jj_3R_157() { - if (jj_scan_token(LBRACE)) return true; - if (jj_3R_29()) return true; - if (jj_scan_token(RENAME)) return true; - if (jj_3R_29()) return true; Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_91()) { jj_scanpos = xsp; break; } + xsp = jj_scanpos; + if (jj_3R_181()) { + jj_scanpos = xsp; + if (jj_3R_182()) return true; + } + xsp = jj_scanpos; + if (jj_3R_183()) { + jj_scanpos = xsp; + if (jj_3R_184()) return true; } - if (jj_scan_token(RBRACE)) return true; return false; } - static private boolean jj_3R_50() + static private boolean jj_3R_56() { if (jj_scan_token(OR)) return true; if (jj_scan_token(OR)) return true; if (jj_scan_token(OR)) return true; - if (jj_3R_35()) return true; + if (jj_3R_41()) return true; return false; } - static private boolean jj_3R_145() + static private boolean jj_3R_87() + { + if (jj_scan_token(LBRACE)) return true; + if (jj_3R_30()) return true; + if (jj_scan_token(RENAME)) return true; + if (jj_3R_30()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_97()) { jj_scanpos = xsp; break; } + } + if (jj_scan_token(RBRACE)) return true; + return false; + } + + static private boolean jj_3R_151() { if (jj_scan_token(FUNC)) return true; if (jj_scan_token(LPARENTH)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_162()) { + if (jj_3R_168()) { jj_scanpos = xsp; - if (jj_3R_163()) { + if (jj_3R_169()) { jj_scanpos = xsp; - if (jj_3R_164()) return true; + if (jj_3R_170()) return true; } } if (jj_scan_token(COMMA)) return true; - if (jj_3R_161()) return true; + if (jj_3R_167()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_152() + static private boolean jj_3R_75() { - if (jj_scan_token(DQUOTE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_178()) { + if (jj_3R_86()) { jj_scanpos = xsp; - if (jj_3R_179()) return true; + if (jj_3R_87()) return true; } - if (jj_scan_token(DQUOTE)) return true; - return false; - } - - static private boolean jj_3R_207() - { - if (jj_3R_148()) return true; return false; } - static private boolean jj_3R_80() + static private boolean jj_3R_86() { if (jj_scan_token(DIVIDE)) return true; if (jj_scan_token(LBRACE)) return true; - if (jj_3R_29()) return true; + if (jj_3R_30()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_90()) { jj_scanpos = xsp; break; } + if (jj_3R_96()) { jj_scanpos = xsp; break; } } if (jj_scan_token(RBRACE)) return true; return false; } - static private boolean jj_3R_69() + static private boolean jj_3R_221() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_80()) { - jj_scanpos = xsp; - if (jj_3R_81()) return true; - } + if (jj_3R_44()) return true; return false; } - static private boolean jj_3R_58() + static private boolean jj_3R_64() { - if (jj_3R_68()) return true; + if (jj_3R_74()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_69()) { jj_scanpos = xsp; break; } + if (jj_3R_75()) { jj_scanpos = xsp; break; } } return false; } - static private boolean jj_3R_159() + static private boolean jj_3R_165() { if (jj_scan_token(MIN)) return true; return false; @@ -4100,43 +4259,41 @@ static private boolean jj_3_8() return false; } - static private boolean jj_3R_144() + static private boolean jj_3R_150() { Token xsp; xsp = jj_scanpos; - if (jj_3R_159()) { + if (jj_3R_165()) { jj_scanpos = xsp; - if (jj_3R_160()) return true; + if (jj_3R_166()) return true; } if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_161()) return true; + if (jj_3R_167()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_217() + static private boolean jj_3R_156() { - Token xsp; - xsp = jj_scanpos; - if (jj_scan_token(86)) { - jj_scanpos = xsp; - if (jj_scan_token(89)) return true; - } + if (jj_scan_token(A)) return true; + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_44()) return true; + if (jj_scan_token(RBRACKET)) return true; return false; } - static private boolean jj_3R_43() + static private boolean jj_3R_49() { if (jj_scan_token(OR)) return true; if (jj_scan_token(OR)) return true; - if (jj_3R_49()) return true; + if (jj_3R_55()) return true; return false; } - static private boolean jj_3R_158() + static private boolean jj_3R_164() { if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_161()) return true; + if (jj_3R_167()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } @@ -4148,285 +4305,267 @@ static private boolean jj_3_10() return false; } - static private boolean jj_3R_218() - { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_217()) return true; - return false; - } - - static private boolean jj_3R_214() - { - if (jj_3R_217()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_218()) { jj_scanpos = xsp; break; } - } - return false; - } - - static private boolean jj_3R_210() - { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_214()) jj_scanpos = xsp; - return false; - } - static private boolean jj_3_2() { - if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_29()) return true; - if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_31()) return true; if (jj_scan_token(COLON)) return true; return false; } - static private boolean jj_3R_143() + static private boolean jj_3R_149() { - if (jj_3R_29()) return true; + if (jj_3R_30()) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_158()) jj_scanpos = xsp; - return false; - } - - static private boolean jj_3R_209() - { - if (jj_scan_token(TIMES)) return true; + if (jj_3R_164()) jj_scanpos = xsp; return false; } - static private boolean jj_3R_205() + static private boolean jj_3R_155() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_209()) { - jj_scanpos = xsp; - if (jj_3R_210()) return true; - } + if (jj_scan_token(E)) return true; + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_44()) return true; + if (jj_scan_token(RBRACKET)) return true; return false; } - static private boolean jj_3R_59() + static private boolean jj_3R_65() { if (jj_scan_token(OR)) return true; if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_29()) return true; + if (jj_3R_30()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_70()) { jj_scanpos = xsp; break; } + if (jj_3R_76()) { jj_scanpos = xsp; break; } } if (jj_scan_token(RBRACKET)) return true; if (jj_scan_token(OR)) return true; - if (jj_3R_58()) return true; + if (jj_3R_64()) return true; return false; } - static private boolean jj_3R_49() + static private boolean jj_3R_55() { - if (jj_3R_58()) return true; + if (jj_3R_64()) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_59()) jj_scanpos = xsp; + if (jj_3R_65()) jj_scanpos = xsp; return false; } - static private boolean jj_3R_141() + static private boolean jj_3_21() { - if (jj_3R_153()) return true; + if (jj_scan_token(C)) return true; + if (jj_scan_token(LE)) return true; return false; } - static private boolean jj_3R_140() + static private boolean jj_3R_147() { - if (jj_3R_152()) return true; + if (jj_3R_159()) return true; return false; } - static private boolean jj_3R_177() + static private boolean jj_3R_146() { - if (jj_3R_146()) return true; + if (jj_3R_158()) return true; return false; } - static private boolean jj_3R_139() + static private boolean jj_3R_210() { - if (jj_3R_151()) return true; + if (jj_3R_44()) return true; return false; } - static private boolean jj_3R_206() + static private boolean jj_3R_145() { - if (jj_3R_147()) return true; + if (jj_3R_157()) return true; return false; } - static private boolean jj_3R_138() + static private boolean jj_3_20() { - if (jj_3R_150()) return true; + if (jj_3R_39()) return true; return false; } - static private boolean jj_3R_176() + static private boolean jj_3R_144() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_206()) { - jj_scanpos = xsp; - if (jj_3R_207()) return true; - } + if (jj_3R_156()) return true; return false; } - static private boolean jj_3R_175() + static private boolean jj_3R_209() { - if (jj_scan_token(DLBRACKET)) return true; - if (jj_3R_205()) return true; - if (jj_scan_token(DRBRACKET)) return true; + if (jj_scan_token(I)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_3R_44()) return true; return false; } - static private boolean jj_3R_137() + static private boolean jj_3_19() { - if (jj_3R_149()) return true; + if (jj_3R_31()) return true; return false; } - static private boolean jj_3R_127() + static private boolean jj_3R_208() + { + if (jj_scan_token(C)) return true; + return false; + } + + static private boolean jj_3R_143() + { + if (jj_3R_155()) return true; + return false; + } + + static private boolean jj_3R_207() + { + if (jj_scan_token(C)) return true; + if (jj_scan_token(LE)) return true; + if (jj_3R_44()) return true; + return false; + } + + static private boolean jj_3R_133() { if (jj_scan_token(DIVIDE)) return true; return false; } - static private boolean jj_3R_216() + static private boolean jj_3R_142() { - if (jj_3R_38()) return true; + if (jj_3R_154()) return true; return false; } - static private boolean jj_3R_174() + static private boolean jj_3R_206() { - if (jj_scan_token(DLT)) return true; - if (jj_3R_205()) return true; - if (jj_scan_token(DGT)) return true; + if (jj_scan_token(S)) return true; return false; } - static private boolean jj_3R_136() + static private boolean jj_3R_180() { - if (jj_3R_148()) return true; + if (jj_3R_53()) return true; return false; } - static private boolean jj_3R_135() + static private boolean jj_3R_141() { - if (jj_3R_33()) return true; + if (jj_3R_39()) return true; return false; } - static private boolean jj_3R_134() + static private boolean jj_3R_140() { - if (jj_3R_147()) return true; + if (jj_3R_153()) return true; return false; } - static private boolean jj_3R_151() + static private boolean jj_3R_205() + { + if (jj_3R_39()) return true; + return false; + } + + static private boolean jj_3R_226() + { + if (jj_3R_31()) return true; + return false; + } + + static private boolean jj_3R_139() + { + if (jj_3R_152()) return true; + return false; + } + + static private boolean jj_3R_179() { Token xsp; xsp = jj_scanpos; - if (jj_3R_174()) { + if (jj_3R_205()) { jj_scanpos = xsp; - if (jj_3R_175()) return true; - } - xsp = jj_scanpos; - if (jj_3R_176()) { + if (jj_3R_206()) { + jj_scanpos = xsp; + if (jj_3R_207()) { + jj_scanpos = xsp; + if (jj_3R_208()) { jj_scanpos = xsp; - if (jj_3R_177()) return true; + if (jj_3R_209()) { + jj_scanpos = xsp; + if (jj_3R_210()) return true; + } + } + } + } } return false; } - static private boolean jj_3R_133() - { - if (jj_3R_146()) return true; - return false; - } - - static private boolean jj_3R_132() + static private boolean jj_3R_138() { - if (jj_3R_145()) return true; + if (jj_3R_151()) return true; return false; } - static private boolean jj_3R_42() + static private boolean jj_3R_48() { - if (jj_3R_49()) return true; + if (jj_3R_55()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_50()) { jj_scanpos = xsp; break; } + if (jj_3R_56()) { jj_scanpos = xsp; break; } } return false; } - static private boolean jj_3R_131() + static private boolean jj_3_18() { - if (jj_3R_144()) return true; + if (jj_3R_31()) return true; return false; } - static private boolean jj_3R_130() + static private boolean jj_3R_137() { - if (jj_3R_143()) return true; + if (jj_3R_150()) return true; return false; } - static private boolean jj_3R_129() + static private boolean jj_3R_136() { - if (jj_3R_142()) return true; + if (jj_3R_149()) return true; return false; } - static private boolean jj_3R_212() + static private boolean jj_3R_135() { - if (jj_3R_38()) return true; + if (jj_3R_148()) return true; return false; } - static private boolean jj_3R_123() + static private boolean jj_3R_129() { if (jj_scan_token(MINUS)) return true; return false; } - static private boolean jj_3R_150() + static private boolean jj_3R_220() { - if (jj_scan_token(A)) return true; - if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_38()) return true; - if (jj_scan_token(RBRACKET)) return true; + if (jj_3R_31()) return true; return false; } - static private boolean jj_3R_128() + static private boolean jj_3R_134() { Token xsp; xsp = jj_scanpos; - if (jj_3R_129()) { - jj_scanpos = xsp; - if (jj_3R_130()) { - jj_scanpos = xsp; - if (jj_3R_131()) { - jj_scanpos = xsp; - if (jj_3R_132()) { - jj_scanpos = xsp; - if (jj_3R_133()) { - jj_scanpos = xsp; - if (jj_3R_134()) { - jj_scanpos = xsp; if (jj_3R_135()) { jj_scanpos = xsp; if (jj_3R_136()) { @@ -4439,7 +4578,19 @@ static private boolean jj_3R_128() jj_scanpos = xsp; if (jj_3R_140()) { jj_scanpos = xsp; - if (jj_3R_141()) return true; + if (jj_3R_141()) { + jj_scanpos = xsp; + if (jj_3R_142()) { + jj_scanpos = xsp; + if (jj_3R_143()) { + jj_scanpos = xsp; + if (jj_3R_144()) { + jj_scanpos = xsp; + if (jj_3R_145()) { + jj_scanpos = xsp; + if (jj_3R_146()) { + jj_scanpos = xsp; + if (jj_3R_147()) return true; } } } @@ -4455,201 +4606,213 @@ static private boolean jj_3R_128() return false; } - static private boolean jj_3R_125() + static private boolean jj_3R_131() { - if (jj_3R_128()) return true; + if (jj_3R_134()) return true; return false; } - static private boolean jj_3R_124() + static private boolean jj_3R_222() { - if (jj_scan_token(MINUS)) return true; - if (jj_3R_120()) return true; + if (jj_scan_token(DIVIDE)) return true; + if (jj_scan_token(LBRACE)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_226()) { + jj_scanpos = xsp; + if (jj_3R_227()) return true; + } + if (jj_scan_token(RBRACE)) return true; return false; } - static private boolean jj_3R_35() + static private boolean jj_3R_130() { - if (jj_3R_42()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_43()) { jj_scanpos = xsp; break; } - } + if (jj_scan_token(MINUS)) return true; + if (jj_3R_126()) return true; return false; } - static private boolean jj_3R_120() + static private boolean jj_3R_215() { + if (jj_scan_token(LBRACE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_124()) { + if (jj_3R_220()) { jj_scanpos = xsp; - if (jj_3R_125()) return true; + if (jj_3R_221()) return true; } + if (jj_scan_token(RBRACE)) return true; + xsp = jj_scanpos; + if (jj_3R_222()) jj_scanpos = xsp; return false; } - static private boolean jj_3R_149() + static private boolean jj_3R_41() { - if (jj_scan_token(E)) return true; - if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_38()) return true; - if (jj_scan_token(RBRACKET)) return true; + if (jj_3R_48()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_49()) { jj_scanpos = xsp; break; } + } return false; } static private boolean jj_3R_126() + { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_130()) { + jj_scanpos = xsp; + if (jj_3R_131()) return true; + } + return false; + } + + static private boolean jj_3R_132() { if (jj_scan_token(TIMES)) return true; return false; } - static private boolean jj_3R_31() + static private boolean jj_3R_34() { - if (jj_3R_35()) return true; + if (jj_3R_41()) return true; return false; } - static private boolean jj_3R_121() + static private boolean jj_3R_127() { Token xsp; xsp = jj_scanpos; - if (jj_3R_126()) { + if (jj_3R_132()) { jj_scanpos = xsp; - if (jj_3R_127()) return true; + if (jj_3R_133()) return true; } - if (jj_3R_120()) return true; + if (jj_3R_126()) return true; return false; } static private boolean jj_3_7() { - if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_29()) return true; - if (jj_scan_token(DQUOTE)) return true; if (jj_3R_31()) return true; + if (jj_3R_34()) return true; return false; } - static private boolean jj_3_18() - { - if (jj_scan_token(C)) return true; - if (jj_scan_token(LE)) return true; - return false; - } - - static private boolean jj_3R_204() - { - if (jj_3R_38()) return true; - return false; - } - - static private boolean jj_3R_116() + static private boolean jj_3R_122() { - if (jj_3R_120()) return true; + if (jj_3R_126()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_121()) { jj_scanpos = xsp; break; } + if (jj_3R_127()) { jj_scanpos = xsp; break; } } return false; } - static private boolean jj_3_17() + static private boolean jj_3R_201() { - if (jj_3R_33()) return true; + if (jj_3R_51()) return true; + if (jj_3R_44()) return true; return false; } - static private boolean jj_3R_203() + static private boolean jj_3R_128() { - if (jj_scan_token(I)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_3R_38()) return true; + if (jj_scan_token(PLUS)) return true; return false; } - static private boolean jj_3_16() + static private boolean jj_3R_200() { - if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_215()) return true; return false; } - static private boolean jj_3R_202() + static private boolean jj_3R_199() { - if (jj_scan_token(C)) return true; + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_35()) return true; + if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_201() + static private boolean jj_3R_204() { - if (jj_scan_token(C)) return true; - if (jj_scan_token(LE)) return true; - if (jj_3R_38()) return true; + if (jj_scan_token(MAX)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_122() + static private boolean jj_3R_178() { - if (jj_scan_token(PLUS)) return true; + if (jj_scan_token(RMAX)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_200() + static private boolean jj_3_1() { - if (jj_scan_token(S)) return true; + if (jj_scan_token(MODULE)) return true; + if (jj_3R_30()) return true; + if (jj_scan_token(EQ)) return true; return false; } - static private boolean jj_3R_173() + static private boolean jj_3R_123() { - if (jj_3R_47()) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_128()) { + jj_scanpos = xsp; + if (jj_3R_129()) return true; + } + if (jj_3R_122()) return true; return false; } - static private boolean jj_3_1() + static private boolean jj_3R_203() { - if (jj_scan_token(MODULE)) return true; - if (jj_3R_29()) return true; + if (jj_scan_token(MIN)) return true; if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_117() + static private boolean jj_3R_177() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_122()) { - jj_scanpos = xsp; - if (jj_3R_123()) return true; - } - if (jj_3R_116()) return true; + if (jj_scan_token(RMIN)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_199() + static private boolean jj_3R_202() { - if (jj_3R_33()) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_215() + static private boolean jj_3R_45() { - if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_29()) return true; - if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_53()) return true; return false; } - static private boolean jj_3R_172() + static private boolean jj_3R_176() { + if (jj_scan_token(R)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_199()) { - jj_scanpos = xsp; - if (jj_3R_200()) { - jj_scanpos = xsp; + if (jj_3R_199()) jj_scanpos = xsp; + xsp = jj_scanpos; + if (jj_3R_200()) jj_scanpos = xsp; + xsp = jj_scanpos; if (jj_3R_201()) { jj_scanpos = xsp; if (jj_3R_202()) { @@ -4660,615 +4823,690 @@ static private boolean jj_3R_172() } } } - } - } return false; } - static private boolean jj_3_15() + static private boolean jj_3R_119() { - if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_122()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_123()) { jj_scanpos = xsp; break; } + } return false; } - static private boolean jj_3R_113() + static private boolean jj_3R_154() { - if (jj_3R_116()) return true; Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_117()) { jj_scanpos = xsp; break; } + xsp = jj_scanpos; + if (jj_3R_176()) { + jj_scanpos = xsp; + if (jj_3R_177()) { + jj_scanpos = xsp; + if (jj_3R_178()) return true; + } } + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_179()) return true; + xsp = jj_scanpos; + if (jj_3R_180()) jj_scanpos = xsp; + if (jj_scan_token(RBRACKET)) return true; return false; } static private boolean jj_3_6() { - if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_31()) return true; return false; } - static private boolean jj_3R_211() + static private boolean jj_3R_120() { - if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_29()) return true; - if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_51()) return true; + if (jj_3R_119()) return true; return false; } - static private boolean jj_3R_213() + static private boolean jj_3R_117() { - if (jj_scan_token(DIVIDE)) return true; - if (jj_scan_token(LBRACE)) return true; + if (jj_3R_119()) return true; Token xsp; - xsp = jj_scanpos; - if (jj_3R_215()) { - jj_scanpos = xsp; - if (jj_3R_216()) return true; + while (true) { + xsp = jj_scanpos; + if (jj_3R_120()) { jj_scanpos = xsp; break; } } - if (jj_scan_token(RBRACE)) return true; return false; } - static private boolean jj_3R_114() + static private boolean jj_3R_118() { - if (jj_3R_45()) return true; - if (jj_3R_113()) return true; + if (jj_3R_121()) return true; + if (jj_3R_117()) return true; return false; } - static private boolean jj_3R_208() + static private boolean jj_3R_50() { - if (jj_scan_token(LBRACE)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_211()) { - jj_scanpos = xsp; - if (jj_3R_212()) return true; - } - if (jj_scan_token(RBRACE)) return true; - xsp = jj_scanpos; - if (jj_3R_213()) jj_scanpos = xsp; + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_35()) return true; + if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_111() + static private boolean jj_3R_43() + { + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; + return false; + } + + static private boolean jj_3R_116() { - if (jj_3R_113()) return true; + if (jj_3R_117()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_114()) { jj_scanpos = xsp; break; } + if (jj_3R_118()) { jj_scanpos = xsp; break; } } return false; } - static private boolean jj_3R_112() + static private boolean jj_3R_42() { - if (jj_3R_115()) return true; - if (jj_3R_111()) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_50()) jj_scanpos = xsp; + if (jj_3R_51()) return true; + if (jj_3R_44()) return true; return false; } - static private boolean jj_3R_110() + static private boolean jj_3R_115() { - if (jj_3R_111()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_112()) { jj_scanpos = xsp; break; } - } + if (jj_3R_116()) return true; return false; } - static private boolean jj_3R_109() + static private boolean jj_3R_114() { - if (jj_3R_110()) return true; + if (jj_scan_token(NOT)) return true; + if (jj_3R_112()) return true; return false; } - static private boolean jj_3R_108() + static private boolean jj_3R_60() { - if (jj_scan_token(NOT)) return true; - if (jj_3R_106()) return true; + if (jj_scan_token(LE)) return true; return false; } - static private boolean jj_3R_101() + static private boolean jj_3R_107() { - if (jj_3R_38()) return true; + if (jj_3R_44()) return true; return false; } - static private boolean jj_3R_99() + static private boolean jj_3R_59() { - if (jj_3R_38()) return true; + if (jj_scan_token(GE)) return true; return false; } - static private boolean jj_3R_97() + static private boolean jj_3R_105() { - if (jj_3R_38()) return true; + if (jj_3R_44()) return true; return false; } - static private boolean jj_3R_95() + static private boolean jj_3R_58() { - if (jj_3R_38()) return true; + if (jj_scan_token(LT)) return true; return false; } - static private boolean jj_3R_195() + static private boolean jj_3R_103() { - if (jj_3R_45()) return true; - if (jj_3R_38()) return true; + if (jj_3R_44()) return true; return false; } - static private boolean jj_3R_194() + static private boolean jj_3R_39() { - if (jj_3R_208()) return true; + if (jj_scan_token(S)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_42()) { + jj_scanpos = xsp; + if (jj_3R_43()) return true; + } + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_44()) return true; + xsp = jj_scanpos; + if (jj_3R_45()) jj_scanpos = xsp; + if (jj_scan_token(RBRACKET)) return true; return false; } - static private boolean jj_3R_193() + static private boolean jj_3R_57() { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_32()) return true; - if (jj_scan_token(RPARENTH)) return true; + if (jj_scan_token(GT)) return true; return false; } - static private boolean jj_3R_41() + static private boolean jj_3R_51() { - if (jj_scan_token(AND)) return true; - if (jj_3R_40()) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_57()) { + jj_scanpos = xsp; + if (jj_3R_58()) { + jj_scanpos = xsp; + if (jj_3R_59()) { + jj_scanpos = xsp; + if (jj_3R_60()) return true; + } + } + } return false; } - static private boolean jj_3R_198() + static private boolean jj_3R_101() { - if (jj_scan_token(MAX)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + if (jj_3R_44()) return true; return false; } - static private boolean jj_3R_171() + static private boolean jj_3R_47() { - if (jj_scan_token(RMAX)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + if (jj_scan_token(AND)) return true; + if (jj_3R_46()) return true; return false; } - static private boolean jj_3R_197() + static private boolean jj_3R_112() { - if (jj_scan_token(MIN)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_114()) { + jj_scanpos = xsp; + if (jj_3R_115()) return true; + } return false; } - static private boolean jj_3R_170() + static private boolean jj_3R_125() { - if (jj_scan_token(RMIN)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + if (jj_scan_token(NE)) return true; return false; } - static private boolean jj_3R_106() + static private boolean jj_3R_121() { Token xsp; xsp = jj_scanpos; - if (jj_3R_108()) { + if (jj_3R_124()) { jj_scanpos = xsp; - if (jj_3R_109()) return true; + if (jj_3R_125()) return true; } return false; } - static private boolean jj_3R_196() + static private boolean jj_3R_124() { if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_39() + static private boolean jj_3R_73() { - if (jj_3R_47()) return true; + if (jj_scan_token(MAX)) return true; return false; } - static private boolean jj_3R_169() + static private boolean jj_3R_72() { - if (jj_scan_token(R)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_193()) jj_scanpos = xsp; - xsp = jj_scanpos; - if (jj_3R_194()) jj_scanpos = xsp; - xsp = jj_scanpos; - if (jj_3R_195()) { - jj_scanpos = xsp; - if (jj_3R_196()) { - jj_scanpos = xsp; - if (jj_3R_197()) { - jj_scanpos = xsp; - if (jj_3R_198()) return true; - } - } - } + if (jj_scan_token(MIN)) return true; return false; } - static private boolean jj_3R_107() + static private boolean jj_3R_113() { if (jj_scan_token(AND)) return true; - if (jj_3R_106()) return true; + if (jj_3R_112()) return true; return false; } - static private boolean jj_3R_148() + static private boolean jj_3R_46() + { + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_54()) return true; + if (jj_scan_token(EQ)) return true; + if (jj_3R_44()) return true; + if (jj_scan_token(RPARENTH)) return true; + return false; + } + + static private boolean jj_3R_110() { + if (jj_3R_112()) return true; Token xsp; - xsp = jj_scanpos; - if (jj_3R_169()) { - jj_scanpos = xsp; - if (jj_3R_170()) { - jj_scanpos = xsp; - if (jj_3R_171()) return true; - } + while (true) { + xsp = jj_scanpos; + if (jj_3R_113()) { jj_scanpos = xsp; break; } } - if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_172()) return true; - xsp = jj_scanpos; - if (jj_3R_173()) jj_scanpos = xsp; - if (jj_scan_token(RBRACKET)) return true; return false; } - static private boolean jj_3R_40() + static private boolean jj_3R_63() { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_48()) return true; - if (jj_scan_token(EQ)) return true; - if (jj_3R_38()) return true; - if (jj_scan_token(RPARENTH)) return true; + if (jj_scan_token(LBRACE)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_72()) { + jj_scanpos = xsp; + if (jj_3R_73()) return true; + } + if (jj_scan_token(RBRACE)) return true; return false; } - static private boolean jj_3R_104() + static private boolean jj_3R_53() { - if (jj_3R_106()) return true; + if (jj_scan_token(LBRACE)) return true; + if (jj_3R_44()) return true; + if (jj_scan_token(RBRACE)) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_107()) { jj_scanpos = xsp; break; } + if (jj_3R_63()) { jj_scanpos = xsp; break; } } return false; } - static private boolean jj_3R_105() + static private boolean jj_3R_54() + { + if (jj_scan_token(REG_IDENTPRIME)) return true; + return false; + } + + static private boolean jj_3R_111() { if (jj_scan_token(OR)) return true; - if (jj_3R_104()) return true; + if (jj_3R_110()) return true; return false; } - static private boolean jj_3R_34() + static private boolean jj_3R_40() { - if (jj_3R_40()) return true; + if (jj_3R_46()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_41()) { jj_scanpos = xsp; break; } + if (jj_3R_47()) { jj_scanpos = xsp; break; } } return false; } static private boolean jj_3_5() { - if (jj_3R_30()) return true; + if (jj_3R_33()) return true; return false; } - static private boolean jj_3R_102() + static private boolean jj_3R_108() { - if (jj_3R_104()) return true; + if (jj_3R_110()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_105()) { jj_scanpos = xsp; break; } + if (jj_3R_111()) { jj_scanpos = xsp; break; } } return false; } - static private boolean jj_3R_30() + static private boolean jj_3R_33() { Token xsp; xsp = jj_scanpos; - if (jj_3R_34()) { + if (jj_3R_40()) { jj_scanpos = xsp; if (jj_scan_token(49)) return true; } return false; } - static private boolean jj_3R_103() + static private boolean jj_3R_219() + { + if (jj_scan_token(COMMA)) return true; + if (jj_3R_31()) return true; + if (jj_scan_token(RENAME)) return true; + if (jj_3R_44()) return true; + return false; + } + + static private boolean jj_3R_214() + { + if (jj_3R_218()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_219()) { jj_scanpos = xsp; break; } + } + return false; + } + + static private boolean jj_3R_109() { if (jj_scan_token(IFF)) return true; - if (jj_3R_102()) return true; + if (jj_3R_108()) return true; return false; } - static private boolean jj_3R_92() + static private boolean jj_3R_98() { - if (jj_3R_102()) return true; + if (jj_3R_108()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_103()) { jj_scanpos = xsp; break; } + if (jj_3R_109()) { jj_scanpos = xsp; break; } } return false; } - static private boolean jj_3R_37() + static private boolean jj_3R_38() { - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_44() + static private boolean jj_3R_225() { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_32()) return true; - if (jj_scan_token(RPARENTH)) return true; + if (jj_scan_token(REG_QUOTED_STRING)) return true; return false; } - static private boolean jj_3R_36() + static private boolean jj_3R_224() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_44()) jj_scanpos = xsp; - if (jj_3R_45()) return true; - if (jj_3R_38()) return true; + if (jj_scan_token(REG_QUOTED_IDENT)) return true; return false; } - static private boolean jj_3R_93() + static private boolean jj_3R_198() + { + if (jj_3R_44()) return true; + return false; + } + + static private boolean jj_3R_99() { if (jj_scan_token(IMPLIES)) return true; - if (jj_3R_92()) return true; + if (jj_3R_98()) return true; return false; } - static private boolean jj_3R_82() + static private boolean jj_3R_37() + { + return false; + } + + static private boolean jj_3R_88() { - if (jj_3R_92()) return true; + if (jj_3R_98()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_93()) { jj_scanpos = xsp; break; } + if (jj_3R_99()) { jj_scanpos = xsp; break; } } return false; } - static private boolean jj_3R_33() + static private boolean jj_3R_218() { - if (jj_scan_token(S)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_36()) { + if (jj_3R_224()) { jj_scanpos = xsp; - if (jj_3R_37()) return true; + if (jj_3R_225()) return true; } - if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_38()) return true; - xsp = jj_scanpos; - if (jj_3R_39()) jj_scanpos = xsp; - if (jj_scan_token(RBRACKET)) return true; return false; } - static private boolean jj_3R_83() + static private boolean jj_3_17() + { + jj_lookingAhead = true; + jj_semLA = getToken(1).kind==REG_IDENT + && getToken(2).kind==COLON; + jj_lookingAhead = false; + if (!jj_semLA || jj_3R_38()) return true; + if (jj_3R_35()) return true; + return false; + } + + static private boolean jj_3R_89() { if (jj_scan_token(QMARK)) return true; - if (jj_3R_82()) return true; + if (jj_3R_88()) return true; if (jj_scan_token(COLON)) return true; - if (jj_3R_75()) return true; + if (jj_3R_81()) return true; + return false; + } + + static private boolean jj_3R_36() + { return false; } static private boolean jj_3_14() { - if (jj_3R_32()) return true; + if (jj_3R_35()) return true; if (jj_scan_token(LPARENTH)) return true; return false; } static private boolean jj_3_13() { - if (jj_3R_32()) return true; + if (jj_3R_35()) return true; if (jj_scan_token(LPARENTH)) return true; return false; } static private boolean jj_3_12() { - if (jj_3R_32()) return true; + if (jj_3R_35()) return true; if (jj_scan_token(LPARENTH)) return true; return false; } static private boolean jj_3_11() { - if (jj_3R_32()) return true; + if (jj_3R_35()) return true; if (jj_scan_token(LPARENTH)) return true; return false; } - static private boolean jj_3R_168() + static private boolean jj_3_16() { - if (jj_3R_47()) return true; + jj_lookingAhead = true; + jj_semLA = getToken(1).kind==NOT + && getToken(2).kind==REG_IDENT + && getToken(2).image.equals("HOA") + && getToken(3).kind==COLON; + jj_lookingAhead = false; + if (!jj_semLA || jj_3R_37()) return true; + if (jj_scan_token(NOT)) return true; + if (jj_3R_35()) return true; + if (jj_scan_token(COLON)) return true; + if (jj_scan_token(LBRACE)) return true; + if (jj_3R_214()) return true; + if (jj_scan_token(RBRACE)) return true; return false; } - static private boolean jj_3R_67() + static private boolean jj_3R_32() { - if (jj_scan_token(MAX)) return true; + if (jj_3R_31()) return true; return false; } - static private boolean jj_3R_66() + static private boolean jj_3R_81() { - if (jj_scan_token(MIN)) return true; + if (jj_3R_88()) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_89()) jj_scanpos = xsp; return false; } - static private boolean jj_3R_75() + static private boolean jj_3R_106() { - if (jj_3R_82()) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_83()) jj_scanpos = xsp; + if (jj_3R_35()) return true; return false; } - static private boolean jj_3R_100() + static private boolean jj_3_15() { - if (jj_3R_32()) return true; + jj_lookingAhead = true; + jj_semLA = getToken(1).kind==REG_IDENT + && getToken(1).image.equals("HOA") + && getToken(2).kind==COLON; + jj_lookingAhead = false; + if (!jj_semLA || jj_3R_36()) return true; + if (jj_3R_35()) return true; + if (jj_scan_token(COLON)) return true; + if (jj_scan_token(LBRACE)) return true; + if (jj_3R_214()) return true; + if (jj_scan_token(RBRACE)) return true; return false; } - static private boolean jj_3R_98() + static private boolean jj_3R_104() { - if (jj_3R_32()) return true; + if (jj_3R_35()) return true; return false; } - static private boolean jj_3R_96() + static private boolean jj_3R_102() { - if (jj_3R_32()) return true; + if (jj_3R_35()) return true; return false; } - static private boolean jj_3R_94() + static private boolean jj_3R_100() { - if (jj_3R_32()) return true; + if (jj_3R_35()) return true; return false; } - static private boolean jj_3R_57() + static private boolean jj_3R_174() { - if (jj_scan_token(LBRACE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_66()) { + if (jj_3_15()) { jj_scanpos = xsp; - if (jj_3R_67()) return true; + if (jj_3_16()) { + jj_scanpos = xsp; + if (jj_3_17()) { + jj_scanpos = xsp; + if (jj_3R_198()) return true; + } + } } - if (jj_scan_token(RBRACE)) return true; return false; } - static private boolean jj_3R_89() + static private boolean jj_3R_189() + { + if (jj_scan_token(OR)) return true; + return false; + } + + static private boolean jj_3R_95() { if (jj_scan_token(EQ)) return true; - if (jj_3R_38()) return true; + if (jj_3R_44()) return true; return false; } - static private boolean jj_3R_88() + static private boolean jj_3R_94() { if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_38()) return true; + if (jj_3R_44()) return true; if (jj_scan_token(COMMA)) return true; - if (jj_3R_38()) return true; + if (jj_3R_44()) return true; if (jj_scan_token(RBRACKET)) return true; return false; } - static private boolean jj_3R_47() + static private boolean jj_3R_35() { - if (jj_scan_token(LBRACE)) return true; - if (jj_3R_38()) return true; - if (jj_scan_token(RBRACE)) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_57()) { jj_scanpos = xsp; break; } - } + if (jj_3R_30()) return true; return false; } - static private boolean jj_3R_87() + static private boolean jj_3R_93() { if (jj_scan_token(GT)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_100()) { + if (jj_3R_106()) { jj_scanpos = xsp; - if (jj_3R_101()) return true; + if (jj_3R_107()) return true; } return false; } - static private boolean jj_3R_86() + static private boolean jj_3R_92() { if (jj_scan_token(GE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_98()) { + if (jj_3R_104()) { jj_scanpos = xsp; - if (jj_3R_99()) return true; + if (jj_3R_105()) return true; } return false; } - static private boolean jj_3R_85() + static private boolean jj_3R_91() { if (jj_scan_token(LT)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_96()) { + if (jj_3R_102()) { jj_scanpos = xsp; - if (jj_3R_97()) return true; + if (jj_3R_103()) return true; } return false; } - static private boolean jj_3R_84() + static private boolean jj_3R_90() { if (jj_scan_token(LE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_94()) { + if (jj_3R_100()) { jj_scanpos = xsp; - if (jj_3R_95()) return true; + if (jj_3R_101()) return true; } return false; } - static private boolean jj_3R_76() + static private boolean jj_3R_82() { Token xsp; xsp = jj_scanpos; - if (jj_3R_84()) { + if (jj_3R_90()) { jj_scanpos = xsp; - if (jj_3R_85()) { + if (jj_3R_91()) { jj_scanpos = xsp; - if (jj_3R_86()) { + if (jj_3R_92()) { jj_scanpos = xsp; - if (jj_3R_87()) { + if (jj_3R_93()) { jj_scanpos = xsp; - if (jj_3R_88()) { + if (jj_3R_94()) { jj_scanpos = xsp; - if (jj_3R_89()) return true; + if (jj_3R_95()) return true; } } } @@ -5277,118 +5515,107 @@ static private boolean jj_3R_76() return false; } - static private boolean jj_3R_61() + static private boolean jj_3R_67() { - if (jj_3R_75()) return true; + if (jj_3R_81()) return true; return false; } - static private boolean jj_3R_74() + static private boolean jj_3R_80() { - if (jj_3R_76()) return true; + if (jj_3R_82()) return true; return false; } - static private boolean jj_3R_73() + static private boolean jj_3R_79() { if (jj_scan_token(G)) return true; return false; } - static private boolean jj_3R_72() + static private boolean jj_3R_78() { if (jj_scan_token(F)) return true; return false; } - static private boolean jj_3R_71() + static private boolean jj_3R_77() { if (jj_scan_token(X)) return true; return false; } - static private boolean jj_3R_60() + static private boolean jj_3R_31() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_71()) { - jj_scanpos = xsp; - if (jj_3R_72()) { - jj_scanpos = xsp; - if (jj_3R_73()) return true; - } - } - xsp = jj_scanpos; - if (jj_3R_74()) jj_scanpos = xsp; - if (jj_3R_55()) return true; + if (jj_scan_token(REG_QUOTED_IDENT)) return true; return false; } - static private boolean jj_3R_54() + static private boolean jj_3R_188() { - if (jj_scan_token(LE)) return true; + if (jj_scan_token(AND)) return true; return false; } - static private boolean jj_3R_189() + static private boolean jj_3R_186() { - if (jj_3R_45()) return true; - if (jj_3R_38()) return true; + if (jj_scan_token(MAX)) return true; return false; } - static private boolean jj_3R_188() + static private boolean jj_3R_66() { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_32()) return true; - if (jj_scan_token(RPARENTH)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_77()) { + jj_scanpos = xsp; + if (jj_3R_78()) { + jj_scanpos = xsp; + if (jj_3R_79()) return true; + } + } + xsp = jj_scanpos; + if (jj_3R_80()) jj_scanpos = xsp; + if (jj_3R_61()) return true; return false; } - static private boolean jj_3R_53() + static private boolean jj_3R_194() { - if (jj_scan_token(GE)) return true; + if (jj_3R_51()) return true; + if (jj_3R_44()) return true; return false; } - static private boolean jj_3R_52() + static private boolean jj_3R_193() { - if (jj_scan_token(LT)) return true; + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_35()) return true; + if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_51() + static private boolean jj_3R_30() { - if (jj_scan_token(GT)) return true; + if (jj_scan_token(REG_IDENT)) return true; return false; } - static private boolean jj_3R_45() + static private boolean jj_3R_197() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_51()) { - jj_scanpos = xsp; - if (jj_3R_52()) { - jj_scanpos = xsp; - if (jj_3R_53()) { - jj_scanpos = xsp; - if (jj_3R_54()) return true; - } - } - } + if (jj_scan_token(MAX)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_192() + static private boolean jj_3R_175() { - if (jj_scan_token(MAX)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + if (jj_3R_53()) return true; return false; } - static private boolean jj_3R_191() + static private boolean jj_3R_196() { if (jj_scan_token(MIN)) return true; if (jj_scan_token(EQ)) return true; @@ -5396,14 +5623,14 @@ static private boolean jj_3R_191() return false; } - static private boolean jj_3R_190() + static private boolean jj_3R_195() { if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_167() + static private boolean jj_3R_173() { if (jj_scan_token(PMAX)) return true; if (jj_scan_token(EQ)) return true; @@ -5411,18 +5638,18 @@ static private boolean jj_3R_167() return false; } - static private boolean jj_3R_55() + static private boolean jj_3R_61() { Token xsp; xsp = jj_scanpos; - if (jj_3R_60()) { + if (jj_3R_66()) { jj_scanpos = xsp; - if (jj_3R_61()) return true; + if (jj_3R_67()) return true; } return false; } - static private boolean jj_3R_166() + static private boolean jj_3R_172() { if (jj_scan_token(PMIN)) return true; if (jj_scan_token(EQ)) return true; @@ -5430,119 +5657,160 @@ static private boolean jj_3R_166() return false; } - static private boolean jj_3R_119() - { - if (jj_scan_token(NE)) return true; - return false; - } - - static private boolean jj_3R_115() - { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_118()) { - jj_scanpos = xsp; - if (jj_3R_119()) return true; - } - return false; - } - - static private boolean jj_3R_118() + static private boolean jj_3R_71() { - if (jj_scan_token(EQ)) return true; + if (jj_3R_82()) return true; return false; } - static private boolean jj_3R_65() + static private boolean jj_3R_70() { - if (jj_3R_76()) return true; + if (jj_scan_token(R)) return true; return false; } - static private boolean jj_3R_64() + static private boolean jj_3R_69() { - if (jj_scan_token(R)) return true; + if (jj_scan_token(W)) return true; return false; } - static private boolean jj_3R_63() + static private boolean jj_3R_191() { - if (jj_scan_token(W)) return true; + if (jj_scan_token(COMMA)) return true; + if (jj_3R_44()) return true; return false; } - static private boolean jj_3R_165() + static private boolean jj_3R_171() { if (jj_scan_token(P)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_188()) jj_scanpos = xsp; + if (jj_3R_193()) jj_scanpos = xsp; xsp = jj_scanpos; - if (jj_3R_189()) { + if (jj_3R_194()) { jj_scanpos = xsp; - if (jj_3R_190()) { + if (jj_3R_195()) { jj_scanpos = xsp; - if (jj_3R_191()) { + if (jj_3R_196()) { jj_scanpos = xsp; - if (jj_3R_192()) return true; + if (jj_3R_197()) return true; } } } return false; } - static private boolean jj_3R_62() + static private boolean jj_3R_68() { if (jj_scan_token(U)) return true; return false; } - static private boolean jj_3R_147() + static private boolean jj_3R_153() { Token xsp; xsp = jj_scanpos; - if (jj_3R_165()) { + if (jj_3R_171()) { jj_scanpos = xsp; - if (jj_3R_166()) { + if (jj_3R_172()) { jj_scanpos = xsp; - if (jj_3R_167()) return true; + if (jj_3R_173()) return true; } } if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_38()) return true; + if (jj_3R_174()) return true; xsp = jj_scanpos; - if (jj_3R_168()) jj_scanpos = xsp; + if (jj_3R_175()) jj_scanpos = xsp; if (jj_scan_token(RBRACKET)) return true; return false; } - static private boolean jj_3R_56() + static private boolean jj_3R_190() + { + if (jj_3R_30()) return true; + return false; + } + + static private boolean jj_3R_62() { Token xsp; xsp = jj_scanpos; - if (jj_3R_62()) { + if (jj_3R_68()) { jj_scanpos = xsp; - if (jj_3R_63()) { + if (jj_3R_69()) { jj_scanpos = xsp; - if (jj_3R_64()) return true; + if (jj_3R_70()) return true; } } xsp = jj_scanpos; - if (jj_3R_65()) jj_scanpos = xsp; - if (jj_3R_55()) return true; + if (jj_3R_71()) jj_scanpos = xsp; + if (jj_3R_61()) return true; return false; } static private boolean jj_3R_187() + { + if (jj_scan_token(PLUS)) return true; + return false; + } + + static private boolean jj_3R_185() + { + if (jj_scan_token(MIN)) return true; + return false; + } + + static private boolean jj_3R_159() + { + if (jj_scan_token(FILTER)) return true; + if (jj_scan_token(LPARENTH)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_185()) { + jj_scanpos = xsp; + if (jj_3R_186()) { + jj_scanpos = xsp; + if (jj_3R_187()) { + jj_scanpos = xsp; + if (jj_3R_188()) { + jj_scanpos = xsp; + if (jj_3R_189()) { + jj_scanpos = xsp; + if (jj_3R_190()) return true; + } + } + } + } + } + if (jj_scan_token(COMMA)) return true; + if (jj_3R_44()) return true; + xsp = jj_scanpos; + if (jj_3R_191()) jj_scanpos = xsp; + if (jj_scan_token(RPARENTH)) return true; + return false; + } + + static private boolean jj_3R_192() { if (jj_scan_token(COMMA)) return true; - if (jj_3R_38()) return true; + if (jj_3R_44()) return true; return false; } - static private boolean jj_3R_48() + static private boolean jj_3R_170() { - if (jj_scan_token(REG_IDENTPRIME)) return true; + if (jj_3R_30()) return true; + return false; + } + + static private boolean jj_3R_52() + { + if (jj_3R_61()) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_62()) jj_scanpos = xsp; return false; } @@ -5557,8 +5825,11 @@ static private boolean jj_3R_48() static private int jj_ntk; static private Token jj_scanpos, jj_lastpos; static private int jj_la; + /** Whether we are looking ahead. */ + static private boolean jj_lookingAhead = false; + static private boolean jj_semLA; static private int jj_gen; - static final private int[] jj_la1 = new int[101]; + static final private int[] jj_la1 = new int[103]; static private int[] jj_la1_0; static private int[] jj_la1_1; static private int[] jj_la1_2; @@ -5568,15 +5839,15 @@ static private boolean jj_3R_48() jj_la1_init_2(); } private static void jj_la1_init_0() { - jj_la1_0 = new int[] {0x514404c0,0x504404c0,0x1000000,0xb01a0848,0x0,0xb01a0848,0xb01a0848,0x0,0xb01a0848,0x400,0x40000000,0x80,0x40000480,0x8000210,0x8000210,0x0,0x40,0x0,0x1000000,0x8000030,0x0,0x2000000,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xa00000,0x0,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0xa01a0808,0x0,0xa0000000,0xa0000000,0x0,0x20000,0x0,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0xa0ba0808,0x0,0x0,0xa4ba0908,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x1000000,0xa0000000,0x0,0xa0000000,0x0,0x0,0x0,}; + jj_la1_0 = new int[] {0x514404c0,0x504404c0,0x1000000,0xb01a0848,0x0,0xb01a0848,0xb01a0848,0x0,0xb01a0848,0x400,0x40000000,0x80,0x40000480,0x8000210,0x8000210,0x0,0x40,0x0,0x1000000,0x8000030,0x0,0x2000000,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xa00000,0x0,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0xa01a0808,0x0,0xa0000000,0xa0000000,0x0,0x20000,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0x0,0x0,0xa0000000,0x0,0x0,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0xa0ba0808,0x0,0x0,0xa4ba0908,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0000000,0x0,0x0,0x0,}; } private static void jj_la1_init_1() { - jj_la1_1 = new int[] {0x187c5,0x83c4,0x10401,0x40127ab8,0x8000000,0x40127ab8,0x40127ab8,0x8000000,0x40127ab8,0x40,0x4,0x8000,0x8144,0x0,0x0,0x280,0x280,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x4012783a,0x200000,0x40020000,0x10000000,0x4012783a,0x0,0x0,0x10000000,0x0,0x10000000,0x10000000,0x0,0x40000000,0xc2000,0x0,0xc2000,0x2,0x0,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x0,0x0,0x800000,0x1000000,0x400000,0x200000,0x40127838,0x0,0x0,0x0,0x0,0x0,0x0,0x40027838,0x40027838,0x40000000,0x0,0x0,0x10000000,0x20000,0x40000000,0x0,0x38,0x0,0x0,0x0,0x40000000,0x40000000,0x0,0x40000000,0x0,0x0,0x3800,0x0,0x4012783a,0x4012783a,0x0,0x4000,0x4012783a,0x0,0x3838,0x40003838,0x10000000,0x0,0x0,0x0,0x0,0x600000,0x10000000,0x0,0x0,0x0,0x4000000,}; + jj_la1_1 = new int[] {0x187c5,0x83c4,0x10401,0x40127ab8,0x8000000,0x40127ab8,0x40127ab8,0x8000000,0x40127ab8,0x40,0x4,0x8000,0x8144,0x0,0x0,0x280,0x280,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x4012783a,0x200000,0x40020000,0x10000000,0x4012783a,0x0,0x0,0x10000000,0x0,0x10000000,0x10000000,0x0,0x40000000,0xc2000,0x0,0xc2000,0x2,0x0,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x0,0x0,0x800000,0x1000000,0x400000,0x200000,0x40127838,0x0,0x0,0x0,0x0,0x0,0x0,0x40027838,0x40027838,0x40000000,0x0,0x0,0x10000000,0x20000,0x40000000,0x0,0x38,0x0,0x4012783a,0x10000000,0x0,0x0,0x40000000,0x40000000,0x0,0x40000000,0x0,0x0,0x3800,0x0,0x4012783a,0x4012783a,0x0,0x4000,0x4012783a,0x0,0x3838,0x40003838,0x10000000,0x0,0x0,0x0,0x600000,0x10000000,0x0,0x0,0x0,0x0,0x4000000,}; } private static void jj_la1_init_2() { - jj_la1_2 = new int[] {0x0,0x0,0x0,0x2e08404,0x0,0x2e08404,0x2e08404,0x0,0x2e08404,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x40,0x0,0x1,0x2000000,0x0,0x1,0x2000000,0x4000,0x2e08404,0x0,0x0,0x0,0x2e08405,0x2000000,0x1,0x0,0x20010,0x0,0x0,0x20010,0x2200000,0x0,0x3341,0x0,0x0,0x3341,0x2e08404,0x2e08404,0x2e08404,0x2e08404,0x2e08404,0x3341,0x100000,0x0,0x0,0x0,0x0,0x2e08404,0xc0,0x3300,0xc000,0xc000,0x30000,0x30000,0x2e08404,0x2e00404,0x0,0x0,0x2000000,0x0,0xc00000,0x0,0x3340,0x0,0x10,0x10,0x0,0x0,0x3340,0x10,0x0,0x10,0x3340,0x0,0x10,0x2e08404,0x2e08404,0x20000,0x0,0x2e08404,0x404,0x0,0x0,0x0,0x2400000,0x10000,0x2400000,0x2000000,0x2004000,0x0,0x2000000,0xc0,0x3300,0x0,}; + jj_la1_2 = new int[] {0x0,0x0,0x0,0x3608404,0x0,0x3608404,0x3608404,0x0,0x3608404,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x40,0x0,0x1,0x1000000,0x0,0x1,0x1000000,0x4000,0x3608404,0x0,0x0,0x0,0x3608405,0x1000000,0x1,0x0,0x20010,0x0,0x0,0x20010,0x3000000,0x0,0x3341,0x0,0x0,0x3341,0x3608404,0x3608404,0x3608404,0x3608404,0x3608404,0x3341,0x100000,0x0,0x0,0x0,0x0,0x3608404,0xc0,0x3300,0xc000,0xc000,0x30000,0x30000,0x3608404,0x3600404,0x0,0x0,0x1000000,0x0,0x600000,0x0,0x3340,0x0,0x10,0x3608404,0x0,0x10,0x0,0x0,0x3340,0x10,0x0,0x10,0x3340,0x0,0x10,0x3608404,0x3608404,0x20000,0x0,0x3608404,0x404,0x0,0x0,0x0,0x1200000,0x10000,0x1200000,0x1004000,0x0,0x6000000,0x1000000,0xc0,0x3300,0x0,}; } - static final private JJCalls[] jj_2_rtns = new JJCalls[18]; + static final private JJCalls[] jj_2_rtns = new JJCalls[21]; static private boolean jj_rescan = false; static private int jj_gc = 0; @@ -5598,7 +5869,7 @@ public PrismParser(java.io.InputStream stream, String encoding) { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 101; i++) jj_la1[i] = -1; + for (int i = 0; i < 103; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5613,7 +5884,7 @@ static public void ReInit(java.io.InputStream stream, String encoding) { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 101; i++) jj_la1[i] = -1; + for (int i = 0; i < 103; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5631,7 +5902,7 @@ public PrismParser(java.io.Reader stream) { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 101; i++) jj_la1[i] = -1; + for (int i = 0; i < 103; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5642,7 +5913,7 @@ static public void ReInit(java.io.Reader stream) { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 101; i++) jj_la1[i] = -1; + for (int i = 0; i < 103; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5659,7 +5930,7 @@ public PrismParser(PrismParserTokenManager tm) { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 101; i++) jj_la1[i] = -1; + for (int i = 0; i < 103; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5669,7 +5940,7 @@ public void ReInit(PrismParserTokenManager tm) { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 101; i++) jj_la1[i] = -1; + for (int i = 0; i < 103; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5733,7 +6004,7 @@ static final public Token getNextToken() { /** Get the specific Token. */ static final public Token getToken(int index) { - Token t = token; + Token t = jj_lookingAhead ? jj_scanpos : token; for (int i = 0; i < index; i++) { if (t.next != null) t = t.next; else t = t.next = token_source.getNextToken(); @@ -5782,12 +6053,12 @@ static private void jj_add_error_token(int kind, int pos) { /** Generate ParseException. */ static public ParseException generateParseException() { jj_expentries.clear(); - boolean[] la1tokens = new boolean[92]; + boolean[] la1tokens = new boolean[93]; if (jj_kind >= 0) { la1tokens[jj_kind] = true; jj_kind = -1; } - for (int i = 0; i < 101; i++) { + for (int i = 0; i < 103; i++) { if (jj_la1[i] == jj_gen) { for (int j = 0; j < 32; j++) { if ((jj_la1_0[i] & (1< | < RENAME: "<-" > | < QMARK: "?" > -| < DQUOTE: "\"" > // Regular expressions | < REG_INT: (["1"-"9"](["0"-"9"])*)|("0") > | < REG_DOUBLE: (["0"-"9"])*(".")?(["0"-"9"])+(["e","E"](["-","+"])?(["0"-"9"])+)? > | < REG_IDENTPRIME: ["_","a"-"z","A"-"Z"](["_","a"-"z","A"-"Z","0"-"9"])*"'" > | < REG_IDENT: ["_","a"-"z","A"-"Z"](["_","a"-"z","A"-"Z","0"-"9"])* > +// REG_QUOTED_IDENT has precedence before general REG_QUOTED_STRING +| < REG_QUOTED_IDENT: "\"" (["_","a"-"z","A"-"Z"](["_","a"-"z","A"-"Z","0"-"9"])*) "\"" > +// REG_QUOTED_STRING: first ", then finitely often either \+arbitrary char or not(\,"), then " +| < REG_QUOTED_STRING: "\"" (("\\" ~[]) | ~["\\","\""] )* "\"" > | < PREPROC: "#"(~["#"])*"#" > // Special catch-all token for lexical errors // (this allows us to throw our usual exceptions in this case) @@ -638,7 +641,7 @@ Property Property() : // (this avoids some common parsing errors for semicolon-less files) // Note also use of lookahead (to colon) to distinguish (optional) name from label reference ( { begin = getToken(1); } - ( LOOKAHEAD( Identifier() ) name = Identifier() )? + ( LOOKAHEAD(QuotedIdentifier() ) name = QuotedIdentifier() )? expr = ExpressionITE(true, false) { prop = new Property(expr, name, getPrecedingCommentBlock(begin)); } ) @@ -705,7 +708,7 @@ void LabelDef(LabelList labelList) throws PrismLangException : } { // Lookahead required because of the error handling clause below - LOOKAHEAD(