From a37a947fc523f1be3748da43430d98715b27210f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 17 Oct 2007 09:02:12 +0000 Subject: [PATCH] Properties files can use model file formulas. Model files can contain labels. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@454 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ExpressionFormula.java | 6 +- prism/src/parser/FormulaList.java | 13 +- prism/src/parser/LabelList.java | 29 + prism/src/parser/ModulesFile.java | 49 + prism/src/parser/PCTLExpression.java | 18 + prism/src/parser/PCTLFormula.java | 8 + prism/src/parser/PCTLFormulaBinary.java | 20 + prism/src/parser/PCTLFormulaNary.java | 28 + prism/src/parser/PCTLFormulaUnary.java | 18 + prism/src/parser/PCTLInit.java | 14 + prism/src/parser/PCTLLabel.java | 18 +- prism/src/parser/PCTLProb.java | 28 + prism/src/parser/PCTLProbBoundedFuture.java | 26 + prism/src/parser/PCTLProbBoundedGlobal.java | 26 + prism/src/parser/PCTLProbBoundedUntil.java | 26 + prism/src/parser/PCTLReward.java | 32 + prism/src/parser/PCTLRewardCumul.java | 20 + prism/src/parser/PCTLRewardInst.java | 20 + prism/src/parser/PCTLRewardSS.java | 14 + prism/src/parser/PCTLSS.java | 28 + prism/src/parser/PrismParser.java | 1208 ++++++++++--------- prism/src/parser/PrismParser.jj | 12 +- prism/src/parser/PropertiesFile.java | 142 ++- prism/src/prism/NondetModelChecker.java | 2 +- prism/src/prism/Prism.java | 2 +- prism/src/prism/ProbModelChecker.java | 2 +- prism/src/prism/StochModelChecker.java | 2 +- prism/src/simulator/SimulatorEngine.java | 2 +- 28 files changed, 1190 insertions(+), 623 deletions(-) diff --git a/prism/src/parser/ExpressionFormula.java b/prism/src/parser/ExpressionFormula.java index 730dde7e..45893a4d 100644 --- a/prism/src/parser/ExpressionFormula.java +++ b/prism/src/parser/ExpressionFormula.java @@ -98,10 +98,8 @@ public class ExpressionFormula extends Expression // return replacement expression return e; } - else { - // error (should never happen) - throw new PrismException("Formula \"" + name + "\" undefined"); - } + + return this; } // create and return a new expression by renaming diff --git a/prism/src/parser/FormulaList.java b/prism/src/parser/FormulaList.java index 4726ae0b..b3ce5c9f 100644 --- a/prism/src/parser/FormulaList.java +++ b/prism/src/parser/FormulaList.java @@ -83,12 +83,18 @@ public class FormulaList // (inside the formulas in this formula list) public void findAllFormulas() throws PrismException + { findAllFormulas(this); } + + // find all formulas (i.e. locate idents which are formulas) + // (from the specified formula list) + + public void findAllFormulas(FormulaList fl) throws PrismException { int i, n; n = formulas.size(); for (i = 0; i < n; i++) { - formulas.setElementAt(getFormula(i).findAllFormulas(this), i); + formulas.setElementAt(getFormula(i).findAllFormulas(fl), i); } } @@ -159,12 +165,15 @@ public class FormulaList // expand any formulas public void expandFormulas() throws PrismException + { expandFormulas(this); } + + public void expandFormulas(FormulaList fl) throws PrismException { int i, n; n = formulas.size(); for (i = 0; i < n; i++) { - formulas.setElementAt(getFormula(i).expandFormulas(this), i); + formulas.setElementAt(getFormula(i).expandFormulas(fl), i); } } diff --git a/prism/src/parser/LabelList.java b/prism/src/parser/LabelList.java index 0fa68d36..14826e8c 100644 --- a/prism/src/parser/LabelList.java +++ b/prism/src/parser/LabelList.java @@ -79,6 +79,35 @@ public class LabelList return names.indexOf(s); } + // find all formulas (i.e. locate idents which are formulas) + // (inside the expressions in this label list) + + public void findAllFormulas(FormulaList formulaList) throws PrismException + { + int i, n; + Expression e; + + n = labels.size(); + for (i = 0; i < n; i++) { + e = getLabel(i); + labels.setElementAt(e.findAllFormulas(formulaList), i); + } + } + + // expand any formulas + + public void expandFormulas(FormulaList formulaList) throws PrismException + { + int i, n; + Expression e; + + n = labels.size(); + for (i = 0; i < n; i++) { + e = getLabel(i); + labels.setElementAt(e.expandFormulas(formulaList), i); + } + } + // find all constants (i.e. locate idents which are constants) public void findAllConstants(ConstantList constantList) throws PrismException diff --git a/prism/src/parser/ModulesFile.java b/prism/src/parser/ModulesFile.java index ec00605a..9cb5441f 100644 --- a/prism/src/parser/ModulesFile.java +++ b/prism/src/parser/ModulesFile.java @@ -43,6 +43,9 @@ public class ModulesFile // formulas (macros) private FormulaList formulaList; + // labels (atomic propositions) + private LabelList labelList; + // constants private ConstantList constantList; @@ -70,6 +73,7 @@ public class ModulesFile { // initialise formulaList = new FormulaList(); // empty - will be overwritten + labelList = new LabelList(); // empty - will be overwritten constantList = new ConstantList(); // empty - will be overwritten type = NONDETERMINISTIC; // default type globals = new Vector(); @@ -87,6 +91,8 @@ public class ModulesFile public void setFormulaList(FormulaList fl) { formulaList = fl; } + public void setLabelList(LabelList ll) { labelList = ll; } + public void setConstantList(ConstantList cl) { constantList = cl; } public void setType(int t) { type = t; } @@ -110,6 +116,8 @@ public class ModulesFile public FormulaList getFormulaList() { return formulaList; } + public LabelList getLabelList() { return labelList; } + public ConstantList getConstantList() { return constantList; } public int getType() { return type; } @@ -222,6 +230,9 @@ public class ModulesFile // sort out any modules defined by renaming sortRenamings(); + // check label identifiers + checkLabelIdents(); + // check module names checkModuleNames(); @@ -280,6 +291,8 @@ public class ModulesFile // look in formula list formulaList.findAllFormulas(); + // look in labels + labelList.findAllFormulas(formulaList); // look in constants constantList.findAllFormulas(formulaList); // look in globals @@ -314,6 +327,8 @@ public class ModulesFile // look in formula list // (best to do this first - sorts out any linked formulas) formulaList.expandFormulas(); + // look in labels + labelList.expandFormulas(formulaList); // look in constants constantList.expandFormulas(formulaList); // look in globals @@ -369,6 +384,29 @@ public class ModulesFile } } + // check label identifiers + + private void checkLabelIdents() throws PrismException + { + int i, n; + String s; + Vector labelIdents; + + // go thru labels + n = labelList.size(); + labelIdents = new Vector(); + for (i = 0; i < n; i++) { + s = labelList.getLabelName(i); + // see if ident has been used already for a label + if (labelIdents.contains(s)) { + throw new PrismException("Duplicated label name \"" + s + "\""); + } + else { + labelIdents.addElement(s); + } + } + } + // check module names private void checkModuleNames() throws PrismException @@ -478,6 +516,8 @@ public class ModulesFile { int i, n; + // look in labels + labelList.findAllConstants(constantList); // look in constants constantList.findAllConstants(constantList); // look in globals @@ -557,6 +597,8 @@ public class ModulesFile // nb: we even check in places where there shouldn't be vars // eg. in constant definitions etc. + // look in labels + labelList.findAllVars(varNames, varTypes); // look in constants constantList.findAllVars(varNames, varTypes); // look in globals @@ -601,6 +643,9 @@ public class ModulesFile Module module; Vector v; + // check labels + labelList.check(); + // check constants constantList.check(); // check globals @@ -809,6 +854,10 @@ public class ModulesFile if (tmp.length() > 0) tmp += "\n"; s += tmp; + tmp = "" + labelList; + if (tmp.length() > 0) tmp += "\n"; + s += tmp; + tmp = "" + constantList; if (tmp.length() > 0) tmp += "\n"; s += tmp; diff --git a/prism/src/parser/PCTLExpression.java b/prism/src/parser/PCTLExpression.java index 9ca6fa79..181fc7da 100644 --- a/prism/src/parser/PCTLExpression.java +++ b/prism/src/parser/PCTLExpression.java @@ -61,6 +61,24 @@ public class PCTLExpression extends PCTLFormula return expr; } + // find all formulas (i.e. locate idents which are formulas) + + public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException + { + expr = expr.findAllFormulas(formulaList); + + return this; + } + + // expand any formulas + + public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException + { + expr = expr.expandFormulas(formulaList); + + return this; + } + // find all constants (i.e. locate idents which are constants) public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException diff --git a/prism/src/parser/PCTLFormula.java b/prism/src/parser/PCTLFormula.java index ef4674c9..1b79ee67 100644 --- a/prism/src/parser/PCTLFormula.java +++ b/prism/src/parser/PCTLFormula.java @@ -65,6 +65,14 @@ public abstract class PCTLFormula // default is ok - do nothing } + // find all formulas (i.e. locate idents which are formulas) + + public abstract PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException; + + // expand any formulas + + public abstract PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException; + // find all constants (i.e. locate idents which are constants) public abstract PCTLFormula findAllConstants(ConstantList constantList) throws PrismException; diff --git a/prism/src/parser/PCTLFormulaBinary.java b/prism/src/parser/PCTLFormulaBinary.java index 6bd007f2..7c600777 100644 --- a/prism/src/parser/PCTLFormulaBinary.java +++ b/prism/src/parser/PCTLFormulaBinary.java @@ -81,6 +81,26 @@ public abstract class PCTLFormulaBinary extends PCTLFormula operand2.checkLabelIdents(labelList); } + // find all formulas (i.e. locate idents which are formulas) + + public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException + { + operand1 = operand1.findAllFormulas(formulaList); + operand2 = operand2.findAllFormulas(formulaList); + + return this; + } + + // expand any formulas + + public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException + { + operand1 = operand1.expandFormulas(formulaList); + operand2 = operand2.expandFormulas(formulaList); + + return this; + } + // find all constants (i.e. locate idents which are constants) public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException diff --git a/prism/src/parser/PCTLFormulaNary.java b/prism/src/parser/PCTLFormulaNary.java index c1b314fc..f2bfd709 100644 --- a/prism/src/parser/PCTLFormulaNary.java +++ b/prism/src/parser/PCTLFormulaNary.java @@ -79,6 +79,34 @@ public abstract class PCTLFormulaNary extends PCTLFormula } } + // find all formulas (i.e. locate idents which are formulas) + + public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException + { + int i, n; + + n = getNumOperands(); + for (i = 0; i < n; i++) { + setOperand(i, getOperand(i).findAllFormulas(formulaList)); + } + + return this; + } + + // expand any formulas + + public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException + { + int i, n; + + n = getNumOperands(); + for (i = 0; i < n; i++) { + setOperand(i, getOperand(i).expandFormulas(formulaList)); + } + + return this; + } + // find all constants (i.e. locate idents which are constants) public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException diff --git a/prism/src/parser/PCTLFormulaUnary.java b/prism/src/parser/PCTLFormulaUnary.java index c210f2f9..56d6a46c 100644 --- a/prism/src/parser/PCTLFormulaUnary.java +++ b/prism/src/parser/PCTLFormulaUnary.java @@ -68,6 +68,24 @@ public abstract class PCTLFormulaUnary extends PCTLFormula operand.checkLabelIdents(labelList); } + // find all formulas (i.e. locate idents which are formulas) + + public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException + { + operand = operand.findAllFormulas(formulaList); + + return this; + } + + // expand any formulas + + public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException + { + operand = operand.expandFormulas(formulaList); + + return this; + } + // find all constants (i.e. locate idents which are constants) public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException diff --git a/prism/src/parser/PCTLInit.java b/prism/src/parser/PCTLInit.java index b22b69dc..15ad851d 100644 --- a/prism/src/parser/PCTLInit.java +++ b/prism/src/parser/PCTLInit.java @@ -42,6 +42,20 @@ public class PCTLInit extends PCTLFormula setType(Expression.BOOLEAN); } + // find all formulas (i.e. locate idents which are formulas) + + public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException + { + return this; + } + + // expand any formulas + + public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException + { + return this; + } + // find all constants (i.e. locate idents which are constants) public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException diff --git a/prism/src/parser/PCTLLabel.java b/prism/src/parser/PCTLLabel.java index cb1c28b9..71314e48 100644 --- a/prism/src/parser/PCTLLabel.java +++ b/prism/src/parser/PCTLLabel.java @@ -62,6 +62,20 @@ public class PCTLLabel extends PCTLFormula } } + // find all formulas (i.e. locate idents which are formulas) + + public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException + { + return this; + } + + // expand any formulas + + public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException + { + return this; + } + // find all constants (i.e. locate idents which are constants) public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException @@ -87,7 +101,7 @@ public class PCTLLabel extends PCTLFormula /** * Convert and build simulator data structures */ - public long toSimulator(SimulatorEngine sim ) throws SimulatorException + public long toSimulator(SimulatorEngine sim) throws SimulatorException { LabelList ll; Expression expr; @@ -95,9 +109,7 @@ public class PCTLLabel extends PCTLFormula int i; // get expression associated with label - ll = sim.getLabelList(); - i = ll.getLabelIndex(getName()); if (i == -1) throw new SimulatorException("Unknown label \"" + getName() + "\" in PCTL formula"); expr = ll.getLabel(i); diff --git a/prism/src/parser/PCTLProb.java b/prism/src/parser/PCTLProb.java index bb3fa4a6..903fe838 100644 --- a/prism/src/parser/PCTLProb.java +++ b/prism/src/parser/PCTLProb.java @@ -115,6 +115,34 @@ public class PCTLProb extends PCTLFormulaUnary if (filter != null) filter.checkLabelIdents(labelList); } + // find all formulas (i.e. locate idents which are formulas) + + public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException + { + // call superclass (unary) + super.findAllFormulas(formulaList); + // also do prob expression + if (prob != null) prob = prob.findAllFormulas(formulaList); + // also do filter + if (filter != null) filter = filter.findAllFormulas(formulaList); + + return this; + } + + // expand any formulas + + public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException + { + // call superclass (unary) + super.expandFormulas(formulaList); + // also do prob expression + if (prob != null) prob = prob.expandFormulas(formulaList); + // also do filter + if (filter != null) filter = filter.expandFormulas(formulaList); + + return this; + } + // find all constants (i.e. locate idents which are constants) public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException diff --git a/prism/src/parser/PCTLProbBoundedFuture.java b/prism/src/parser/PCTLProbBoundedFuture.java index 522ade3c..39af5534 100644 --- a/prism/src/parser/PCTLProbBoundedFuture.java +++ b/prism/src/parser/PCTLProbBoundedFuture.java @@ -55,6 +55,32 @@ public class PCTLProbBoundedFuture extends PCTLFormulaUnary return uBound; } + // find all formulas (i.e. locate idents which are formulas) + + public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException + { + // call superclass (binary) + super.findAllFormulas(formulaList); + // also do bound expressions + if (lBound != null) lBound = lBound.findAllFormulas(formulaList); + if (uBound != null) uBound = uBound.findAllFormulas(formulaList); + + return this; + } + + // expand any formulas + + public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException + { + // call superclass (binary) + super.expandFormulas(formulaList); + // also do bound expressions + if (lBound != null) lBound = lBound.expandFormulas(formulaList); + if (uBound != null) uBound = uBound.expandFormulas(formulaList); + + return this; + } + // find all constants (i.e. locate idents which are constants) public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException diff --git a/prism/src/parser/PCTLProbBoundedGlobal.java b/prism/src/parser/PCTLProbBoundedGlobal.java index 20718407..7be3ae95 100644 --- a/prism/src/parser/PCTLProbBoundedGlobal.java +++ b/prism/src/parser/PCTLProbBoundedGlobal.java @@ -55,6 +55,32 @@ public class PCTLProbBoundedGlobal extends PCTLFormulaUnary return uBound; } + // find all formulas (i.e. locate idents which are formulas) + + public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException + { + // call superclass (binary) + super.findAllFormulas(formulaList); + // also do bound expressions + if (lBound != null) lBound = lBound.findAllFormulas(formulaList); + if (uBound != null) uBound = uBound.findAllFormulas(formulaList); + + return this; + } + + // expand any formulas + + public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException + { + // call superclass (binary) + super.expandFormulas(formulaList); + // also do bound expressions + if (lBound != null) lBound = lBound.expandFormulas(formulaList); + if (uBound != null) uBound = uBound.expandFormulas(formulaList); + + return this; + } + // find all constants (i.e. locate idents which are constants) public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException diff --git a/prism/src/parser/PCTLProbBoundedUntil.java b/prism/src/parser/PCTLProbBoundedUntil.java index ad5e07bd..9c3e69ba 100644 --- a/prism/src/parser/PCTLProbBoundedUntil.java +++ b/prism/src/parser/PCTLProbBoundedUntil.java @@ -56,6 +56,32 @@ public class PCTLProbBoundedUntil extends PCTLFormulaBinary return uBound; } + // find all formulas (i.e. locate idents which are formulas) + + public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException + { + // call superclass (binary) + super.findAllFormulas(formulaList); + // also do bound expressions + if (lBound != null) lBound = lBound.findAllFormulas(formulaList); + if (uBound != null) uBound = uBound.findAllFormulas(formulaList); + + return this; + } + + // expand any formulas + + public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException + { + // call superclass (binary) + super.expandFormulas(formulaList); + // also do bound expressions + if (lBound != null) lBound = lBound.expandFormulas(formulaList); + if (uBound != null) uBound = uBound.expandFormulas(formulaList); + + return this; + } + // find all constants (i.e. locate idents which are constants) public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException diff --git a/prism/src/parser/PCTLReward.java b/prism/src/parser/PCTLReward.java index 8d7780c8..8673bfe2 100644 --- a/prism/src/parser/PCTLReward.java +++ b/prism/src/parser/PCTLReward.java @@ -135,6 +135,38 @@ public class PCTLReward extends PCTLFormulaUnary if (filter != null) filter.checkLabelIdents(labelList); } + // find all formulas (i.e. locate idents which are formulas) + + public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException + { + // call superclass (unary) + super.findAllFormulas(formulaList); + // also do reward expression + if (reward != null) reward = reward.findAllFormulas(formulaList); + // also do reward struct index + if (rewardStructIndex != null) if (rewardStructIndex instanceof Expression) rewardStructIndex = ((Expression)rewardStructIndex).findAllFormulas(formulaList); + // also do filter + if (filter != null) filter = filter.findAllFormulas(formulaList); + + return this; + } + + // expand any formulas + + public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException + { + // call superclass (unary) + super.expandFormulas(formulaList); + // also do reward expression + if (reward != null) reward = reward.expandFormulas(formulaList); + // also do reward struct index + if (rewardStructIndex != null) if (rewardStructIndex instanceof Expression) rewardStructIndex = ((Expression)rewardStructIndex).expandFormulas(formulaList); + // also do filter + if (filter != null) filter = filter.expandFormulas(formulaList); + + return this; + } + // find all constants (i.e. locate idents which are constants) public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException diff --git a/prism/src/parser/PCTLRewardCumul.java b/prism/src/parser/PCTLRewardCumul.java index 40c4560c..7d275358 100644 --- a/prism/src/parser/PCTLRewardCumul.java +++ b/prism/src/parser/PCTLRewardCumul.java @@ -48,6 +48,26 @@ public class PCTLRewardCumul extends PCTLFormula return bound; } + // find all formulas (i.e. locate idents which are formulas) + + public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException + { + // do bound + if (bound != null) bound = bound.findAllFormulas(formulaList); + + return this; + } + + // expand any formulas + + public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException + { + // do bound + if (bound != null) bound = bound.expandFormulas(formulaList); + + return this; + } + // find all constants (i.e. locate idents which are constants) public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException diff --git a/prism/src/parser/PCTLRewardInst.java b/prism/src/parser/PCTLRewardInst.java index c1813919..d14856aa 100644 --- a/prism/src/parser/PCTLRewardInst.java +++ b/prism/src/parser/PCTLRewardInst.java @@ -48,6 +48,26 @@ public class PCTLRewardInst extends PCTLFormula return time; } + // find all formulas (i.e. locate idents which are formulas) + + public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException + { + // do time + if (time != null) time = time.findAllFormulas(formulaList); + + return this; + } + + // expand any formulas + + public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException + { + // do time + if (time != null) time = time.expandFormulas(formulaList); + + return this; + } + // find all constants (i.e. locate idents which are constants) public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException diff --git a/prism/src/parser/PCTLRewardSS.java b/prism/src/parser/PCTLRewardSS.java index 912b7669..bc86b914 100644 --- a/prism/src/parser/PCTLRewardSS.java +++ b/prism/src/parser/PCTLRewardSS.java @@ -40,6 +40,20 @@ public class PCTLRewardSS extends PCTLFormula { } + // find all formulas (i.e. locate idents which are formulas) + + public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException + { + return this; + } + + // expand any formulas + + public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException + { + return this; + } + // find all constants (i.e. locate idents which are constants) public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException diff --git a/prism/src/parser/PCTLSS.java b/prism/src/parser/PCTLSS.java index afa6c20d..77d302e2 100644 --- a/prism/src/parser/PCTLSS.java +++ b/prism/src/parser/PCTLSS.java @@ -78,6 +78,34 @@ public class PCTLSS extends PCTLFormulaUnary if (filter != null) filter.checkLabelIdents(labelList); } + // find all formulas (i.e. locate idents which are formulas) + + public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException + { + // call superclass (unary) + super.findAllFormulas(formulaList); + // also do prob expression + if (prob != null) prob = prob.findAllFormulas(formulaList); + // also do filter + if (filter != null) filter = filter.findAllFormulas(formulaList); + + return this; + } + + // expand any formulas + + public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException + { + // call superclass (unary) + super.expandFormulas(formulaList); + // also do prob expression + if (prob != null) prob = prob.expandFormulas(formulaList); + // also do filter + if (filter != null) filter = filter.expandFormulas(formulaList); + + return this; + } + // find all constants (i.e. locate idents which are constants) public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index 87991c06..4dc7c398 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -145,6 +145,7 @@ public class PrismParser implements PrismParserConstants { // clear all vectors/stacks formulaList = new FormulaList(); + labelList = new LabelList(); constantList = new ConstantList(); stack.clear(); reverseStack.clear(); @@ -176,6 +177,7 @@ public class PrismParser implements PrismParserConstants { ReInit(str); // clear all vectors/stacks + formulaList = new FormulaList(); labelList = new LabelList(); constantList = new ConstantList(); stack.clear(); @@ -332,18 +334,20 @@ public class PrismParser implements PrismParserConstants { } else if (jj_2_3(2147483647)) { FormulaDef(); } else if (jj_2_4(2147483647)) { - ConstantDef(); + LabelDef(); } else if (jj_2_5(2147483647)) { - GlobalDecl(); + ConstantDef(); } else if (jj_2_6(2147483647)) { - Module(); + GlobalDecl(); } else if (jj_2_7(2147483647)) { - RenamedModule(); + Module(); } else if (jj_2_8(2147483647)) { - SystemComp(); + RenamedModule(); } else if (jj_2_9(2147483647)) { - RewardStruct(); + SystemComp(); } else if (jj_2_10(2147483647)) { + RewardStruct(); + } else if (jj_2_11(2147483647)) { Init(); } else { jj_consume_token(-1); @@ -356,8 +360,9 @@ public class PrismParser implements PrismParserConstants { // create new ModulesFile object ModulesFile modulesFile = new ModulesFile(); - // pass lists of formulas, constants to ModulesFile + // pass lists of formulas, labels, constants to ModulesFile modulesFile.setFormulaList(formulaList); + modulesFile.setLabelList(labelList); modulesFile.setConstantList(constantList); // set type (default is nondeterministic) @@ -422,16 +427,16 @@ public class PrismParser implements PrismParserConstants { static final public PropertiesFile PropertiesFile() throws ParseException { label_2: while (true) { - if (jj_2_11(2147483647)) { + if (jj_2_12(2147483647)) { ; } else { break label_2; } - if (jj_2_12(2147483647)) { + if (jj_2_13(2147483647)) { LabelDef(); - } else if (jj_2_13(2147483647)) { - ConstantDef(); } else if (jj_2_14(2147483647)) { + ConstantDef(); + } else if (jj_2_15(2147483647)) { SinglePCTLFormula(); } else { jj_consume_token(-1); @@ -443,7 +448,8 @@ public class PrismParser implements PrismParserConstants { // (pass in associated ModulesFile) PropertiesFile propertiesFile = new PropertiesFile(modulesFile); - // pass lists of labels, constants to PropertiesFile + // pass lists of formulas, labels, constants to PropertiesFile + propertiesFile.setFormulaList(formulaList); propertiesFile.setLabelList(labelList); propertiesFile.setConstantList(constantList); @@ -482,17 +488,17 @@ public class PrismParser implements PrismParserConstants { // keyword denoting module type (nondeterministic, probabilistic, ...) static final public int ModulesFileType() throws ParseException { - if (jj_2_15(2147483647)) { + if (jj_2_16(2147483647)) { jj_consume_token(PROBABILISTIC); - } else if (jj_2_16(2147483647)) { - jj_consume_token(NONDETERMINISTIC); } else if (jj_2_17(2147483647)) { - jj_consume_token(STOCHASTIC); + jj_consume_token(NONDETERMINISTIC); } else if (jj_2_18(2147483647)) { - jj_consume_token(DTMC); + jj_consume_token(STOCHASTIC); } else if (jj_2_19(2147483647)) { - jj_consume_token(MDP); + jj_consume_token(DTMC); } else if (jj_2_20(2147483647)) { + jj_consume_token(MDP); + } else if (jj_2_21(2147483647)) { jj_consume_token(CTMC); } else { jj_consume_token(-1); @@ -532,11 +538,11 @@ public class PrismParser implements PrismParserConstants { static final public void ConstantDef() throws ParseException { String s; Token t = null; - if (jj_2_28(2147483647)) { + if (jj_2_29(2147483647)) { jj_consume_token(CONST); jj_consume_token(INT); s = Identifier(); - if (jj_2_21(2147483647)) { + if (jj_2_22(2147483647)) { t = jj_consume_token(EQ); Expression(); } else { @@ -551,11 +557,11 @@ public class PrismParser implements PrismParserConstants { else { constantList.addConstant(s, null, Expression.INT); } - } else if (jj_2_29(2147483647)) { + } else if (jj_2_30(2147483647)) { jj_consume_token(CONST); jj_consume_token(DOUBLE); s = Identifier(); - if (jj_2_22(2147483647)) { + if (jj_2_23(2147483647)) { t = jj_consume_token(EQ); Expression(); } else { @@ -570,11 +576,11 @@ public class PrismParser implements PrismParserConstants { else { constantList.addConstant(s, null, Expression.DOUBLE); } - } else if (jj_2_30(2147483647)) { + } else if (jj_2_31(2147483647)) { jj_consume_token(CONST); jj_consume_token(BOOL); s = Identifier(); - if (jj_2_23(2147483647)) { + if (jj_2_24(2147483647)) { t = jj_consume_token(EQ); Expression(); } else { @@ -589,10 +595,10 @@ public class PrismParser implements PrismParserConstants { else { constantList.addConstant(s, null, Expression.BOOLEAN); } - } else if (jj_2_31(2147483647)) { + } else if (jj_2_32(2147483647)) { jj_consume_token(CONST); s = Identifier(); - if (jj_2_24(2147483647)) { + if (jj_2_25(2147483647)) { t = jj_consume_token(EQ); Expression(); } else { @@ -607,17 +613,17 @@ public class PrismParser implements PrismParserConstants { else { constantList.addConstant(s, null, Expression.INT); } - } else if (jj_2_32(2147483647)) { - if (jj_2_25(2147483647)) { + } else if (jj_2_33(2147483647)) { + if (jj_2_26(2147483647)) { jj_consume_token(RATE); - } else if (jj_2_26(2147483647)) { + } else if (jj_2_27(2147483647)) { jj_consume_token(PROB); } else { jj_consume_token(-1); throw new ParseException(); } s = Identifier(); - if (jj_2_27(2147483647)) { + if (jj_2_28(2147483647)) { t = jj_consume_token(EQ); Expression(); } else { @@ -654,7 +660,7 @@ public class PrismParser implements PrismParserConstants { name = Identifier(); label_3: while (true) { - if (jj_2_33(2147483647)) { + if (jj_2_34(2147483647)) { ; } else { break label_3; @@ -663,7 +669,7 @@ public class PrismParser implements PrismParserConstants { } label_4: while (true) { - if (jj_2_34(2147483647)) { + if (jj_2_35(2147483647)) { ; } else { break label_4; @@ -719,7 +725,7 @@ public class PrismParser implements PrismParserConstants { Token t = null; // put '*' marker on stack stack.push(new Character('*')); - if (jj_2_37(2147483647)) { + if (jj_2_38(2147483647)) { name = Identifier(); jj_consume_token(COLON); jj_consume_token(LBRACKET); @@ -727,7 +733,7 @@ public class PrismParser implements PrismParserConstants { jj_consume_token(DOTS); Expression(); jj_consume_token(RBRACKET); - if (jj_2_35(2147483647)) { + if (jj_2_36(2147483647)) { jj_consume_token(INIT); Expression(); } else { @@ -754,11 +760,11 @@ public class PrismParser implements PrismParserConstants { stack.pop(); // put Declaration object back on stack stack.push(new Declaration(name, l, h, s)); - } else if (jj_2_38(2147483647)) { + } else if (jj_2_39(2147483647)) { name = Identifier(); jj_consume_token(COLON); jj_consume_token(BOOL); - if (jj_2_36(2147483647)) { + if (jj_2_37(2147483647)) { jj_consume_token(INIT); Expression(); } else { @@ -788,7 +794,7 @@ public class PrismParser implements PrismParserConstants { String s = null; Token t = null; jj_consume_token(LBRACKET); - if (jj_2_39(2147483647)) { + if (jj_2_40(2147483647)) { s = Identifier(); } else { ; @@ -822,7 +828,7 @@ public class PrismParser implements PrismParserConstants { static final public void Updates() throws ParseException { // put '*' marker on stack stack.push(new Character('*')); - if (jj_2_41(2147483647)) { + if (jj_2_42(2147483647)) { Update(); // create new Updates object Updates u = new Updates(); @@ -831,11 +837,11 @@ public class PrismParser implements PrismParserConstants { stack.pop(); // put updates on to stack stack.push(u); - } else if (jj_2_42(2147483647)) { + } else if (jj_2_43(2147483647)) { ProbUpdate(); label_5: while (true) { - if (jj_2_40(2147483647)) { + if (jj_2_41(2147483647)) { ; } else { break label_5; @@ -879,11 +885,11 @@ public class PrismParser implements PrismParserConstants { static final public void Update() throws ParseException { // put '*' marker on stack stack.push(new Character('*')); - if (jj_2_44(2147483647)) { + if (jj_2_45(2147483647)) { UpdateElement(); label_6: while (true) { - if (jj_2_43(2147483647)) { + if (jj_2_44(2147483647)) { ; } else { break label_6; @@ -909,7 +915,7 @@ public class PrismParser implements PrismParserConstants { stack.pop(); // push completed Update object back on stack stack.push(u); - } else if (jj_2_45(2147483647)) { + } else if (jj_2_46(2147483647)) { jj_consume_token(TRUE); // create new (empty) Update object Update u = new Update(); @@ -925,7 +931,7 @@ public class PrismParser implements PrismParserConstants { static final public void UpdateElement() throws ParseException { String var=""; - if (jj_2_46(2147483647)) { + if (jj_2_47(2147483647)) { jj_consume_token(LPARENTH); var = IdentifierPrime(); jj_consume_token(EQ); @@ -934,7 +940,7 @@ public class PrismParser implements PrismParserConstants { // expression is now already on stack // put variable identifier String on too stack.push(var); - } else if (jj_2_47(2147483647)) { + } else if (jj_2_48(2147483647)) { var = IdentifierPrime(); jj_consume_token(EQ); Expression(); @@ -979,7 +985,7 @@ public class PrismParser implements PrismParserConstants { Rename(); label_7: while (true) { - if (jj_2_48(2147483647)) { + if (jj_2_49(2147483647)) { ; } else { break label_7; @@ -991,18 +997,18 @@ public class PrismParser implements PrismParserConstants { static final public void Rename() throws ParseException { String id1, id2; - if (jj_2_49(2147483647)) { + if (jj_2_50(2147483647)) { id1 = Identifier(); - } else if (jj_2_50(2147483647)) { + } else if (jj_2_51(2147483647)) { jj_consume_token(MIN); id1="min"; - } else if (jj_2_51(2147483647)) { + } else if (jj_2_52(2147483647)) { jj_consume_token(MAX); id1="max"; - } else if (jj_2_52(2147483647)) { + } else if (jj_2_53(2147483647)) { jj_consume_token(FLOOR); id1="floor"; - } else if (jj_2_53(2147483647)) { + } else if (jj_2_54(2147483647)) { jj_consume_token(CEIL); id1="ceil"; } else { @@ -1010,18 +1016,18 @@ public class PrismParser implements PrismParserConstants { throw new ParseException(); } jj_consume_token(EQ); - if (jj_2_54(2147483647)) { + if (jj_2_55(2147483647)) { id2 = Identifier(); - } else if (jj_2_55(2147483647)) { + } else if (jj_2_56(2147483647)) { jj_consume_token(MIN); id2="min"; - } else if (jj_2_56(2147483647)) { + } else if (jj_2_57(2147483647)) { jj_consume_token(MAX); id2="max"; - } else if (jj_2_57(2147483647)) { + } else if (jj_2_58(2147483647)) { jj_consume_token(FLOOR); id2="floor"; - } else if (jj_2_58(2147483647)) { + } else if (jj_2_59(2147483647)) { jj_consume_token(CEIL); id2="ceil"; } else { @@ -1042,13 +1048,13 @@ public class PrismParser implements PrismParserConstants { // system definition component static final public void SystemParallels() throws ParseException { - if (jj_2_59(2147483647)) { + if (jj_2_60(2147483647)) { SystemFullParallel(); - } else if (jj_2_60(2147483647)) { - SystemInterleaved(); } else if (jj_2_61(2147483647)) { - SystemParallel(); + SystemInterleaved(); } else if (jj_2_62(2147483647)) { + SystemParallel(); + } else if (jj_2_63(2147483647)) { SystemHideRename(); } else { jj_consume_token(-1); @@ -1066,7 +1072,7 @@ public class PrismParser implements PrismParserConstants { jj_consume_token(OR); jj_consume_token(OR); SystemHideRename(); - if (jj_2_63(2147483647)) { + if (jj_2_64(2147483647)) { ; } else { break label_8; @@ -1098,7 +1104,7 @@ public class PrismParser implements PrismParserConstants { jj_consume_token(OR); jj_consume_token(OR); SystemHideRename(); - if (jj_2_64(2147483647)) { + if (jj_2_65(2147483647)) { ; } else { break label_9; @@ -1127,7 +1133,7 @@ public class PrismParser implements PrismParserConstants { SystemAction(); label_10: while (true) { - if (jj_2_65(2147483647)) { + if (jj_2_66(2147483647)) { ; } else { break label_10; @@ -1164,18 +1170,18 @@ public class PrismParser implements PrismParserConstants { SystemAtomic(); label_11: while (true) { - if (jj_2_66(2147483647)) { + if (jj_2_67(2147483647)) { ; } else { break label_11; } - if (jj_2_69(2147483647)) { + if (jj_2_70(2147483647)) { jj_consume_token(DIVIDE); jj_consume_token(LBRACE); SystemAction(); label_12: while (true) { - if (jj_2_67(2147483647)) { + if (jj_2_68(2147483647)) { ; } else { break label_12; @@ -1199,14 +1205,14 @@ public class PrismParser implements PrismParserConstants { } // put the SystemHide on the stack stack.push(s); - } else if (jj_2_70(2147483647)) { + } else if (jj_2_71(2147483647)) { jj_consume_token(LBRACE); SystemAction(); jj_consume_token(RENAME); SystemAction(); label_13: while (true) { - if (jj_2_68(2147483647)) { + if (jj_2_69(2147483647)) { ; } else { break label_13; @@ -1241,9 +1247,9 @@ public class PrismParser implements PrismParserConstants { // system definition component (bottom level) static final public void SystemAtomic() throws ParseException { - if (jj_2_71(2147483647)) { + if (jj_2_72(2147483647)) { SystemModule(); - } else if (jj_2_72(2147483647)) { + } else if (jj_2_73(2147483647)) { SystemBrackets(); } else { jj_consume_token(-1); @@ -1284,7 +1290,7 @@ public class PrismParser implements PrismParserConstants { // put '*' marker on stack stack.push(new Character('*')); jj_consume_token(REWARDS); - if (jj_2_73(2147483647)) { + if (jj_2_74(2147483647)) { jj_consume_token(DQUOTE); s = Identifier(); jj_consume_token(DQUOTE); @@ -1293,7 +1299,7 @@ public class PrismParser implements PrismParserConstants { } label_14: while (true) { - if (jj_2_74(2147483647)) { + if (jj_2_75(2147483647)) { ; } else { break label_14; @@ -1322,9 +1328,9 @@ public class PrismParser implements PrismParserConstants { double d; String s = ""; Token t = null; - if (jj_2_76(2147483647)) { + if (jj_2_77(2147483647)) { t = jj_consume_token(LBRACKET); - if (jj_2_75(2147483647)) { + if (jj_2_76(2147483647)) { s = Identifier(); } else { ; @@ -1372,7 +1378,7 @@ public class PrismParser implements PrismParserConstants { static final public void PCTLImplies() throws ParseException { Token t = null; PCTLOr(); - if (jj_2_77(2147483647)) { + if (jj_2_78(2147483647)) { t = jj_consume_token(IMPLIES); PCTLOr(); } else { @@ -1392,7 +1398,7 @@ public class PrismParser implements PrismParserConstants { PCTLAnd(); label_15: while (true) { - if (jj_2_78(2147483647)) { + if (jj_2_79(2147483647)) { ; } else { break label_15; @@ -1427,7 +1433,7 @@ public class PrismParser implements PrismParserConstants { PCTLNot(); label_16: while (true) { - if (jj_2_79(2147483647)) { + if (jj_2_80(2147483647)) { ; } else { break label_16; @@ -1458,7 +1464,7 @@ public class PrismParser implements PrismParserConstants { static final public void PCTLNot() throws ParseException { Token t = null; - if (jj_2_80(2147483647)) { + if (jj_2_81(2147483647)) { t = jj_consume_token(NOT); } else { ; @@ -1477,34 +1483,34 @@ public class PrismParser implements PrismParserConstants { Token tf = null; // detects if a filter is included Token tfmin = null; // detects if min of filter requested Token tfmax = null; - if (jj_2_96(2147483647)) { - if (jj_2_81(2147483647)) { + if (jj_2_97(2147483647)) { + if (jj_2_82(2147483647)) { jj_consume_token(P); relOp = LtGt(); Expression(); - } else if (jj_2_82(2147483647)) { + } else if (jj_2_83(2147483647)) { jj_consume_token(P); jj_consume_token(EQ); jj_consume_token(QMARK); relOp="="; - } else if (jj_2_83(2147483647)) { + } else if (jj_2_84(2147483647)) { jj_consume_token(P); jj_consume_token(MIN); jj_consume_token(EQ); jj_consume_token(QMARK); relOp="min="; - } else if (jj_2_84(2147483647)) { + } else if (jj_2_85(2147483647)) { jj_consume_token(P); jj_consume_token(MAX); jj_consume_token(EQ); jj_consume_token(QMARK); relOp="max="; - } else if (jj_2_85(2147483647)) { + } else if (jj_2_86(2147483647)) { jj_consume_token(PMIN); jj_consume_token(EQ); jj_consume_token(QMARK); relOp="min="; - } else if (jj_2_86(2147483647)) { + } else if (jj_2_87(2147483647)) { jj_consume_token(PMAX); jj_consume_token(EQ); jj_consume_token(QMARK); @@ -1514,36 +1520,36 @@ public class PrismParser implements PrismParserConstants { throw new ParseException(); } jj_consume_token(LBRACKET); - if (jj_2_87(2147483647)) { + if (jj_2_88(2147483647)) { PCTLProbNext(); - } else if (jj_2_88(2147483647)) { - PCTLProbBoundedUntil(); } else if (jj_2_89(2147483647)) { - PCTLProbUntil(); + PCTLProbBoundedUntil(); } else if (jj_2_90(2147483647)) { - PCTLProbBoundedFutureGlobal(); + PCTLProbUntil(); } else if (jj_2_91(2147483647)) { + PCTLProbBoundedFutureGlobal(); + } else if (jj_2_92(2147483647)) { PCTLProbFutureGlobal(); } else { jj_consume_token(-1); throw new ParseException(); } - if (jj_2_95(2147483647)) { + if (jj_2_96(2147483647)) { tf = jj_consume_token(LBRACE); PCTLFormula(); jj_consume_token(RBRACE); label_17: while (true) { - if (jj_2_92(2147483647)) { + if (jj_2_93(2147483647)) { ; } else { break label_17; } - if (jj_2_93(2147483647)) { + if (jj_2_94(2147483647)) { tfmin = jj_consume_token(LBRACE); jj_consume_token(MIN); jj_consume_token(RBRACE); - } else if (jj_2_94(2147483647)) { + } else if (jj_2_95(2147483647)) { tfmax = jj_consume_token(LBRACE); jj_consume_token(MAX); jj_consume_token(RBRACE); @@ -1577,7 +1583,7 @@ public class PrismParser implements PrismParserConstants { } // push result onto stack stack.push(pp); - } else if (jj_2_97(2147483647)) { + } else if (jj_2_98(2147483647)) { PCTLSS(); } else { jj_consume_token(-1); @@ -1604,13 +1610,13 @@ public class PrismParser implements PrismParserConstants { Token tr = null; PCTLFormula(); jj_consume_token(UNTIL); - if (jj_2_98(2147483647)) { + if (jj_2_99(2147483647)) { tle = jj_consume_token(LE); Expression(); - } else if (jj_2_99(2147483647)) { + } else if (jj_2_100(2147483647)) { tge = jj_consume_token(GE); Expression(); - } else if (jj_2_100(2147483647)) { + } else if (jj_2_101(2147483647)) { tr = jj_consume_token(LBRACKET); Expression(); jj_consume_token(COMMA); @@ -1674,21 +1680,21 @@ public class PrismParser implements PrismParserConstants { Token tle = null; // detects if a <= time bound is used Token tge = null; // detects if a >= time bound is used Token tr = null; - if (jj_2_101(2147483647)) { + if (jj_2_102(2147483647)) { tfuture = jj_consume_token(FUTURE); - } else if (jj_2_102(2147483647)) { + } else if (jj_2_103(2147483647)) { tglobal = jj_consume_token(GLOB); } else { jj_consume_token(-1); throw new ParseException(); } - if (jj_2_103(2147483647)) { + if (jj_2_104(2147483647)) { tle = jj_consume_token(LE); Expression(); - } else if (jj_2_104(2147483647)) { + } else if (jj_2_105(2147483647)) { tge = jj_consume_token(GE); Expression(); - } else if (jj_2_105(2147483647)) { + } else if (jj_2_106(2147483647)) { tr = jj_consume_token(LBRACKET); Expression(); jj_consume_token(COMMA); @@ -1732,9 +1738,9 @@ public class PrismParser implements PrismParserConstants { static final public void PCTLProbFutureGlobal() throws ParseException { Token tfuture = null; // detects if a future formula is used Token tglobal = null; - if (jj_2_106(2147483647)) { + if (jj_2_107(2147483647)) { tfuture = jj_consume_token(FUTURE); - } else if (jj_2_107(2147483647)) { + } else if (jj_2_108(2147483647)) { tglobal = jj_consume_token(GLOB); } else { jj_consume_token(-1); @@ -1756,12 +1762,12 @@ public class PrismParser implements PrismParserConstants { static final public void PCTLSS() throws ParseException { String relOp; Token tf = null; - if (jj_2_111(2147483647)) { - if (jj_2_108(2147483647)) { + if (jj_2_112(2147483647)) { + if (jj_2_109(2147483647)) { jj_consume_token(S); relOp = LtGt(); Expression(); - } else if (jj_2_109(2147483647)) { + } else if (jj_2_110(2147483647)) { jj_consume_token(S); jj_consume_token(EQ); jj_consume_token(QMARK); @@ -1772,7 +1778,7 @@ public class PrismParser implements PrismParserConstants { } jj_consume_token(LBRACKET); PCTLFormula(); - if (jj_2_110(2147483647)) { + if (jj_2_111(2147483647)) { tf = jj_consume_token(LBRACE); PCTLFormula(); jj_consume_token(RBRACE); @@ -1798,7 +1804,7 @@ public class PrismParser implements PrismParserConstants { } // push result onto stack stack.push(ss); - } else if (jj_2_112(2147483647)) { + } else if (jj_2_113(2147483647)) { PCTLReward(); } else { jj_consume_token(-1); @@ -1814,16 +1820,16 @@ public class PrismParser implements PrismParserConstants { Token tfmax = null; // detects if max of filter requested boolean b = false; // detects if a reward struct index (expression) is included String s = null; - if (jj_2_131(2147483647)) { - if (jj_2_120(2147483647)) { + if (jj_2_132(2147483647)) { + if (jj_2_121(2147483647)) { jj_consume_token(R); - if (jj_2_115(2147483647)) { + if (jj_2_116(2147483647)) { jj_consume_token(LBRACE); - if (jj_2_113(2147483647)) { + if (jj_2_114(2147483647)) { jj_consume_token(DQUOTE); s = Identifier(); jj_consume_token(DQUOTE); - } else if (jj_2_114(2147483647)) { + } else if (jj_2_115(2147483647)) { Expression(); b=true; } else { @@ -1834,19 +1840,19 @@ public class PrismParser implements PrismParserConstants { } else { ; } - if (jj_2_116(2147483647)) { + if (jj_2_117(2147483647)) { relOp = LtGt(); Expression(); - } else if (jj_2_117(2147483647)) { + } else if (jj_2_118(2147483647)) { jj_consume_token(EQ); jj_consume_token(QMARK); relOp="="; - } else if (jj_2_118(2147483647)) { + } else if (jj_2_119(2147483647)) { jj_consume_token(MIN); jj_consume_token(EQ); jj_consume_token(QMARK); relOp="min="; - } else if (jj_2_119(2147483647)) { + } else if (jj_2_120(2147483647)) { jj_consume_token(MAX); jj_consume_token(EQ); jj_consume_token(QMARK); @@ -1855,12 +1861,12 @@ public class PrismParser implements PrismParserConstants { jj_consume_token(-1); throw new ParseException(); } - } else if (jj_2_121(2147483647)) { + } else if (jj_2_122(2147483647)) { jj_consume_token(RMIN); jj_consume_token(EQ); jj_consume_token(QMARK); relOp="min="; - } else if (jj_2_122(2147483647)) { + } else if (jj_2_123(2147483647)) { jj_consume_token(RMAX); jj_consume_token(EQ); jj_consume_token(QMARK); @@ -1870,34 +1876,34 @@ public class PrismParser implements PrismParserConstants { throw new ParseException(); } jj_consume_token(LBRACKET); - if (jj_2_123(2147483647)) { + if (jj_2_124(2147483647)) { PCTLRewardCumul(); - } else if (jj_2_124(2147483647)) { - PCTLRewardInst(); } else if (jj_2_125(2147483647)) { - PCTLRewardReach(); + PCTLRewardInst(); } else if (jj_2_126(2147483647)) { + PCTLRewardReach(); + } else if (jj_2_127(2147483647)) { PCTLRewardSS(); } else { jj_consume_token(-1); throw new ParseException(); } - if (jj_2_130(2147483647)) { + if (jj_2_131(2147483647)) { tf = jj_consume_token(LBRACE); PCTLFormula(); jj_consume_token(RBRACE); label_18: while (true) { - if (jj_2_127(2147483647)) { + if (jj_2_128(2147483647)) { ; } else { break label_18; } - if (jj_2_128(2147483647)) { + if (jj_2_129(2147483647)) { tfmin = jj_consume_token(LBRACE); jj_consume_token(MIN); jj_consume_token(RBRACE); - } else if (jj_2_129(2147483647)) { + } else if (jj_2_130(2147483647)) { tfmax = jj_consume_token(LBRACE); jj_consume_token(MAX); jj_consume_token(RBRACE); @@ -1934,7 +1940,7 @@ public class PrismParser implements PrismParserConstants { } // push result onto stack stack.push(pr); - } else if (jj_2_132(2147483647)) { + } else if (jj_2_133(2147483647)) { PCTLInit(); } else { jj_consume_token(-1); @@ -1999,12 +2005,12 @@ public class PrismParser implements PrismParserConstants { // init static final public void PCTLInit() throws ParseException { - if (jj_2_133(2147483647)) { + if (jj_2_134(2147483647)) { jj_consume_token(DQUOTE); jj_consume_token(INIT); jj_consume_token(DQUOTE); stack.push(new PCTLInit()); - } else if (jj_2_134(2147483647)) { + } else if (jj_2_135(2147483647)) { PCTLLabel(); } else { jj_consume_token(-1); @@ -2015,12 +2021,12 @@ public class PrismParser implements PrismParserConstants { // label static final public void PCTLLabel() throws ParseException { String s; - if (jj_2_135(2147483647)) { + if (jj_2_136(2147483647)) { jj_consume_token(DQUOTE); s = Identifier(); jj_consume_token(DQUOTE); stack.push(new PCTLLabel(s)); - } else if (jj_2_136(2147483647)) { + } else if (jj_2_137(2147483647)) { PCTLBrackets(); } else { jj_consume_token(-1); @@ -2030,14 +2036,14 @@ public class PrismParser implements PrismParserConstants { // brackets static final public void PCTLBrackets() throws ParseException { - if (jj_2_137(2147483647)) { + if (jj_2_138(2147483647)) { jj_consume_token(LPARENTH); PCTLFormula(); jj_consume_token(RPARENTH); PCTLBrackets e = new PCTLBrackets(); e.setOperand((PCTLFormula)stack.pop()); stack.push(e); - } else if (jj_2_138(2147483647)) { + } else if (jj_2_139(2147483647)) { PCTLExpression(); } else { jj_consume_token(-1); @@ -2065,7 +2071,7 @@ public class PrismParser implements PrismParserConstants { Expression(); jj_consume_token(COLON); Expression(); - if (jj_2_139(2147483647)) { + if (jj_2_140(2147483647)) { t = jj_consume_token(COLON); Expression(); } else { @@ -2098,7 +2104,7 @@ public class PrismParser implements PrismParserConstants { // expression (if-then-else) static final public void ExpressionITE() throws ParseException { - if (jj_2_140(2147483647)) { + if (jj_2_141(2147483647)) { ExpressionOr(); jj_consume_token(QMARK); ExpressionOr(); @@ -2109,7 +2115,7 @@ public class PrismParser implements PrismParserConstants { t = (Expression)stack.pop(); c = (Expression)stack.pop(); stack.push(new ExpressionITE(c, t, e)); - } else if (jj_2_141(2147483647)) { + } else if (jj_2_142(2147483647)) { ExpressionOr(); } else { jj_consume_token(-1); @@ -2122,7 +2128,7 @@ public class PrismParser implements PrismParserConstants { // put '*' marker on stack stack.push(new Character('*')); ExpressionAnd(); - if (jj_2_142(2147483647)) { + if (jj_2_143(2147483647)) { jj_consume_token(OR); ExpressionOr(); } else { @@ -2156,7 +2162,7 @@ public class PrismParser implements PrismParserConstants { ExpressionNot(); label_19: while (true) { - if (jj_2_143(2147483647)) { + if (jj_2_144(2147483647)) { ; } else { break label_19; @@ -2188,7 +2194,7 @@ public class PrismParser implements PrismParserConstants { // expression (not) static final public void ExpressionNot() throws ParseException { Token t = null; - if (jj_2_144(2147483647)) { + if (jj_2_145(2147483647)) { t = jj_consume_token(NOT); } else { ; @@ -2210,7 +2216,7 @@ public class PrismParser implements PrismParserConstants { Expression e, e1, e2; // put '*' marker on stack stack.push(new Character('*')); - if (jj_2_148(2147483647)) { + if (jj_2_149(2147483647)) { ExpressionPlusMinus(); relOp = LtGt(); ExpressionPlusMinus(); @@ -2223,14 +2229,14 @@ public class PrismParser implements PrismParserConstants { stack.pop(); // push the ExpressionRelOp on to the stack stack.push(ero); - } else if (jj_2_149(2147483647)) { + } else if (jj_2_150(2147483647)) { ExpressionPlusMinus(); relOp = EqNeq(); // store the left hand side expression so that it // doesn't get mixed up with those on the right hand side e = (Expression)stack.pop(); ExpressionPlusMinus(); - if (jj_2_145(2147483647)) { + if (jj_2_146(2147483647)) { jj_consume_token(DOTS); // push a "2" on to the stack to indicate there are a pair of expressions here // (it is sandwiched between pair in stack) @@ -2241,14 +2247,14 @@ public class PrismParser implements PrismParserConstants { } label_20: while (true) { - if (jj_2_146(2147483647)) { + if (jj_2_147(2147483647)) { ; } else { break label_20; } jj_consume_token(COMMA); ExpressionPlusMinus(); - if (jj_2_147(2147483647)) { + if (jj_2_148(2147483647)) { jj_consume_token(DOTS); // push a "2" on to the stack to indicate there are a pair of expressions here // (it is sandwiched between pair in stack) @@ -2307,7 +2313,7 @@ public class PrismParser implements PrismParserConstants { // push the ExpressionRange on to the stack stack.push(er); } - } else if (jj_2_150(2147483647)) { + } else if (jj_2_151(2147483647)) { ExpressionPlusMinus(); // but still pop marker off stack e = (Expression)stack.pop(); @@ -2325,14 +2331,14 @@ public class PrismParser implements PrismParserConstants { ExpressionTimesDivide(); label_21: while (true) { - if (jj_2_151(2147483647)) { + if (jj_2_152(2147483647)) { ; } else { break label_21; } - if (jj_2_152(2147483647)) { + if (jj_2_153(2147483647)) { t = jj_consume_token(PLUS); - } else if (jj_2_153(2147483647)) { + } else if (jj_2_154(2147483647)) { t = jj_consume_token(MINUS); } else { jj_consume_token(-1); @@ -2365,14 +2371,14 @@ public class PrismParser implements PrismParserConstants { ExpressionUnaryMinus(); label_22: while (true) { - if (jj_2_154(2147483647)) { + if (jj_2_155(2147483647)) { ; } else { break label_22; } - if (jj_2_155(2147483647)) { + if (jj_2_156(2147483647)) { t = jj_consume_token(TIMES); - } else if (jj_2_156(2147483647)) { + } else if (jj_2_157(2147483647)) { t = jj_consume_token(DIVIDE); } else { jj_consume_token(-1); @@ -2401,14 +2407,14 @@ public class PrismParser implements PrismParserConstants { // expression: unary minus (right associative) static final public void ExpressionUnaryMinus() throws ParseException { - if (jj_2_157(2147483647)) { + if (jj_2_158(2147483647)) { jj_consume_token(MINUS); ExpressionFunc(); // create new expression and push to stack ExpressionUnaryMinus e = new ExpressionUnaryMinus(); e.setOperand((Expression)stack.pop()); stack.push(e); - } else if (jj_2_158(2147483647)) { + } else if (jj_2_159(2147483647)) { ExpressionFunc(); } else { jj_consume_token(-1); @@ -2422,18 +2428,18 @@ public class PrismParser implements PrismParserConstants { String s = null; // put '*' marker on stack stack.push(new Character('*')); - if (jj_2_171(2147483647)) { - if (jj_2_168(2147483647)) { - if (jj_2_159(2147483647)) { + if (jj_2_172(2147483647)) { + if (jj_2_169(2147483647)) { + if (jj_2_160(2147483647)) { jj_consume_token(MIN); s="min"; - } else if (jj_2_160(2147483647)) { + } else if (jj_2_161(2147483647)) { jj_consume_token(MAX); s="max"; - } else if (jj_2_161(2147483647)) { + } else if (jj_2_162(2147483647)) { jj_consume_token(FLOOR); s="floor"; - } else if (jj_2_162(2147483647)) { + } else if (jj_2_163(2147483647)) { jj_consume_token(CEIL); s="ceil"; } else { @@ -2441,21 +2447,21 @@ public class PrismParser implements PrismParserConstants { throw new ParseException(); } jj_consume_token(LPARENTH); - } else if (jj_2_169(2147483647)) { + } else if (jj_2_170(2147483647)) { tFunc = jj_consume_token(FUNC); jj_consume_token(LPARENTH); - if (jj_2_163(2147483647)) { + if (jj_2_164(2147483647)) { s = Identifier(); - } else if (jj_2_164(2147483647)) { + } else if (jj_2_165(2147483647)) { jj_consume_token(MIN); s="min"; - } else if (jj_2_165(2147483647)) { + } else if (jj_2_166(2147483647)) { jj_consume_token(MAX); s="max"; - } else if (jj_2_166(2147483647)) { + } else if (jj_2_167(2147483647)) { jj_consume_token(FLOOR); s="floor"; - } else if (jj_2_167(2147483647)) { + } else if (jj_2_168(2147483647)) { jj_consume_token(CEIL); s="ceil"; } else { @@ -2470,7 +2476,7 @@ public class PrismParser implements PrismParserConstants { Expression(); label_23: while (true) { - if (jj_2_170(2147483647)) { + if (jj_2_171(2147483647)) { ; } else { break label_23; @@ -2496,7 +2502,7 @@ public class PrismParser implements PrismParserConstants { e.setOldStyle(tFunc == null); // put the ExpressionFunc on the stack stack.push(e); - } else if (jj_2_172(2147483647)) { + } else if (jj_2_173(2147483647)) { ExpressionIdent(); // remove '*' marker Expression e = (Expression)stack.pop(); @@ -2511,12 +2517,12 @@ public class PrismParser implements PrismParserConstants { // expression (identifier) static final public void ExpressionIdent() throws ParseException { String ident; - if (jj_2_173(2147483647)) { + if (jj_2_174(2147483647)) { ident = Identifier(); ExpressionIdent e = new ExpressionIdent(); e.setName(ident); stack.push(e); - } else if (jj_2_174(2147483647)) { + } else if (jj_2_175(2147483647)) { ExpressionLiteral(); } else { jj_consume_token(-1); @@ -2528,25 +2534,25 @@ public class PrismParser implements PrismParserConstants { static final public void ExpressionLiteral() throws ParseException { int i; String d; - if (jj_2_175(2147483647)) { + if (jj_2_176(2147483647)) { i = Int(); ExpressionInt e = new ExpressionInt(); e.setValue(i); stack.push(e); - } else if (jj_2_176(2147483647)) { + } else if (jj_2_177(2147483647)) { d = Double(); ExpressionDouble e = new ExpressionDouble(); e.setValue(d); stack.push(e); - } else if (jj_2_177(2147483647)) { + } else if (jj_2_178(2147483647)) { jj_consume_token(TRUE); ExpressionTrue e = new ExpressionTrue(); stack.push(e); - } else if (jj_2_178(2147483647)) { + } else if (jj_2_179(2147483647)) { jj_consume_token(FALSE); ExpressionFalse e = new ExpressionFalse(); stack.push(e); - } else if (jj_2_179(2147483647)) { + } else if (jj_2_180(2147483647)) { ExpressionBrackets(); } else { jj_consume_token(-1); @@ -2587,9 +2593,9 @@ public class PrismParser implements PrismParserConstants { // one of the relational operators: =, != static final public String EqNeq() throws ParseException { - if (jj_2_180(2147483647)) { + if (jj_2_181(2147483647)) { jj_consume_token(EQ); - } else if (jj_2_181(2147483647)) { + } else if (jj_2_182(2147483647)) { jj_consume_token(NE); } else { jj_consume_token(-1); @@ -2601,13 +2607,13 @@ public class PrismParser implements PrismParserConstants { // one of the relational operators: >, <, >=, <= static final public String LtGt() throws ParseException { - if (jj_2_182(2147483647)) { + if (jj_2_183(2147483647)) { jj_consume_token(GT); - } else if (jj_2_183(2147483647)) { - jj_consume_token(LT); } else if (jj_2_184(2147483647)) { - jj_consume_token(GE); + jj_consume_token(LT); } else if (jj_2_185(2147483647)) { + jj_consume_token(GE); + } else if (jj_2_186(2147483647)) { jj_consume_token(LE); } else { jj_consume_token(-1); @@ -3929,57 +3935,34 @@ public class PrismParser implements PrismParserConstants { finally { jj_save(184, xla); } } - static final private boolean jj_3_98() { - if (jj_scan_token(LE)) return true; - if (jj_3R_35()) return true; - return false; - } - - static final private boolean jj_3R_73() { - Token xsp; - xsp = jj_scanpos; - if (jj_3_140()) { - jj_scanpos = xsp; - if (jj_3_141()) return true; - } - return false; - } - - static final private boolean jj_3_179() { - if (jj_3R_84()) return true; - return false; - } - - static final private boolean jj_3_140() { - if (jj_3R_72()) return true; - if (jj_scan_token(QMARK)) return true; - if (jj_3R_72()) return true; - if (jj_scan_token(COLON)) return true; - if (jj_3R_73()) return true; - return false; + static final private boolean jj_2_186(int xla) { + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return !jj_3_186(); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(185, xla); } } - static final private boolean jj_3_162() { + static final private boolean jj_3_163() { if (jj_scan_token(CEIL)) return true; return false; } - static final private boolean jj_3_178() { + static final private boolean jj_3_179() { if (jj_scan_token(FALSE)) return true; return false; } - static final private boolean jj_3_165() { + static final private boolean jj_3_166() { if (jj_scan_token(MAX)) return true; return false; } - static final private boolean jj_3_58() { + static final private boolean jj_3_59() { if (jj_scan_token(CEIL)) return true; return false; } - static final private boolean jj_3_53() { + static final private boolean jj_3_54() { if (jj_scan_token(CEIL)) return true; return false; } @@ -3989,22 +3972,22 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_177() { + static final private boolean jj_3_178() { if (jj_scan_token(TRUE)) return true; return false; } - static final private boolean jj_3_90() { + static final private boolean jj_3_91() { if (jj_3R_59()) return true; return false; } - static final private boolean jj_3_176() { + static final private boolean jj_3_177() { if (jj_3R_83()) return true; return false; } - static final private boolean jj_3_27() { + static final private boolean jj_3_28() { if (jj_scan_token(EQ)) return true; if (jj_3R_35()) return true; return false; @@ -4015,11 +3998,11 @@ public class PrismParser implements PrismParserConstants { if (jj_scan_token(UNTIL)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_98()) { - jj_scanpos = xsp; if (jj_3_99()) { jj_scanpos = xsp; - if (jj_3_100()) return true; + if (jj_3_100()) { + jj_scanpos = xsp; + if (jj_3_101()) return true; } } if (jj_3R_61()) return true; @@ -4034,7 +4017,7 @@ public class PrismParser implements PrismParserConstants { Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_65()) { jj_scanpos = xsp; break; } + if (jj_3_66()) { jj_scanpos = xsp; break; } } if (jj_scan_token(RBRACKET)) return true; if (jj_scan_token(OR)) return true; @@ -4042,7 +4025,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_64() { + static final private boolean jj_3_65() { if (jj_scan_token(OR)) return true; if (jj_scan_token(OR)) return true; if (jj_scan_token(OR)) return true; @@ -4053,15 +4036,15 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_81() { Token xsp; xsp = jj_scanpos; - if (jj_3_175()) { - jj_scanpos = xsp; if (jj_3_176()) { jj_scanpos = xsp; if (jj_3_177()) { jj_scanpos = xsp; if (jj_3_178()) { jj_scanpos = xsp; - if (jj_3_179()) return true; + if (jj_3_179()) { + jj_scanpos = xsp; + if (jj_3_180()) return true; } } } @@ -4069,65 +4052,65 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_28() { + static final private boolean jj_3R_29() { if (jj_scan_token(MODULE)) return true; if (jj_3R_36()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_33()) { jj_scanpos = xsp; break; } + if (jj_3_34()) { jj_scanpos = xsp; break; } } while (true) { xsp = jj_scanpos; - if (jj_3_34()) { jj_scanpos = xsp; break; } + if (jj_3_35()) { jj_scanpos = xsp; break; } } if (jj_scan_token(ENDMODULE)) return true; return false; } - static final private boolean jj_3_175() { + static final private boolean jj_3_176() { if (jj_3R_82()) return true; return false; } - static final private boolean jj_3_161() { + static final private boolean jj_3_162() { if (jj_scan_token(FLOOR)) return true; return false; } - static final private boolean jj_3_164() { + static final private boolean jj_3_165() { if (jj_scan_token(MIN)) return true; return false; } - static final private boolean jj_3_89() { + static final private boolean jj_3_90() { if (jj_3R_58()) return true; return false; } - static final private boolean jj_3_174() { + static final private boolean jj_3_175() { if (jj_3R_81()) return true; return false; } - static final private boolean jj_3_57() { + static final private boolean jj_3_58() { if (jj_scan_token(FLOOR)) return true; return false; } - static final private boolean jj_3_52() { + static final private boolean jj_3_53() { if (jj_scan_token(FLOOR)) return true; return false; } - static final private boolean jj_3_94() { + static final private boolean jj_3_95() { if (jj_scan_token(LBRACE)) return true; if (jj_scan_token(MAX)) return true; if (jj_scan_token(RBRACE)) return true; return false; } - static final private boolean jj_3R_27() { + static final private boolean jj_3R_28() { if (jj_scan_token(GLOBAL)) return true; if (jj_3R_37()) return true; return false; @@ -4142,25 +4125,25 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_80() { Token xsp; xsp = jj_scanpos; - if (jj_3_173()) { + if (jj_3_174()) { jj_scanpos = xsp; - if (jj_3_174()) return true; + if (jj_3_175()) return true; } return false; } - static final private boolean jj_3_173() { + static final private boolean jj_3_174() { if (jj_3R_36()) return true; return false; } - static final private boolean jj_3_24() { + static final private boolean jj_3_25() { if (jj_scan_token(EQ)) return true; if (jj_3R_35()) return true; return false; } - static final private boolean jj_3_26() { + static final private boolean jj_3_27() { if (jj_scan_token(PROB)) return true; return false; } @@ -4168,43 +4151,43 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_45() { if (jj_3R_47()) return true; Token xsp; - if (jj_3_64()) return true; + if (jj_3_65()) return true; while (true) { xsp = jj_scanpos; - if (jj_3_64()) { jj_scanpos = xsp; break; } + if (jj_3_65()) { jj_scanpos = xsp; break; } } return false; } - static final private boolean jj_3_97() { + static final private boolean jj_3_98() { if (jj_3R_62()) return true; return false; } - static final private boolean jj_3_23() { + static final private boolean jj_3_24() { if (jj_scan_token(EQ)) return true; if (jj_3R_35()) return true; return false; } - static final private boolean jj_3_63() { + static final private boolean jj_3_64() { if (jj_scan_token(OR)) return true; if (jj_scan_token(OR)) return true; if (jj_3R_47()) return true; return false; } - static final private boolean jj_3_163() { + static final private boolean jj_3_164() { if (jj_3R_36()) return true; return false; } - static final private boolean jj_3_25() { + static final private boolean jj_3_26() { if (jj_scan_token(RATE)) return true; return false; } - static final private boolean jj_3_160() { + static final private boolean jj_3_161() { if (jj_scan_token(MAX)) return true; return false; } @@ -4214,63 +4197,63 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_172() { + static final private boolean jj_3_173() { if (jj_3R_80()) return true; return false; } - static final private boolean jj_3_32() { + static final private boolean jj_3_33() { Token xsp; xsp = jj_scanpos; - if (jj_3_25()) { + if (jj_3_26()) { jj_scanpos = xsp; - if (jj_3_26()) return true; + if (jj_3_27()) return true; } if (jj_3R_36()) return true; xsp = jj_scanpos; - if (jj_3_27()) jj_scanpos = xsp; + if (jj_3_28()) jj_scanpos = xsp; if (jj_scan_token(SEMICOLON)) return true; return false; } - static final private boolean jj_3_88() { + static final private boolean jj_3_89() { if (jj_3R_57()) return true; return false; } - static final private boolean jj_3_22() { + static final private boolean jj_3_23() { if (jj_scan_token(EQ)) return true; if (jj_3R_35()) return true; return false; } - static final private boolean jj_3_170() { + static final private boolean jj_3_171() { if (jj_scan_token(COMMA)) return true; if (jj_3R_35()) return true; return false; } - static final private boolean jj_3_56() { + static final private boolean jj_3_57() { if (jj_scan_token(MAX)) return true; return false; } - static final private boolean jj_3_51() { + static final private boolean jj_3_52() { if (jj_scan_token(MAX)) return true; return false; } - static final private boolean jj_3_31() { + static final private boolean jj_3_32() { if (jj_scan_token(CONST)) return true; if (jj_3R_36()) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_24()) jj_scanpos = xsp; + if (jj_3_25()) jj_scanpos = xsp; if (jj_scan_token(SEMICOLON)) return true; return false; } - static final private boolean jj_3_138() { + static final private boolean jj_3_139() { if (jj_3R_71()) return true; return false; } @@ -4278,49 +4261,49 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_44() { if (jj_3R_47()) return true; Token xsp; - if (jj_3_63()) return true; + if (jj_3_64()) return true; while (true) { xsp = jj_scanpos; - if (jj_3_63()) { jj_scanpos = xsp; break; } + if (jj_3_64()) { jj_scanpos = xsp; break; } } return false; } - static final private boolean jj_3_92() { + static final private boolean jj_3_93() { Token xsp; xsp = jj_scanpos; - if (jj_3_93()) { + if (jj_3_94()) { jj_scanpos = xsp; - if (jj_3_94()) return true; + if (jj_3_95()) return true; } return false; } - static final private boolean jj_3_93() { + static final private boolean jj_3_94() { if (jj_scan_token(LBRACE)) return true; if (jj_scan_token(MIN)) return true; if (jj_scan_token(RBRACE)) return true; return false; } - static final private boolean jj_3_95() { + static final private boolean jj_3_96() { if (jj_scan_token(LBRACE)) return true; if (jj_3R_61()) return true; if (jj_scan_token(RBRACE)) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_92()) { jj_scanpos = xsp; break; } + if (jj_3_93()) { jj_scanpos = xsp; break; } } return false; } - static final private boolean jj_3_87() { + static final private boolean jj_3_88() { if (jj_3R_56()) return true; return false; } - static final private boolean jj_3_21() { + static final private boolean jj_3_22() { if (jj_scan_token(EQ)) return true; if (jj_3R_35()) return true; return false; @@ -4329,27 +4312,27 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_70() { Token xsp; xsp = jj_scanpos; - if (jj_3_137()) { + if (jj_3_138()) { jj_scanpos = xsp; - if (jj_3_138()) return true; + if (jj_3_139()) return true; } return false; } - static final private boolean jj_3_169() { + static final private boolean jj_3_170() { if (jj_scan_token(FUNC)) return true; if (jj_scan_token(LPARENTH)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_163()) { - jj_scanpos = xsp; if (jj_3_164()) { jj_scanpos = xsp; if (jj_3_165()) { jj_scanpos = xsp; if (jj_3_166()) { jj_scanpos = xsp; - if (jj_3_167()) return true; + if (jj_3_167()) { + jj_scanpos = xsp; + if (jj_3_168()) return true; } } } @@ -4358,40 +4341,40 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_159() { + static final private boolean jj_3_160() { if (jj_scan_token(MIN)) return true; return false; } - static final private boolean jj_3_137() { + static final private boolean jj_3_138() { if (jj_scan_token(LPARENTH)) return true; if (jj_3R_61()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } - static final private boolean jj_3_20() { + static final private boolean jj_3_21() { if (jj_scan_token(CTMC)) return true; return false; } - static final private boolean jj_3_86() { + static final private boolean jj_3_87() { if (jj_scan_token(PMAX)) return true; if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static final private boolean jj_3_168() { + static final private boolean jj_3_169() { Token xsp; xsp = jj_scanpos; - if (jj_3_159()) { - jj_scanpos = xsp; if (jj_3_160()) { jj_scanpos = xsp; if (jj_3_161()) { jj_scanpos = xsp; - if (jj_3_162()) return true; + if (jj_3_162()) { + jj_scanpos = xsp; + if (jj_3_163()) return true; } } } @@ -4399,7 +4382,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_85() { + static final private boolean jj_3_86() { if (jj_scan_token(PMIN)) return true; if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; @@ -4409,30 +4392,30 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_79() { Token xsp; xsp = jj_scanpos; - if (jj_3_171()) { + if (jj_3_172()) { jj_scanpos = xsp; - if (jj_3_172()) return true; + if (jj_3_173()) return true; } return false; } - static final private boolean jj_3_171() { + static final private boolean jj_3_172() { Token xsp; xsp = jj_scanpos; - if (jj_3_168()) { + if (jj_3_169()) { jj_scanpos = xsp; - if (jj_3_169()) return true; + if (jj_3_170()) return true; } if (jj_3R_35()) return true; while (true) { xsp = jj_scanpos; - if (jj_3_170()) { jj_scanpos = xsp; break; } + if (jj_3_171()) { jj_scanpos = xsp; break; } } if (jj_scan_token(RPARENTH)) return true; return false; } - static final private boolean jj_3_84() { + static final private boolean jj_3_85() { if (jj_scan_token(P)) return true; if (jj_scan_token(MAX)) return true; if (jj_scan_token(EQ)) return true; @@ -4440,18 +4423,18 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_30() { + static final private boolean jj_3_31() { if (jj_scan_token(CONST)) return true; if (jj_scan_token(BOOL)) return true; if (jj_3R_36()) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_23()) jj_scanpos = xsp; + if (jj_3_24()) jj_scanpos = xsp; if (jj_scan_token(SEMICOLON)) return true; return false; } - static final private boolean jj_3_83() { + static final private boolean jj_3_84() { if (jj_scan_token(P)) return true; if (jj_scan_token(MIN)) return true; if (jj_scan_token(EQ)) return true; @@ -4459,31 +4442,31 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_62() { + static final private boolean jj_3_63() { if (jj_3R_47()) return true; return false; } - static final private boolean jj_3_82() { + static final private boolean jj_3_83() { if (jj_scan_token(P)) return true; if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static final private boolean jj_3_81() { + static final private boolean jj_3_82() { if (jj_scan_token(P)) return true; if (jj_3R_55()) return true; if (jj_3R_35()) return true; return false; } - static final private boolean jj_3_136() { + static final private boolean jj_3_137() { if (jj_3R_70()) return true; return false; } - static final private boolean jj_3_61() { + static final private boolean jj_3_62() { if (jj_3R_46()) return true; return false; } @@ -4491,23 +4474,21 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_89() { Token xsp; xsp = jj_scanpos; - if (jj_3_96()) { + if (jj_3_97()) { jj_scanpos = xsp; - if (jj_3_97()) return true; + if (jj_3_98()) return true; } return false; } - static final private boolean jj_3_19() { + static final private boolean jj_3_20() { if (jj_scan_token(MDP)) return true; return false; } - static final private boolean jj_3_96() { + static final private boolean jj_3_97() { Token xsp; xsp = jj_scanpos; - if (jj_3_81()) { - jj_scanpos = xsp; if (jj_3_82()) { jj_scanpos = xsp; if (jj_3_83()) { @@ -4516,7 +4497,9 @@ public class PrismParser implements PrismParserConstants { jj_scanpos = xsp; if (jj_3_85()) { jj_scanpos = xsp; - if (jj_3_86()) return true; + if (jj_3_86()) { + jj_scanpos = xsp; + if (jj_3_87()) return true; } } } @@ -4524,26 +4507,26 @@ public class PrismParser implements PrismParserConstants { } if (jj_scan_token(LBRACKET)) return true; xsp = jj_scanpos; - if (jj_3_87()) { - jj_scanpos = xsp; if (jj_3_88()) { jj_scanpos = xsp; if (jj_3_89()) { jj_scanpos = xsp; if (jj_3_90()) { jj_scanpos = xsp; - if (jj_3_91()) return true; + if (jj_3_91()) { + jj_scanpos = xsp; + if (jj_3_92()) return true; } } } } xsp = jj_scanpos; - if (jj_3_95()) jj_scanpos = xsp; + if (jj_3_96()) jj_scanpos = xsp; if (jj_scan_token(RBRACKET)) return true; return false; } - static final private boolean jj_3_60() { + static final private boolean jj_3_61() { if (jj_3R_45()) return true; return false; } @@ -4551,25 +4534,25 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_86() { Token xsp; xsp = jj_scanpos; - if (jj_3_59()) { - jj_scanpos = xsp; if (jj_3_60()) { jj_scanpos = xsp; if (jj_3_61()) { jj_scanpos = xsp; - if (jj_3_62()) return true; + if (jj_3_62()) { + jj_scanpos = xsp; + if (jj_3_63()) return true; } } } return false; } - static final private boolean jj_3_59() { + static final private boolean jj_3_60() { if (jj_3R_44()) return true; return false; } - static final private boolean jj_3_55() { + static final private boolean jj_3_56() { if (jj_scan_token(MIN)) return true; return false; } @@ -4577,57 +4560,57 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_69() { Token xsp; xsp = jj_scanpos; - if (jj_3_135()) { + if (jj_3_136()) { jj_scanpos = xsp; - if (jj_3_136()) return true; + if (jj_3_137()) return true; } return false; } - static final private boolean jj_3_50() { + static final private boolean jj_3_51() { if (jj_scan_token(MIN)) return true; return false; } - static final private boolean jj_3_135() { + static final private boolean jj_3_136() { if (jj_scan_token(DQUOTE)) return true; if (jj_3R_36()) return true; if (jj_scan_token(DQUOTE)) return true; return false; } - static final private boolean jj_3_156() { + static final private boolean jj_3_157() { if (jj_scan_token(DIVIDE)) return true; return false; } - static final private boolean jj_3_158() { + static final private boolean jj_3_159() { if (jj_3R_79()) return true; return false; } - static final private boolean jj_3_29() { + static final private boolean jj_3_30() { if (jj_scan_token(CONST)) return true; if (jj_scan_token(DOUBLE)) return true; if (jj_3R_36()) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_22()) jj_scanpos = xsp; + if (jj_3_23()) jj_scanpos = xsp; if (jj_scan_token(SEMICOLON)) return true; return false; } - static final private boolean jj_3_18() { + static final private boolean jj_3_19() { if (jj_scan_token(DTMC)) return true; return false; } - static final private boolean jj_3_134() { + static final private boolean jj_3_135() { if (jj_3R_69()) return true; return false; } - static final private boolean jj_3R_30() { + static final private boolean jj_3R_31() { if (jj_scan_token(SYSTEM)) return true; if (jj_3R_86()) return true; if (jj_scan_token(ENDSYSTEM)) return true; @@ -4637,25 +4620,25 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_78() { Token xsp; xsp = jj_scanpos; - if (jj_3_157()) { + if (jj_3_158()) { jj_scanpos = xsp; - if (jj_3_158()) return true; + if (jj_3_159()) return true; } return false; } - static final private boolean jj_3_157() { + static final private boolean jj_3_158() { if (jj_scan_token(MINUS)) return true; if (jj_3R_79()) return true; return false; } - static final private boolean jj_3_155() { + static final private boolean jj_3_156() { if (jj_scan_token(TIMES)) return true; return false; } - static final private boolean jj_3_80() { + static final private boolean jj_3_81() { if (jj_scan_token(NOT)) return true; return false; } @@ -4663,26 +4646,26 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_68() { Token xsp; xsp = jj_scanpos; - if (jj_3_133()) { + if (jj_3_134()) { jj_scanpos = xsp; - if (jj_3_134()) return true; + if (jj_3_135()) return true; } return false; } - static final private boolean jj_3_133() { + static final private boolean jj_3_134() { if (jj_scan_token(DQUOTE)) return true; if (jj_scan_token(INIT)) return true; if (jj_scan_token(DQUOTE)) return true; return false; } - static final private boolean jj_3_154() { + static final private boolean jj_3_155() { Token xsp; xsp = jj_scanpos; - if (jj_3_155()) { + if (jj_3_156()) { jj_scanpos = xsp; - if (jj_3_156()) return true; + if (jj_3_157()) return true; } if (jj_3R_78()) return true; return false; @@ -4691,23 +4674,23 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_54() { Token xsp; xsp = jj_scanpos; - if (jj_3_80()) jj_scanpos = xsp; + if (jj_3_81()) jj_scanpos = xsp; if (jj_3R_89()) return true; return false; } - static final private boolean jj_3R_26() { + static final private boolean jj_3R_27() { Token xsp; xsp = jj_scanpos; - if (jj_3_28()) { - jj_scanpos = xsp; if (jj_3_29()) { jj_scanpos = xsp; if (jj_3_30()) { jj_scanpos = xsp; if (jj_3_31()) { jj_scanpos = xsp; - if (jj_3_32()) return true; + if (jj_3_32()) { + jj_scanpos = xsp; + if (jj_3_33()) return true; } } } @@ -4715,34 +4698,34 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_28() { + static final private boolean jj_3_29() { if (jj_scan_token(CONST)) return true; if (jj_scan_token(INT)) return true; if (jj_3R_36()) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_21()) jj_scanpos = xsp; + if (jj_3_22()) jj_scanpos = xsp; if (jj_scan_token(SEMICOLON)) return true; return false; } - static final private boolean jj_3_17() { + static final private boolean jj_3_18() { if (jj_scan_token(STOCHASTIC)) return true; return false; } - static final private boolean jj_3_48() { + static final private boolean jj_3_49() { if (jj_scan_token(COMMA)) return true; if (jj_3R_43()) return true; return false; } - static final private boolean jj_3_54() { + static final private boolean jj_3_55() { if (jj_3R_36()) return true; return false; } - static final private boolean jj_3_49() { + static final private boolean jj_3_50() { if (jj_3R_36()) return true; return false; } @@ -4750,30 +4733,30 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_43() { Token xsp; xsp = jj_scanpos; - if (jj_3_49()) { - jj_scanpos = xsp; if (jj_3_50()) { jj_scanpos = xsp; if (jj_3_51()) { jj_scanpos = xsp; if (jj_3_52()) { jj_scanpos = xsp; - if (jj_3_53()) return true; + if (jj_3_53()) { + jj_scanpos = xsp; + if (jj_3_54()) return true; } } } } if (jj_scan_token(EQ)) return true; xsp = jj_scanpos; - if (jj_3_54()) { - jj_scanpos = xsp; if (jj_3_55()) { jj_scanpos = xsp; if (jj_3_56()) { jj_scanpos = xsp; if (jj_3_57()) { jj_scanpos = xsp; - if (jj_3_58()) return true; + if (jj_3_58()) { + jj_scanpos = xsp; + if (jj_3_59()) return true; } } } @@ -4781,17 +4764,22 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3_11() { + if (jj_3R_33()) return true; + return false; + } + static final private boolean jj_3R_67() { if (jj_scan_token(S)) return true; return false; } - static final private boolean jj_3_153() { + static final private boolean jj_3_154() { if (jj_scan_token(MINUS)) return true; return false; } - static final private boolean jj_3_79() { + static final private boolean jj_3_80() { if (jj_scan_token(AND)) return true; if (jj_3R_54()) return true; return false; @@ -4802,12 +4790,12 @@ public class PrismParser implements PrismParserConstants { Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_48()) { jj_scanpos = xsp; break; } + if (jj_3_49()) { jj_scanpos = xsp; break; } } return false; } - static final private boolean jj_3R_33() { + static final private boolean jj_3R_26() { if (jj_scan_token(LABEL)) return true; if (jj_scan_token(DQUOTE)) return true; if (jj_3R_36()) return true; @@ -4818,12 +4806,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_10() { - if (jj_3R_32()) return true; - return false; - } - - static final private boolean jj_3_16() { + static final private boolean jj_3_17() { if (jj_scan_token(NONDETERMINISTIC)) return true; return false; } @@ -4833,33 +4816,38 @@ public class PrismParser implements PrismParserConstants { Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_154()) { jj_scanpos = xsp; break; } + if (jj_3_155()) { jj_scanpos = xsp; break; } } return false; } - static final private boolean jj_3_152() { + static final private boolean jj_3_153() { if (jj_scan_token(PLUS)) return true; return false; } - static final private boolean jj_3_151() { + static final private boolean jj_3_152() { Token xsp; xsp = jj_scanpos; - if (jj_3_152()) { + if (jj_3_153()) { jj_scanpos = xsp; - if (jj_3_153()) return true; + if (jj_3_154()) return true; } if (jj_3R_77()) return true; return false; } + static final private boolean jj_3_10() { + if (jj_3R_32()) return true; + return false; + } + static final private boolean jj_3R_53() { if (jj_3R_54()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_79()) { jj_scanpos = xsp; break; } + if (jj_3_80()) { jj_scanpos = xsp; break; } } return false; } @@ -4879,12 +4867,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_9() { - if (jj_3R_31()) return true; - return false; - } - - static final private boolean jj_3R_29() { + static final private boolean jj_3R_30() { if (jj_scan_token(MODULE)) return true; if (jj_3R_36()) return true; if (jj_scan_token(EQ)) return true; @@ -4896,16 +4879,19 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_15() { + static final private boolean jj_3_16() { if (jj_scan_token(PROBABILISTIC)) return true; return false; } + static final private boolean jj_3_9() { + if (jj_3R_31()) return true; + return false; + } + static final private boolean jj_3R_24() { Token xsp; xsp = jj_scanpos; - if (jj_3_15()) { - jj_scanpos = xsp; if (jj_3_16()) { jj_scanpos = xsp; if (jj_3_17()) { @@ -4914,7 +4900,9 @@ public class PrismParser implements PrismParserConstants { jj_scanpos = xsp; if (jj_3_19()) { jj_scanpos = xsp; - if (jj_3_20()) return true; + if (jj_3_20()) { + jj_scanpos = xsp; + if (jj_3_21()) return true; } } } @@ -4923,13 +4911,18 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_78() { + static final private boolean jj_3_79() { if (jj_scan_token(OR)) return true; if (jj_3R_53()) return true; return false; } - static final private boolean jj_3_126() { + static final private boolean jj_3_15() { + if (jj_3R_34()) return true; + return false; + } + + static final private boolean jj_3_127() { if (jj_3R_67()) return true; return false; } @@ -4941,22 +4934,17 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_8() { - if (jj_3R_30()) return true; - return false; - } - static final private boolean jj_3R_75() { if (jj_3R_77()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_151()) { jj_scanpos = xsp; break; } + if (jj_3_152()) { jj_scanpos = xsp; break; } } return false; } - static final private boolean jj_3_47() { + static final private boolean jj_3_48() { if (jj_3R_42()) return true; if (jj_scan_token(EQ)) return true; if (jj_3R_35()) return true; @@ -4968,12 +4956,22 @@ public class PrismParser implements PrismParserConstants { Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_78()) { jj_scanpos = xsp; break; } + if (jj_3_79()) { jj_scanpos = xsp; break; } } return false; } - static final private boolean jj_3_77() { + static final private boolean jj_3_8() { + if (jj_3R_30()) return true; + return false; + } + + static final private boolean jj_3_14() { + if (jj_3R_27()) return true; + return false; + } + + static final private boolean jj_3_78() { if (jj_scan_token(IMPLIES)) return true; if (jj_3R_52()) return true; return false; @@ -4982,14 +4980,14 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_41() { Token xsp; xsp = jj_scanpos; - if (jj_3_46()) { + if (jj_3_47()) { jj_scanpos = xsp; - if (jj_3_47()) return true; + if (jj_3_48()) return true; } return false; } - static final private boolean jj_3_46() { + static final private boolean jj_3_47() { if (jj_scan_token(LPARENTH)) return true; if (jj_3R_42()) return true; if (jj_scan_token(EQ)) return true; @@ -4998,12 +4996,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_14() { - if (jj_3R_34()) return true; - return false; - } - - static final private boolean jj_3_125() { + static final private boolean jj_3_126() { if (jj_3R_66()) return true; return false; } @@ -5015,7 +5008,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_150() { + static final private boolean jj_3_151() { if (jj_3R_75()) return true; return false; } @@ -5025,14 +5018,14 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_129() { + static final private boolean jj_3_130() { if (jj_scan_token(LBRACE)) return true; if (jj_scan_token(MAX)) return true; if (jj_scan_token(RBRACE)) return true; return false; } - static final private boolean jj_3_114() { + static final private boolean jj_3_115() { if (jj_3R_35()) return true; return false; } @@ -5041,22 +5034,30 @@ public class PrismParser implements PrismParserConstants { if (jj_3R_52()) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_77()) jj_scanpos = xsp; + if (jj_3_78()) jj_scanpos = xsp; return false; } - static final private boolean jj_3_132() { - if (jj_3R_68()) return true; + static final private boolean jj_3_13() { + if (jj_3R_26()) return true; return false; } - static final private boolean jj_3_13() { - if (jj_3R_26()) return true; + static final private boolean jj_3_12() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_13()) { + jj_scanpos = xsp; + if (jj_3_14()) { + jj_scanpos = xsp; + if (jj_3_15()) return true; + } + } return false; } - static final private boolean jj_3_6() { - if (jj_3R_28()) return true; + static final private boolean jj_3_133() { + if (jj_3R_68()) return true; return false; } @@ -5065,37 +5066,24 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_45() { + static final private boolean jj_3_46() { if (jj_scan_token(TRUE)) return true; return false; } - static final private boolean jj_3_43() { - if (jj_scan_token(AND)) return true; - if (jj_3R_41()) return true; - return false; - } - - static final private boolean jj_3_124() { - if (jj_3R_65()) return true; + static final private boolean jj_3_6() { + if (jj_3R_28()) return true; return false; } - static final private boolean jj_3_12() { - if (jj_3R_33()) return true; + static final private boolean jj_3_44() { + if (jj_scan_token(AND)) return true; + if (jj_3R_41()) return true; return false; } - static final private boolean jj_3_11() { - Token xsp; - xsp = jj_scanpos; - if (jj_3_12()) { - jj_scanpos = xsp; - if (jj_3_13()) { - jj_scanpos = xsp; - if (jj_3_14()) return true; - } - } + static final private boolean jj_3_125() { + if (jj_3R_65()) return true; return false; } @@ -5104,128 +5092,128 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_147() { + static final private boolean jj_3_148() { if (jj_scan_token(DOTS)) return true; if (jj_3R_75()) return true; return false; } - static final private boolean jj_3_5() { - if (jj_3R_27()) return true; + static final private boolean jj_3_75() { + if (jj_3R_51()) return true; return false; } - static final private boolean jj_3_74() { - if (jj_3R_51()) return true; + static final private boolean jj_3_5() { + if (jj_3R_27()) return true; return false; } static final private boolean jj_3R_40() { Token xsp; xsp = jj_scanpos; - if (jj_3_44()) { + if (jj_3_45()) { jj_scanpos = xsp; - if (jj_3_45()) return true; + if (jj_3_46()) return true; } return false; } - static final private boolean jj_3_44() { + static final private boolean jj_3_45() { if (jj_3R_41()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_43()) { jj_scanpos = xsp; break; } + if (jj_3_44()) { jj_scanpos = xsp; break; } } return false; } - static final private boolean jj_3_127() { + static final private boolean jj_3_128() { Token xsp; xsp = jj_scanpos; - if (jj_3_128()) { + if (jj_3_129()) { jj_scanpos = xsp; - if (jj_3_129()) return true; + if (jj_3_130()) return true; } return false; } - static final private boolean jj_3_128() { + static final private boolean jj_3_129() { if (jj_scan_token(LBRACE)) return true; if (jj_scan_token(MIN)) return true; if (jj_scan_token(RBRACE)) return true; return false; } - static final private boolean jj_3_130() { + static final private boolean jj_3_131() { if (jj_scan_token(LBRACE)) return true; if (jj_3R_61()) return true; if (jj_scan_token(RBRACE)) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_127()) { jj_scanpos = xsp; break; } + if (jj_3_128()) { jj_scanpos = xsp; break; } } return false; } - static final private boolean jj_3_123() { + static final private boolean jj_3_124() { if (jj_3R_64()) return true; return false; } - static final private boolean jj_3_113() { + static final private boolean jj_3_114() { if (jj_scan_token(DQUOTE)) return true; if (jj_3R_36()) return true; if (jj_scan_token(DQUOTE)) return true; return false; } - static final private boolean jj_3_75() { + static final private boolean jj_3_76() { if (jj_3R_36()) return true; return false; } - static final private boolean jj_3_4() { - if (jj_3R_26()) return true; - return false; - } - - static final private boolean jj_3_122() { + static final private boolean jj_3_123() { if (jj_scan_token(RMAX)) return true; if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static final private boolean jj_3_145() { + static final private boolean jj_3_146() { if (jj_scan_token(DOTS)) return true; if (jj_3R_75()) return true; return false; } - static final private boolean jj_3_121() { + static final private boolean jj_3_122() { if (jj_scan_token(RMIN)) return true; if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static final private boolean jj_3R_32() { + static final private boolean jj_3R_33() { if (jj_scan_token(INIT)) return true; if (jj_3R_35()) return true; if (jj_scan_token(ENDINIT)) return true; return false; } - static final private boolean jj_3_119() { + static final private boolean jj_3_4() { + if (jj_3R_26()) return true; + return false; + } + + static final private boolean jj_3_120() { if (jj_scan_token(MAX)) return true; if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static final private boolean jj_3_118() { + static final private boolean jj_3_119() { if (jj_scan_token(MIN)) return true; if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; @@ -5239,43 +5227,43 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_116() { + static final private boolean jj_3_117() { if (jj_3R_55()) return true; if (jj_3R_35()) return true; return false; } - static final private boolean jj_3_117() { + static final private boolean jj_3_118() { if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static final private boolean jj_3_115() { + static final private boolean jj_3_116() { if (jj_scan_token(LBRACE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_113()) { + if (jj_3_114()) { jj_scanpos = xsp; - if (jj_3_114()) return true; + if (jj_3_115()) return true; } if (jj_scan_token(RBRACE)) return true; return false; } - static final private boolean jj_3_120() { + static final private boolean jj_3_121() { if (jj_scan_token(R)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_115()) jj_scanpos = xsp; + if (jj_3_116()) jj_scanpos = xsp; xsp = jj_scanpos; - if (jj_3_116()) { - jj_scanpos = xsp; if (jj_3_117()) { jj_scanpos = xsp; if (jj_3_118()) { jj_scanpos = xsp; - if (jj_3_119()) return true; + if (jj_3_119()) { + jj_scanpos = xsp; + if (jj_3_120()) return true; } } } @@ -5285,56 +5273,51 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_63() { Token xsp; xsp = jj_scanpos; - if (jj_3_131()) { + if (jj_3_132()) { jj_scanpos = xsp; - if (jj_3_132()) return true; + if (jj_3_133()) return true; } return false; } - static final private boolean jj_3_76() { + static final private boolean jj_3_77() { if (jj_scan_token(LBRACKET)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_75()) jj_scanpos = xsp; + if (jj_3_76()) jj_scanpos = xsp; if (jj_scan_token(RBRACKET)) return true; return false; } - static final private boolean jj_3_131() { + static final private boolean jj_3_132() { Token xsp; xsp = jj_scanpos; - if (jj_3_120()) { - jj_scanpos = xsp; if (jj_3_121()) { jj_scanpos = xsp; - if (jj_3_122()) return true; + if (jj_3_122()) { + jj_scanpos = xsp; + if (jj_3_123()) return true; } } if (jj_scan_token(LBRACKET)) return true; xsp = jj_scanpos; - if (jj_3_123()) { - jj_scanpos = xsp; if (jj_3_124()) { jj_scanpos = xsp; if (jj_3_125()) { jj_scanpos = xsp; - if (jj_3_126()) return true; + if (jj_3_126()) { + jj_scanpos = xsp; + if (jj_3_127()) return true; } } } xsp = jj_scanpos; - if (jj_3_130()) jj_scanpos = xsp; + if (jj_3_131()) jj_scanpos = xsp; if (jj_scan_token(RBRACKET)) return true; return false; } - static final private boolean jj_3_3() { - if (jj_3R_25()) return true; - return false; - } - - static final private boolean jj_3_110() { + static final private boolean jj_3_111() { if (jj_scan_token(LBRACE)) return true; if (jj_3R_61()) return true; if (jj_scan_token(RBRACE)) return true; @@ -5344,7 +5327,7 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_51() { Token xsp; xsp = jj_scanpos; - if (jj_3_76()) jj_scanpos = xsp; + if (jj_3_77()) jj_scanpos = xsp; if (jj_3R_35()) return true; if (jj_scan_token(COLON)) return true; if (jj_3R_35()) return true; @@ -5352,34 +5335,39 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_40() { + static final private boolean jj_3_3() { + if (jj_3R_25()) return true; + return false; + } + + static final private boolean jj_3_41() { if (jj_scan_token(PLUS)) return true; if (jj_3R_39()) return true; return false; } - static final private boolean jj_3_146() { + static final private boolean jj_3_147() { if (jj_scan_token(COMMA)) return true; if (jj_3R_75()) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_147()) jj_scanpos = xsp; + if (jj_3_148()) jj_scanpos = xsp; return false; } - static final private boolean jj_3_73() { + static final private boolean jj_3_74() { if (jj_scan_token(DQUOTE)) return true; if (jj_3R_36()) return true; if (jj_scan_token(DQUOTE)) return true; return false; } - static final private boolean jj_3_112() { + static final private boolean jj_3_113() { if (jj_3R_63()) return true; return false; } - static final private boolean jj_3_105() { + static final private boolean jj_3_106() { if (jj_scan_token(LBRACKET)) return true; if (jj_3R_35()) return true; if (jj_scan_token(COMMA)) return true; @@ -5388,52 +5376,52 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_42() { + static final private boolean jj_3_43() { if (jj_3R_39()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_40()) { jj_scanpos = xsp; break; } + if (jj_3_41()) { jj_scanpos = xsp; break; } } return false; } - static final private boolean jj_3_149() { + static final private boolean jj_3_150() { if (jj_3R_75()) return true; if (jj_3R_76()) return true; if (jj_3R_75()) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_145()) jj_scanpos = xsp; + if (jj_3_146()) jj_scanpos = xsp; while (true) { xsp = jj_scanpos; - if (jj_3_146()) { jj_scanpos = xsp; break; } + if (jj_3_147()) { jj_scanpos = xsp; break; } } return false; } - static final private boolean jj_3_109() { + static final private boolean jj_3_110() { if (jj_scan_token(S)) return true; if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static final private boolean jj_3_108() { + static final private boolean jj_3_109() { if (jj_scan_token(S)) return true; if (jj_3R_55()) return true; if (jj_3R_35()) return true; return false; } - static final private boolean jj_3R_31() { + static final private boolean jj_3R_32() { if (jj_scan_token(REWARDS)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_73()) jj_scanpos = xsp; + if (jj_3_74()) jj_scanpos = xsp; while (true) { xsp = jj_scanpos; - if (jj_3_74()) { jj_scanpos = xsp; break; } + if (jj_3_75()) { jj_scanpos = xsp; break; } } if (jj_scan_token(ENDREWARDS)) return true; return false; @@ -5442,14 +5430,14 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_87() { Token xsp; xsp = jj_scanpos; - if (jj_3_41()) { + if (jj_3_42()) { jj_scanpos = xsp; - if (jj_3_42()) return true; + if (jj_3_43()) return true; } return false; } - static final private boolean jj_3_41() { + static final private boolean jj_3_42() { if (jj_3R_40()) return true; return false; } @@ -5457,24 +5445,24 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_91() { Token xsp; xsp = jj_scanpos; - if (jj_3_148()) { - jj_scanpos = xsp; if (jj_3_149()) { jj_scanpos = xsp; - if (jj_3_150()) return true; + if (jj_3_150()) { + jj_scanpos = xsp; + if (jj_3_151()) return true; } } return false; } - static final private boolean jj_3_148() { + static final private boolean jj_3_149() { if (jj_3R_75()) return true; if (jj_3R_55()) return true; if (jj_3R_75()) return true; return false; } - static final private boolean jj_3_104() { + static final private boolean jj_3_105() { if (jj_scan_token(GE)) return true; if (jj_3R_35()) return true; return false; @@ -5483,29 +5471,29 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_62() { Token xsp; xsp = jj_scanpos; - if (jj_3_111()) { + if (jj_3_112()) { jj_scanpos = xsp; - if (jj_3_112()) return true; + if (jj_3_113()) return true; } return false; } - static final private boolean jj_3_111() { + static final private boolean jj_3_112() { Token xsp; xsp = jj_scanpos; - if (jj_3_108()) { + if (jj_3_109()) { jj_scanpos = xsp; - if (jj_3_109()) return true; + if (jj_3_110()) return true; } if (jj_scan_token(LBRACKET)) return true; if (jj_3R_61()) return true; xsp = jj_scanpos; - if (jj_3_110()) jj_scanpos = xsp; + if (jj_3_111()) jj_scanpos = xsp; if (jj_scan_token(RBRACKET)) return true; return false; } - static final private boolean jj_3_107() { + static final private boolean jj_3_108() { if (jj_scan_token(GLOB)) return true; return false; } @@ -5529,7 +5517,10 @@ public class PrismParser implements PrismParserConstants { jj_scanpos = xsp; if (jj_3_9()) { jj_scanpos = xsp; - if (jj_3_10()) return true; + if (jj_3_10()) { + jj_scanpos = xsp; + if (jj_3_11()) return true; + } } } } @@ -5553,7 +5544,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_39() { + static final private boolean jj_3_40() { if (jj_3R_36()) return true; return false; } @@ -5563,17 +5554,17 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_185() { + static final private boolean jj_3_186() { if (jj_scan_token(LE)) return true; return false; } - static final private boolean jj_3_144() { + static final private boolean jj_3_145() { if (jj_scan_token(NOT)) return true; return false; } - static final private boolean jj_3_106() { + static final private boolean jj_3_107() { if (jj_scan_token(FUTURE)) return true; return false; } @@ -5581,7 +5572,7 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_74() { Token xsp; xsp = jj_scanpos; - if (jj_3_144()) jj_scanpos = xsp; + if (jj_3_145()) jj_scanpos = xsp; if (jj_3R_91()) return true; return false; } @@ -5589,9 +5580,9 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_60() { Token xsp; xsp = jj_scanpos; - if (jj_3_106()) { + if (jj_3_107()) { jj_scanpos = xsp; - if (jj_3_107()) return true; + if (jj_3_108()) return true; } if (jj_3R_61()) return true; return false; @@ -5602,7 +5593,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_68() { + static final private boolean jj_3_69() { if (jj_scan_token(COMMA)) return true; if (jj_3R_48()) return true; if (jj_scan_token(RENAME)) return true; @@ -5614,7 +5605,7 @@ public class PrismParser implements PrismParserConstants { if (jj_scan_token(LBRACKET)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_39()) jj_scanpos = xsp; + if (jj_3_40()) jj_scanpos = xsp; if (jj_scan_token(RBRACKET)) return true; if (jj_3R_35()) return true; if (jj_scan_token(RARROW)) return true; @@ -5623,12 +5614,12 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_184() { + static final private boolean jj_3_185() { if (jj_scan_token(GE)) return true; return false; } - static final private boolean jj_3_103() { + static final private boolean jj_3_104() { if (jj_scan_token(LE)) return true; if (jj_3R_35()) return true; return false; @@ -5639,12 +5630,12 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_183() { + static final private boolean jj_3_184() { if (jj_scan_token(LT)) return true; return false; } - static final private boolean jj_3_143() { + static final private boolean jj_3_144() { if (jj_scan_token(AND)) return true; if (jj_3R_74()) return true; return false; @@ -5655,7 +5646,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_182() { + static final private boolean jj_3_183() { if (jj_scan_token(GT)) return true; return false; } @@ -5663,35 +5654,35 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_55() { Token xsp; xsp = jj_scanpos; - if (jj_3_182()) { - jj_scanpos = xsp; if (jj_3_183()) { jj_scanpos = xsp; if (jj_3_184()) { jj_scanpos = xsp; - if (jj_3_185()) return true; + if (jj_3_185()) { + jj_scanpos = xsp; + if (jj_3_186()) return true; } } } return false; } - static final private boolean jj_3_102() { + static final private boolean jj_3_103() { if (jj_scan_token(GLOB)) return true; return false; } - static final private boolean jj_3_181() { + static final private boolean jj_3_182() { if (jj_scan_token(NE)) return true; return false; } - static final private boolean jj_3_72() { + static final private boolean jj_3_73() { if (jj_3R_50()) return true; return false; } - static final private boolean jj_3_36() { + static final private boolean jj_3_37() { if (jj_scan_token(INIT)) return true; if (jj_3R_35()) return true; return false; @@ -5700,30 +5691,30 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_88() { Token xsp; xsp = jj_scanpos; - if (jj_3_71()) { + if (jj_3_72()) { jj_scanpos = xsp; - if (jj_3_72()) return true; + if (jj_3_73()) return true; } return false; } - static final private boolean jj_3_38() { + static final private boolean jj_3_39() { if (jj_3R_36()) return true; if (jj_scan_token(COLON)) return true; if (jj_scan_token(BOOL)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_36()) jj_scanpos = xsp; + if (jj_3_37()) jj_scanpos = xsp; if (jj_scan_token(SEMICOLON)) return true; return false; } - static final private boolean jj_3_71() { + static final private boolean jj_3_72() { if (jj_3R_49()) return true; return false; } - static final private boolean jj_3_100() { + static final private boolean jj_3_101() { if (jj_scan_token(LBRACKET)) return true; if (jj_3R_35()) return true; if (jj_scan_token(COMMA)) return true; @@ -5732,7 +5723,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_180() { + static final private boolean jj_3_181() { if (jj_scan_token(EQ)) return true; return false; } @@ -5740,9 +5731,9 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_76() { Token xsp; xsp = jj_scanpos; - if (jj_3_180()) { + if (jj_3_181()) { jj_scanpos = xsp; - if (jj_3_181()) return true; + if (jj_3_182()) return true; } return false; } @@ -5752,23 +5743,23 @@ public class PrismParser implements PrismParserConstants { Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_143()) { jj_scanpos = xsp; break; } + if (jj_3_144()) { jj_scanpos = xsp; break; } } return false; } - static final private boolean jj_3_67() { + static final private boolean jj_3_68() { if (jj_scan_token(COMMA)) return true; if (jj_3R_48()) return true; return false; } - static final private boolean jj_3_167() { + static final private boolean jj_3_168() { if (jj_scan_token(CEIL)) return true; return false; } - static final private boolean jj_3_101() { + static final private boolean jj_3_102() { if (jj_scan_token(FUTURE)) return true; return false; } @@ -5776,23 +5767,23 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_59() { Token xsp; xsp = jj_scanpos; - if (jj_3_101()) { + if (jj_3_102()) { jj_scanpos = xsp; - if (jj_3_102()) return true; + if (jj_3_103()) return true; } xsp = jj_scanpos; - if (jj_3_103()) { - jj_scanpos = xsp; if (jj_3_104()) { jj_scanpos = xsp; - if (jj_3_105()) return true; + if (jj_3_105()) { + jj_scanpos = xsp; + if (jj_3_106()) return true; } } if (jj_3R_61()) return true; return false; } - static final private boolean jj_3_142() { + static final private boolean jj_3_143() { if (jj_scan_token(OR)) return true; if (jj_3R_72()) return true; return false; @@ -5803,13 +5794,13 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_35() { + static final private boolean jj_3_36() { if (jj_scan_token(INIT)) return true; if (jj_3R_35()) return true; return false; } - static final private boolean jj_3_65() { + static final private boolean jj_3_66() { if (jj_scan_token(COMMA)) return true; if (jj_3R_48()) return true; return false; @@ -5818,14 +5809,14 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_37() { Token xsp; xsp = jj_scanpos; - if (jj_3_37()) { + if (jj_3_38()) { jj_scanpos = xsp; - if (jj_3_38()) return true; + if (jj_3_39()) return true; } return false; } - static final private boolean jj_3_37() { + static final private boolean jj_3_38() { if (jj_3R_36()) return true; if (jj_scan_token(COLON)) return true; if (jj_scan_token(LBRACKET)) return true; @@ -5835,12 +5826,12 @@ public class PrismParser implements PrismParserConstants { if (jj_scan_token(RBRACKET)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_35()) jj_scanpos = xsp; + if (jj_3_36()) jj_scanpos = xsp; if (jj_scan_token(SEMICOLON)) return true; return false; } - static final private boolean jj_3_70() { + static final private boolean jj_3_71() { if (jj_scan_token(LBRACE)) return true; if (jj_3R_48()) return true; if (jj_scan_token(RENAME)) return true; @@ -5848,13 +5839,13 @@ public class PrismParser implements PrismParserConstants { Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_68()) { jj_scanpos = xsp; break; } + if (jj_3_69()) { jj_scanpos = xsp; break; } } if (jj_scan_token(RBRACE)) return true; return false; } - static final private boolean jj_3_99() { + static final private boolean jj_3_100() { if (jj_scan_token(GE)) return true; if (jj_3R_35()) return true; return false; @@ -5865,22 +5856,22 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_66() { + static final private boolean jj_3_67() { Token xsp; xsp = jj_scanpos; - if (jj_3_69()) { + if (jj_3_70()) { jj_scanpos = xsp; - if (jj_3_70()) return true; + if (jj_3_71()) return true; } return false; } - static final private boolean jj_3_34() { + static final private boolean jj_3_35() { if (jj_3R_38()) return true; return false; } - static final private boolean jj_3_139() { + static final private boolean jj_3_140() { if (jj_scan_token(COLON)) return true; if (jj_3R_35()) return true; return false; @@ -5890,11 +5881,11 @@ public class PrismParser implements PrismParserConstants { if (jj_3R_92()) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_142()) jj_scanpos = xsp; + if (jj_3_143()) jj_scanpos = xsp; return false; } - static final private boolean jj_3_166() { + static final private boolean jj_3_167() { if (jj_scan_token(FLOOR)) return true; return false; } @@ -5906,24 +5897,24 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_91() { + static final private boolean jj_3_92() { if (jj_3R_60()) return true; return false; } - static final private boolean jj_3_141() { + static final private boolean jj_3_142() { if (jj_3R_72()) return true; return false; } - static final private boolean jj_3_69() { + static final private boolean jj_3_70() { if (jj_scan_token(DIVIDE)) return true; if (jj_scan_token(LBRACE)) return true; if (jj_3R_48()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_67()) { jj_scanpos = xsp; break; } + if (jj_3_68()) { jj_scanpos = xsp; break; } } if (jj_scan_token(RBRACE)) return true; return false; @@ -5941,16 +5932,46 @@ public class PrismParser implements PrismParserConstants { Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_66()) { jj_scanpos = xsp; break; } + if (jj_3_67()) { jj_scanpos = xsp; break; } } return false; } - static final private boolean jj_3_33() { + static final private boolean jj_3_34() { if (jj_3R_37()) return true; return false; } + static final private boolean jj_3_99() { + if (jj_scan_token(LE)) return true; + if (jj_3R_35()) return true; + return false; + } + + static final private boolean jj_3R_73() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_141()) { + jj_scanpos = xsp; + if (jj_3_142()) return true; + } + return false; + } + + static final private boolean jj_3_180() { + if (jj_3R_84()) return true; + return false; + } + + static final private boolean jj_3_141() { + if (jj_3R_72()) return true; + if (jj_scan_token(QMARK)) return true; + if (jj_3R_72()) return true; + if (jj_scan_token(COLON)) return true; + if (jj_3R_73()) return true; + return false; + } + static private boolean jj_initialized_once = false; static public PrismParserTokenManager token_source; static SimpleCharStream jj_input_stream; @@ -5979,7 +6000,7 @@ public class PrismParser implements PrismParserConstants { private static void jj_la1_2() { jj_la1_2 = new int[] {}; } - static final private JJCalls[] jj_2_rtns = new JJCalls[185]; + static final private JJCalls[] jj_2_rtns = new JJCalls[186]; static private boolean jj_rescan = false; static private int jj_gc = 0; @@ -6223,7 +6244,7 @@ public class PrismParser implements PrismParserConstants { static final private void jj_rescan_token() { jj_rescan = true; - for (int i = 0; i < 185; i++) { + for (int i = 0; i < 186; i++) { try { JJCalls p = jj_2_rtns[i]; do { @@ -6415,6 +6436,7 @@ public class PrismParser implements PrismParserConstants { case 182: jj_3_183(); break; case 183: jj_3_184(); break; case 184: jj_3_185(); break; + case 185: jj_3_186(); break; } } p = p.next; diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index 70555c3b..6113b84f 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -177,6 +177,7 @@ public class PrismParser // clear all vectors/stacks formulaList = new FormulaList(); + labelList = new LabelList(); constantList = new ConstantList(); stack.clear(); reverseStack.clear(); @@ -208,6 +209,7 @@ public class PrismParser ReInit(str); // clear all vectors/stacks + formulaList = new FormulaList(); labelList = new LabelList(); constantList = new ConstantList(); stack.clear(); @@ -466,7 +468,7 @@ ModulesFile ModulesFile() : } { ( - ( ( type=ModulesFileType() {typeSpecs++;} ) | FormulaDef() | ConstantDef() | GlobalDecl() | Module() | RenamedModule() | SystemComp() | RewardStruct() | Init() )* + ( ( type=ModulesFileType() {typeSpecs++;} ) | FormulaDef() | LabelDef() | ConstantDef() | GlobalDecl() | Module() | RenamedModule() | SystemComp() | RewardStruct() | Init() )* ) { @@ -475,8 +477,9 @@ ModulesFile ModulesFile() : // create new ModulesFile object ModulesFile modulesFile = new ModulesFile(); - // pass lists of formulas, constants to ModulesFile + // pass lists of formulas, labels, constants to ModulesFile modulesFile.setFormulaList(formulaList); + modulesFile.setLabelList(labelList); modulesFile.setConstantList(constantList); // set type (default is nondeterministic) @@ -543,13 +546,14 @@ PropertiesFile PropertiesFile() : { } { - ( ( LabelDef() | ConstantDef() | SinglePCTLFormula() )* ) // possibly several pctl formulas then eof + ( ( /*FormulaDef() |*/ LabelDef() | ConstantDef() | SinglePCTLFormula() )* ) // possibly several pctl formulas then eof { // create new PropertiesFile object // (pass in associated ModulesFile) PropertiesFile propertiesFile = new PropertiesFile(modulesFile); - // pass lists of labels, constants to PropertiesFile + // pass lists of formulas, labels, constants to PropertiesFile + propertiesFile.setFormulaList(formulaList); propertiesFile.setLabelList(labelList); propertiesFile.setConstantList(constantList); diff --git a/prism/src/parser/PropertiesFile.java b/prism/src/parser/PropertiesFile.java index 47adf90d..9749d7c9 100644 --- a/prism/src/parser/PropertiesFile.java +++ b/prism/src/parser/PropertiesFile.java @@ -37,8 +37,12 @@ public class PropertiesFile // associated ModulesFile (for constants, ...) private ModulesFile modulesFile; + // formulas (macros) + private FormulaList formulaList; + // labels (atomic propositions) private LabelList labelList; + private LabelList combinedLabelList; // constants private ConstantList constantList; @@ -49,6 +53,7 @@ public class PropertiesFile private Vector comments; // list of all identifiers used + private Vector modulesFileIdents; private Vector allIdentsUsed; // actual values of constants @@ -60,8 +65,11 @@ public class PropertiesFile { // initialise modulesFile = mf; - labelList = null; - constantList = null; + modulesFileIdents = modulesFile.getAllIdentsUsed(); + formulaList = new FormulaList(); // empty - will be overwritten + labelList = new LabelList(); // empty - will be overwritten + combinedLabelList = new LabelList(); + constantList = new ConstantList(); // empty - will be overwritten properties = new Vector(); comments = new Vector(); allIdentsUsed = new Vector(); @@ -70,6 +78,8 @@ public class PropertiesFile // set up methods - these are called by the parser to create a PropertiesFile object + public void setFormulaList(FormulaList fl) { formulaList = fl; } + public void setLabelList(LabelList ll) { labelList = ll; } public void setConstantList(ConstantList cl) { constantList = cl; } @@ -84,8 +94,12 @@ public class PropertiesFile // accessor methods + public FormulaList getFormulaList() { return formulaList; } + public LabelList getLabelList() { return labelList; } + public LabelList getCombinedLabelList() { return combinedLabelList; } + public ConstantList getConstantList() { return constantList; } public int getNumProperties() { return properties.size(); } @@ -98,6 +112,16 @@ public class PropertiesFile public void tidyUp() throws PrismException { + // check formula identifiers + checkFormulaIdents(); + // find all instances of formulas + // (i.e. locate idents which are formulas) + findAllFormulas(); + // check formulas for cyclic dependencies + formulaList.findCycles(); + // expand any formulas + expandFormulas(); + // check label identifiers checkLabelIdents(); @@ -118,6 +142,82 @@ public class PropertiesFile check(); } + // check formula identifiers + + private void checkFormulaIdents() throws PrismException + { + int i, n; + String s; + + n = formulaList.size(); + for (i = 0; i < n; i++) { + s = formulaList.getFormulaName(i); + // see if ident has been used elsewhere + if (modulesFileIdents.contains(s)) { + throw new PrismException("Identifier \"" + s + "\" already used in model file"); + } + else if (allIdentsUsed.contains(s)) { + throw new PrismException("Duplicated identifier \"" + s + "\""); + } + else { + allIdentsUsed.addElement(s); + } + } + } + + // find all formulas (i.e. locate idents which are formulas) + + private void findAllFormulas() throws PrismException + { + int i, n; + + // note: we have to look for both formulas defined here + // and those defined in the modules file + + // look in formula list + formulaList.findAllFormulas(modulesFile.getFormulaList()); + formulaList.findAllFormulas(); + // look in labels + labelList.findAllFormulas(modulesFile.getFormulaList()); + labelList.findAllFormulas(formulaList); + // look in constants + constantList.findAllFormulas(modulesFile.getFormulaList()); + constantList.findAllFormulas(formulaList); + // look in properties + n = properties.size(); + for (i = 0; i < n; i++) { + setProperty(i, getProperty(i).findAllFormulas(modulesFile.getFormulaList())); + setProperty(i, getProperty(i).findAllFormulas(formulaList)); + } + } + + // expand any formulas + + private void expandFormulas() throws PrismException + { + int i, n; + + // note: we have to look for both formulas defined here + // and those defined in the modules file + + // look in formula list + // (best to do this first - sorts out any linked formulas) + formulaList.expandFormulas(modulesFile.getFormulaList()); + formulaList.expandFormulas(); + // look in labels + labelList.expandFormulas(modulesFile.getFormulaList()); + labelList.expandFormulas(formulaList); + // look in constants + constantList.expandFormulas(modulesFile.getFormulaList()); + constantList.expandFormulas(formulaList); + // look in properties + n = properties.size(); + for (i = 0; i < n; i++) { + setProperty(i, getProperty(i).expandFormulas(modulesFile.getFormulaList())); + setProperty(i, getProperty(i).expandFormulas(formulaList)); + } + } + // check label identifiers // also check reference to these identifiers in properties @@ -126,25 +226,41 @@ public class PropertiesFile int i, n; String s; Vector labelIdents; + LabelList mfLabels; + // get label list from model file + mfLabels = modulesFile.getLabelList(); + // add model file lables to combined label list + n = mfLabels.size(); + for (i = 0; i < n; i++) { + // do we need to clone these Expressions? hopefully not - they shouldn't be modified again + combinedLabelList.addLabel(mfLabels.getLabelName(i), mfLabels.getLabel(i)); + } // go thru labels n = labelList.size(); labelIdents = new Vector(); for (i = 0; i < n; i++) { s = labelList.getLabelName(i); + // see if ident has been used already for a label in model file + if (mfLabels.getLabelIndex(s) != -1) { + throw new PrismException("Label \"" + s + "\" already defined in model file"); + } // see if ident has been used already for a label if (labelIdents.contains(s)) { throw new PrismException("Duplicated label name \"" + s + "\""); } + // store identifier + // and add label to combined list else { labelIdents.addElement(s); + combinedLabelList.addLabel(s, labelList.getLabel(i)); } } // now go thru properties and check that any PCTLLabel objects refer only to existing labels n = properties.size(); for (i = 0; i < n; i++) { - getProperty(i).checkLabelIdents(labelList); + getProperty(i).checkLabelIdents(combinedLabelList); } } @@ -154,26 +270,20 @@ public class PropertiesFile { int i, n; String s; - Vector mfIdents, constIdents; - - // get idents used in modules file - mfIdents = modulesFile.getAllIdentsUsed(); - // create vector to store new idents - constIdents = new Vector(); // go thru constants n = constantList.size(); for (i = 0; i < n; i++) { s = constantList.getConstantName(i); // see if ident has been used elsewhere - if (mfIdents.contains(s)) { + if (modulesFileIdents.contains(s)) { throw new PrismException("Identifier \"" + s + "\" already used in model file"); } - else if (constIdents.contains(s)) { + else if (allIdentsUsed.contains(s)) { throw new PrismException("Duplicated identifier \"" + s + "\""); } else { - constIdents.addElement(s); + allIdentsUsed.addElement(s); } } } @@ -278,6 +388,10 @@ public class PropertiesFile String s = "", tmp, tmp2; int i, j, n; + tmp = "" + formulaList; + if (tmp.length() > 0) tmp += "\n"; + s += tmp; + tmp = "" + labelList; if (tmp.length() > 0) tmp += "\n"; s += tmp; @@ -309,6 +423,10 @@ public class PropertiesFile String s = "", tmp; int i, n; + tmp = "" + formulaList; + if (tmp.length() > 0) tmp += "\n"; + s += tmp; + tmp = "" + labelList.toTreeString(); if (tmp.length() > 0) tmp += "\n"; s += tmp; diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 26250b0c..8792fd69 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1110,7 +1110,7 @@ public class NondetModelChecker implements ModelChecker return dd; } // get expression associated with label - ll = propertiesFile.getLabelList(); + ll = propertiesFile.getCombinedLabelList(); i = ll.getLabelIndex(pctl.getName()); if (i == -1) throw new PrismException("Unknown label \"" + pctl.getName() + "\" in PCTL formula"); expr = ll.getLabel(i); diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 2178f0a6..73804da4 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1073,7 +1073,7 @@ public class Prism implements PrismSettingsListener ll = null; n = 0; } else { - ll = propertiesFile.getLabelList(); + ll = propertiesFile.getCombinedLabelList(); n = ll.size(); } diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 699bdee4..191da56a 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -1113,7 +1113,7 @@ public class ProbModelChecker implements ModelChecker return dd; } // get expression associated with label - ll = propertiesFile.getLabelList(); + ll = propertiesFile.getCombinedLabelList(); i = ll.getLabelIndex(pctl.getName()); if (i == -1) throw new PrismException("Unknown label \"" + pctl.getName() + "\" in PCTL formula"); expr = ll.getLabel(i); diff --git a/prism/src/prism/StochModelChecker.java b/prism/src/prism/StochModelChecker.java index e49502a8..516c034c 100644 --- a/prism/src/prism/StochModelChecker.java +++ b/prism/src/prism/StochModelChecker.java @@ -1855,7 +1855,7 @@ public class StochModelChecker implements ModelChecker return dd; } // get expression associated with label - ll = propertiesFile.getLabelList(); + ll = propertiesFile.getCombinedLabelList(); i = ll.getLabelIndex(pctl.getName()); if (i == -1) throw new PrismException("Unknown label \"" + pctl.getName() + "\" in CSL formula"); expr = ll.getLabel(i); diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 1d9f6697..e226a15e 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -2320,7 +2320,7 @@ public class SimulatorEngine */ public LabelList getLabelList() { - return propertiesFile.getLabelList(); + return propertiesFile.getCombinedLabelList(); } // Methods to compute parameters for simulation