diff --git a/.classpath b/.classpath index 06fd0b5d77..da69d8471d 100644 --- a/.classpath +++ b/.classpath @@ -15,5 +15,6 @@ + diff --git a/prism-tests/functionality/verify/mdps/reach/mdp_simple.nm.props.args b/prism-tests/functionality/verify/mdps/reach/mdp_simple.nm.props.args index fecd1a44ec..eef11583d8 100644 --- a/prism-tests/functionality/verify/mdps/reach/mdp_simple.nm.props.args +++ b/prism-tests/functionality/verify/mdps/reach/mdp_simple.nm.props.args @@ -5,6 +5,7 @@ -ex -gs -ex -politer -ex -modpoliter +-ex -lp -s -ii -m -ii -h -ii diff --git a/prism-tests/functionality/verify/mdps/rewards/rewpoliter.nm.props.args b/prism-tests/functionality/verify/mdps/rewards/rewpoliter.nm.props.args index a07d393efe..8ac1eeed3b 100644 --- a/prism-tests/functionality/verify/mdps/rewards/rewpoliter.nm.props.args +++ b/prism-tests/functionality/verify/mdps/rewards/rewpoliter.nm.props.args @@ -4,3 +4,4 @@ -valiter -h -valiter -ex -gs -ex +-gs -lp diff --git a/prism-tests/pmc/lec13and14mdp.nm b/prism-tests/pmc/lec13and14mdp.nm index 3a450e896a..92180962c4 100644 --- a/prism-tests/pmc/lec13and14mdp.nm +++ b/prism-tests/pmc/lec13and14mdp.nm @@ -16,3 +16,8 @@ s:[0..3]; endmodule label "a" = s=2; + +rewards + [] true : 0.6; + true : 0.4; +endrewards diff --git a/prism-tests/pmc/lec13and14mdp.nm.props b/prism-tests/pmc/lec13and14mdp.nm.props index 39c31250a9..a7ce9916ea 100644 --- a/prism-tests/pmc/lec13and14mdp.nm.props +++ b/prism-tests/pmc/lec13and14mdp.nm.props @@ -12,3 +12,8 @@ filter(forall, P<0.1 [ F "a" ] <=> false); // RESULT: true filter(forall, P>0 [ F "a" ] <=> (s=0|s=1|s=2)); + + // RESULT: 5/3 + Rmin=? [ F "a" ]; + // RESULT: Infinity + Rmax=? [ F "a" ]; diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 0a6919f234..6f0a816a11 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -47,8 +47,18 @@ import explicit.rewards.MCRewardsFromMDPRewards; import explicit.rewards.MDPRewards; import explicit.rewards.Rewards; +import gurobi.GRB; +import gurobi.GRBEnv; +import gurobi.GRBException; +import gurobi.GRBLinExpr; +import gurobi.GRBModel; +import gurobi.GRBVar; +import lpsolve.LpSolve; +import lpsolve.LpSolveException; import parser.ast.Expression; import parser.type.TypeDouble; +import prism.Accuracy; +import prism.Accuracy.AccuracyLevel; import prism.AccuracyFactory; import prism.OptionsIntervalIteration; import prism.Prism; @@ -71,6 +81,10 @@ */ public class MDPModelChecker extends ProbModelChecker { + enum LPSolver { LPSOLVE, GUROBI }; + + protected LPSolver lpSolver = LPSolver.GUROBI; + /** * Create a new MDPModelChecker, inherit basic state from parent (unless null). */ @@ -301,12 +315,6 @@ public ModelCheckerResult computeReachProbs(MDP mdp, BitSet remain, BitSet targe boolean doPmaxQuotient = this.doPmaxQuotient; - // Switch to a supported method, if necessary - if (mdpSolnMethod == MDPSolnMethod.LINEAR_PROGRAMMING) { - mdpSolnMethod = MDPSolnMethod.GAUSS_SEIDEL; - mainLog.printWarning("Switching to MDP solution method \"" + mdpSolnMethod.fullName() + "\""); - } - // Check for some unsupported combinations if (mdpSolnMethod == MDPSolnMethod.VALUE_ITERATION && valIterDir == ValIterDir.ABOVE) { if (!(precomp && prob0)) @@ -336,6 +344,14 @@ public ModelCheckerResult computeReachProbs(MDP mdp, BitSet remain, BitSet targe throw new PrismException("Policy iteration methods cannot be passed 'known' values for some states"); } } + if (mdpSolnMethod == MDPSolnMethod.LINEAR_PROGRAMMING) { + if (!(precomp && prob0)) { + throw new PrismNotSupportedException("Prob0 precomputation must be enabled for linear programming"); + } + if (!min && (genStrat || exportAdv)) { + throw new PrismNotSupportedException("Currently, explicit engine does not support adversary construction for linear programming and Rmax"); + } + } if (doPmaxQuotient && min) { // for Pmin, don't do quotient @@ -527,6 +543,9 @@ protected ModelCheckerResult computeReachProbsNumeric(MDP mdp, MDPSolnMethod met } res = computeReachProbsModPolIter(mdp, no, yes, min, strat); break; + case LINEAR_PROGRAMMING: + res = computeReachProbsLP(mdp, no, yes, min, strat); + break; default: throw new PrismException("Unknown MDP solution method " + mdpSolnMethod.fullName()); } @@ -744,6 +763,96 @@ public BitSet prob1(MDPGeneric mdp, BitSet remain, BitSet target, boolean min return u; } + /** + * Zero total rewards precomputation algorithm, i.e., determine the states of an MDP + * from which the min/max expected total cumulative rewards is zero. + * @param mdp The MDP + * @param mdpRewards The rewards + * @param min Min or max rewards (true=min, false=max) + */ + public BitSet rewTot0(MDPGeneric mdp, MDPRewards mdpRewards, boolean min) + { + int n, iters; + BitSet v, soln; + boolean v_done; + long timer; + + // Start precomputation + timer = System.currentTimeMillis(); + if (!silentPrecomputations) + mainLog.println("Starting RewTot0 (" + (min ? "min" : "max") + ")..."); + + // Initialise vectors + n = mdp.getNumStates(); + v = new BitSet(n); + soln = new BitSet(n); + + // Fixed point loop + iters = 0; + v_done = false; + // Least fixed point - start from 0 + v.clear(); + soln.clear(); + while (!v_done) { + iters++; + rewTot0step(mdp, mdpRewards, v, min, soln); + // Check termination (inner) + v_done = soln.equals(v); + // v = soln + v.clear(); + v.or(soln); + } + + // Negate + v.flip(0, n); + + // Finished precomputation + timer = System.currentTimeMillis() - timer; + if (!silentPrecomputations) { + mainLog.print("RewTot0 (" + (min ? "min" : "max") + ")"); + mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); + } + + return v; + } + + /** + * Perform a single step of zero total rewards precomputation algorithm, + * i.e., set bit i of {@code result} iff, there is a positive (state or transition) + * reward or, for some/all choices, there is a transition to a state in {@code u}. + * @param mdp The MDP + * @param mdpRewards The rewards + * @param u Set of states {@code u} + * @param forall For-all or there-exists (true=for-all, false=there-exists) + * @param result Store results here + */ + private void rewTot0step(final MDPGeneric mdp, final MDPRewards mdpRewards, final BitSet u, final boolean forall, BitSet result) + { + int n = mdp.getNumStates(); + for (int s = 0; s < n; s++) { + if (mdpRewards.getStateReward(s) > 0) { + result.set(s); + continue; + } + boolean b1 = forall; // there exists or for all + for (int choice = 0, numChoices = mdp.getNumChoices(s); choice < numChoices; choice++) { + boolean b2 = mdpRewards.getTransitionReward(s, choice) > 0 || mdp.someSuccessorsInSet(s, choice, u); + if (forall) { + if (!b2) { + b1 = false; + break; + } + } else { + if (b2) { + b1 = true; + break; + } + } + } + result.set(s, b1); + } + } + /** * Compute reachability probabilities using value iteration. * Optionally, store optimal (memoryless) strategy info. @@ -1181,6 +1290,233 @@ protected ModelCheckerResult computeReachProbsModPolIter(MDP mdp, BitSet no, Bit return res; } + /** + * Compute reachability probabilities using linear programming. + * @param mdp: The MDP + * @param no: Probability 0 states + * @param yes: Probability 1 states + * @param min: Min or max probabilities (true=min, false=max) + * @param strat Storage for (memoryless) strategy choice indices (ignored if null) + */ + protected ModelCheckerResult computeReachProbsLP(MDP mdp, BitSet no, BitSet yes, boolean min, int strat[]) throws PrismException + { + double soln[] = null; + long timer; + + // Start solution + timer = System.currentTimeMillis(); + mainLog.println("Starting linear programming (" + (min ? "min" : "max") + ")..."); + + // Store num states + int n = mdp.getNumStates(); + + // Determine set of states actually need to perform computation for + BitSet unknown = new BitSet(); + unknown.set(0, n); + unknown.andNot(yes); + unknown.andNot(no); + + switch (lpSolver) { + case LPSOLVE: + soln = solveReachProbsLPWithLPSolve(mdp, no, yes, unknown, min, strat); + break; + case GUROBI: + soln = solveReachProbsLPWithGurobi(mdp, no, yes, unknown, min, strat); + break; + } + + // We do an extra iteration of VI (using GS since we have just one solution vector) + // If strategy generation was requested (strat != null), this takes care of it + // (NB: that only works reliably for min - max needs more work - but this is disallowed earlier) + // It also has the side-effect of sometimes fixing small round-off errors from LP + mdp.mvMultGSMinMax(soln, min, unknown, false, true, strat); + + // Finished solution + timer = System.currentTimeMillis() - timer; + mainLog.print("Linear programming"); + mainLog.println(" took " + timer / 1000.0 + " seconds."); + + // Return results + // (Note we don't add the strategy - the one passed in is already there + // and might have some existing choices stored for other states). + ModelCheckerResult res = new ModelCheckerResult(); + res.soln = soln; + res.accuracy = new Accuracy(AccuracyLevel.EXACT_FLOATING_POINT); + res.timeTaken = timer / 1000.0; + return res; + } + + /** + * Solve the linear program for reachability probabilities with LPSolve. + * @param mdp: The MDP + * @param no: Probability 0 states + * @param yes: Probability 1 states + * @param maybe: Maybe states + * @param min: Min or max probabilities (true=min, false=max) + * @param strat Storage for (memoryless) strategy choice indices (ignored if null) + */ + protected double[] solveReachProbsLPWithLPSolve(MDP mdp, BitSet no, BitSet yes, BitSet unknown, boolean min, int strat[]) throws PrismException + { + double soln[] = null; + int n = mdp.getNumStates(); + try { + // Initialise LP solver + LpSolve solver = LpSolve.makeLp(0, n); + solver.setVerbose(lpsolve.LpSolve.CRITICAL); + solver.setAddRowmode(true); + // Set up arrays for passing LP to solver + double row[] = new double[n + 1]; + int colno[] = new int[n + 1]; + // Set objective function + if (min) { + solver.setMaxim(); + } else { + solver.setMinim(); + } + for (int s : new IterableBitSet(unknown)) { + row[s + 1] = 1.0; + } + solver.setObjFn(row); + // Add constraints + for (int s = 0; s < n; s++) { + solver.setBounds(s + 1, 0, 1); + if (yes.get(s)) { + row[0] = 1.0; + colno[0] = s + 1; + solver.addConstraintex(1, row, colno, LpSolve.EQ, 1.0); + } else if (no.get(s)) { + row[0] = 1.0; + colno[0] = s + 1; + solver.addConstraintex(1, row, colno, LpSolve.EQ, 0.0); + } else { + int numChoices = mdp.getNumChoices(s); + for (int i = 0; i < numChoices; i++) { + int count = 0; + row[count] = 1.0; + colno[count] = s + 1; + count++; + Iterator> iter = mdp.getTransitionsIterator(s, i); + while (iter.hasNext()) { + Map.Entry e = iter.next(); + int t = e.getKey(); + double p = e.getValue(); + if (t == s) { + row[0] -= p; + } else { + row[count] = -p; + colno[count] = t + 1; + count++; + } + } + solver.addConstraintex(count, row, colno, min ? LpSolve.LE : LpSolve.GE, 0.0); + } + } + } + // Solve LP + solver.setAddRowmode(false); + //solver.printLp(); + int lpRes = solver.solve(); + if (lpRes == lpsolve.LpSolve.OPTIMAL) { + soln = solver.getPtrVariables(); + } else { + throw new PrismException("Error solving LP" + (lpRes == lpsolve.LpSolve.INFEASIBLE ? " (infeasible)" : "")); + } + // Clean up + solver.deleteLp(); + // Return solution + return soln; + } catch (LpSolveException e) { + throw new PrismException("Error solving LP: " +e.getMessage()); + } + } + + /** + * Solve the linear program for reachability probabilities with Gurobi. + * @param mdp: The MDP + * @param no: Probability 0 states + * @param yes: Probability 1 states + * @param maybe: Maybe states + * @param min: Min or max probabilities (true=min, false=max) + * @param strat Storage for (memoryless) strategy choice indices (ignored if null) + */ + protected double[] solveReachProbsLPWithGurobi(MDP mdp, BitSet no, BitSet yes, BitSet unknown, boolean min, int strat[]) throws PrismException + { + double soln[] = null; + int n = mdp.getNumStates(); + try { + // Initialise LP solver + GRBEnv env = new GRBEnv("gurobi.log"); + env.set(GRB.IntParam.OutputFlag, 0); + GRBModel model = new GRBModel(env); + // Set up LP variables + objective function + GRBVar xVars[] = new GRBVar[n]; + for (int s = 0; s < n; s++) { + xVars[s] = model.addVar(0.0, 1.0, unknown.get(s) ? 1.0 : 0.0, GRB.CONTINUOUS, "x" + s); + } + model.set(GRB.IntAttr.ModelSense, min ? -1 : 1); + // Set up arrays for passing LP to solver + double row[] = new double[n + 1]; + int colno[] = new int[n + 1]; + // Add constraints + int counter = 0; + for (int s = 0; s < n; s++) { + if (yes.get(s)) { + GRBLinExpr expr = new GRBLinExpr(); + expr.addTerm(1.0, xVars[s]); + model.addConstr(expr, GRB.EQUAL, 1.0, "c" + counter++); + } else if (no.get(s)) { + GRBLinExpr expr = new GRBLinExpr(); + expr.addTerm(1.0, xVars[s]); + model.addConstr(expr, GRB.EQUAL, 0.0, "c" + counter++); + } else { + int numChoices = mdp.getNumChoices(s); + for (int i = 0; i < numChoices; i++) { + int count = 0; + row[count] = 1.0; + colno[count] = s + 1; + count++; + Iterator> iter = mdp.getTransitionsIterator(s, i); + while (iter.hasNext()) { + Map.Entry e = iter.next(); + int t = e.getKey(); + double p = e.getValue(); + if (t == s) { + row[0] -= p; + } else { + row[count] = -p; + colno[count] = t + 1; + count++; + } + } + GRBLinExpr expr = new GRBLinExpr(); + for (int j = 0; j < count; j++) { + expr.addTerm(row[j], xVars[colno[j] - 1]); + } + model.addConstr(expr, min ? GRB.LESS_EQUAL : GRB.GREATER_EQUAL, 0.0, "c" + counter++); + } + } + } + // Solve LP + //model.write("gurobi.lp"); + model.optimize(); + if (model.get(GRB.IntAttr.Status) == GRB.Status.OPTIMAL) { + soln = new double[n]; + for (int s = 0; s < n; s++) { + soln[s] = xVars[s].get(GRB.DoubleAttr.X); + } + } else { + throw new PrismException("Error solving LP" + (model.get(GRB.IntAttr.Status) == GRB.Status.INFEASIBLE ? " (infeasible)" : "")); + } + // Clean up + model.dispose(); + env.dispose(); + // Return solution + return soln; + } catch (GRBException e) { + throw new PrismException("Error solving LP: " +e.getMessage()); + } + } + /** * Construct strategy information for min/max reachability probabilities. * (More precisely, list of indices of choices resulting in min/max.) @@ -2053,7 +2389,7 @@ public ModelCheckerResult computeReachRewards(MDP mdp, MDPRewards mdpRewards, Bi MDPSolnMethod mdpSolnMethod = this.mdpSolnMethod; // Switch to a supported method, if necessary - if (!(mdpSolnMethod == MDPSolnMethod.VALUE_ITERATION || mdpSolnMethod == MDPSolnMethod.GAUSS_SEIDEL || mdpSolnMethod == MDPSolnMethod.POLICY_ITERATION)) { + if (!(mdpSolnMethod == MDPSolnMethod.VALUE_ITERATION || mdpSolnMethod == MDPSolnMethod.GAUSS_SEIDEL || mdpSolnMethod == MDPSolnMethod.POLICY_ITERATION || mdpSolnMethod == MDPSolnMethod.LINEAR_PROGRAMMING)) { mdpSolnMethod = MDPSolnMethod.GAUSS_SEIDEL; mainLog.printWarning("Switching to MDP solution method \"" + mdpSolnMethod.fullName() + "\""); } @@ -2069,6 +2405,14 @@ public ModelCheckerResult computeReachRewards(MDP mdp, MDPRewards mdpRewards, Bi throw new PrismNotSupportedException("Currently, explicit engine only supports interval iteration with value iteration or Gauss-Seidel for MDPs"); } } + if (mdpSolnMethod == MDPSolnMethod.LINEAR_PROGRAMMING) { + if (!(precomp && prob1)) { + throw new PrismNotSupportedException("Prob1 precomputation must be enabled for linear programming"); + } + if (!min && (genStrat || exportAdv)) { + throw new PrismNotSupportedException("Currently, explicit engine does not support adversary construction for linear programming and Rmax"); + } + } // Start expected reachability timer = System.currentTimeMillis(); @@ -2234,6 +2578,9 @@ protected ModelCheckerResult computeReachRewardsNumeric(MDP mdp, MDPRewards mdpR } res = computeReachRewardsPolIter(mdp, mdpRewards, target, inf, min, strat); break; + case LINEAR_PROGRAMMING: + res = computeReachRewardsLP(mdp, mdpRewards, target, inf, min, strat); + break; default: throw new PrismException("Unknown MDP solution method " + method.fullName()); } @@ -2617,6 +2964,130 @@ protected ModelCheckerResult computeReachRewardsPolIter(MDP mdp, MDPRewards mdpR return res; } + /** + * Compute expected reachability rewards using linear programming. + * @param mdp: The MDP + * @param mdpRewards The rewards + * @param target Target states + * @param inf States for which reward is infinite + * @param min: Min or max probabilities (true=min, false=max) + * @param strat Storage for (memoryless) strategy choice indices (ignored if null) + */ + protected ModelCheckerResult computeReachRewardsLP(MDP mdp, MDPRewards mdpRewards, BitSet target, BitSet inf, boolean min, int strat[]) throws PrismException + { + double soln[] = null; + long timer; + + // Start solution + timer = System.currentTimeMillis(); + mainLog.println("Starting linear programming (" + (min ? "min" : "max") + ")..."); + + // Store num states + int n = mdp.getNumStates(); + + // Determine set of states actually need to perform computation for + BitSet unknown = new BitSet(); + unknown.set(0, n); + unknown.andNot(target); + unknown.andNot(inf); + + try { + // Initialise LP solver + LpSolve solver = LpSolve.makeLp(0, n); + solver.setVerbose(lpsolve.LpSolve.CRITICAL); + solver.setAddRowmode(true); + // Set up arrays for passing LP to solver + double row[] = new double[n + 1]; + int colno[] = new int[n + 1]; + // Set objective function + if (min) { + solver.setMaxim(); + } else { + solver.setMinim(); + } + for (int s : new IterableBitSet(unknown)) { + row[s + 1] = 1.0; + } + solver.setObjFn(row); + // Add constraints + for (int s = 0; s < n; s++) { + solver.setBounds(s + 1, 0, Double.POSITIVE_INFINITY); + if (!unknown.get(s)) { + row[0] = 1.0; + colno[0] = s + 1; + solver.addConstraintex(1, row, colno, LpSolve.EQ, 0.0); + } else { + int numChoices = mdp.getNumChoices(s); + for (int i = 0; i < numChoices; i++) { + int count = 0; + row[count] = 1.0; + colno[count] = s + 1; + count++; + boolean toInf = false; + Iterator> iter = mdp.getTransitionsIterator(s, i); + while (iter.hasNext()) { + Map.Entry e = iter.next(); + int t = e.getKey(); + double p = e.getValue(); + if (t == s) { + row[0] -= p; + } else { + row[count] = -p; + colno[count] = t + 1; + count++; + } + toInf = toInf || inf.get(t); + } + // We ignore choices that may lead to an inf states + // (inf states are not handled by the LP so given value 0) + if (!toInf) { + double rew = mdpRewards.getStateReward(s) + mdpRewards.getTransitionReward(s, i); + solver.addConstraintex(count, row, colno, min ? LpSolve.LE : LpSolve.GE, rew); + } + } + } + } + // Solve LP + solver.setAddRowmode(false); + //solver.printLp(); + int lpRes = solver.solve(); + if (lpRes == lpsolve.LpSolve.OPTIMAL) { + soln = solver.getPtrVariables(); + } else { + throw new PrismException("Error solving LP" + (lpRes == lpsolve.LpSolve.INFEASIBLE ? " (infeasible)" : "")); + } + // Clean up + solver.deleteLp(); + } catch (LpSolveException e) { + throw new PrismException("Error solving LP: " +e.getMessage()); + } + + // Set value for states with infinite rewards + for (int s : new IterableBitSet(inf)) { + soln[s] = Double.POSITIVE_INFINITY; + } + + // We do an extra iteration of VI (using GS since we have just one solution vector) + // If strategy generation was requested (strat != null), this takes care of it + // (NB: that only works reliably for min - max needs more work - but this is disallowed earlier) + // It also has the side-effect of sometimes fixing small round-off errors from LP + mdp.mvMultRewGSMinMax(soln, mdpRewards, min, unknown, false, true, strat); + + // Finished solution + timer = System.currentTimeMillis() - timer; + mainLog.print("Linear programming"); + mainLog.println(" took " + timer / 1000.0 + " seconds."); + + // Return results + // (Note we don't add the strategy - the one passed in is already there + // and might have some existing choices stored for other states). + ModelCheckerResult res = new ModelCheckerResult(); + res.soln = soln; + res.accuracy = new Accuracy(AccuracyLevel.EXACT_FLOATING_POINT); + res.timeTaken = timer / 1000.0; + return res; + } + /** * Construct strategy information for min/max expected reachability. * (More precisely, list of indices of choices resulting in min/max.) @@ -2634,6 +3105,171 @@ public List expReachStrategy(MDP mdp, MDPRewards mdpRewards, int state, return mdp.mvMultRewMinMaxSingleChoices(state, lastSoln, mdpRewards, min, val); } + /** + * Compute a multi-strategy for... + * @param mdp: The MDP + * @param mdpRewards The rewards + * @param target Target states + * @param inf States for which reward is infinite + * @param min: Min or max probabilities (true=min, false=max) + * @param strat Storage for (memoryless) strategy choice indices (ignored if null) + */ + public ModelCheckerResult computeMultiStrategy(MDP mdp, MDPRewards mdpRewards, double bound) throws PrismException + { + boolean min = true; + double soln[] = null; + + // Start solution + long timer = System.currentTimeMillis(); + mainLog.println("Starting linear programming (" + (min ? "min" : "max") + ")..."); + + // Store MDP info + int n = mdp.getNumStates(); + int sInit = mdp.getFirstInitialState(); + // Find states where max expected total reward is 0 + BitSet maxRew0 = rewTot0(mdp, mdpRewards, false); + + try { + // Initialise MILP solver + GRBEnv env = new GRBEnv("gurobi.log"); + env.set(GRB.IntParam.OutputFlag, 0); + GRBModel model = new GRBModel(env); + // Set up MILP variables (real) + GRBVar xVars[] = new GRBVar[n]; + for (int s = 0; s < n; s++) { + xVars[s] = model.addVar(0.0, maxRew0.get(s) ? 0.0 : GRB.INFINITY, 0.0, GRB.CONTINUOUS, "x" + s); + } + // Set up MILP variables (binary) + GRBVar yaVars[][] = new GRBVar[n][]; + for (int s = 0; s < n; s++) { + int nc = mdp.getNumChoices(s); + yaVars[s] = new GRBVar[nc]; + for (int j = 0; j < nc; j++) { + yaVars[s][j] = model.addVar(0.0, 1.0, 0.0, GRB.BINARY, "y" + s + "_" + j + mdp.getAction(s, j)); + } + } + + double scale = 100.0; + + // Set up objective function + GRBLinExpr exprObj = new GRBLinExpr(); + exprObj.addTerm(-1.0, xVars[sInit]); + //double rhs = 0.0; + for (int s = 0; s < n; s++) { + int nc = mdp.getNumChoices(s); + for (int j = 0; j < nc; j++) { + double phi_s_j = 1.0 * scale; + exprObj.addTerm(-phi_s_j, yaVars[s][j]); + //rhs -= phi_s_j; + } + } + model.setObjective(exprObj, GRB.MINIMIZE); + + // Set up arrays for passing MILP to solver + double row[] = new double[n + 1]; + int colno[] = new int[n + 1]; + // Add constraints + int counter = 0; + double b = bound; + GRBLinExpr expr = new GRBLinExpr(); + expr.addTerm(1.0, xVars[sInit]); + model.addConstr(expr, GRB.GREATER_EQUAL, b, "c" + counter++); + for (int s = 0; s < n; s++) { + expr = new GRBLinExpr(); + int nc = mdp.getNumChoices(s); + for (int j = 0; j < nc; j++) { + expr.addTerm(1.0, yaVars[s][j]); + } + model.addConstr(expr, GRB.GREATER_EQUAL, 1.0, "c" + counter++); + } + for (int s = 0; s < n; s++) { + int numChoices = mdp.getNumChoices(s); + for (int i = 0; i < numChoices; i++) { + int count = 0; + row[count] = 1.0; + colno[count] = s + 1; + count++; + Iterator> iter = mdp.getTransitionsIterator(s, i); + while (iter.hasNext()) { + Map.Entry e = iter.next(); + int t = e.getKey(); + double p = e.getValue(); + if (t == s) { + row[0] -= p; + } else { + row[count] = -p; + colno[count] = t + 1; + count++; + } + } + // TODO state rewards? + double r = mdpRewards.getTransitionReward(s, i); + expr = new GRBLinExpr(); + for (int j = 0; j < count; j++) { + expr.addTerm(row[j], xVars[colno[j] - 1]); + } + expr.addTerm(scale, yaVars[s][i]); + model.addConstr(expr, GRB.LESS_EQUAL, r + scale, "c" + counter++); + } + } + // Solve MILP + //model.write("gurobi.lp"); + model.optimize(); + if (model.get(GRB.IntAttr.Status) == GRB.Status.INFEASIBLE) { +// model.computeIIS(); +// System.out.println("\nThe following constraint(s) " + "cannot be satisfied:"); +// for (GRBConstr c : model.getConstrs()) { +// if (c.get(GRB.IntAttr.IISConstr) == 1) { +// System.out.println(c.get(GRB.StringAttr.ConstrName)); +// } +// } + throw new PrismException("Error solving LP: " + "infeasible"); + } + if (model.get(GRB.IntAttr.Status) == GRB.Status.UNBOUNDED) { + throw new PrismException("Error solving LP: " + "unbounded"); + } + if (model.get(GRB.IntAttr.Status) != GRB.Status.OPTIMAL) { + throw new PrismException("Error solving LP: " + "non-optimal " + model.get(GRB.IntAttr.Status)); + } + soln = new double[n]; + for (int s = 0; s < n; s++) { + System.out.println(xVars[s].get(GRB.StringAttr.VarName) + " = "+xVars[s].get(GRB.DoubleAttr.X)); + soln[s] = xVars[s].get(GRB.DoubleAttr.X); + } + for (int s = 0; s < n; s++) { + int numChoices = mdp.getNumChoices(s); + for (int i = 0; i < numChoices; i++) { + System.out.println(yaVars[s][i].get(GRB.StringAttr.VarName) + " = " + yaVars[s][i].get(GRB.DoubleAttr.X)); + } + } + // Print multi-strategy + for (int s = 0; s < n; s++) { + mainLog.print(s + ":"); + int numChoices = mdp.getNumChoices(s); + for (int i = 0; i < numChoices; i++) { + if (yaVars[s][i].get(GRB.DoubleAttr.X) > 0) { + mainLog.print(" " + mdp.getAction(s, i)); + } + } + mainLog.println(); + } + + // Clean up + model.dispose(); + env.dispose(); + } catch (GRBException e) { + throw new PrismException("Error solving LP: " +e.getMessage()); + } + + + // Return results + ModelCheckerResult res = new ModelCheckerResult(); +// res.accuracy = AccuracyFactory.boundedNumericalIterations(); + res.soln = soln; +// res.timeTaken = timer / 1000.0; + return res; + } + /** * Restrict a (memoryless) strategy for an MDP, stored as an integer array of choice indices, * to the states of the MDP that are reachable under that strategy. diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index bcbab17412..582356fd96 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -49,6 +49,7 @@ import parser.type.TypePathDouble; import prism.AccuracyFactory; import prism.IntegerBound; +import prism.ModelType; import prism.OpRelOpBound; import prism.Prism; import prism.PrismComponent; @@ -565,8 +566,12 @@ protected StateValues checkExpressionStrategy(Model model, ExpressionStrategy ex } Expression exprSub = exprs.get(0); // Pass onto relevant method: + // Multi-strategy + if ("multi".equals(expr.getModifier())) { + return checkExpressionMultiStrategy(model, expr, forAll, coalition, statesOfInterest); + } // P operator - if (exprSub instanceof ExpressionProb) { + else if (exprSub instanceof ExpressionProb) { return checkExpressionProb(model, (ExpressionProb) exprSub, forAll, coalition, statesOfInterest); } // R operator @@ -579,6 +584,50 @@ else if (exprSub instanceof ExpressionReward) { } } + /** + * Model check a <<>> operator requesting a multi-strategy + * @param statesOfInterest the states of interest, see checkExpression() + */ + protected StateValues checkExpressionMultiStrategy(Model model, ExpressionStrategy expr, boolean forAll, Coalition coalition, BitSet statesOfInterest) throws PrismException + { + // Only support "exists" (<<>>) currently + if (forAll) { + throw new PrismException("Multi-strategies not supported for " + expr.getOperatorString()); + } + // Only support R[C] currently + Expression exprSub = expr.getOperands().get(0); + if (!(exprSub instanceof ExpressionReward)) { + throw new PrismException("Multi-strategy synthesis only supports R[C] properties currently"); + } + ExpressionReward exprRew = (ExpressionReward) exprSub; + if (!(exprRew.getExpression() instanceof ExpressionTemporal)) { + throw new PrismException("Multi-strategy synthesis only supports R[C] properties currently"); + } + ExpressionTemporal exprTemp = (ExpressionTemporal) exprRew.getExpression(); + if (!(exprTemp.getOperator() == ExpressionTemporal.R_C) && !exprTemp.hasBounds()) { + throw new PrismException("Multi-strategy synthesis only supports R[C] properties currently"); + } + + // Get info from R operator + OpRelOpBound opInfo = exprRew.getRelopBoundInfo(constantValues); + MinMax minMax = opInfo.getMinMax(model.getModelType(), false); + + // Build rewards + int r = exprRew.getRewardStructIndexByIndexObject(rewardGen, constantValues); + mainLog.println("Building reward structure..."); + Rewards modelRewards = constructRewards(model, r); + + // Only support MDPs + if (model.getModelType() != ModelType.MDP) { + throw new PrismNotSupportedException("Multi-strategy synthesis not supported for " + model.getModelType() + "s"); + } + + ModelCheckerResult res = ((MDPModelChecker) this).computeMultiStrategy((MDP) model, (MDPRewards) modelRewards, opInfo.getBound()); + + result.setStrategy(res.strat); + return StateValues.createFromDoubleArrayResult(res, model); + } + /** * Model check a P operator expression and return the values for the statesOfInterest. * @param statesOfInterest the states of interest, see checkExpression() diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index 1fc4e02508..f9ef80e5da 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -3278,6 +3278,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression // (Property) expression: ATL strategy operators <<>> and [[]] static final public Expression ExpressionStrategy(boolean prop, boolean pathprop) throws ParseException {ExpressionStrategy ret; + ExpressionIdent modifier = null; Expression expr; Token begin = null; if (!prop) {if (true) throw generateParseException();} @@ -3302,6 +3303,17 @@ static class ExpressionPair { public Expression expr1 = null; public Expression throw new ParseException(); } switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { + case LBRACE:{ + jj_consume_token(LBRACE); + modifier = IdentifierExpression(); + jj_consume_token(RBRACE); + break; + } + default: + jj_la1[89] = jj_gen; + ; + } + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { case PMAX: case PMIN: case P: @@ -3322,7 +3334,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[89] = jj_gen; + jj_la1[90] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3335,11 +3347,12 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[90] = jj_gen; + jj_la1[91] = jj_gen; jj_consume_token(-1); throw new ParseException(); } -ret.setPosition(begin, getToken(0)); +ret.setModifier(modifier == null ? null : modifier.getName()); + ret.setPosition(begin, getToken(0)); {if ("" != null) return ret;} throw new Error("Missing return statement in function"); } @@ -3355,7 +3368,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[93] = jj_gen; + jj_la1[94] = jj_gen; switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { case REG_INT: case REG_IDENT:{ @@ -3369,7 +3382,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[91] = jj_gen; + jj_la1[92] = jj_gen; break label_29; } jj_consume_token(COMMA); @@ -3379,7 +3392,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[92] = jj_gen; + jj_la1[93] = jj_gen; ; } exprStrat.setCoalition(coalition); @@ -3399,7 +3412,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[94] = jj_gen; + jj_la1[95] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3426,7 +3439,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[95] = jj_gen; + jj_la1[96] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3477,7 +3490,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[96] = jj_gen; + jj_la1[97] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3490,7 +3503,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression break; } default: - jj_la1[97] = jj_gen; + jj_la1[98] = jj_gen; ; } jj_consume_token(RPARENTH); @@ -3539,7 +3552,7 @@ String Identifier() throws ParseException { break; } default: - jj_la1[98] = jj_gen; + jj_la1[99] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3576,7 +3589,7 @@ int EqNeq() throws ParseException { break; } default: - jj_la1[99] = jj_gen; + jj_la1[100] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3608,7 +3621,7 @@ int LtGt() throws ParseException { break; } default: - jj_la1[100] = jj_gen; + jj_la1[101] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3634,7 +3647,7 @@ int LtGt() throws ParseException { break; } default: - jj_la1[101] = jj_gen; + jj_la1[102] = jj_gen; ; } jj_consume_token(0); @@ -3793,8 +3806,7 @@ static private boolean jj_2_18(int xla) static private boolean jj_3R_ExpressionFilter_1903_11_187() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_Expression_1155_9_39()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; return false; } @@ -3804,23 +3816,29 @@ static private boolean jj_3R_ExpressionFuncOldStyle_1494_37_163() return false; } - static private boolean jj_3R_SystemAtomic_1135_10_80() + static private boolean jj_3R_ExpressionFilter_1902_11_184() { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_SystemDefn_1012_9_32()) return true; - if (jj_scan_token(RPARENTH)) return true; + if (jj_scan_token(PLUS)) return true; return false; } - static private boolean jj_3R_ExpressionFilter_1899_11_186() + static private boolean jj_3R_ExpressionFilter_1901_11_182() { - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_scan_token(MIN)) return true; return false; } - static private boolean jj_3R_ExpressionFilter_1898_11_183() + static private boolean jj_3R_SystemAtomic_1135_10_80() { - if (jj_scan_token(PLUS)) return true; + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_SystemDefn_1012_9_32()) return true; + if (jj_scan_token(RPARENTH)) return true; + return false; + } + + static private boolean jj_3R_ExpressionLabel_1880_30_180() + { + if (jj_3R_Identifier_1923_9_30()) return true; return false; } @@ -3833,17 +3851,11 @@ static private boolean jj_3R_ExpressionLiteral_1517_9_155() static private boolean jj_3R_SystemAtomic_1133_10_79() { if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; if (jj_scan_token(DQUOTE)) return true; return false; } - static private boolean jj_3R_ExpressionFilter_1897_11_181() - { - if (jj_scan_token(MIN)) return true; - return false; - } - static private boolean jj_3R_ExpressionLiteral_1516_9_143() { Token xsp; @@ -3861,22 +3873,16 @@ static private boolean jj_3R_ExpressionLiteral_1516_9_143() return false; } - static private boolean jj_3R_ExpressionLabel_1876_30_179() - { - if (jj_3R_Identifier_1919_9_30()) return true; - return false; - } - static private boolean jj_3R_SystemAtomic_1131_9_78() { - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; return false; } static private boolean jj_3R_SystemParallel_1075_65_71() { if (jj_scan_token(COMMA)) return true; - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; return false; } @@ -3886,37 +3892,23 @@ static private boolean jj_3R_ExpressionFuncMinMax_1480_42_161() return false; } - static private boolean jj_3R_SystemAtomic_1128_9_69() - { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_SystemAtomic_1131_9_78()) { - jj_scanpos = xsp; - if (jj_3R_SystemAtomic_1133_10_79()) { - jj_scanpos = xsp; - if (jj_3R_SystemAtomic_1135_10_80()) return true; - } - } - return false; - } - - static private boolean jj_3R_ExpressionFilter_1892_9_154() + static private boolean jj_3R_ExpressionFilter_1896_9_154() { if (jj_scan_token(FILTER)) return true; if (jj_scan_token(LPARENTH)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_ExpressionFilter_1897_11_181()) { + if (jj_3R_ExpressionFilter_1901_11_182()) { jj_scanpos = xsp; - if (jj_3R_ExpressionFilter_1897_35_182()) { + if (jj_3R_ExpressionFilter_1901_35_183()) { jj_scanpos = xsp; - if (jj_3R_ExpressionFilter_1898_11_183()) { + if (jj_3R_ExpressionFilter_1902_11_184()) { jj_scanpos = xsp; - if (jj_3R_ExpressionFilter_1898_34_184()) { + if (jj_3R_ExpressionFilter_1902_34_185()) { jj_scanpos = xsp; - if (jj_3R_ExpressionFilter_1898_56_185()) { + if (jj_3R_ExpressionFilter_1902_56_186()) { jj_scanpos = xsp; - if (jj_3R_ExpressionFilter_1899_11_186()) return true; + if (jj_3R_ExpressionFilter_1903_11_187()) return true; } } } @@ -3925,18 +3917,32 @@ static private boolean jj_3R_ExpressionFilter_1892_9_154() if (jj_scan_token(COMMA)) return true; if (jj_3R_Expression_1155_9_39()) return true; xsp = jj_scanpos; - if (jj_3R_ExpressionFilter_1903_11_187()) jj_scanpos = xsp; + if (jj_3R_ExpressionFilter_1907_11_188()) jj_scanpos = xsp; if (jj_scan_token(RPARENTH)) return true; return false; } + static private boolean jj_3R_SystemAtomic_1128_9_69() + { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_SystemAtomic_1131_9_78()) { + jj_scanpos = xsp; + if (jj_3R_SystemAtomic_1133_10_79()) { + jj_scanpos = xsp; + if (jj_3R_SystemAtomic_1135_10_80()) return true; + } + } + return false; + } + static private boolean jj_3R_ExpressionFuncArgs_1506_9_162() { if (jj_3R_Expression_1155_9_39()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_ExpressionFuncArgs_1506_72_188()) { jj_scanpos = xsp; break; } + if (jj_3R_ExpressionFuncArgs_1506_72_189()) { jj_scanpos = xsp; break; } } return false; } @@ -3944,9 +3950,9 @@ static private boolean jj_3R_ExpressionFuncArgs_1506_9_162() static private boolean jj_3R_SystemHideRename_1112_19_92() { if (jj_scan_token(COMMA)) return true; - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; if (jj_scan_token(RENAME)) return true; - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; return false; } @@ -3971,12 +3977,25 @@ static private boolean jj_3_3() return false; } + static private boolean jj_3R_ExpressionLabel_1878_9_153() + { + if (jj_scan_token(DQUOTE)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_ExpressionLabel_1880_30_180()) { + jj_scanpos = xsp; + if (jj_3R_ExpressionLabel_1880_47_181()) return true; + } + if (jj_scan_token(DQUOTE)) return true; + return false; + } + static private boolean jj_3R_SystemHideRename_1109_11_82() { if (jj_scan_token(LBRACE)) return true; - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; if (jj_scan_token(RENAME)) return true; - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; Token xsp; while (true) { xsp = jj_scanpos; @@ -4014,20 +4033,7 @@ static private boolean jj_3R_ExpressionFuncOldStyle_1494_9_146() return false; } - static private boolean jj_3R_ExpressionLabel_1874_9_153() - { - if (jj_scan_token(DQUOTE)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_ExpressionLabel_1876_30_179()) { - jj_scanpos = xsp; - if (jj_3R_ExpressionLabel_1876_47_180()) return true; - } - if (jj_scan_token(DQUOTE)) return true; - return false; - } - - static private boolean jj_3R_ExpressionStrategy_1827_51_208() + static private boolean jj_3R_ExpressionStrategy_1830_51_209() { if (jj_3R_ExpressionReward_1688_9_149()) return true; return false; @@ -4037,7 +4043,7 @@ static private boolean jj_3R_SystemHideRename_1103_9_81() { if (jj_scan_token(DIVIDE)) return true; if (jj_scan_token(LBRACE)) return true; - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; Token xsp; while (true) { xsp = jj_scanpos; @@ -4082,6 +4088,17 @@ static private boolean jj_3_8() return false; } + static private boolean jj_3R_ExpressionStrategyCoalitionPlayer_1864_9_219() + { + Token xsp; + xsp = jj_scanpos; + if (jj_scan_token(91)) { + jj_scanpos = xsp; + if (jj_scan_token(94)) return true; + } + return false; + } + static private boolean jj_3R_ExpressionFuncMinMax_1480_9_145() { Token xsp; @@ -4096,14 +4113,10 @@ static private boolean jj_3R_ExpressionFuncMinMax_1480_9_145() return false; } - static private boolean jj_3R_ExpressionStrategyCoalitionPlayer_1860_9_218() + static private boolean jj_3R_ExpressionStrategyCoalition_1853_11_220() { - Token xsp; - xsp = jj_scanpos; - if (jj_scan_token(91)) { - jj_scanpos = xsp; - if (jj_scan_token(94)) return true; - } + if (jj_scan_token(COMMA)) return true; + if (jj_3R_ExpressionStrategyCoalitionPlayer_1864_9_219()) return true; return false; } @@ -4115,6 +4128,25 @@ static private boolean jj_3R_SystemFullParallel_1027_71_44() return false; } + static private boolean jj_3R_ExpressionStrategyCoalition_1852_11_216() + { + if (jj_3R_ExpressionStrategyCoalitionPlayer_1864_9_219()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_ExpressionStrategyCoalition_1853_11_220()) { jj_scanpos = xsp; break; } + } + return false; + } + + static private boolean jj_3R_ExpressionStrategyCoalition_1852_9_212() + { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_ExpressionStrategyCoalition_1852_11_216()) jj_scanpos = xsp; + return false; + } + static private boolean jj_3R_ExpressionFuncOrIdent_1467_11_159() { if (jj_scan_token(LPARENTH)) return true; @@ -4130,63 +4162,37 @@ static private boolean jj_3_10() return false; } - static private boolean jj_3R_ExpressionStrategyCoalition_1849_11_219() - { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_ExpressionStrategyCoalitionPlayer_1860_9_218()) return true; - return false; - } - - static private boolean jj_3R_ExpressionStrategyCoalition_1848_11_215() + static private boolean jj_3R_ExpressionStrategyCoalition_1850_9_211() { - if (jj_3R_ExpressionStrategyCoalitionPlayer_1860_9_218()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_ExpressionStrategyCoalition_1849_11_219()) { jj_scanpos = xsp; break; } - } + if (jj_scan_token(TIMES)) return true; return false; } - static private boolean jj_3R_ExpressionStrategyCoalition_1848_9_211() + static private boolean jj_3R_ExpressionStrategyCoalition_1850_9_207() { Token xsp; xsp = jj_scanpos; - if (jj_3R_ExpressionStrategyCoalition_1848_11_215()) jj_scanpos = xsp; + if (jj_3R_ExpressionStrategyCoalition_1850_9_211()) { + jj_scanpos = xsp; + if (jj_3R_ExpressionStrategyCoalition_1852_9_212()) return true; + } return false; } static private boolean jj_3R_ExpressionFuncOrIdent_1465_9_144() { - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; Token xsp; xsp = jj_scanpos; if (jj_3R_ExpressionFuncOrIdent_1467_11_159()) jj_scanpos = xsp; return false; } - static private boolean jj_3R_ExpressionStrategyCoalition_1846_9_210() - { - if (jj_scan_token(TIMES)) return true; - return false; - } - - static private boolean jj_3R_ExpressionStrategyCoalition_1846_9_206() - { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_ExpressionStrategyCoalition_1846_9_210()) { - jj_scanpos = xsp; - if (jj_3R_ExpressionStrategyCoalition_1848_9_211()) return true; - } - return false; - } - static private boolean jj_3R_SystemParallel_1074_11_60() { if (jj_scan_token(OR)) return true; if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; Token xsp; while (true) { xsp = jj_scanpos; @@ -4207,57 +4213,65 @@ static private boolean jj_3R_SystemParallel_1072_9_50() return false; } + static private boolean jj_3R_ExpressionStrategy_1832_11_179() + { + if (jj_3R_ExpressionParenth_1556_9_147()) return true; + return false; + } + static private boolean jj_3R_ExpressionBasic_1443_17_142() { - if (jj_3R_ExpressionFilter_1892_9_154()) return true; + if (jj_3R_ExpressionFilter_1896_9_154()) return true; return false; } - static private boolean jj_3R_ExpressionBasic_1441_17_141() + static private boolean jj_3R_ExpressionStrategy_1830_11_208() { - if (jj_3R_ExpressionLabel_1874_9_153()) return true; + if (jj_3R_ExpressionProb_1580_9_148()) return true; return false; } - static private boolean jj_3R_ExpressionStrategy_1829_11_178() + static private boolean jj_3R_ExpressionBasic_1441_17_141() { - if (jj_3R_ExpressionParenth_1556_9_147()) return true; + if (jj_3R_ExpressionLabel_1878_9_153()) return true; return false; } - static private boolean jj_3R_ExpressionBasic_1439_17_140() + static private boolean jj_3R_ExpressionStrategy_1830_9_178() { - if (jj_3R_ExpressionStrategy_1820_9_152()) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_ExpressionStrategy_1830_11_208()) { + jj_scanpos = xsp; + if (jj_3R_ExpressionStrategy_1830_51_209()) return true; + } return false; } - static private boolean jj_3R_ExpressionStrategy_1827_11_207() + static private boolean jj_3R_ExpressionBasic_1439_17_140() { - if (jj_3R_ExpressionProb_1580_9_148()) return true; + if (jj_3R_ExpressionStrategy_1821_9_152()) return true; return false; } - static private boolean jj_3R_ExpressionBasic_1437_17_139() + static private boolean jj_3R_ExpressionStrategy_1827_11_177() { - if (jj_3R_ExpressionForAll_1801_9_151()) return true; + if (jj_scan_token(LBRACE)) return true; + if (jj_3R_IdentifierExpression_1934_9_33()) return true; + if (jj_scan_token(RBRACE)) return true; return false; } - static private boolean jj_3R_ExpressionStrategy_1827_9_177() + static private boolean jj_3R_ExpressionBasic_1437_17_139() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_ExpressionStrategy_1827_11_207()) { - jj_scanpos = xsp; - if (jj_3R_ExpressionStrategy_1827_51_208()) return true; - } + if (jj_3R_ExpressionForAll_1801_9_151()) return true; return false; } - static private boolean jj_3R_ExpressionStrategy_1824_11_176() + static private boolean jj_3R_ExpressionStrategy_1825_11_176() { if (jj_scan_token(DLBRACKET)) return true; - if (jj_3R_ExpressionStrategyCoalition_1846_9_206()) return true; + if (jj_3R_ExpressionStrategyCoalition_1850_9_207()) return true; if (jj_scan_token(DRBRACKET)) return true; return false; } @@ -4268,23 +4282,23 @@ static private boolean jj_3R_ExpressionBasic_1435_17_138() return false; } - static private boolean jj_3R_ExpressionTimesDivide_1387_64_128() + static private boolean jj_3R_ExpressionStrategy_1824_10_175() { - if (jj_scan_token(DIVIDE)) return true; + if (jj_scan_token(DLT)) return true; + if (jj_3R_ExpressionStrategyCoalition_1850_9_207()) return true; + if (jj_scan_token(DGT)) return true; return false; } - static private boolean jj_3R_RewardIndex_1732_101_217() + static private boolean jj_3R_ExpressionTimesDivide_1387_64_128() { - if (jj_3R_Expression_1155_9_39()) return true; + if (jj_scan_token(DIVIDE)) return true; return false; } - static private boolean jj_3R_ExpressionStrategy_1823_10_175() + static private boolean jj_3R_RewardIndex_1732_101_218() { - if (jj_scan_token(DLT)) return true; - if (jj_3R_ExpressionStrategyCoalition_1846_9_206()) return true; - if (jj_scan_token(DGT)) return true; + if (jj_3R_Expression_1155_9_39()) return true; return false; } @@ -4300,28 +4314,30 @@ static private boolean jj_3R_ExpressionBasic_1431_17_136() return false; } - static private boolean jj_3R_ExpressionBasic_1429_17_135() - { - if (jj_3R_ExpressionProb_1580_9_148()) return true; - return false; - } - - static private boolean jj_3R_ExpressionStrategy_1820_9_152() + static private boolean jj_3R_ExpressionStrategy_1821_9_152() { Token xsp; xsp = jj_scanpos; - if (jj_3R_ExpressionStrategy_1823_10_175()) { + if (jj_3R_ExpressionStrategy_1824_10_175()) { jj_scanpos = xsp; - if (jj_3R_ExpressionStrategy_1824_11_176()) return true; + if (jj_3R_ExpressionStrategy_1825_11_176()) return true; } xsp = jj_scanpos; - if (jj_3R_ExpressionStrategy_1827_9_177()) { + if (jj_3R_ExpressionStrategy_1827_11_177()) jj_scanpos = xsp; + xsp = jj_scanpos; + if (jj_3R_ExpressionStrategy_1830_9_178()) { jj_scanpos = xsp; - if (jj_3R_ExpressionStrategy_1829_11_178()) return true; + if (jj_3R_ExpressionStrategy_1832_11_179()) return true; } return false; } + static private boolean jj_3R_ExpressionBasic_1429_17_135() + { + if (jj_3R_ExpressionProb_1580_9_148()) return true; + return false; + } + static private boolean jj_3R_ExpressionBasic_1426_17_134() { if (jj_3R_ExpressionParenth_1556_9_147()) return true; @@ -4348,7 +4364,7 @@ static private boolean jj_3R_SystemInterleaved_1048_9_43() static private boolean jj_3_2() { if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; if (jj_scan_token(DQUOTE)) return true; if (jj_scan_token(COLON)) return true; return false; @@ -4372,7 +4388,7 @@ static private boolean jj_3R_ExpressionBasic_1418_17_130() return false; } - static private boolean jj_3R_RewardIndex_1730_87_213() + static private boolean jj_3R_RewardIndex_1730_87_214() { if (jj_3R_Expression_1155_9_39()) return true; return false; @@ -4508,7 +4524,7 @@ static private boolean jj_3R_ExpressionTimesDivide_1387_17_122() static private boolean jj_3_7() { if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; if (jj_scan_token(DQUOTE)) return true; if (jj_3R_SystemDefn_1012_9_32()) return true; return false; @@ -4521,7 +4537,7 @@ static private boolean jj_3_18() return false; } - static private boolean jj_3R_ExpressionRewardContents_1767_11_205() + static private boolean jj_3R_ExpressionRewardContents_1767_11_206() { if (jj_3R_Expression_1155_9_39()) return true; return false; @@ -4544,7 +4560,7 @@ static private boolean jj_3_17() return false; } - static private boolean jj_3R_ExpressionRewardContents_1764_11_204() + static private boolean jj_3R_ExpressionRewardContents_1764_11_205() { if (jj_scan_token(I)) return true; if (jj_scan_token(EQ)) return true; @@ -4558,13 +4574,13 @@ static private boolean jj_3_16() return false; } - static private boolean jj_3R_ExpressionRewardContents_1763_11_203() + static private boolean jj_3R_ExpressionRewardContents_1763_11_204() { if (jj_scan_token(C)) return true; return false; } - static private boolean jj_3R_ExpressionRewardContents_1762_11_202() + static private boolean jj_3R_ExpressionRewardContents_1762_11_203() { if (jj_scan_token(C)) return true; if (jj_scan_token(LE)) return true; @@ -4578,7 +4594,7 @@ static private boolean jj_3R_ExpressionPlusMinus_1370_19_123() return false; } - static private boolean jj_3R_ExpressionRewardContents_1759_11_201() + static private boolean jj_3R_ExpressionRewardContents_1759_11_202() { if (jj_scan_token(S)) return true; return false; @@ -4602,16 +4618,16 @@ static private boolean jj_3R_ExpressionPlusMinus_1370_17_118() return false; } - static private boolean jj_3R_ExpressionRewardContents_1758_9_200() + static private boolean jj_3R_ExpressionRewardContents_1758_9_201() { if (jj_3R_ExpressionSS_1644_9_34()) return true; return false; } - static private boolean jj_3R_RewardIndex_1732_33_216() + static private boolean jj_3R_RewardIndex_1732_33_217() { if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; if (jj_scan_token(DQUOTE)) return true; return false; } @@ -4620,17 +4636,17 @@ static private boolean jj_3R_ExpressionRewardContents_1755_9_173() { Token xsp; xsp = jj_scanpos; - if (jj_3R_ExpressionRewardContents_1758_9_200()) { + if (jj_3R_ExpressionRewardContents_1758_9_201()) { jj_scanpos = xsp; - if (jj_3R_ExpressionRewardContents_1759_11_201()) { + if (jj_3R_ExpressionRewardContents_1759_11_202()) { jj_scanpos = xsp; - if (jj_3R_ExpressionRewardContents_1762_11_202()) { + if (jj_3R_ExpressionRewardContents_1762_11_203()) { jj_scanpos = xsp; - if (jj_3R_ExpressionRewardContents_1763_11_203()) { + if (jj_3R_ExpressionRewardContents_1763_11_204()) { jj_scanpos = xsp; - if (jj_3R_ExpressionRewardContents_1764_11_204()) { + if (jj_3R_ExpressionRewardContents_1764_11_205()) { jj_scanpos = xsp; - if (jj_3R_ExpressionRewardContents_1767_11_205()) return true; + if (jj_3R_ExpressionRewardContents_1767_11_206()) return true; } } } @@ -4656,23 +4672,23 @@ static private boolean jj_3R_ExpressionPlusMinus_1368_9_114() return false; } - static private boolean jj_3R_RewardIndex_1730_22_212() + static private boolean jj_3R_RewardIndex_1730_22_213() { if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; if (jj_scan_token(DQUOTE)) return true; return false; } - static private boolean jj_3R_RewardIndex_1732_11_214() + static private boolean jj_3R_RewardIndex_1732_11_215() { if (jj_scan_token(DIVIDE)) return true; if (jj_scan_token(LBRACE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_RewardIndex_1732_33_216()) { + if (jj_3R_RewardIndex_1732_33_217()) { jj_scanpos = xsp; - if (jj_3R_RewardIndex_1732_101_217()) return true; + if (jj_3R_RewardIndex_1732_101_218()) return true; } if (jj_scan_token(RBRACE)) return true; return false; @@ -4680,23 +4696,23 @@ static private boolean jj_3R_RewardIndex_1732_11_214() static private boolean jj_3R_ExpressionRelop_1348_11_115() { - if (jj_3R_LtGt_1980_9_46()) return true; + if (jj_3R_LtGt_1984_9_46()) return true; if (jj_3R_ExpressionPlusMinus_1368_9_114()) return true; return false; } - static private boolean jj_3R_RewardIndex_1730_9_209() + static private boolean jj_3R_RewardIndex_1730_9_210() { if (jj_scan_token(LBRACE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_RewardIndex_1730_22_212()) { + if (jj_3R_RewardIndex_1730_22_213()) { jj_scanpos = xsp; - if (jj_3R_RewardIndex_1730_87_213()) return true; + if (jj_3R_RewardIndex_1730_87_214()) return true; } if (jj_scan_token(RBRACE)) return true; xsp = jj_scanpos; - if (jj_3R_RewardIndex_1732_11_214()) jj_scanpos = xsp; + if (jj_3R_RewardIndex_1732_11_215()) jj_scanpos = xsp; return false; } @@ -4714,14 +4730,14 @@ static private boolean jj_3R_ExpressionRelop_1347_9_112() static private boolean jj_3_1() { if (jj_scan_token(MODULE)) return true; - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; if (jj_scan_token(EQ)) return true; return false; } static private boolean jj_3R_ExpressionEquality_1334_11_113() { - if (jj_3R_EqNeq_1970_9_116()) return true; + if (jj_3R_EqNeq_1974_9_116()) return true; if (jj_3R_ExpressionRelop_1347_9_112()) return true; return false; } @@ -4780,28 +4796,28 @@ static private boolean jj_3R_TimeBound_1231_99_96() return false; } - static private boolean jj_3R_ExpressionReward_1693_18_196() + static private boolean jj_3R_ExpressionReward_1693_18_197() { - if (jj_3R_LtGt_1980_9_46()) return true; + if (jj_3R_LtGt_1984_9_46()) return true; if (jj_3R_Expression_1155_9_39()) return true; return false; } - static private boolean jj_3R_ExpressionReward_1692_18_195() + static private boolean jj_3R_ExpressionReward_1692_18_196() { - if (jj_3R_RewardIndex_1730_9_209()) return true; + if (jj_3R_RewardIndex_1730_9_210()) return true; return false; } - static private boolean jj_3R_ExpressionReward_1691_19_194() + static private boolean jj_3R_ExpressionReward_1691_19_195() { if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_IdentifierExpression_1930_9_33()) return true; + if (jj_3R_IdentifierExpression_1934_9_33()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_ExpressionReward_1696_13_199() + static private boolean jj_3R_ExpressionReward_1696_13_200() { if (jj_scan_token(MAX)) return true; if (jj_scan_token(EQ)) return true; @@ -4817,7 +4833,7 @@ static private boolean jj_3R_ExpressionReward_1699_10_172() return false; } - static private boolean jj_3R_ExpressionReward_1695_13_198() + static private boolean jj_3R_ExpressionReward_1695_13_199() { if (jj_scan_token(MIN)) return true; if (jj_scan_token(EQ)) return true; @@ -4844,7 +4860,7 @@ static private boolean jj_3R_ExpressionNot_1316_9_107() return false; } - static private boolean jj_3R_ExpressionReward_1694_13_197() + static private boolean jj_3R_ExpressionReward_1694_13_198() { if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; @@ -4862,17 +4878,17 @@ static private boolean jj_3R_ExpressionReward_1690_10_170() if (jj_scan_token(R)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_ExpressionReward_1691_19_194()) jj_scanpos = xsp; + if (jj_3R_ExpressionReward_1691_19_195()) jj_scanpos = xsp; xsp = jj_scanpos; - if (jj_3R_ExpressionReward_1692_18_195()) jj_scanpos = xsp; + if (jj_3R_ExpressionReward_1692_18_196()) jj_scanpos = xsp; xsp = jj_scanpos; - if (jj_3R_ExpressionReward_1693_18_196()) { + if (jj_3R_ExpressionReward_1693_18_197()) { jj_scanpos = xsp; - if (jj_3R_ExpressionReward_1694_13_197()) { + if (jj_3R_ExpressionReward_1694_13_198()) { jj_scanpos = xsp; - if (jj_3R_ExpressionReward_1695_13_198()) { + if (jj_3R_ExpressionReward_1695_13_199()) { jj_scanpos = xsp; - if (jj_3R_ExpressionReward_1696_13_199()) return true; + if (jj_3R_ExpressionReward_1696_13_200()) return true; } } } @@ -4969,7 +4985,7 @@ static private boolean jj_3R_ExpressionSS_1649_17_38() static private boolean jj_3R_ExpressionSS_1647_19_45() { if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_IdentifierExpression_1930_9_33()) return true; + if (jj_3R_IdentifierExpression_1934_9_33()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } @@ -4979,7 +4995,7 @@ static private boolean jj_3R_ExpressionSS_1647_17_37() Token xsp; xsp = jj_scanpos; if (jj_3R_ExpressionSS_1647_19_45()) jj_scanpos = xsp; - if (jj_3R_LtGt_1980_9_46()) return true; + if (jj_3R_LtGt_1984_9_46()) return true; if (jj_3R_Expression_1155_9_39()) return true; return false; } @@ -4987,7 +5003,7 @@ static private boolean jj_3R_ExpressionSS_1647_17_37() static private boolean jj_3R_UpdateElement_888_9_41() { if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_IdentifierPrime_1952_9_49()) return true; + if (jj_3R_IdentifierPrime_1956_9_49()) return true; if (jj_scan_token(EQ)) return true; if (jj_3R_Expression_1155_9_39()) return true; if (jj_scan_token(RPARENTH)) return true; @@ -5068,28 +5084,28 @@ static private boolean jj_3R_Update_873_9_31() static private boolean jj_3_14() { - if (jj_3R_IdentifierExpression_1930_9_33()) return true; + if (jj_3R_IdentifierExpression_1934_9_33()) return true; if (jj_scan_token(LPARENTH)) return true; return false; } static private boolean jj_3_13() { - if (jj_3R_IdentifierExpression_1930_9_33()) return true; + if (jj_3R_IdentifierExpression_1934_9_33()) return true; if (jj_scan_token(LPARENTH)) return true; return false; } static private boolean jj_3_12() { - if (jj_3R_IdentifierExpression_1930_9_33()) return true; + if (jj_3R_IdentifierExpression_1934_9_33()) return true; if (jj_scan_token(LPARENTH)) return true; return false; } static private boolean jj_3_11() { - if (jj_3R_IdentifierExpression_1930_9_33()) return true; + if (jj_3R_IdentifierExpression_1934_9_33()) return true; if (jj_scan_token(LPARENTH)) return true; return false; } @@ -5123,25 +5139,25 @@ static private boolean jj_3R_ExpressionITE_1248_9_76() static private boolean jj_3R_TimeBound_1234_20_101() { - if (jj_3R_IdentifierExpression_1930_9_33()) return true; + if (jj_3R_IdentifierExpression_1934_9_33()) return true; return false; } static private boolean jj_3R_TimeBound_1233_20_99() { - if (jj_3R_IdentifierExpression_1930_9_33()) return true; + if (jj_3R_IdentifierExpression_1934_9_33()) return true; return false; } static private boolean jj_3R_TimeBound_1232_20_97() { - if (jj_3R_IdentifierExpression_1930_9_33()) return true; + if (jj_3R_IdentifierExpression_1934_9_33()) return true; return false; } static private boolean jj_3R_TimeBound_1231_20_95() { - if (jj_3R_IdentifierExpression_1930_9_33()) return true; + if (jj_3R_IdentifierExpression_1934_9_33()) return true; return false; } @@ -5289,80 +5305,80 @@ static private boolean jj_3R_ExpressionTemporalUnary_1211_19_72() return false; } - static private boolean jj_3R_ExpressionTemporalUnary_1209_17_61() - { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_ExpressionTemporalUnary_1211_19_72()) { - jj_scanpos = xsp; - if (jj_3R_ExpressionTemporalUnary_1212_19_73()) { - jj_scanpos = xsp; - if (jj_3R_ExpressionTemporalUnary_1213_19_74()) return true; - } - } - xsp = jj_scanpos; - if (jj_3R_ExpressionTemporalUnary_1214_19_75()) jj_scanpos = xsp; - if (jj_3R_ExpressionTemporalUnary_1207_9_56()) return true; - return false; - } - - static private boolean jj_3R_LtGt_1983_9_55() + static private boolean jj_3R_LtGt_1987_9_55() { if (jj_scan_token(LE)) return true; return false; } - static private boolean jj_3R_ExpressionProb_1583_25_190() - { - if (jj_3R_LtGt_1980_9_46()) return true; - if (jj_3R_Expression_1155_9_39()) return true; - return false; - } - - static private boolean jj_3R_ExpressionProb_1582_26_189() - { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_IdentifierExpression_1930_9_33()) return true; - if (jj_scan_token(RPARENTH)) return true; - return false; - } - - static private boolean jj_3R_LtGt_1982_9_54() + static private boolean jj_3R_LtGt_1986_9_54() { if (jj_scan_token(GE)) return true; return false; } - static private boolean jj_3R_LtGt_1981_9_53() + static private boolean jj_3R_LtGt_1985_9_53() { if (jj_scan_token(LT)) return true; return false; } - static private boolean jj_3R_LtGt_1980_9_52() + static private boolean jj_3R_LtGt_1984_9_52() { if (jj_scan_token(GT)) return true; return false; } - static private boolean jj_3R_LtGt_1980_9_46() + static private boolean jj_3R_LtGt_1984_9_46() { Token xsp; xsp = jj_scanpos; - if (jj_3R_LtGt_1980_9_52()) { + if (jj_3R_LtGt_1984_9_52()) { jj_scanpos = xsp; - if (jj_3R_LtGt_1981_9_53()) { + if (jj_3R_LtGt_1985_9_53()) { jj_scanpos = xsp; - if (jj_3R_LtGt_1982_9_54()) { + if (jj_3R_LtGt_1986_9_54()) { jj_scanpos = xsp; - if (jj_3R_LtGt_1983_9_55()) return true; + if (jj_3R_LtGt_1987_9_55()) return true; } } } return false; } - static private boolean jj_3R_ExpressionProb_1586_17_193() + static private boolean jj_3R_ExpressionTemporalUnary_1209_17_61() + { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_ExpressionTemporalUnary_1211_19_72()) { + jj_scanpos = xsp; + if (jj_3R_ExpressionTemporalUnary_1212_19_73()) { + jj_scanpos = xsp; + if (jj_3R_ExpressionTemporalUnary_1213_19_74()) return true; + } + } + xsp = jj_scanpos; + if (jj_3R_ExpressionTemporalUnary_1214_19_75()) jj_scanpos = xsp; + if (jj_3R_ExpressionTemporalUnary_1207_9_56()) return true; + return false; + } + + static private boolean jj_3R_ExpressionProb_1583_25_191() + { + if (jj_3R_LtGt_1984_9_46()) return true; + if (jj_3R_Expression_1155_9_39()) return true; + return false; + } + + static private boolean jj_3R_ExpressionProb_1582_26_190() + { + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_IdentifierExpression_1934_9_33()) return true; + if (jj_scan_token(RPARENTH)) return true; + return false; + } + + static private boolean jj_3R_ExpressionProb_1586_17_194() { if (jj_scan_token(MAX)) return true; if (jj_scan_token(EQ)) return true; @@ -5370,7 +5386,7 @@ static private boolean jj_3R_ExpressionProb_1586_17_193() return false; } - static private boolean jj_3R_ExpressionProb_1585_17_192() + static private boolean jj_3R_ExpressionProb_1585_17_193() { if (jj_scan_token(MIN)) return true; if (jj_scan_token(EQ)) return true; @@ -5378,60 +5394,60 @@ static private boolean jj_3R_ExpressionProb_1585_17_192() return false; } - static private boolean jj_3R_ExpressionProb_1584_17_191() + static private boolean jj_3R_ExpressionProb_1584_17_192() { if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_ExpressionProb_1589_10_168() + static private boolean jj_3R_EqNeq_1975_9_120() { - if (jj_scan_token(PMAX)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + if (jj_scan_token(NE)) return true; return false; } - static private boolean jj_3R_ExpressionTemporalUnary_1207_9_56() + static private boolean jj_3R_EqNeq_1974_9_116() { Token xsp; xsp = jj_scanpos; - if (jj_3R_ExpressionTemporalUnary_1209_17_61()) { + if (jj_3R_EqNeq_1974_9_119()) { jj_scanpos = xsp; - if (jj_3R_ExpressionTemporalUnary_1218_17_62()) return true; + if (jj_3R_EqNeq_1975_9_120()) return true; } return false; } - static private boolean jj_3R_ExpressionProb_1588_10_167() + static private boolean jj_3R_EqNeq_1974_9_119() { - if (jj_scan_token(PMIN)) return true; if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_EqNeq_1971_9_120() + static private boolean jj_3R_ExpressionProb_1589_10_168() { - if (jj_scan_token(NE)) return true; + if (jj_scan_token(PMAX)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_EqNeq_1970_9_116() + static private boolean jj_3R_ExpressionTemporalUnary_1207_9_56() { Token xsp; xsp = jj_scanpos; - if (jj_3R_EqNeq_1970_9_119()) { + if (jj_3R_ExpressionTemporalUnary_1209_17_61()) { jj_scanpos = xsp; - if (jj_3R_EqNeq_1971_9_120()) return true; + if (jj_3R_ExpressionTemporalUnary_1218_17_62()) return true; } return false; } - static private boolean jj_3R_EqNeq_1970_9_119() + static private boolean jj_3R_ExpressionProb_1588_10_167() { + if (jj_scan_token(PMIN)) return true; if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } @@ -5458,15 +5474,15 @@ static private boolean jj_3R_ExpressionProb_1582_10_166() if (jj_scan_token(P)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_ExpressionProb_1582_26_189()) jj_scanpos = xsp; + if (jj_3R_ExpressionProb_1582_26_190()) jj_scanpos = xsp; xsp = jj_scanpos; - if (jj_3R_ExpressionProb_1583_25_190()) { + if (jj_3R_ExpressionProb_1583_25_191()) { jj_scanpos = xsp; - if (jj_3R_ExpressionProb_1584_17_191()) { + if (jj_3R_ExpressionProb_1584_17_192()) { jj_scanpos = xsp; - if (jj_3R_ExpressionProb_1585_17_192()) { + if (jj_3R_ExpressionProb_1585_17_193()) { jj_scanpos = xsp; - if (jj_3R_ExpressionProb_1586_17_193()) return true; + if (jj_3R_ExpressionProb_1586_17_194()) return true; } } } @@ -5515,22 +5531,22 @@ static private boolean jj_3R_ExpressionTemporalBinary_1188_17_57() return false; } - static private boolean jj_3R_ExpressionFuncArgs_1506_72_188() + static private boolean jj_3R_IdentifierPrime_1956_9_49() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_Expression_1155_9_39()) return true; + if (jj_scan_token(REG_IDENTPRIME)) return true; return false; } - static private boolean jj_3R_IdentifierPrime_1952_9_49() + static private boolean jj_3R_ExpressionFuncArgs_1506_72_189() { - if (jj_scan_token(REG_IDENTPRIME)) return true; + if (jj_scan_token(COMMA)) return true; + if (jj_3R_Expression_1155_9_39()) return true; return false; } static private boolean jj_3R_ExpressionFuncOldStyle_1494_83_165() { - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; return false; } @@ -5543,7 +5559,7 @@ static private boolean jj_3R_ExpressionTemporalBinary_1185_9_47() return false; } - static private boolean jj_3R_ExpressionFilter_1898_56_185() + static private boolean jj_3R_ExpressionFilter_1902_56_186() { if (jj_scan_token(OR)) return true; return false; @@ -5552,7 +5568,7 @@ static private boolean jj_3R_ExpressionFilter_1898_56_185() static private boolean jj_3R_SystemHideRename_1105_81_91() { if (jj_scan_token(COMMA)) return true; - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; return false; } @@ -5564,9 +5580,9 @@ static private boolean jj_3R_ExpressionParenth_1556_9_147() return false; } - static private boolean jj_3R_IdentifierExpression_1930_9_33() + static private boolean jj_3R_IdentifierExpression_1934_9_33() { - if (jj_3R_Identifier_1919_9_30()) return true; + if (jj_3R_Identifier_1923_9_30()) return true; return false; } @@ -5576,43 +5592,43 @@ static private boolean jj_3R_ExpressionFuncOldStyle_1494_60_164() return false; } - static private boolean jj_3R_ExpressionLiteral_1543_9_158() + static private boolean jj_3R_ExpressionFilter_1902_34_185() { - if (jj_scan_token(FALSE)) return true; + if (jj_scan_token(AND)) return true; return false; } - static private boolean jj_3R_ExpressionLiteral_1541_9_157() + static private boolean jj_3R_ExpressionFilter_1901_35_183() { - if (jj_scan_token(TRUE)) return true; + if (jj_scan_token(MAX)) return true; return false; } - static private boolean jj_3R_ExpressionFilter_1898_34_184() + static private boolean jj_3R_ExpressionLiteral_1543_9_158() { - if (jj_scan_token(AND)) return true; + if (jj_scan_token(FALSE)) return true; return false; } - static private boolean jj_3R_ExpressionFilter_1897_35_182() + static private boolean jj_3R_ExpressionLiteral_1541_9_157() { - if (jj_scan_token(MAX)) return true; + if (jj_scan_token(TRUE)) return true; return false; } - static private boolean jj_3R_Expression_1155_9_39() + static private boolean jj_3R_Identifier_1923_9_30() { - if (jj_3R_ExpressionTemporalBinary_1185_9_47()) return true; + if (jj_scan_token(REG_IDENT)) return true; return false; } - static private boolean jj_3R_Identifier_1919_9_30() + static private boolean jj_3R_Expression_1155_9_39() { - if (jj_scan_token(REG_IDENT)) return true; + if (jj_3R_ExpressionTemporalBinary_1185_9_47()) return true; return false; } - static private boolean jj_3R_ExpressionLabel_1876_47_180() + static private boolean jj_3R_ExpressionLabel_1880_47_181() { if (jj_scan_token(INIT)) return true; return false; @@ -5624,6 +5640,13 @@ static private boolean jj_3R_ExpressionLiteral_1530_9_156() return false; } + static private boolean jj_3R_ExpressionFilter_1907_11_188() + { + if (jj_scan_token(COMMA)) return true; + if (jj_3R_Expression_1155_9_39()) return true; + return false; + } + static private boolean jj_initialized_once = false; /** Generated Token Manager. */ static public PrismParserTokenManager token_source; @@ -5636,7 +5659,7 @@ static private boolean jj_3R_ExpressionLiteral_1530_9_156() static private Token jj_scanpos, jj_lastpos; static private int jj_la; static private int jj_gen; - static final private int[] jj_la1 = new int[102]; + static final private int[] jj_la1 = new int[103]; static private int[] jj_la1_0; static private int[] jj_la1_1; static private int[] jj_la1_2; @@ -5648,16 +5671,16 @@ static private boolean jj_3R_ExpressionLiteral_1530_9_156() jj_la1_init_3(); } private static void jj_la1_init_0() { - jj_la1_0 = new int[] {0xa28804c0,0xa08804c0,0x2000000,0x60340848,0x0,0x60340848,0x60340848,0x0,0x60340848,0x400,0x80000000,0x80,0x80000480,0x10000210,0x10000210,0x0,0x40,0x0,0x2000000,0x10000030,0x0,0x4000000,0x0,0x0,0x0,0x41740808,0x0,0x0,0x0,0x41740808,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x1400000,0x0,0x41740808,0x41740808,0x41740808,0x41740808,0x41740808,0x0,0x0,0x0,0x0,0x0,0x0,0x40340808,0x0,0x0,0x0,0x0,0x0,0x0,0x40340808,0x40340808,0x0,0x40000000,0x40000000,0x0,0x40000,0x0,0x40000000,0x0,0x0,0x0,0x40000000,0x0,0x0,0x0,0x0,0x0,0x40000000,0x0,0x0,0x41740808,0x41740808,0x0,0x0,0x49740908,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x2000000,0x40000000,0x0,0x40000000,0x0,0x0,0x0,}; + jj_la1_0 = new int[] {0xa28804c0,0xa08804c0,0x2000000,0x60340848,0x0,0x60340848,0x60340848,0x0,0x60340848,0x400,0x80000000,0x80,0x80000480,0x10000210,0x10000210,0x0,0x40,0x0,0x2000000,0x10000030,0x0,0x4000000,0x0,0x0,0x0,0x41740808,0x0,0x0,0x0,0x41740808,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x1400000,0x0,0x41740808,0x41740808,0x41740808,0x41740808,0x41740808,0x0,0x0,0x0,0x0,0x0,0x0,0x40340808,0x0,0x0,0x0,0x0,0x0,0x0,0x40340808,0x40340808,0x0,0x40000000,0x40000000,0x0,0x40000,0x0,0x40000000,0x0,0x0,0x0,0x40000000,0x0,0x0,0x0,0x0,0x0,0x40000000,0x0,0x0,0x41740808,0x41740808,0x0,0x0,0x49740908,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x2000000,0x40000000,0x0,0x40000000,0x0,0x0,0x0,}; } private static void jj_la1_init_1() { - jj_la1_1 = new int[] {0x30fe3a,0x107e08,0x208032,0x24f51c1,0x0,0x24f51c1,0x24f51c1,0x0,0x24f51c1,0x800,0x8,0x100000,0x102e08,0x0,0x0,0x5000,0x5000,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x24f01c5,0x4000000,0x400000,0x0,0x24f01c5,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x1840000,0x0,0x1840000,0x4,0x0,0x24f01c5,0x24f01c5,0x24f01c5,0x24f01c5,0x24f01c5,0x0,0x0,0x10000000,0x20000000,0x8000000,0x4000000,0x24f01c1,0x0,0x0,0x0,0x0,0x0,0x0,0x4f01c1,0x4f01c1,0x0,0x1,0x1,0x0,0x400000,0x0,0x1,0x1c0,0x0,0x0,0x1,0x0,0x0,0x0,0x0,0x0,0x1,0x70000,0x0,0x24f01c5,0x24f01c5,0x0,0x80000,0x24f01c5,0x0,0x701c0,0x701c0,0x0,0x0,0x0,0x0,0x0,0xc000001,0x0,0x1,0x0,0x0,0x80000000,}; + jj_la1_1 = new int[] {0x30fe3a,0x107e08,0x208032,0x24f51c1,0x0,0x24f51c1,0x24f51c1,0x0,0x24f51c1,0x800,0x8,0x100000,0x102e08,0x0,0x0,0x5000,0x5000,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x24f01c5,0x4000000,0x400000,0x0,0x24f01c5,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x1840000,0x0,0x1840000,0x4,0x0,0x24f01c5,0x24f01c5,0x24f01c5,0x24f01c5,0x24f01c5,0x0,0x0,0x10000000,0x20000000,0x8000000,0x4000000,0x24f01c1,0x0,0x0,0x0,0x0,0x0,0x0,0x4f01c1,0x4f01c1,0x0,0x1,0x1,0x0,0x400000,0x0,0x1,0x1c0,0x0,0x0,0x1,0x0,0x0,0x0,0x0,0x0,0x1,0x70000,0x0,0x24f01c5,0x24f01c5,0x0,0x80000,0x24f01c5,0x0,0x0,0x701c0,0x701c0,0x0,0x0,0x0,0x0,0x0,0xc000001,0x0,0x1,0x0,0x0,0x80000000,}; } private static void jj_la1_init_2() { - jj_la1_2 = new int[] {0x0,0x0,0x0,0x5c108088,0x1,0x5c108088,0x5c108088,0x1,0x5c108088,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x800,0x0,0x20,0x40000000,0x0,0x20,0x40000000,0x80000,0x5c108088,0x0,0x8,0x2,0x5c1080a8,0x40000000,0x20,0x2,0x2,0x400200,0x2,0x2,0x400200,0x44000008,0x0,0x66820,0x0,0x0,0x66820,0x5c108088,0x5c108088,0x5c108088,0x5c108088,0x5c108088,0x66820,0x2000000,0x0,0x0,0x0,0x0,0x5c108088,0x1800,0x66000,0x180000,0x180000,0x600000,0x600000,0x5c108088,0x5c008088,0x8,0x0,0x40000000,0x2,0x18000000,0x8,0x66800,0x0,0x200,0x200,0x0,0x8,0x66808,0x200,0x8,0x200,0x66800,0x0,0x200,0x5c108088,0x5c108088,0x400000,0x0,0x5c108088,0x8080,0x0,0x8,0x2,0x48000000,0x200000,0x48000000,0x40000000,0x40080000,0x2,0x40000000,0x1800,0x66000,0x0,}; + jj_la1_2 = new int[] {0x0,0x0,0x0,0x5c108088,0x1,0x5c108088,0x5c108088,0x1,0x5c108088,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x800,0x0,0x20,0x40000000,0x0,0x20,0x40000000,0x80000,0x5c108088,0x0,0x8,0x2,0x5c1080a8,0x40000000,0x20,0x2,0x2,0x400200,0x2,0x2,0x400200,0x44000008,0x0,0x66820,0x0,0x0,0x66820,0x5c108088,0x5c108088,0x5c108088,0x5c108088,0x5c108088,0x66820,0x2000000,0x0,0x0,0x0,0x0,0x5c108088,0x1800,0x66000,0x180000,0x180000,0x600000,0x600000,0x5c108088,0x5c008088,0x8,0x0,0x40000000,0x2,0x18000000,0x8,0x66800,0x0,0x200,0x200,0x0,0x8,0x66808,0x200,0x8,0x200,0x66800,0x0,0x200,0x5c108088,0x5c108088,0x400000,0x0,0x5c108088,0x8080,0x200,0x0,0x8,0x2,0x48000000,0x200000,0x48000000,0x40000000,0x40080000,0x2,0x40000000,0x1800,0x66000,0x0,}; } private static void jj_la1_init_3() { - jj_la1_3 = new int[] {0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,}; + jj_la1_3 = new int[] {0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,}; } static final private JJCalls[] jj_2_rtns = new JJCalls[18]; static private boolean jj_rescan = false; @@ -5681,7 +5704,7 @@ public PrismParser(java.io.InputStream stream, String encoding) { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 102; i++) jj_la1[i] = -1; + for (int i = 0; i < 103; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5696,7 +5719,7 @@ static public void ReInit(java.io.InputStream stream, String encoding) { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 102; i++) jj_la1[i] = -1; + for (int i = 0; i < 103; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5714,7 +5737,7 @@ public PrismParser(java.io.Reader stream) { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 102; i++) jj_la1[i] = -1; + for (int i = 0; i < 103; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5733,7 +5756,7 @@ static public void ReInit(java.io.Reader stream) { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 102; i++) jj_la1[i] = -1; + for (int i = 0; i < 103; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5750,7 +5773,7 @@ public PrismParser(PrismParserTokenManager tm) { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 102; i++) jj_la1[i] = -1; + for (int i = 0; i < 103; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5760,7 +5783,7 @@ public void ReInit(PrismParserTokenManager tm) { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 102; i++) jj_la1[i] = -1; + for (int i = 0; i < 103; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5896,7 +5919,7 @@ static public ParseException generateParseException() { la1tokens[jj_kind] = true; jj_kind = -1; } - for (int i = 0; i < 102; i++) { + for (int i = 0; i < 103; i++) { if (jj_la1[i] == jj_gen) { for (int j = 0; j < 32; j++) { if ((jj_la1_0[i] & (1<> or [[...]] (( begin = { ret = new ExpressionStrategy(true); } ExpressionStrategyCoalition(ret) ) | (begin = { ret = new ExpressionStrategy(false); } ExpressionStrategyCoalition(ret) )) + // Optional modifier + ( modifier = IdentifierExpression() )? // Child expression ( ( expr = ExpressionProb(prop, pathprop) | expr = ExpressionReward(prop, pathprop) ) @@ -1830,6 +1833,7 @@ Expression ExpressionStrategy(boolean prop, boolean pathprop) : { ret.addOperand(expr); } )) { + ret.setModifier(modifier == null ? null : modifier.getName()); ret.setPosition(begin, getToken(0)); return ret; } diff --git a/prism/src/parser/ast/ExpressionStrategy.java b/prism/src/parser/ast/ExpressionStrategy.java index 152ef47756..e85264d9a5 100644 --- a/prism/src/parser/ast/ExpressionStrategy.java +++ b/prism/src/parser/ast/ExpressionStrategy.java @@ -45,6 +45,9 @@ public class ExpressionStrategy extends Expression /** Coalition info (for game models) */ protected Coalition coalition = new Coalition(); + /** Optional "modifier" to specify variants */ + protected String modifier = null; + /** Child expression(s) */ protected List operands = new ArrayList(); @@ -86,6 +89,14 @@ public void setCoalition(List coalition) this.coalition.setPlayers(coalition); } + /** + * Set the (optional) "modifier" for this operator. + */ + public void setModifier(String modifier) + { + this.modifier = modifier; + } + public void setSingleOperand(Expression expression) { operands.clear(); @@ -138,6 +149,22 @@ public boolean hasSingleOperand() return singleOperand; } + /** + * Get the (optional) "modifier" for this operator. + */ + public String getModifier() + { + return modifier; + } + + /** + * Get a string representing the modifier as a suffix for the operator. + */ + public String getModifierString() + { + return modifier == null ? "" : "{" + modifier + "}"; + } + public int getNumOperands() { return operands.size(); @@ -217,6 +244,7 @@ public String toString() s += (thereExists ? "<<" : "[["); s += coalition; s += (thereExists ? ">> " : "]] "); + s += getModifierString(); if (singleOperand) { s += operands.get(0); } else { @@ -240,6 +268,7 @@ public int hashCode() final int prime = 31; int result = 1; result = prime * result + ((coalition == null) ? 0 : coalition.hashCode()); + result = prime * result + ((modifier == null) ? 0 : modifier.hashCode()); result = prime * result + ((operands == null) ? 0 : operands.hashCode()); result = prime * result + (singleOperand ? 1231 : 1237); result = prime * result + (thereExists ? 1231 : 1237); @@ -261,6 +290,11 @@ public boolean equals(Object obj) return false; } else if (!coalition.equals(other.coalition)) return false; + if (modifier == null) { + if (other.modifier != null) + return false; + } else if (!modifier.equals(other.modifier)) + return false; if (operands == null) { if (other.operands != null) return false; diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index b91cecf4e8..064968ad13 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -210,7 +210,11 @@ protected StateValues checkExpressionStrategy(ExpressionStrategy expr, JDDNode s coalition = null; } - // Process operand(s) + // Multi-strategies not supported + if ("multi".equals(expr.getModifier())) { + throw new PrismNotSupportedException("Multi-strategy synthesis not supported by this engine"); + } + List exprs = expr.getOperands(); // Pass onto relevant method: // Single P operator