From ec285b66b14f222d2914020e2aecc36ac8592629 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 21 Oct 2015 23:36:08 +0000 Subject: [PATCH] Some tidying in multi-objective code (auto format). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10809 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/MultiObjModelChecker.java | 193 +++++++++++----------- 1 file changed, 96 insertions(+), 97 deletions(-) diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index cd2c2152..4d67768d 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/prism/src/prism/MultiObjModelChecker.java @@ -54,9 +54,9 @@ import jdd.JDDVars; */ public class MultiObjModelChecker extends PrismComponent { - protected Prism prism; + protected Prism prism; protected boolean verbose; - + /** * Create a new MultiObjModelChecker, inherit basic state from parent (unless null). */ @@ -68,8 +68,9 @@ public class MultiObjModelChecker extends PrismComponent } //TODO: dra's element is changed here, not neat. - protected NondetModel constructDRAandProductMulti(NondetModel model, LTLModelChecker mcLtl, ModelChecker modelChecker, Expression ltl, int i, DA dra[], Operator operator, - Expression targetExpr, JDDVars draDDRowVars, JDDVars draDDColVars, JDDNode ddStateIndex) throws PrismException + protected NondetModel constructDRAandProductMulti(NondetModel model, LTLModelChecker mcLtl, ModelChecker modelChecker, Expression ltl, int i, + DA dra[], Operator operator, Expression targetExpr, JDDVars draDDRowVars, JDDVars draDDColVars, JDDNode ddStateIndex) + throws PrismException { // TODO (JK): Adapt to support simple path formulas with bounds via DRA construction @@ -87,7 +88,7 @@ public class MultiObjModelChecker extends PrismComponent long l = System.currentTimeMillis(); LTL2DA ltl2da = new LTL2DA(this); dra[i] = ltl2da.convertLTLFormulaToDRA(ltl, modelChecker.getConstantValues()); - mainLog.print("DRA has " + dra[i].size() + " states, " + ", " + dra[i].getAcceptance().getSizeStatistics()+"."); + mainLog.print("DRA has " + dra[i].size() + " states, " + ", " + dra[i].getAcceptance().getSizeStatistics() + "."); l = System.currentTimeMillis() - l; mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds."); // If required, export DRA @@ -169,7 +170,7 @@ public class MultiObjModelChecker extends PrismComponent //computes accepting end component for the Rabin automaton dra. //Vojta: in addition to calling a method which does the computation //there are some other bits which I don't currently understand - protected JDDNode computeAcceptingEndComponent(DA dra, NondetModel modelProduct, JDDVars draDDRowVars, JDDVars draDDColVars, + protected JDDNode computeAcceptingEndComponent(DA dra, NondetModel modelProduct, JDDVars draDDRowVars, JDDVars draDDColVars, List allecs, List statesH, List statesL, //Vojta: at the time of writing this I have no idea what these two parameters do, so I don't know how to call them LTLModelChecker mcLtl, boolean conflictformulaeGtOne, String name) throws PrismException { @@ -190,7 +191,7 @@ public class MultiObjModelChecker extends PrismComponent } protected void removeNonZeroMecsForMax(NondetModel modelProduct, LTLModelChecker mcLtl, List rewardsIndex, OpsAndBoundsList opsAndBounds, - int numTargets, DA dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[]) throws PrismException + int numTargets, DA dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[]) throws PrismException { List mecs = mcLtl.findMECStates(modelProduct, modelProduct.getReach()); JDDNode removedActions = JDD.Constant(0); @@ -234,7 +235,7 @@ public class MultiObjModelChecker extends PrismComponent Vector tmptargetDDs = new Vector(); List tmpmultitargetDDs = new ArrayList(); List tmpmultitargetIDs = new ArrayList(); - ArrayList> tmpdra = new ArrayList>(); + ArrayList> tmpdra = new ArrayList>(); ArrayList tmpdraDDRowVars = new ArrayList(); ArrayList tmpdraDDColVars = new ArrayList(); int count = 0; @@ -248,7 +249,7 @@ public class MultiObjModelChecker extends PrismComponent } if (count > 0) { // TODO: distinguish whether rtarget is empty - DA newdra[] = new DA[count]; + DA newdra[] = new DA[count]; tmpdra.toArray(newdra); JDDVars newdraDDRowVars[] = new JDDVars[count]; tmpdraDDRowVars.toArray(newdraDDRowVars); @@ -262,7 +263,8 @@ public class MultiObjModelChecker extends PrismComponent for (int i = 0; i < opsAndBounds.probSize(); i++) { if (opsAndBounds.getProbOperator(i) != Operator.P_MAX) { - tmpOpsAndBounds.add(opsAndBounds.getOpRelOpBound(i), opsAndBounds.getProbOperator(i), opsAndBounds.getProbBound(i), opsAndBounds.getProbStepBound(i)); + tmpOpsAndBounds.add(opsAndBounds.getOpRelOpBound(i), opsAndBounds.getProbOperator(i), opsAndBounds.getProbBound(i), + opsAndBounds.getProbStepBound(i)); } } tmpOpsAndBounds.add(new OpRelOpBound("R", RelOp.MAX, -1.0), Operator.R_MAX, -1.0, -1); @@ -302,11 +304,11 @@ public class MultiObjModelChecker extends PrismComponent //TODO is conflictformulae actually just no of prob? protected void checkConflictsInObjectives(NondetModel modelProduct, LTLModelChecker mcLtl, int conflictformulae, int numTargets, - OpsAndBoundsList opsAndBounds, DA dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[], List targetDDs, + OpsAndBoundsList opsAndBounds, DA dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[], List targetDDs, List> allstatesH, List> allstatesL, List multitargetDDs, List multitargetIDs) throws PrismException { - DA[] tmpdra = new DA[conflictformulae]; + DA[] tmpdra = new DA[conflictformulae]; JDDVars[] tmpdraDDRowVars = new JDDVars[conflictformulae]; JDDVars[] tmpdraDDColVars = new JDDVars[conflictformulae]; List tmptargetDDs = new ArrayList(conflictformulae); @@ -354,9 +356,9 @@ public class MultiObjModelChecker extends PrismComponent } } - protected void findTargetStates(NondetModel modelProduct, LTLModelChecker mcLtl, int numTargets, int conflictformulae, boolean reachExpr[], DA dra[], - JDDVars draDDRowVars[], JDDVars draDDColVars[], List targetDDs, List multitargetDDs, List multitargetIDs) - throws PrismException + protected void findTargetStates(NondetModel modelProduct, LTLModelChecker mcLtl, int numTargets, int conflictformulae, boolean reachExpr[], + DA dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[], List targetDDs, List multitargetDDs, + List multitargetIDs) throws PrismException { int i, j; long l; @@ -459,7 +461,7 @@ public class MultiObjModelChecker extends PrismComponent // check if there are conflicts in objectives if (conflictformulae > 1) { - DA[] tmpdra = new DA[conflictformulae]; + DA[] tmpdra = new DA[conflictformulae]; JDDVars[] tmpdraDDRowVars = new JDDVars[conflictformulae]; JDDVars[] tmpdraDDColVars = new JDDVars[conflictformulae]; List tmptargetDDs = new ArrayList(conflictformulae); @@ -638,19 +640,19 @@ public class MultiObjModelChecker extends PrismComponent engine = Prism.SPARSE; } mainLog.println("Engine: " + Prism.getEngineString(engine)); - + int method = prism.getMDPMultiSolnMethod(); - + try { if (engine != Prism.SPARSE) throw new PrismNotSupportedException("Currently only sparse engine supports multi-objective properties"); - + 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(), @@ -679,8 +681,7 @@ public class MultiObjModelChecker extends PrismComponent 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); + throw new PrismException("Don't know how to model-check using the method: " + method); } } catch (PrismException e) { throw e; @@ -697,12 +698,12 @@ public class MultiObjModelChecker extends PrismComponent JDD.Deref(rewards.get(i)); } } - + return value; } - protected Object weightedMultiReachProbs(NondetModel modelProduct, JDDNode yes_ones, JDDNode maybe, JDDNode st, JDDNode[] targets, List rewards, OpsAndBoundsList opsAndBounds) - throws PrismException + protected Object weightedMultiReachProbs(NondetModel modelProduct, JDDNode yes_ones, JDDNode maybe, JDDNode st, JDDNode[] targets, List rewards, + OpsAndBoundsList opsAndBounds) throws PrismException { int numberOfMaximizing = opsAndBounds.numberOfNumerical(); @@ -710,14 +711,14 @@ public class MultiObjModelChecker extends PrismComponent throw new PrismException("Number of maximizing objectives must be at most 2"); 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"); - + throw new PrismException("Number of maximizing objectives can be 2 or 3 only if there are no other (i.e. bounded) objectives present"); + if (numberOfMaximizing >= 2) { return generateParetoCurve(modelProduct, yes_ones, maybe, st, targets, rewards, opsAndBounds); } else return targetDrivenMultiReachProbs(modelProduct, yes_ones, maybe, st, targets, rewards, opsAndBounds); } - + protected TileList generateParetoCurve(NondetModel modelProduct, JDDNode yes_ones, JDDNode maybe, final JDDNode st, JDDNode[] targets, List rewards, OpsAndBoundsList opsAndBounds) throws PrismException { @@ -725,12 +726,11 @@ public class MultiObjModelChecker extends PrismComponent int rewardStepBounds[] = new int[rewards.size()]; for (int i = 0; i < rewardStepBounds.length; i++) rewardStepBounds[i] = opsAndBounds.getRewardStepBound(i); - + int probStepBounds[] = new int[targets.length]; for (int i = 0; i < probStepBounds.length; i++) probStepBounds[i] = opsAndBounds.getProbStepBound(i); - - + double timer = System.currentTimeMillis(); boolean min = false; @@ -742,7 +742,7 @@ public class MultiObjModelChecker extends PrismComponent rewards.set(i, negated); //boundsRewards.set(i, -1 * boundsRewards.get(i)); } - + if (opsAndBounds.getRewardOperator(i) == Operator.R_MIN) { JDDNode negated = JDD.Apply(JDD.TIMES, JDD.Constant(-1), rewards.get(i)); //JDD.Ref(negated); @@ -750,7 +750,7 @@ public class MultiObjModelChecker extends PrismComponent //boundsRewards.set(i, -1 * boundsRewards.get(i)); } } - + double tolerance = settings.getDouble(PrismSettings.PRISM_PARETO_EPSILON); int maxIters = settings.getInteger(PrismSettings.PRISM_MULTI_MAX_POINTS); @@ -797,7 +797,7 @@ public class MultiObjModelChecker extends PrismComponent for (int i = 0; i < dimProb; i++) { double[] result; - + double[] weights = new double[dimProb + dimReward]; weights[i] = 1.0; /*if (prism.getMDPMultiSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) { @@ -812,15 +812,15 @@ public class MultiObjModelChecker extends PrismComponent new double[] { 1.0 }, null); }*/ if (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL) { - result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), - modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary, - trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds); + result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, + rewardStepBounds); } else { - result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), - modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary, - trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds); + result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, + rewardStepBounds); } - + //The following is thrown because in this case the i-th dimension is //zero and we might have problems when getting an separating hyperplane. /*if (result[0] == 0) @@ -851,36 +851,36 @@ public class MultiObjModelChecker extends PrismComponent new double[] { 1.0 }, new int[] { rewardStepBounds[i] }); }*/ if (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL) { - result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), - modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary, - trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds); + result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, + rewardStepBounds); } else { - result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), - modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary, - trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds); + result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, + rewardStepBounds); } - + numberOfPoints++; targetPoint = new Point(result); pointsForInitialTile.add(targetPoint); - + if (verbose) { mainLog.println("Upper bound is " + Arrays.toString(result)); } } - + if (verbose) mainLog.println("Points for initial tile: " + pointsForInitialTile); - + Tile initialTile = new Tile(pointsForInitialTile); TileList tileList = new TileList(initialTile, opsAndBounds, tolerance); - + Point direction = tileList.getCandidateHyperplane(); - + if (verbose) { mainLog.println("The initial direction is " + direction); } - + boolean decided = false; int iters = 0; while (iters < maxIters) { @@ -894,24 +894,24 @@ public class MultiObjModelChecker extends PrismComponent double[] result; if (prism.getMDPSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) { - result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), - modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary, - trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds); + result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, + rewardStepBounds); } else { - result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), - modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary, - trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds); + result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, + rewardStepBounds); } - - /* //Minimizing operators are negated, and for Pareto we need to maximize. - for (int i = 0; i < dimProb; i++) { - if (opsAndBounds.getOperator(i) == Operator.P_MIN) { - result[i] = -(1-result[i]); - } - } */ - + + /* //Minimizing operators are negated, and for Pareto we need to maximize. + for (int i = 0; i < dimProb; i++) { + if (opsAndBounds.getOperator(i) == Operator.P_MIN) { + result[i] = -(1-result[i]); + } + } */ + numberOfPoints++; - + //collect the numbers obtained from methods executed above. Point newPoint = new Point(result); @@ -931,7 +931,7 @@ public class MultiObjModelChecker extends PrismComponent if (verbose) { mainLog.println("New direction is " + direction); //mainLog.println("TileList: " + tileList); - + } if (direction == null) { @@ -950,18 +950,18 @@ public class MultiObjModelChecker extends PrismComponent + " target point iterations, try increasing this number using the -multimaxpoints switch."); else { String paretoFile = settings.getString(PrismSettings.PRISM_EXPORT_PARETO_FILENAME); - + //export to file if required if (paretoFile != null && !paretoFile.equals("")) { MultiObjUtils.exportPareto(tileList, paretoFile); mainLog.println("Exported Pareto curve. To see it, run\n etc/scripts/prism-pareto.py " + paretoFile); } - + mainLog.println("Computed " + tileList.getNumberOfDifferentPoints() + " points altogether:\n"); - mainLog.println(tileList.getPoints().toString()); - + mainLog.println(tileList.getPoints().toString()); + return tileList; - } + } } protected double targetDrivenMultiReachProbs(NondetModel modelProduct, JDDNode yes_ones, JDDNode maybe, final JDDNode st, JDDNode[] targets, @@ -971,12 +971,11 @@ public class MultiObjModelChecker extends PrismComponent int rewardStepBounds[] = new int[rewards.size()]; for (int i = 0; i < rewardStepBounds.length; i++) rewardStepBounds[i] = opsAndBounds.getRewardStepBound(i); - + int probStepBounds[] = new int[targets.length]; for (int i = 0; i < probStepBounds.length; i++) probStepBounds[i] = opsAndBounds.getProbStepBound(i); - - + double timer = System.currentTimeMillis(); boolean min = false; @@ -988,7 +987,7 @@ public class MultiObjModelChecker extends PrismComponent rewards.set(i, negated); //boundsRewards.set(i, -1 * boundsRewards.get(i)); } - + if (opsAndBounds.getRewardOperator(i) == Operator.R_MIN) { JDDNode negated = JDD.Apply(JDD.TIMES, JDD.Constant(-1), rewards.get(i)); //JDD.Ref(negated); @@ -996,10 +995,11 @@ public class MultiObjModelChecker extends PrismComponent //boundsRewards.set(i, -1 * boundsRewards.get(i)); } } - + boolean maximizingProb = (opsAndBounds.probSize() > 0 && (opsAndBounds.getProbOperator(0) == Operator.P_MAX || opsAndBounds.getProbOperator(0) == Operator.P_MIN)); boolean maximizingReward = (opsAndBounds.rewardSize() > 0 && (opsAndBounds.getRewardOperator(0) == Operator.R_MAX || opsAndBounds.getRewardOperator(0) == Operator.R_MIN)); - boolean maximizingNegated = (maximizingProb && opsAndBounds.getProbOperator(0) == Operator.P_MIN) || (maximizingReward && opsAndBounds.getRewardOperator(0) == Operator.R_MIN); + boolean maximizingNegated = (maximizingProb && opsAndBounds.getProbOperator(0) == Operator.P_MIN) + || (maximizingReward && opsAndBounds.getRewardOperator(0) == Operator.R_MIN); int maxIters = settings.getInteger(PrismSettings.PRISM_MULTI_MAX_POINTS); @@ -1064,17 +1064,17 @@ public class MultiObjModelChecker extends PrismComponent double[] result; if (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL) { //System.out.println("Doing GS"); - result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, null, null, new NDSparseMatrix[] { rewSparseMatrices[0] }, - new double[] { 1.0 }, new int[] { rewardStepBounds[0] }); + result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, null, null, new NDSparseMatrix[] { rewSparseMatrices[0] }, + new double[] { 1.0 }, new int[] { rewardStepBounds[0] }); } else { //System.out.println("Not doing GS"); - result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, null, null, new NDSparseMatrix[] { rewSparseMatrices[0] }, - new double[] { 1.0 }, new int[] { rewardStepBounds[0] }); + result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, null, null, new NDSparseMatrix[] { rewSparseMatrices[0] }, + new double[] { 1.0 }, new int[] { rewardStepBounds[0] }); } numberOfPoints++; - + targetPoint.setCoord(dimProb, result[0]); if (verbose) { @@ -1083,7 +1083,7 @@ public class MultiObjModelChecker extends PrismComponent } Point direction = MultiObjUtils.getWeights(targetPoint, computedPoints); - + if (verbose) { mainLog.println("The initial target point is " + targetPoint); mainLog.println("The initial direction is " + direction); @@ -1103,16 +1103,16 @@ public class MultiObjModelChecker extends PrismComponent double[] result; if (prism.getMDPSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) { - result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), - modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary, - trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds); + result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, + rewardStepBounds); } else { - result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), - modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary, - trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds); + result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, + rewardStepBounds); } numberOfPoints++; - + //collect the numbers obtained from methods executed above. Point newPoint = new Point(result); @@ -1123,7 +1123,6 @@ public class MultiObjModelChecker extends PrismComponent computedPoints.add(newPoint); computedDirections.add(direction); - //if (prism.getExportMultiGraphs()) // MultiObjUtils.printGraphFileDebug(targetPoint, computedPoints, computedDirections, prism.getExportMultiGraphsDir(), output++);