From 0d099446aae07b0b983f678147e5a1069ff26d9d Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 16 Nov 2015 15:04:38 +0000 Subject: [PATCH] Refactoring and commenting in multi-objective model checking. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10886 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/MultiObjModelChecker.java | 192 ++++++++++++---------- prism/src/prism/NondetModelChecker.java | 21 ++- 2 files changed, 118 insertions(+), 95 deletions(-) diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index 567bef99..3981904d 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/prism/src/prism/MultiObjModelChecker.java @@ -525,26 +525,36 @@ public class MultiObjModelChecker extends PrismComponent return k; } - // compute (max) probabilities for multi-objective reachability - - protected Object computeMultiReachProbs(NondetModel modelProduct, LTLModelChecker mcLtl, List rewards, JDDNode st, List targets, + /** + * Perform multi-objective model checking computation. + * Solves achievability, numerical or Pareto queries over n objectives. + * + * @param model The MDP + * @param mcLtl An LTL model checker (for finding end components) + * @param transRewards MTBDDs for transition rewards (reward objectives only) + * @param start BDD giving the (initial) state for which values are to be computed + * @param targets BDDs giving sets of target states (probability objectives only) + * @param combinations + * @param combinationIDs + * @param opsAndBounds Information about the list of objectives + * @param hasconflictobjectives + */ + protected Object computeMultiReachProbs(NondetModel model, LTLModelChecker mcLtl, List transRewards, JDDNode start, List targets, List combinations, List combinationIDs, OpsAndBoundsList opsAndBounds, boolean hasconflictobjectives) throws PrismException { JDDNode yes, no, maybe, bottomec = null; Object value; - int i, j, n; - // Local copy of setting - int engine = settings.getChoice(PrismSettings.PRISM_ENGINE); - + int i, j, numTargets; //JDDNode maybe_r = null; // maybe states for the reward formula //JDDNode trr = null; // transition rewards //int op1 = relOps.get(0).intValue(); // the operator of the first objective query - n = targets.size(); + // Get number of targets + numTargets = targets.size(); - JDDNode labels[] = new JDDNode[n]; + JDDNode labels[] = new JDDNode[numTargets]; // Build temporary DDs for combined targets - for (i = 0; i < n; i++) { + for (i = 0; i < numTargets; i++) { JDD.Ref(targets.get(i)); JDDNode tmp = targets.get(i); if (combinations != null) { @@ -560,18 +570,17 @@ public class MultiObjModelChecker extends PrismComponent // If required, export info about target states if (prism.getExportTarget()) { - JDDNode labels2[] = new JDDNode[n + 1]; - String labelNames[] = new String[n + 1]; - labels2[0] = modelProduct.getStart(); + JDDNode labels2[] = new JDDNode[numTargets + 1]; + String labelNames[] = new String[numTargets + 1]; + labels2[0] = model.getStart(); labelNames[0] = "init"; - for (i = 0; i < n; i++) { + for (i = 0; i < numTargets; i++) { labels2[i + 1] = labels[i]; labelNames[i + 1] = "target" + i; } try { mainLog.print("\nExporting target states info to file \"" + prism.getExportTargetFilename() + "\"..."); - PrismMTBDD.ExportLabels(labels2, labelNames, "l", modelProduct.getAllDDRowVars(), modelProduct.getODD(), Prism.EXPORT_PLAIN, - prism.getExportTargetFilename()); + PrismMTBDD.ExportLabels(labels2, labelNames, "l", model.getAllDDRowVars(), model.getODD(), Prism.EXPORT_PLAIN, prism.getExportTargetFilename()); } catch (FileNotFoundException e) { mainLog.println("\nWarning: Could not export target to file \"" + prism.getExportTargetFilename() + "\""); } @@ -580,7 +589,7 @@ public class MultiObjModelChecker extends PrismComponent // yes - union of targets (just to compute no) yes = JDD.Constant(0); //n = targets.size(); - for (i = 0; i < n; i++) { + for (i = 0; i < numTargets; i++) { JDD.Ref(targets.get(i)); yes = JDD.Or(yes, targets.get(i)); } @@ -591,13 +600,13 @@ public class MultiObjModelChecker extends PrismComponent } if (opsAndBounds.rewardSize() == 0) - no = PrismMTBDD.Prob0A(modelProduct.getTrans01(), modelProduct.getReach(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), modelProduct.getReach(), yes); + no = PrismMTBDD.Prob0A(model.getTrans01(), model.getReach(), model.getAllDDRowVars(), model.getAllDDColVars(), model.getAllDDNondetVars(), + model.getReach(), yes); else { no = JDD.Constant(0); - bottomec = PrismMTBDD.Prob0A(modelProduct.getTrans01(), modelProduct.getReach(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), modelProduct.getReach(), yes); - List becs = mcLtl.findBottomEndComponents(modelProduct, bottomec); + bottomec = PrismMTBDD.Prob0A(model.getTrans01(), model.getReach(), model.getAllDDRowVars(), model.getAllDDColVars(), model.getAllDDNondetVars(), + model.getReach(), yes); + List becs = mcLtl.findBottomEndComponents(model, bottomec); JDD.Deref(bottomec); bottomec = JDD.Constant(0); for (JDDNode ec : becs) @@ -614,73 +623,81 @@ public class MultiObjModelChecker extends PrismComponent }*/ // maybe - JDD.Ref(modelProduct.getReach()); + JDD.Ref(model.getReach()); JDD.Ref(yes); JDD.Ref(no); - maybe = JDD.And(modelProduct.getReach(), JDD.Not(JDD.Or(yes, no))); + maybe = JDD.And(model.getReach(), JDD.Not(JDD.Or(yes, no))); - for (i = 0; i < rewards.size(); i++) { - JDDNode tmp = rewards.remove(i); + for (i = 0; i < transRewards.size(); i++) { + JDDNode tmp = transRewards.remove(i); JDD.Ref(no); tmp = JDD.Apply(JDD.TIMES, tmp, JDD.Not(no)); - rewards.add(i, tmp); + transRewards.add(i, tmp); } // print out yes/no/maybe - mainLog.print("\nyes = " + JDD.GetNumMintermsString(yes, modelProduct.getAllDDRowVars().n())); - mainLog.print(", no = " + JDD.GetNumMintermsString(no, modelProduct.getAllDDRowVars().n())); - mainLog.print(", maybe = " + JDD.GetNumMintermsString(maybe, modelProduct.getAllDDRowVars().n()) + "\n"); + mainLog.print("\nyes = " + JDD.GetNumMintermsString(yes, model.getAllDDRowVars().n())); + mainLog.print(", no = " + JDD.GetNumMintermsString(no, model.getAllDDRowVars().n())); + mainLog.print(", maybe = " + JDD.GetNumMintermsString(maybe, model.getAllDDRowVars().n()) + "\n"); // compute probabilities mainLog.println("\nComputing remaining probabilities..."); - // switch engine, if necessary + + // Local copies of settings + int engine = settings.getChoice(PrismSettings.PRISM_ENGINE); + int method = prism.getMDPMultiSolnMethod(); + + // Switch engine, if necessary if (engine == Prism.HYBRID) { mainLog.println("Switching engine since only sparse engine currently supports this computation..."); engine = Prism.SPARSE; } mainLog.println("Engine: " + Prism.getEngineString(engine)); - int method = prism.getMDPMultiSolnMethod(); - try { - if (engine != Prism.SPARSE) + // Check for unsupported options + if (engine != Prism.SPARSE) { throw new PrismNotSupportedException("Currently only sparse engine supports multi-objective properties"); + } + if (method == Prism.MDP_MULTI_LP && opsAndBounds.numberOfNumerical() > 1) { + throw new PrismNotSupportedException("Pareto curve generation is not currently supported using linear programming"); + } + // Do computation + // Linear programming if (method == Prism.MDP_MULTI_LP) { - //LP currently does not support Pareto - if (opsAndBounds.numberOfNumerical() > 1) { - throw new PrismNotSupportedException("Linear programming method currently does not support generating of Pareto curves."); - } - if (opsAndBounds.rewardSize() > 0) { if (hasconflictobjectives) { - value = PrismSparse.NondetMultiReachReward1(modelProduct.getTrans(), modelProduct.getTransActions(), modelProduct.getSynchs(), - modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), - targets, combinations, combinationIDs, opsAndBounds, maybe, st, rewards, bottomec); + value = PrismSparse.NondetMultiReachReward1(model.getTrans(), model.getTransActions(), model.getSynchs(), model.getODD(), + model.getAllDDRowVars(), model.getAllDDColVars(), model.getAllDDNondetVars(), targets, combinations, combinationIDs, + opsAndBounds, maybe, start, transRewards, bottomec); } else { - value = PrismSparse.NondetMultiReachReward(modelProduct.getTrans(), modelProduct.getTransActions(), modelProduct.getSynchs(), - modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), - targets, opsAndBounds, maybe, st, rewards, bottomec); + value = PrismSparse.NondetMultiReachReward(model.getTrans(), model.getTransActions(), model.getSynchs(), model.getODD(), + model.getAllDDRowVars(), model.getAllDDColVars(), model.getAllDDNondetVars(), targets, opsAndBounds, maybe, start, transRewards, + bottomec); } } else { if (hasconflictobjectives) { - value = PrismSparse.NondetMultiReach1(modelProduct.getTrans(), modelProduct.getTransActions(), modelProduct.getSynchs(), - modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), - targets, combinations, combinationIDs, opsAndBounds, maybe, st); + value = PrismSparse.NondetMultiReach1(model.getTrans(), model.getTransActions(), model.getSynchs(), model.getODD(), + model.getAllDDRowVars(), model.getAllDDColVars(), model.getAllDDNondetVars(), targets, combinations, combinationIDs, + opsAndBounds, maybe, start); } else { - value = PrismSparse.NondetMultiReach(modelProduct.getTrans(), modelProduct.getTransActions(), modelProduct.getSynchs(), - modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), - targets, opsAndBounds, maybe, st); + value = PrismSparse.NondetMultiReach(model.getTrans(), model.getTransActions(), model.getSynchs(), model.getODD(), + model.getAllDDRowVars(), model.getAllDDColVars(), model.getAllDDNondetVars(), targets, opsAndBounds, maybe, start); } } - } else if (method == Prism.MDP_MULTI_GAUSSSEIDEL || method == Prism.MDP_MULTI_VALITER) { + } + // Value iteration + else if (method == Prism.MDP_MULTI_GAUSSSEIDEL || method == Prism.MDP_MULTI_VALITER) { double timePre = System.currentTimeMillis(); - value = weightedMultiReachProbs(modelProduct, yes, maybe, st, labels, rewards, opsAndBounds); + value = weightedMultiReachProbs(model, yes, maybe, start, labels, transRewards, opsAndBounds); double timePost = System.currentTimeMillis(); double time = ((double) (timePost - timePre)) / 1000.0; mainLog.println("Multi-objective value iterations took " + time + " s."); - } else { - throw new PrismException("Don't know how to model-check using the method: " + method); + } + // Unknown method (shouldn't happen) + else { + throw new PrismException("Unknown multi-objective model checking method"); } } catch (PrismException e) { throw e; @@ -693,29 +710,32 @@ public class MultiObjModelChecker extends PrismComponent JDD.Deref(maybe); for (int k = 0; k < labels.length; k++) JDD.Deref(labels[k]); - for (i = 0; i < rewards.size(); i++) { - JDD.Deref(rewards.get(i)); + for (i = 0; i < transRewards.size(); i++) { + JDD.Deref(transRewards.get(i)); } } return value; } - protected Object weightedMultiReachProbs(NondetModel modelProduct, JDDNode yes_ones, JDDNode maybe, JDDNode st, JDDNode[] targets, List rewards, + protected Object weightedMultiReachProbs(NondetModel modelProduct, JDDNode yes_ones, JDDNode maybe, JDDNode start, JDDNode[] targets, List rewards, OpsAndBoundsList opsAndBounds) throws PrismException { - int numberOfMaximizing = opsAndBounds.numberOfNumerical(); - - if (numberOfMaximizing > 2) - throw new PrismException("Number of maximizing objectives must be at most 2"); + int numNumericalObjectives = opsAndBounds.numberOfNumerical(); - if (numberOfMaximizing >= 2 && opsAndBounds.probSize() + opsAndBounds.rewardSize() > numberOfMaximizing) - throw new PrismException("Number of maximizing objectives can be 2 or 3 only if there are no other (i.e. bounded) objectives present"); + // Check for unsupported computations + if (numNumericalObjectives > 2) { + throw new PrismException("Pareto curve generation is currently only supported for 2 objectives"); + } + if (numNumericalObjectives >= 2 && opsAndBounds.probSize() + opsAndBounds.rewardSize() > numNumericalObjectives) { + throw new PrismException("Pareto curve generation is currently not allowed if there are other (bounded) objectives"); + } - if (numberOfMaximizing >= 2) { - return generateParetoCurve(modelProduct, yes_ones, maybe, st, targets, rewards, opsAndBounds); + // Pareto computation or achievability/numerical computation + if (numNumericalObjectives >= 2) { + return generateParetoCurve(modelProduct, yes_ones, maybe, start, targets, rewards, opsAndBounds); } else { - return targetDrivenMultiReachProbs(modelProduct, yes_ones, maybe, st, targets, rewards, opsAndBounds); + return targetDrivenMultiReachProbs(modelProduct, yes_ones, maybe, start, targets, rewards, opsAndBounds); } } @@ -735,12 +755,12 @@ public class MultiObjModelChecker extends PrismComponent boolean min = false; // Determine whether we are using Gauss-Seidel value iteration - boolean useGS = (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL); + boolean useGS = (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL); if (opsAndBounds.numberOfStepBounded() > 0) { mainLog.println("Not using Guass-Seidel since there are step-bounded objectives"); useGS = false; } - + //convert minimizing rewards to maximizing for (int i = 0; i < opsAndBounds.rewardSize(); i++) { if (opsAndBounds.getRewardOperator(i) == Operator.R_LE) { @@ -762,7 +782,7 @@ public class MultiObjModelChecker extends PrismComponent int maxIters = settings.getInteger(PrismSettings.PRISM_MULTI_MAX_POINTS); int exportAdvSetting = settings.getChoice(PrismSettings.PRISM_EXPORT_ADV); - + NativeIntArray adversary = new NativeIntArray((int) modelProduct.getNumStates()); int dimProb = targets.length; int dimReward = rewards.size(); @@ -795,7 +815,7 @@ public class MultiObjModelChecker extends PrismComponent NDSparseMatrix.AddActionsToNDSparseMatrix(a, modelProduct.getTransActions(), modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), trans_matrix); } - + //create double vectors for probabilistic objectives for (int i = 0; i < dimProb; i++) { probDoubleVectors[i] = new DoubleVector(targets[i], modelProduct.getAllDDRowVars(), modelProduct.getODD()); @@ -812,7 +832,7 @@ public class MultiObjModelChecker extends PrismComponent // Disable adversary generation (if it was switched on) for these initial computations PrismNative.setExportAdv(Prism.EXPORT_ADV_NONE); - + for (int i = 0; i < dimProb; i++) { mainLog.println("Computing maximum values for probability objective " + (i + 1) + "/" + dimProb); double[] result; @@ -824,8 +844,8 @@ public class MultiObjModelChecker extends PrismComponent modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, rewSparseMatrices, weights); } else { result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), probDoubleVectors, probStepBounds, rewSparseMatrices, weights, - rewardStepBounds); + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), probDoubleVectors, probStepBounds, + rewSparseMatrices, weights, rewardStepBounds); } //The following is thrown because in this case the i-th dimension is @@ -852,8 +872,8 @@ public class MultiObjModelChecker extends PrismComponent modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, rewSparseMatrices, weights); } else { result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), probDoubleVectors, probStepBounds, rewSparseMatrices, weights, - rewardStepBounds); + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), probDoubleVectors, probStepBounds, + rewSparseMatrices, weights, rewardStepBounds); } numberOfPoints++; @@ -868,7 +888,7 @@ public class MultiObjModelChecker extends PrismComponent // Reinstate temporarily-disabled adversary generation setting PrismNative.setExportAdv(exportAdvSetting); - + if (verbose) mainLog.println("Points for initial tile: " + pointsForInitialTile); @@ -897,15 +917,15 @@ public class MultiObjModelChecker extends PrismComponent if (settings.getChoice(PrismSettings.PRISM_EXPORT_ADV) != Prism.EXPORT_ADV_NONE) { PrismNative.setExportAdvFilename(PrismUtils.addCounterSuffixToFilename(advFileName, iters)); } - + double[] result; if (useGS) { result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, rewSparseMatrices, weights); } else { result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), probDoubleVectors, probStepBounds, rewSparseMatrices, weights, - rewardStepBounds); + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), probDoubleVectors, probStepBounds, + rewSparseMatrices, weights, rewardStepBounds); } /* //Minimizing operators are negated, and for Pareto we need to maximize. @@ -985,12 +1005,12 @@ public class MultiObjModelChecker extends PrismComponent boolean min = false; // Determine whether we are using Gauss-Seidel value iteration - boolean useGS = (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL); + boolean useGS = (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL); if (opsAndBounds.numberOfStepBounded() > 0) { mainLog.println("Not using Guass-Seidel since there are step-bounded objectives"); useGS = false; } - + //convert minimizing rewards to maximizing for (int i = 0; i < opsAndBounds.rewardSize(); i++) { if (opsAndBounds.getRewardOperator(i) == Operator.R_LE) { @@ -1082,8 +1102,8 @@ public class MultiObjModelChecker extends PrismComponent } else { //System.out.println("Not doing GS"); result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), null, null, new NDSparseMatrix[] { rewSparseMatrices[0] }, - new double[] { 1.0 }, new int[] { rewardStepBounds[0] }); + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), null, null, + new NDSparseMatrix[] { rewSparseMatrices[0] }, new double[] { 1.0 }, new int[] { rewardStepBounds[0] }); } numberOfPoints++; @@ -1119,8 +1139,8 @@ public class MultiObjModelChecker extends PrismComponent modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, rewSparseMatrices, weights); } else { result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), probDoubleVectors, probStepBounds, rewSparseMatrices, weights, - rewardStepBounds); + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), probDoubleVectors, probStepBounds, + rewSparseMatrices, weights, rewardStepBounds); } numberOfPoints++; diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index d31109e6..a47ef344 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -479,8 +479,7 @@ public class NondetModelChecker extends NonProbModelChecker // Check format and extract bounds/etc. int numObjectives = exprs.size(); OpsAndBoundsList opsAndBounds = new OpsAndBoundsList(); - List rewards = new ArrayList(numObjectives); - List transRewardsList = new ArrayList(numObjectives); + List transRewardsList = new ArrayList(); List pathFormulas = new ArrayList(numObjectives); for (int i = 0; i < numObjectives; i++) { extractInfoFromMultiObjectiveOperand((ExpressionQuant) exprs.get(i), opsAndBounds, transRewardsList, pathFormulas); @@ -534,13 +533,15 @@ public class NondetModelChecker extends NonProbModelChecker // Replace min by max and <= by >= opsAndBounds.makeAllProbUp(); - //print some info + // Print some info outputProductMulti(modelProduct); - for (JDDNode rindex : transRewardsList) { - JDD.Ref(rindex); + // Construct rewards for product model + List transRewardsListProduct = new ArrayList(); + for (JDDNode transRewards : transRewardsList) { + JDD.Ref(transRewards); JDD.Ref(modelProduct.getTrans01()); - rewards.add(JDD.Apply(JDD.TIMES, rindex, modelProduct.getTrans01())); + transRewardsListProduct.add(JDD.Apply(JDD.TIMES, transRewards, modelProduct.getTrans01())); } // Removing actions with non-zero reward from the product for maximum cases @@ -592,7 +593,7 @@ public class NondetModelChecker extends NonProbModelChecker List allecs = mcMo.computeAllEcs(modelProduct, mcLtl, allstatesH, allstatesL, acceptanceVector_H, acceptanceVector_L, draDDRowVars, draDDColVars, opsAndBounds, numObjectives); - // Create array to store target DDs + // Create array to store BDDs for targets (i.e. accepting EC states); probability objectives only List targetDDs = new ArrayList(numObjectives); for (int i = 0; i < numObjectives; i++) { if (opsAndBounds.isProbabilityObjective(i)) { @@ -600,6 +601,7 @@ public class NondetModelChecker extends NonProbModelChecker targetDDs.add(mcMo.computeAcceptingEndComponent(dra[i], modelProduct, draDDRowVars[i], draDDColVars[i], allecs, allstatesH.get(i), allstatesL.get(i), mcLtl, conflictformulae > 1)); } else { + // (not used currently) // Fixme: maybe not efficient if (pathFormulas.get(i) != null) { JDDNode dd = checkExpressionDD(pathFormulas.get(i)); @@ -641,7 +643,8 @@ public class NondetModelChecker extends NonProbModelChecker modelProduct.trans01 = tmptrans01; } - Object value = mcMo.computeMultiReachProbs(modelProduct, mcLtl, rewards, modelProduct.getStart(), targetDDs, multitargetDDs, multitargetIDs, opsAndBounds, + // Do multi-objective computation + Object value = mcMo.computeMultiReachProbs(modelProduct, mcLtl, transRewardsListProduct, modelProduct.getStart(), targetDDs, multitargetDDs, multitargetIDs, opsAndBounds, conflictformulae > 1); // Deref, clean up @@ -697,7 +700,7 @@ public class NondetModelChecker extends NonProbModelChecker * * @param exprQuant The operator for the objective * @param opsAndBounds Where to add info about ops/bounds - * @param transRewardsList Where to add the transition rewards + * @param transRewardsList Where to add the transition rewards (R operators only) * @param pathFormulas Where to store the path formulas (for P operators; null for R operators) */ protected void extractInfoFromMultiObjectiveOperand(ExpressionQuant exprQuant, OpsAndBoundsList opsAndBounds, List transRewardsList,