diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java new file mode 100644 index 00000000..d8083e26 --- /dev/null +++ b/prism/src/prism/MultiObjModelChecker.java @@ -0,0 +1,1196 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Birmingham/Oxford) +// * Vojtech Forejt (University of Oxford) +// * Hongyang Qu (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package prism; + +import java.io.FileNotFoundException; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.BitSet; +import java.util.List; +import java.util.Vector; + +import parser.ast.Expression; + +import dv.DoubleVector; + +import mtbdd.PrismMTBDD; +import sparse.NDSparseMatrix; +import sparse.PrismSparse; + +import jdd.JDD; +import jdd.JDDNode; +import jdd.JDDVars; + +/** + * Multi-objective model checking functionality + */ +public class MultiObjModelChecker extends PrismComponent +{ + protected Prism prism; + protected boolean verbose; + + /** + * Create a new MultiObjModelChecker, inherit basic state from parent (unless null). + */ + public MultiObjModelChecker(PrismComponent parent, Prism prism) throws PrismException + { + super(parent); + this.prism = prism; + this.verbose = prism.getVerbose(); + } + + //TODO: dra's element is changed here, not neat. + protected NondetModel constructDRAandProductMulti(NondetModel model, LTLModelChecker mcLtl, ModelChecker modelChecker, Expression ltl, int i, DRA dra[], Operator operator, + Expression targetExpr, JDDVars draDDRowVars, JDDVars draDDColVars, JDDNode ddStateIndex) throws PrismException + { + // Model check maximal state formulas + Vector labelDDs = new Vector(); + ltl = mcLtl.checkMaximalStateFormulas(modelChecker, model, targetExpr.deepCopy(), labelDDs); + + // Convert LTL formula to deterministic Rabin automaton (DRA) + // For min probabilities, need to negate the formula + // (add parentheses to allow re-parsing if required) + if (Operator.isMinOrLe(operator)) + ltl = Expression.Not(Expression.Parenth(ltl)); + mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); + long l = System.currentTimeMillis(); + dra[i] = LTLModelChecker.convertLTLFormulaToDRA(ltl); + mainLog.print("DRA has " + dra[i].size() + " states, " + ", " + dra[i].getNumAcceptancePairs() + " pairs."); + l = System.currentTimeMillis() - l; + mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds."); + // If required, export DRA + if (prism.getSettings().getExportPropAut()) { + String exportPropAutFilename = PrismUtils.addCounterSuffixToFilename(prism.getSettings().getExportPropAutFilename(), i); + mainLog.println("Exporting DRA to file \"" + exportPropAutFilename + "\"..."); + PrismLog out = new PrismFileLog(exportPropAutFilename); + out.println(dra); + out.close(); + //dra.printDot(new java.io.PrintStream("dra.dot")); + } + + // Build product of MDP and automaton + mainLog.println("\nConstructing MDP-DRA product..."); + + NondetModel modelNew = mcLtl.constructProductMDP(dra[i], model, labelDDs, draDDRowVars, draDDColVars, false, i == 0 ? ddStateIndex : model.getStart()); + + modelNew.printTransInfo(mainLog, prism.getExtraDDInfo()); + // Deref label BDDs + for (int j = 0; j < labelDDs.size(); j++) { + JDD.Deref(labelDDs.get(j)); + } + return modelNew; + } + + /** + * + * @param modelProduct + * @param rewardsIndex + * @param relOpsReward + * @return True if some transitions were removed + */ + protected boolean removeNonZeroRewardTrans(NondetModel modelProduct, List rewardsIndex, OpsAndBoundsList opsAndBounds) + { + boolean transchanged = false; + for (int i = 0; i < rewardsIndex.size(); i++) + if (opsAndBounds.getRewardOperator(i) == Operator.R_MIN || opsAndBounds.getRewardOperator(i) == Operator.R_LE) { + // Get non-zero reward actions + JDD.Ref(rewardsIndex.get(i)); + JDDNode actions = JDD.GreaterThan(rewardsIndex.get(i), 0.0); + if (!actions.equals(JDD.ZERO)) { + //mainLog.println("Removing non-zero reward actions in reward #" + i); + JDD.Ref(actions); + if (!transchanged) + JDD.Ref(modelProduct.getTrans()); + JDDNode tmp = JDD.ITE(actions, JDD.Constant(0), modelProduct.getTrans()); + modelProduct.trans = tmp; + if (!transchanged) + JDD.Ref(modelProduct.getTrans01()); + tmp = JDD.ITE(actions, JDD.Constant(0), modelProduct.getTrans01()); + modelProduct.trans01 = tmp; + transchanged = true; + } + } + return transchanged; + } + + protected List computeAllEcs(NondetModel modelProduct, LTLModelChecker mcLtl, ArrayList> allstatesH, + ArrayList> allstatesL, JDDNode acceptanceVector_H, JDDNode acceptanceVector_L, JDDVars draDDRowVars[], JDDVars draDDColVars[], + OpsAndBoundsList opsAndBounds, int numTargets) throws PrismException + { + //use acceptanceVector_H and acceptanceVector_L to speed up scc computation + JDD.Ref(acceptanceVector_H); + JDD.Ref(modelProduct.getTrans01()); + JDDNode candidateStates = JDD.Apply(JDD.TIMES, modelProduct.getTrans01(), acceptanceVector_H); + for (int i = 0; i < numTargets; i++) + if (opsAndBounds.isProbabilityObjective(i)) { + acceptanceVector_H = JDD.PermuteVariables(acceptanceVector_H, draDDRowVars[i], draDDColVars[i]); + } + candidateStates = JDD.Apply(JDD.TIMES, candidateStates, acceptanceVector_H); + candidateStates = JDD.ThereExists(candidateStates, modelProduct.getAllDDColVars()); + candidateStates = JDD.ThereExists(candidateStates, modelProduct.getAllDDNondetVars()); + // find all maximal end components + List allecs = mcLtl.findMECStates(modelProduct, candidateStates, acceptanceVector_L); + JDD.Deref(candidateStates); + JDD.Deref(acceptanceVector_L); + return allecs; + } + + //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(DRA 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 + { + mainLog.println("\nFinding accepting end components for " + name + "..."); + long l = System.currentTimeMillis(); + // increase ref count for checking conflict formulas + if (conflictformulaeGtOne) { + for (JDDNode n : statesH) + JDD.Ref(n); + for (JDDNode n : statesL) + JDD.Ref(n); + } + JDDNode ret = mcLtl.findMultiAcceptingStates(dra, modelProduct, draDDRowVars, draDDColVars, false, allecs, statesH, statesL); + //targetDDs.add(mcLtl.findMultiAcceptingStates(dra[i], modelProduct, draDDRowVars[i], draDDColVars[i], false)); + l = System.currentTimeMillis() - l; + mainLog.println("Time for end component identification: " + l / 1000.0 + " seconds."); + return ret; + } + + protected void removeNonZeroMecsForMax(NondetModel modelProduct, LTLModelChecker mcLtl, List rewardsIndex, OpsAndBoundsList opsAndBounds, + int numTargets, DRA dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[]) throws PrismException + { + List mecs = mcLtl.findMECStates(modelProduct, modelProduct.getReach()); + JDDNode removedActions = JDD.Constant(0); + JDDNode rmecs = JDD.Constant(0); + for (int i = 0; i < rewardsIndex.size(); i++) + if (opsAndBounds.getRewardOperator(i) == Operator.R_MAX || opsAndBounds.getRewardOperator(i) == Operator.R_GE) { + JDD.Ref(rewardsIndex.get(i)); + JDDNode actions = JDD.GreaterThan(rewardsIndex.get(i), 0.0); + if (!actions.equals(JDD.ZERO)) + for (int j = 0; j < mecs.size(); j++) { + JDDNode mec = mecs.get(j); + JDD.Ref(mec); + JDDNode mecactions = mcLtl.maxStableSetTrans1(modelProduct, mec); + JDD.Ref(actions); + mecactions = JDD.And(actions, mecactions); + if (!mecactions.equals(JDD.ZERO)) { + JDD.Ref(mec); + rmecs = JDD.Or(rmecs, mec); + } + removedActions = JDD.Or(removedActions, mecactions); + } + JDD.Deref(actions); + } + for (JDDNode mec : mecs) + JDD.Deref(mec); + // TODO: check if the model satisfies the LTL constraints + if (!rmecs.equals(JDD.ZERO)) { + boolean constraintViolated = false; + if (JDD.AreInterecting(modelProduct.getStart(), rmecs)) { + constraintViolated = true; + JDD.Deref(rmecs); + } else { + // find all action pointing to mecs from outside a + JDD.Ref(rmecs); + JDDNode rtarget = JDD.PermuteVariables(rmecs, modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars()); + JDD.Ref(modelProduct.getTrans01()); + rtarget = JDD.And(modelProduct.getTrans01(), rtarget); + rtarget = JDD.And(rtarget, JDD.Not(rmecs)); + //rtarget = JDD.ThereExists(rtarget, modelProduct.getAllDDColVars()); + // find target states for LTL formulae + Vector tmptargetDDs = new Vector(); + List tmpmultitargetDDs = new ArrayList(); + List tmpmultitargetIDs = new ArrayList(); + ArrayList> tmpdra = new ArrayList>(); + ArrayList tmpdraDDRowVars = new ArrayList(); + ArrayList tmpdraDDColVars = new ArrayList(); + int count = 0; + for (int i = 0; i < numTargets; i++) + if (opsAndBounds.isProbabilityObjective(i) && opsAndBounds.getOperator(i) != Operator.P_MAX + && opsAndBounds.getOperator(i) != Operator.P_MIN) { + tmpdra.add(dra[i]); + tmpdraDDRowVars.add(draDDRowVars[i]); + tmpdraDDColVars.add(draDDColVars[i]); + count++; + } + if (count > 0) { + // TODO: distinguish whether rtarget is empty + DRA newdra[] = new DRA[count]; + tmpdra.toArray(newdra); + JDDVars newdraDDRowVars[] = new JDDVars[count]; + tmpdraDDRowVars.toArray(newdraDDRowVars); + JDDVars newdraDDColVars[] = new JDDVars[count]; + tmpdraDDColVars.toArray(newdraDDColVars); + + findTargetStates(modelProduct, mcLtl, count, count, new boolean[count], newdra, newdraDDRowVars, newdraDDColVars, tmptargetDDs, + tmpmultitargetDDs, tmpmultitargetIDs); + + OpsAndBoundsList tmpOpsAndBounds = new OpsAndBoundsList(); + + for (int i = 0; i < opsAndBounds.probSize(); i++) { + if (opsAndBounds.getProbOperator(i) != Operator.P_MAX) { + tmpOpsAndBounds.add(opsAndBounds.getProbOperator(i), opsAndBounds.getProbBound(i), opsAndBounds.getProbStepBound(i)); + } + } + + tmpOpsAndBounds.add(Operator.R_MAX, -1.0, -1); + + ArrayList tmprewards = new ArrayList(1); + tmprewards.add(rtarget); + double prob = (Double) computeMultiReachProbs(modelProduct, mcLtl, tmprewards, modelProduct.getStart(), tmptargetDDs, tmpmultitargetDDs, + tmpmultitargetIDs, tmpOpsAndBounds, count > 1); + if (prob > 0.0) { // LTL formulae can be satisfied + constraintViolated = true; + } else if (Double.isNaN(prob)) + throw new PrismException("The LTL formulae in multi-objective query cannot be satisfied!\n"); + } else { + // end components with non-zero rewards can always be reached + constraintViolated = true; + } + + //JDD.Deref(rtarget); + for (JDDNode tt : tmptargetDDs) + JDD.Deref(tt); + for (JDDNode tt : tmpmultitargetDDs) + JDD.Deref(tt); + } + if (constraintViolated) { + throw new PrismException("Cannot use multi-objective model checking with maximising objectives and non-zero reward end compoments"); + } + + JDD.Ref(removedActions); + modelProduct.trans = JDD.Apply(JDD.TIMES, modelProduct.trans, JDD.Not(removedActions)); + modelProduct.trans01 = JDD.Apply(JDD.TIMES, modelProduct.trans01, JDD.Not(removedActions)); + } else { + JDD.Deref(rmecs); + JDD.Deref(removedActions); + } + + } + + //TODO is conflictformulae actually just no of prob? + protected void checkConflictsInObjectives(NondetModel modelProduct, LTLModelChecker mcLtl, int conflictformulae, int numTargets, + OpsAndBoundsList opsAndBounds, DRA dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[], List targetDDs, + List> allstatesH, List> allstatesL, List multitargetDDs, List multitargetIDs) + throws PrismException + { + DRA[] tmpdra = new DRA[conflictformulae]; + JDDVars[] tmpdraDDRowVars = new JDDVars[conflictformulae]; + JDDVars[] tmpdraDDColVars = new JDDVars[conflictformulae]; + List tmptargetDDs = new ArrayList(conflictformulae); + List> tmpallstatesH = new ArrayList>(conflictformulae); + List> tmpallstatesL = new ArrayList>(conflictformulae); + int count = 0; + for (int i = 0; i < numTargets; i++) + if (opsAndBounds.isProbabilityObjective(i)) { + tmpdra[count] = dra[i]; + tmpdraDDRowVars[count] = draDDRowVars[i]; + tmpdraDDColVars[count] = draDDColVars[i]; + // tricky part; double check when reachExpr is set for efficiency + tmptargetDDs.add(targetDDs.get(count)); + tmpallstatesH.add(allstatesH.get(i)); + tmpallstatesL.add(allstatesL.get(i)); + count++; + } + List> tmpmultitargetIDs = new ArrayList>(); + + mcLtl.findMultiConflictAcceptingStates(tmpdra, modelProduct, tmpdraDDRowVars, tmpdraDDColVars, tmptargetDDs, tmpallstatesH, tmpallstatesL, + multitargetDDs, tmpmultitargetIDs); + // again. double check when reachExpr is set + count = 0; + for (int i = 0; i < numTargets; i++) + if (opsAndBounds.isProbabilityObjective(i)) { + targetDDs.remove(count); + targetDDs.add(count, tmptargetDDs.get(count)); + count++; + } + + // deal with reachability targets + for (int i = 0; i < tmpmultitargetIDs.size(); i++) { + multitargetIDs.add(changeToInteger(tmpmultitargetIDs.get(i))); + //System.out.println("multitargetIDs["+i+"] = " + multitargetIDs.get(i)); + } + + for (int i = 0; i < numTargets; i++) + if (opsAndBounds.isProbabilityObjective(i)) { + List tmpLH = allstatesH.get(i); + for (JDDNode n : tmpLH) + JDD.Deref(n); + tmpLH = allstatesL.get(i); + for (JDDNode n : tmpLH) + JDD.Deref(n); + } + } + + protected void findTargetStates(NondetModel modelProduct, LTLModelChecker mcLtl, int numTargets, int conflictformulae, boolean reachExpr[], DRA dra[], + JDDVars draDDRowVars[], JDDVars draDDColVars[], List targetDDs, List multitargetDDs, List multitargetIDs) + throws PrismException + { + int i, j; + long l; + + // Compute all maximal end components + ArrayList> allstatesH = new ArrayList>(numTargets); + ArrayList> allstatesL = new ArrayList>(numTargets); + JDDNode acceptanceVector_H = JDD.Constant(0); + JDDNode acceptanceVector_L = JDD.Constant(0); + for (i = 0; i < numTargets; i++) { + if (!reachExpr[i]) { + ArrayList statesH = new ArrayList(); + ArrayList statesL = new ArrayList(); + for (int k = 0; k < dra[i].getNumAcceptancePairs(); k++) { + JDDNode tmpH = JDD.Constant(0); + JDDNode tmpL = JDD.Constant(0); + for (j = 0; j < dra[i].size(); j++) { + if (!dra[i].getAcceptanceL(k).get(j)) { + tmpH = JDD.SetVectorElement(tmpH, draDDRowVars[i], j, 1.0); + } + if (dra[i].getAcceptanceK(k).get(j)) { + tmpL = JDD.SetVectorElement(tmpL, draDDRowVars[i], j, 1.0); + } + } + statesH.add(tmpH); + JDD.Ref(tmpH); + acceptanceVector_H = JDD.Or(acceptanceVector_H, tmpH); + statesL.add(tmpL); + JDD.Ref(tmpL); + acceptanceVector_L = JDD.Or(acceptanceVector_L, tmpL); + } + allstatesH.add(i, statesH); + allstatesL.add(i, statesL); + } else { + allstatesH.add(i, null); + allstatesL.add(i, null); + } + } + + // Find accepting maximum end components for each LTL formula + List allecs = null; + //use acceptanceVector_H and acceptanceVector_L to speed up scc computation + /*// check number of states in each scc + allecs = mcLtl.findEndComponents(modelProduct, modelProduct.getReach()); + StateListMTBDD vl; + int totalNum = 0; + for(JDDNode set : allecs) { + vl = new StateListMTBDD(set, modelProduct); + totalNum += vl.size() - 1; + } + mainLog.println("Total number of states can be saved: " + totalNum);*/ + + JDD.Ref(acceptanceVector_H); + JDD.Ref(modelProduct.getTrans01()); + JDDNode candidateStates = JDD.Apply(JDD.TIMES, modelProduct.getTrans01(), acceptanceVector_H); + for (i = 0; i < numTargets; i++) + if (!reachExpr[i]) { + acceptanceVector_H = JDD.PermuteVariables(acceptanceVector_H, draDDRowVars[i], draDDColVars[i]); + } + candidateStates = JDD.Apply(JDD.TIMES, candidateStates, acceptanceVector_H); + candidateStates = JDD.ThereExists(candidateStates, modelProduct.getAllDDColVars()); + candidateStates = JDD.ThereExists(candidateStates, modelProduct.getAllDDNondetVars()); + // find all maximal end components + allecs = mcLtl.findMECStates(modelProduct, candidateStates, acceptanceVector_L); + JDD.Deref(candidateStates); + JDD.Deref(acceptanceVector_L); + + for (i = 0; i < numTargets; i++) { + if (!reachExpr[i]) { + //mainLog.println("\nFinding accepting end components for " + targetName[i] + "..."); + l = System.currentTimeMillis(); + // increase ref count for checking conflict formulas + if (conflictformulae > 1) { + List tmpLH = allstatesH.get(i); + for (JDDNode n : tmpLH) + JDD.Ref(n); + tmpLH = allstatesL.get(i); + for (JDDNode n : tmpLH) + JDD.Ref(n); + } + targetDDs.add(mcLtl.findMultiAcceptingStates(dra[i], modelProduct, draDDRowVars[i], draDDColVars[i], false, allecs, allstatesH.get(i), + allstatesL.get(i))); + //targetDDs.add(mcLtl.findMultiAcceptingStates(dra[i], modelProduct, draDDRowVars[i], draDDColVars[i], false)); + l = System.currentTimeMillis() - l; + mainLog.println("Time for end component identification: " + l / 1000.0 + " seconds."); + } /*else { + // Fixme: maybe not efficient + if(targetExprs.get(i) != null) { + dd = checkExpressionDD(targetExprs.get(i)); + JDD.Ref(modelProduct.getReach()); + dd = JDD.And(dd, modelProduct.getReach()); + targetDDs.add(dd); + } + }*/ + //mainLog.print("\n number of targets = " + JDD.GetNumMintermsString(targetDDs.get(i), modelProduct.getAllDDRowVars().n())); + //if(i>0) + // mainLog.print("\n total number of targets = " + + // JDD.GetNumMintermsString(JDD.Or(targetDDs.get(i), targetDDs.get(i-1)), modelProduct.getAllDDRowVars().n())); + } + + // check if there are conflicts in objectives + if (conflictformulae > 1) { + DRA[] tmpdra = new DRA[conflictformulae]; + JDDVars[] tmpdraDDRowVars = new JDDVars[conflictformulae]; + JDDVars[] tmpdraDDColVars = new JDDVars[conflictformulae]; + List tmptargetDDs = new ArrayList(conflictformulae); + List> tmpallstatesH = new ArrayList>(conflictformulae); + List> tmpallstatesL = new ArrayList>(conflictformulae); + int count = 0; + for (i = 0; i < numTargets; i++) + if (!reachExpr[i]) { + tmpdra[count] = dra[i]; + tmpdraDDRowVars[count] = draDDRowVars[i]; + tmpdraDDColVars[count] = draDDColVars[i]; + // tricky part; double check when reachExpr is set for efficiency + tmptargetDDs.add(targetDDs.get(count)); + tmpallstatesH.add(allstatesH.get(i)); + tmpallstatesL.add(allstatesL.get(i)); + count++; + } + //multitargetDDs = new ArrayList(); + List> tmpmultitargetIDs = new ArrayList>(); + + mcLtl.findMultiConflictAcceptingStates(tmpdra, modelProduct, tmpdraDDRowVars, tmpdraDDColVars, tmptargetDDs, tmpallstatesH, tmpallstatesL, + multitargetDDs, tmpmultitargetIDs); + // again. double check when reachExpr is set + count = 0; + for (i = 0; i < numTargets; i++) + if (!reachExpr[i]) { + targetDDs.remove(count); + targetDDs.add(count, tmptargetDDs.get(count)); + count++; + } + + // deal with reachability targets + //multitargetIDs = new ArrayList(tmpmultitargetIDs.size()); + for (i = 0; i < tmpmultitargetIDs.size(); i++) { + multitargetIDs.add(changeToInteger(tmpmultitargetIDs.get(i))); + } + + for (i = 0; i < numTargets; i++) + if (!reachExpr[i]) { + List tmpLH = allstatesH.get(i); + for (JDDNode n : tmpLH) + JDD.Deref(n); + tmpLH = allstatesL.get(i); + for (JDDNode n : tmpLH) + JDD.Deref(n); + } + } + + for (JDDNode ec : allecs) + JDD.Deref(ec); + } + + private int changeToInteger(List ids) + { + int k = 0; + for (int i = 0; i < ids.size(); i++) { + int j = 1; + if (ids.get(i) > 0) + j = j << ids.get(i); + k += j; + } + return k; + } + + // compute (max) probabilities for multi-objective reachability + + protected Object computeMultiReachProbs(NondetModel modelProduct, LTLModelChecker mcLtl, List rewards, JDDNode st, 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 = prism.getEngine(); + + //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(); + + JDDNode labels[] = new JDDNode[n]; + String labelNames[] = new String[n]; + // Build temporary DDs for combined targets + for (i = 0; i < n; i++) { + JDD.Ref(targets.get(i)); + JDDNode tmp = targets.get(i); + if (combinations != null) { + for (j = 0; j < combinations.size(); j++) { + if ((combinationIDs.get(j) & (1 << i)) > 0) { + JDD.Ref(combinations.get(j)); + tmp = JDD.Or(tmp, combinations.get(j)); + } + } + } + labels[i] = tmp; + labelNames[i] = "target" + i; + } + + if (prism.getExportTarget()) { + try { + mainLog.print("\nExporting target states info to file \"" + prism.getExportTargetFilename() + "\"..."); + PrismMTBDD.ExportLabels(labels, labelNames, "l", modelProduct.getAllDDRowVars(), modelProduct.getODD(), Prism.EXPORT_PLAIN, + prism.getExportTargetFilename()); + } catch (FileNotFoundException e) { + mainLog.println("\nWarning: Could not export target to file \"" + prism.getExportTargetFilename() + "\""); + } + } + + // yes - union of targets (just to compute no) + yes = JDD.Constant(0); + //n = targets.size(); + for (i = 0; i < n; i++) { + JDD.Ref(targets.get(i)); + yes = JDD.Or(yes, targets.get(i)); + } + if (combinations != null) + for (i = 0; i < combinations.size(); i++) { + JDD.Ref(combinations.get(i)); + yes = JDD.Or(yes, combinations.get(i)); + } + + if (opsAndBounds.rewardSize() == 0) + no = PrismMTBDD.Prob0A(modelProduct.getTrans01(), modelProduct.getReach(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), + modelProduct.getAllDDNondetVars(), modelProduct.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); + JDD.Deref(bottomec); + bottomec = JDD.Constant(0); + for (JDDNode ec : becs) + bottomec = JDD.Or(bottomec, ec); + } + + /*if(op1>2) { // the first query is about reward + JDDNode no_r = PrismMTBDD.Prob0A(modelProduct.getTrans01(), modelProduct.getReach(), + modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), + modelProduct.getAllDDNondetVars(), modelProduct.getReach(), targets.get(0)); + JDD.Ref(no_r); + maybe_r = JDD.And(modelProduct.getReach(), JDD.Not(JDD.Or(targets.get(0), no_r))); + trr = modelProduct.getTransRewards(); + }*/ + + // maybe + JDD.Ref(modelProduct.getReach()); + JDD.Ref(yes); + JDD.Ref(no); + maybe = JDD.And(modelProduct.getReach(), JDD.Not(JDD.Or(yes, no))); + + for (i = 0; i < rewards.size(); i++) { + JDDNode tmp = rewards.remove(i); + JDD.Ref(no); + tmp = JDD.Apply(JDD.TIMES, tmp, JDD.Not(no)); + rewards.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"); + + // compute probabilities + mainLog.println("\nComputing remaining probabilities..."); + // 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) + throw new PrismException("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 PrismException("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); + } else { + value = PrismSparse.NondetMultiReachReward(modelProduct.getTrans(), modelProduct.getTransActions(), modelProduct.getSynchs(), + modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), + targets, opsAndBounds, maybe, st, rewards, 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); + } else { + value = PrismSparse.NondetMultiReach(modelProduct.getTrans(), modelProduct.getTransActions(), modelProduct.getSynchs(), + modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), + targets, opsAndBounds, maybe, st); + } + } + } 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); + 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); + } + } catch (PrismException e) { + throw e; + } finally { + // derefs + if (opsAndBounds.rewardSize() > 0) + JDD.Deref(bottomec); + JDD.Deref(yes); + JDD.Deref(no); + 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)); + } + } + + return value; + } + + protected Object weightedMultiReachProbs(NondetModel modelProduct, JDDNode yes_ones, JDDNode maybe, JDDNode st, 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 3"); + + 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"); + + 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 + { + int numberOfPoints = 0; + 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; + + //convert minimizing rewards to maximizing + for (int i = 0; i < opsAndBounds.rewardSize(); i++) { + if (opsAndBounds.getRewardOperator(i) == Operator.R_LE) { + JDDNode negated = JDD.Apply(JDD.TIMES, JDD.Constant(-1), rewards.get(i)); + //JDD.Ref(negated); + 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); + rewards.set(i, negated); + //boundsRewards.set(i, -1 * boundsRewards.get(i)); + } + } + + double tolerance = prism.getSettings().getDouble(PrismSettings.PRISM_PARETO_EPSILON); + int maxIters = prism.getSettings().getInteger(PrismSettings.PRISM_MULTI_MAX_POINTS); + + NativeIntArray adversary = new NativeIntArray((int) modelProduct.getNumStates()); + int dimProb = targets.length; + int dimReward = rewards.size(); + Point targetPoint = new Point(dimProb + dimReward); + ArrayList computedPoints = new ArrayList(); + ArrayList computedDirections = new ArrayList(); + ArrayList pointsForInitialTile = new ArrayList(); + + //create vectors and sparse matrices for the objectives + final DoubleVector[] probDoubleVectors = new DoubleVector[dimProb]; + final NDSparseMatrix[] rewSparseMatrices = new NDSparseMatrix[dimReward]; + + JDD.Ref(modelProduct.getTrans()); + JDD.Ref(modelProduct.getReach()); + + //create a sparse matrix for transitions + JDDNode a = JDD.Apply(JDD.TIMES, modelProduct.getTrans(), modelProduct.getReach()); + + if (!min) { + JDD.Ref(a); + JDDNode tmp = JDD.And(JDD.Equals(a, 1.0), JDD.Identity(modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars())); + a = JDD.ITE(tmp, JDD.Constant(0), a); + } + + NDSparseMatrix trans_matrix = NDSparseMatrix.BuildNDSparseMatrix(a, modelProduct.getODD(), modelProduct.getAllDDRowVars(), + modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars()); + + //create double vectors for probabilistic objectives + for (int i = 0; i < dimProb; i++) { + probDoubleVectors[i] = new DoubleVector(targets[i], modelProduct.getAllDDRowVars(), modelProduct.getODD()); + } + + //create sparse matrices for reward objectives + for (int i = 0; i < dimReward; i++) { + NDSparseMatrix rew_matrix = NDSparseMatrix.BuildSubNDSparseMatrix(a, modelProduct.getODD(), modelProduct.getAllDDRowVars(), + modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), rewards.get(i)); + rewSparseMatrices[i] = rew_matrix; + } + + JDD.Deref(a); + + 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) { + //System.out.println("Doing GS"); + result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, new DoubleVector[] {probDoubleVectors[i]}, new int[] {probStepBounds[i]}, null, + new double[] { 1.0 }, null); + } else { + //System.out.println("Not doing GS"); + result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, new DoubleVector[] {probDoubleVectors[i]}, new int[] {probStepBounds[i]}, null, + new double[] { 1.0 }, null); + }*/ + 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); + } else { + 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) + throw new PrismException("The probabilistic objective number " + i + " is degenerate since the optimal value is also the least optimal value." ); + */ + targetPoint = new Point(result); + pointsForInitialTile.add(targetPoint); + } + + for (int i = 0; i < dimReward; i++) { + if (verbose) { + mainLog.println("Getting an upper bound on maximizing objective " + i); + } + + double[] result; + double[] weights = new double[dimProb + dimReward]; + weights[i] = 1.0; + /*System.out.println(prism.getMDPSolnMethod()); + if (prism.getMDPSolnMethod() == 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[i] }, + new double[] { 1.0 }, new int[] { rewardStepBounds[i] }); + } 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[i] }, + new double[] { 1.0 }, new int[] { rewardStepBounds[i] }); + }*/ + 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); + } else { + 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) { + iters++; + + //create the weights array + double[] weights = new double[dimProb + dimReward]; + for (int i = 0; i < dimProb + dimReward; i++) { + weights[i] = direction.getCoord(i); + } + + 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); + } else { + 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]); + } + } */ + + numberOfPoints++; + + //collect the numbers obtained from methods executed above. + Point newPoint = new Point(result); + + if (verbose) { + mainLog.println("\n" + numberOfPoints + ": New point is " + newPoint + "."); + mainLog.println("TileList:" + tileList); + } + + computedPoints.add(newPoint); + computedDirections.add(direction); + + tileList.addNewPoint(newPoint); + //mainLog.println("\nTiles after adding: " + tileList); + //compute new direction + direction = tileList.getCandidateHyperplane(); + + if (verbose) { + mainLog.println("New direction is " + direction); + //mainLog.println("TileList: " + tileList); + + } + + if (direction == null) { + //no tile could be improved + decided = true; + break; + } + } + + timer = System.currentTimeMillis() - timer; + mainLog.println("The value iteration(s) took " + timer / 1000.0 + " seconds altogether."); + mainLog.println("Number of weight vectors used: " + numberOfPoints); + + if (!decided) + throw new PrismException("The computation did not finish in " + maxIters + + " target point iterations, try increasing this number using the -multimaxpoints switch."); + else { + String paretoFile = prism.getSettings().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()); + + return tileList; + } + } + + protected double targetDrivenMultiReachProbs(NondetModel modelProduct, JDDNode yes_ones, JDDNode maybe, final JDDNode st, JDDNode[] targets, + List rewards, OpsAndBoundsList opsAndBounds) throws PrismException + { + int numberOfPoints = 0; + 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; + + //convert minimizing rewards to maximizing + for (int i = 0; i < opsAndBounds.rewardSize(); i++) { + if (opsAndBounds.getRewardOperator(i) == Operator.R_LE) { + JDDNode negated = JDD.Apply(JDD.TIMES, JDD.Constant(-1), rewards.get(i)); + //JDD.Ref(negated); + 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); + rewards.set(i, negated); + //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); + + int maxIters = prism.getSettings().getInteger(PrismSettings.PRISM_MULTI_MAX_POINTS); + + NativeIntArray adversary = new NativeIntArray((int) modelProduct.getNumStates()); + int dimProb = targets.length; + int dimReward = rewards.size(); + Point targetPoint = new Point(dimProb + dimReward); + ArrayList computedPoints = new ArrayList(); + ArrayList computedDirections = new ArrayList(); + + //create vectors and sparse matrices for the objectives + final DoubleVector[] probDoubleVectors = new DoubleVector[dimProb]; + final NDSparseMatrix[] rewSparseMatrices = new NDSparseMatrix[dimReward]; + + JDD.Ref(modelProduct.getTrans()); + JDD.Ref(modelProduct.getReach()); + + //create a sparse matrix for transitions + JDDNode a = JDD.Apply(JDD.TIMES, modelProduct.getTrans(), modelProduct.getReach()); + + if (!min) { + JDD.Ref(a); + JDDNode tmp = JDD.And(JDD.Equals(a, 1.0), JDD.Identity(modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars())); + a = JDD.ITE(tmp, JDD.Constant(0), a); + } + + NDSparseMatrix trans_matrix = NDSparseMatrix.BuildNDSparseMatrix(a, modelProduct.getODD(), modelProduct.getAllDDRowVars(), + modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars()); + + //create double vectors for probabilistic objectives + for (int i = 0; i < dimProb; i++) { + probDoubleVectors[i] = new DoubleVector(targets[i], modelProduct.getAllDDRowVars(), modelProduct.getODD()); + } + + //create sparse matrices for reward objectives + for (int i = 0; i < dimReward; i++) { + NDSparseMatrix rew_matrix = NDSparseMatrix.BuildSubNDSparseMatrix(a, modelProduct.getODD(), modelProduct.getAllDDRowVars(), + modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), rewards.get(i)); + rewSparseMatrices[i] = rew_matrix; + } + + JDD.Deref(a); + + //initialize the target point + for (int i = 0; i < dimProb; i++) { + targetPoint.setCoord(i, opsAndBounds.getProbBound(i)); + } + if (maximizingProb) { + targetPoint.setCoord(0, 1.0); + } + + for (int i = 0; i < dimReward; i++) { + //multiply by -1 in case of minimizing, that converts it to maximizing. + double t = (opsAndBounds.getRewardOperator(i) == Operator.R_LE) ? -opsAndBounds.getRewardBound(i) : opsAndBounds.getRewardBound(i); + targetPoint.setCoord(i + dimProb, t); + } + if (maximizingReward) { + if (verbose) { + mainLog.println("Getting an upper bound on maximizing objective"); + } + + double[] result; + if (prism.getMDPSolnMethod() == 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] }); + } 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] }); + } + numberOfPoints++; + + targetPoint.setCoord(dimProb, result[0]); + + if (verbose) { + mainLog.println("Upper bound is " + result[0]); + } + } + + Point direction = MultiObjUtils.getWeights(targetPoint, computedPoints); + + if (verbose) { + mainLog.println("The initial target point is " + targetPoint); + mainLog.println("The initial direction is " + direction); + } + + boolean decided = false; + boolean isAchievable = false; + int iters = 0; + while (iters < maxIters) { + iters++; + + //create the weights array + double[] weights = new double[dimProb + dimReward]; + for (int i = 0; i < dimProb + dimReward; i++) { + weights[i] = direction.getCoord(i); + } + + 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); + } else { + 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); + + if (verbose) { + mainLog.println("New point is " + newPoint + "."); + } + + computedPoints.add(newPoint); + computedDirections.add(direction); + + + //if (prism.getExportMultiGraphs()) + // MultiObjUtils.printGraphFileDebug(targetPoint, computedPoints, computedDirections, prism.getExportMultiGraphsDir(), output++); + + //check if the new point together with the direction shows the point is unreachable + double dNew = 0.0; + for (int i = 0; i < dimProb + dimReward; i++) { + dNew += newPoint.getCoord(i) * direction.getCoord(i); + } + + double dTarget = 0.0; + for (int i = 0; i < dimProb + dimReward; i++) { + dTarget += targetPoint.getCoord(i) * direction.getCoord(i); + } + + if (dTarget > dNew) { + if (maximizingProb || maximizingReward) { + int maximizingCoord = (maximizingProb) ? 0 : dimProb; + double rest = dNew - (dTarget - direction.getCoord(maximizingCoord) * targetPoint.getCoord(maximizingCoord)); + if ((!maximizingNegated && rest < 0) || (maximizingNegated && rest > 0)) { + //target can't be lowered + decided = true; + targetPoint.setCoord(maximizingCoord, Double.NaN); + if (verbose) + mainLog.println("Decided, target is " + targetPoint); + break; + } else { + double lowered = rest / direction.getCoord(maximizingCoord); + targetPoint.setCoord(maximizingCoord, lowered); + //HACK + if (lowered == Double.NEGATIVE_INFINITY) { + targetPoint.setCoord(maximizingCoord, Double.NaN); + mainLog.println("\nThe constraints are not achievable!\n"); + decided = true; + isAchievable = false; + break; + } + if (verbose) + mainLog.println("Target lowered to " + targetPoint); + + //if (prism.getExportMultiGraphs()) + // MultiObjUtils.printGraphFileDebug(targetPoint, computedPoints, computedDirections, prism.getExportMultiGraphsDir(), output++); + } + } else { + decided = true; + isAchievable = false; + break; + } + } + + //compute new direction + direction = MultiObjUtils.getWeights(targetPoint, computedPoints); + + if (verbose) { + mainLog.println("New direction is " + direction); + } + + if (direction == null || computedDirections.contains(direction)) //The second disjunct is for convergence + { + //there is no hyperplane strictly separating the target from computed points + //hence we can conclude that the point is reachable + decided = true; + isAchievable = true; + break; + } + } + + timer = System.currentTimeMillis() - timer; + mainLog.println("The value iteration(s) took " + timer / 1000.0 + " seconds altogether."); + mainLog.println("Number of weight vectors used: " + numberOfPoints); + + if (!decided) + throw new PrismException("The computation did not finish in " + maxIters + + " target point iterations, try increasing this number using the -multimaxpoints switch."); + if (maximizingProb || maximizingReward) { + int maximizingCoord = (maximizingProb) ? 0 : dimProb; + return (maximizingNegated) ? -targetPoint.getCoord(maximizingCoord) : targetPoint.getCoord(maximizingCoord); + } else { + return (isAchievable) ? 1.0 : 0.0; + } + } +} diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 24715481..9ed1d10d 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -2,7 +2,7 @@ // // Copyright (c) 2002- // Authors: -// * Dave Parker (University of Oxford, formerly University of Birmingham) +// * Dave Parker (University of Birmingham/Oxford) // * Vojtech Forejt (University of Oxford) // * Hongyang Qu (University of Oxford) // * Carlos S. Bederian (Universidad Nacional de Cordoba) @@ -307,453 +307,10 @@ public class NondetModelChecker extends NonProbModelChecker } } - //takes one operand of multi-objective expression and extracts operator, values and reward functions from it. - protected void extractInfoFromMultiObjectiveOperand(Expression operand, OpsAndBoundsList opsAndBounds, List rewardsIndex, List targetName, - List targetExprs, boolean isFirst) throws PrismException - { - int stepBound = 0; - ExpressionProb exprProb = null; - ExpressionReward exprReward = null; - ExpressionTemporal exprTemp; - RelOp relOp; - if (operand instanceof ExpressionProb) { - exprProb = (ExpressionProb) operand; - exprReward = null; - relOp = exprProb.getRelOp(); - } else if (operand instanceof ExpressionReward) { - exprReward = (ExpressionReward) operand; - exprProb = null; - relOp = exprReward.getRelOp(); - Object rs = exprReward.getRewardStructIndex(); - JDDNode transRewards = null; - JDDNode stateRewards = null; - if (model.getNumRewardStructs() == 0) - throw new PrismException("Model has no rewards specified"); - if (rs == null) { - transRewards = model.getTransRewards(0); - stateRewards = model.getStateRewards(0); - } else if (rs instanceof Expression) { - int j = ((Expression) rs).evaluateInt(constantValues); - rs = new Integer(j); // for better error reporting below - transRewards = model.getTransRewards(j - 1); - stateRewards = model.getStateRewards(j - 1); - } else if (rs instanceof String) { - transRewards = model.getTransRewards((String) rs); - stateRewards = model.getStateRewards((String) rs); - } - - //check if there are state rewards and display a warning - if (stateRewards != null && !stateRewards.equals(JDD.ZERO)) - throw new PrismException("Multi-objective model checking does not support state rewards; please convert to transition rewards"); - if (transRewards == null) - throw new PrismException("Invalid reward structure index \"" + rs + "\""); - rewardsIndex.add(transRewards); - } else { - throw new PrismException("Multi-objective properties can only contain P and R operators"); - } - // Get the cumulative step bound for reward - if (exprReward != null) { - exprTemp = (ExpressionTemporal) exprReward.getExpression(); - - // We only allow C or C<=k reward operators, others such as F are not supported currently - if (exprTemp.getOperator() != ExpressionTemporal.R_C) { - throw new PrismException("Reward operators in multi-objective properties must be C or C<=k (" + exprTemp.getOperatorSymbol() - + " is not yet supported)"); - } - - if (exprTemp.getUpperBound() != null) { - //This is the case of C<=k - stepBound = exprTemp.getUpperBound().evaluateInt(constantValues); - } else { - //Here we just have C - stepBound = -1; - } - /*if (exprTemp.getOperator() != ExpressionTemporal.R_F) { - throw new PrismException("Multi-objective only supports F operator for rewards"); - }*/ - } - if (exprProb != null) {// || ((ExpressionTemporal) exprReward.getExpression()).getOperator() != ExpressionTemporal.R_C) { - exprTemp = (ExpressionTemporal) exprProb.getExpression(); - //TODO we currently ignore the lower bound - if (exprTemp.getUpperBound() != null) { - stepBound = exprTemp.getUpperBound().evaluateInt(constantValues); - } - else - stepBound = -1; - } - - // Get info from P/R operator - // Store relational operator - if (relOp.isStrict()) - throw new PrismException("Multi-objective properties can not use strict inequalities on P/R operators"); - Operator op; - if (relOp == RelOp.MAX) { - op = (exprProb != null) ? Operator.P_MAX : Operator.R_MAX; - } else if (relOp == RelOp.GEQ) { - op = (exprProb != null) ? Operator.P_GE : Operator.R_GE; - } else if (relOp == RelOp.MIN) { - op = (exprProb != null) ? Operator.P_MIN : Operator.R_MIN; - } else if (relOp == RelOp.LEQ) { - op = (exprProb != null) ? Operator.P_LE : Operator.R_LE; - } else - throw new PrismException("Multi-objective properties can only contain P/R operators with max/min=? or lower/upper probability bounds"); - // Store probability/rewards bound - Expression pb = (exprProb != null) ? exprProb.getProb() : exprReward.getReward(); - if (pb != null) { - double p = pb.evaluateDouble(constantValues); - if ((exprProb != null) && (p < 0 || p > 1)) - throw new PrismException("Invalid probability bound " + p + " in P operator"); - if ((exprProb == null) && (p < 0)) - throw new PrismException("Invalid reward bound " + p + " in P operator"); - if (exprProb != null && relOp == RelOp.LEQ) - p = 1 - p; - - opsAndBounds.add(op, p, stepBound); - } else { - opsAndBounds.add(op, -1.0, stepBound); - } - - // Now extract targets - // Also store which ones are just reachability (in reachExpr) - if (exprProb != null) { - targetExprs.add(exprProb.getExpression()); - // TODO check if the following line is unneeded: it only kept track of probs vs rewards - // reachExpr[i] = false; - targetName.add(exprProb.getExpression().toString()); - } else { - targetExprs.add(null); - // TODO check if the following line is unneeded: it only kept track of probs vs rewards - // reachExpr[i] = true; - targetName.add(""); - } - } - - //Prints info about the product model in multi-objective - protected void outputProductMulti(NondetModel modelProduct) throws PrismException - { - // Print product info - mainLog.println(); - modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo()); - - // Output product, if required - if (prism.getExportProductTrans()) { - try { - mainLog.println("\nExporting product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"..."); - prism.exportTransToFile(modelProduct, true, Prism.EXPORT_PLAIN, new File(prism.getExportProductTransFilename())); - } catch (FileNotFoundException e) { - mainLog.printWarning("Could not export product transition matrix to file \"" + prism.getExportProductTransFilename() + "\""); - } - } - if (prism.getExportProductStates()) { - try { - mainLog.println("\nExporting product state space to file \"" + prism.getExportProductStatesFilename() + "\"..."); - prism.exportStatesToFile(modelProduct, Prism.EXPORT_PLAIN, new File(prism.getExportProductStatesFilename())); - } catch (FileNotFoundException e) { - mainLog.printWarning("Could not export product state space to file \"" + prism.getExportProductStatesFilename() + "\""); - } - } - } - - //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(DRA 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 - { - mainLog.println("\nFinding accepting end components for " + name + "..."); - long l = System.currentTimeMillis(); - // increase ref count for checking conflict formulas - if (conflictformulaeGtOne) { - for (JDDNode n : statesH) - JDD.Ref(n); - for (JDDNode n : statesL) - JDD.Ref(n); - } - JDDNode ret = mcLtl.findMultiAcceptingStates(dra, modelProduct, draDDRowVars, draDDColVars, false, allecs, statesH, statesL); - //targetDDs.add(mcLtl.findMultiAcceptingStates(dra[i], modelProduct, draDDRowVars[i], draDDColVars[i], false)); - l = System.currentTimeMillis() - l; - mainLog.println("Time for end component identification: " + l / 1000.0 + " seconds."); - return ret; - } - - protected void removeNonZeroMecsForMax(NondetModel modelProduct, LTLModelChecker mcLtl, List rewardsIndex, OpsAndBoundsList opsAndBounds, - int numTargets, DRA dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[]) throws PrismException - { - List mecs = mcLtl.findMECStates(modelProduct, modelProduct.getReach()); - JDDNode removedActions = JDD.Constant(0); - JDDNode rmecs = JDD.Constant(0); - boolean mecflags[] = new boolean[mecs.size()]; - for (int i = 0; i < rewardsIndex.size(); i++) - if (opsAndBounds.getRewardOperator(i) == Operator.R_MAX || opsAndBounds.getRewardOperator(i) == Operator.R_GE) { - JDD.Ref(rewardsIndex.get(i)); - JDDNode actions = JDD.GreaterThan(rewardsIndex.get(i), 0.0); - if (!actions.equals(JDD.ZERO)) - for (int j = 0; j < mecs.size(); j++) { - JDDNode mec = mecs.get(j); - JDD.Ref(mec); - JDDNode mecactions = mcLtl.maxStableSetTrans1(modelProduct, mec); - JDD.Ref(actions); - mecactions = JDD.And(actions, mecactions); - if (!mecactions.equals(JDD.ZERO)) { - JDD.Ref(mec); - rmecs = JDD.Or(rmecs, mec); - } - removedActions = JDD.Or(removedActions, mecactions); - } - JDD.Deref(actions); - } - for (JDDNode mec : mecs) - JDD.Deref(mec); - // TODO: check if the model satisfies the LTL constraints - if (!rmecs.equals(JDD.ZERO)) { - boolean constraintViolated = false; - if (JDD.AreInterecting(modelProduct.getStart(), rmecs)) { - constraintViolated = true; - JDD.Deref(rmecs); - } else { - // find all action pointing to mecs from outside a - JDD.Ref(rmecs); - JDDNode rtarget = JDD.PermuteVariables(rmecs, modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars()); - JDD.Ref(modelProduct.getTrans01()); - rtarget = JDD.And(modelProduct.getTrans01(), rtarget); - rtarget = JDD.And(rtarget, JDD.Not(rmecs)); - //rtarget = JDD.ThereExists(rtarget, modelProduct.getAllDDColVars()); - // find target states for LTL formulae - Vector tmptargetDDs = new Vector(); - List tmpmultitargetDDs = new ArrayList(); - List tmpmultitargetIDs = new ArrayList(); - ArrayList> tmpdra = new ArrayList>(); - ArrayList tmpdraDDRowVars = new ArrayList(); - ArrayList tmpdraDDColVars = new ArrayList(); - int count = 0; - for (int i = 0; i < numTargets; i++) - if (opsAndBounds.isProbabilityObjective(i) && opsAndBounds.getOperator(i) != Operator.P_MAX - && opsAndBounds.getOperator(i) != Operator.P_MIN) { - tmpdra.add(dra[i]); - tmpdraDDRowVars.add(draDDRowVars[i]); - tmpdraDDColVars.add(draDDColVars[i]); - count++; - } - if (count > 0) { - // TODO: distinguish whether rtarget is empty - DRA newdra[] = new DRA[count]; - tmpdra.toArray(newdra); - JDDVars newdraDDRowVars[] = new JDDVars[count]; - tmpdraDDRowVars.toArray(newdraDDRowVars); - JDDVars newdraDDColVars[] = new JDDVars[count]; - tmpdraDDColVars.toArray(newdraDDColVars); - - findTargetStates(modelProduct, mcLtl, count, count, new boolean[count], newdra, newdraDDRowVars, newdraDDColVars, tmptargetDDs, - tmpmultitargetDDs, tmpmultitargetIDs); - - OpsAndBoundsList tmpOpsAndBounds = new OpsAndBoundsList(); - - for (int i = 0; i < opsAndBounds.probSize(); i++) { - if (opsAndBounds.getProbOperator(i) != Operator.P_MAX) { - tmpOpsAndBounds.add(opsAndBounds.getProbOperator(i), - opsAndBounds.getProbBound(i), - opsAndBounds.getProbStepBound(i)); - } - } - - tmpOpsAndBounds.add(Operator.R_MAX, -1.0, -1); - - ArrayList tmprewards = new ArrayList(1); - tmprewards.add(rtarget); - double prob = (Double) computeMultiReachProbs(modelProduct, mcLtl, tmprewards, modelProduct.getStart(), tmptargetDDs, tmpmultitargetDDs, - tmpmultitargetIDs, tmpOpsAndBounds, count > 1); - if (prob > 0.0) { // LTL formulae can be satisfied - constraintViolated = true; - } else if (Double.isNaN(prob)) - throw new PrismException("The LTL formulae in multi-objective query cannot be satisfied!\n"); - } else { - // end components with non-zero rewards can always be reached - constraintViolated = true; - } - - //JDD.Deref(rtarget); - for (JDDNode tt : tmptargetDDs) - JDD.Deref(tt); - for (JDDNode tt : tmpmultitargetDDs) - JDD.Deref(tt); - } - if (constraintViolated) { - throw new PrismException("Cannot use multi-objective model checking with maximising objectives and non-zero reward end compoments"); - } - - JDD.Ref(removedActions); - modelProduct.trans = JDD.Apply(JDD.TIMES, modelProduct.trans, JDD.Not(removedActions)); - modelProduct.trans01 = JDD.Apply(JDD.TIMES, modelProduct.trans01, JDD.Not(removedActions)); - } else { - JDD.Deref(rmecs); - JDD.Deref(removedActions); - } - - } - - //TODO is conflictformulae actually just no of prob? - protected void checkConflictsInObjectives(NondetModel modelProduct, LTLModelChecker mcLtl, int conflictformulae, int numTargets, - OpsAndBoundsList opsAndBounds, DRA dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[], List targetDDs, - List> allstatesH, List> allstatesL, List multitargetDDs, List multitargetIDs) - throws PrismException - { - DRA[] tmpdra = new DRA[conflictformulae]; - JDDVars[] tmpdraDDRowVars = new JDDVars[conflictformulae]; - JDDVars[] tmpdraDDColVars = new JDDVars[conflictformulae]; - List tmptargetDDs = new ArrayList(conflictformulae); - List> tmpallstatesH = new ArrayList>(conflictformulae); - List> tmpallstatesL = new ArrayList>(conflictformulae); - int count = 0; - for (int i = 0; i < numTargets; i++) - if (opsAndBounds.isProbabilityObjective(i)) { - tmpdra[count] = dra[i]; - tmpdraDDRowVars[count] = draDDRowVars[i]; - tmpdraDDColVars[count] = draDDColVars[i]; - // tricky part; double check when reachExpr is set for efficiency - tmptargetDDs.add(targetDDs.get(count)); - tmpallstatesH.add(allstatesH.get(i)); - tmpallstatesL.add(allstatesL.get(i)); - count++; - } - List> tmpmultitargetIDs = new ArrayList>(); - - mcLtl.findMultiConflictAcceptingStates(tmpdra, modelProduct, tmpdraDDRowVars, tmpdraDDColVars, tmptargetDDs, tmpallstatesH, tmpallstatesL, - multitargetDDs, tmpmultitargetIDs); - // again. double check when reachExpr is set - count = 0; - for (int i = 0; i < numTargets; i++) - if (opsAndBounds.isProbabilityObjective(i)) { - targetDDs.remove(count); - targetDDs.add(count, tmptargetDDs.get(count)); - count++; - } - - // deal with reachability targets - for (int i = 0; i < tmpmultitargetIDs.size(); i++) { - multitargetIDs.add(changeToInteger(tmpmultitargetIDs.get(i))); - //System.out.println("multitargetIDs["+i+"] = " + multitargetIDs.get(i)); - } - - for (int i = 0; i < numTargets; i++) - if (opsAndBounds.isProbabilityObjective(i)) { - List tmpLH = allstatesH.get(i); - for (JDDNode n : tmpLH) - JDD.Deref(n); - tmpLH = allstatesL.get(i); - for (JDDNode n : tmpLH) - JDD.Deref(n); - } - } - - protected void addDummyFormula(NondetModel modelProduct, LTLModelChecker mcLtl, List targetDDs, OpsAndBoundsList opsAndBounds) - throws PrismException - { - List tmpecs = mcLtl.findMECStates(modelProduct, modelProduct.getReach()); - JDDNode acceptingStates = JDD.Constant(0); - for (JDDNode set : tmpecs) - acceptingStates = JDD.Or(acceptingStates, set); - targetDDs.add(acceptingStates); - opsAndBounds.add(Operator.P_GE, 0.0, -1); - } - - //TODO: dra's element is changed here, not neat. - protected NondetModel constructDRAandProductMulti(NondetModel model, LTLModelChecker mcLtl, Expression ltl, int i, DRA dra[], Operator operator, - Expression targetExpr, JDDVars draDDRowVars, JDDVars draDDColVars, JDDNode ddStateIndex) throws PrismException - { - // Model check maximal state formulas - Vector labelDDs = new Vector(); - ltl = mcLtl.checkMaximalStateFormulas(this, model, targetExpr.deepCopy(), labelDDs); - - // Convert LTL formula to deterministic Rabin automaton (DRA) - // For min probabilities, need to negate the formula - // (add parentheses to allow re-parsing if required) - if (Operator.isMinOrLe(operator)) - ltl = Expression.Not(Expression.Parenth(ltl)); - mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); - long l = System.currentTimeMillis(); - dra[i] = LTLModelChecker.convertLTLFormulaToDRA(ltl); - mainLog.print("DRA has " + dra[i].size() + " states, " + ", " + dra[i].getNumAcceptancePairs() + " pairs."); - l = System.currentTimeMillis() - l; - mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds."); - // If required, export DRA - if (prism.getSettings().getExportPropAut()) { - String exportPropAutFilename = PrismUtils.addCounterSuffixToFilename(prism.getSettings().getExportPropAutFilename(), i); - mainLog.println("Exporting DRA to file \"" + exportPropAutFilename + "\"..."); - PrismLog out = new PrismFileLog(exportPropAutFilename); - out.println(dra); - out.close(); - //dra.printDot(new java.io.PrintStream("dra.dot")); - } - - // Build product of MDP and automaton - mainLog.println("\nConstructing MDP-DRA product..."); - - NondetModel modelNew = mcLtl.constructProductMDP(dra[i], model, labelDDs, draDDRowVars, draDDColVars, false, i == 0 ? ddStateIndex : model.getStart()); - - modelNew.printTransInfo(mainLog, prism.getExtraDDInfo()); - // Deref label BDDs - for (int j = 0; j < labelDDs.size(); j++) { - JDD.Deref(labelDDs.get(j)); - } - return modelNew; - } - - protected List computeAllEcs(NondetModel modelProduct, LTLModelChecker mcLtl, ArrayList> allstatesH, - ArrayList> allstatesL, JDDNode acceptanceVector_H, JDDNode acceptanceVector_L, JDDVars draDDRowVars[], JDDVars draDDColVars[], - OpsAndBoundsList opsAndBounds, int numTargets) throws PrismException - { - //use acceptanceVector_H and acceptanceVector_L to speed up scc computation - JDD.Ref(acceptanceVector_H); - JDD.Ref(modelProduct.getTrans01()); - JDDNode candidateStates = JDD.Apply(JDD.TIMES, modelProduct.getTrans01(), acceptanceVector_H); - for (int i = 0; i < numTargets; i++) - if (opsAndBounds.isProbabilityObjective(i)) { - acceptanceVector_H = JDD.PermuteVariables(acceptanceVector_H, draDDRowVars[i], draDDColVars[i]); - } - candidateStates = JDD.Apply(JDD.TIMES, candidateStates, acceptanceVector_H); - candidateStates = JDD.ThereExists(candidateStates, modelProduct.getAllDDColVars()); - candidateStates = JDD.ThereExists(candidateStates, modelProduct.getAllDDNondetVars()); - // find all maximal end components - List allecs = mcLtl.findMECStates(modelProduct, candidateStates, acceptanceVector_L); - JDD.Deref(candidateStates); - JDD.Deref(acceptanceVector_L); - return allecs; - } - /** - * - * @param modelProduct - * @param rewardsIndex - * @param relOpsReward - * @return True if some transitions were removed + * Model check a multi-objective expression and return the result. + * For multi-objective queries, we only find the value for one state. */ - protected boolean removeNonZeroRewardTrans(NondetModel modelProduct, List rewardsIndex, OpsAndBoundsList opsAndBounds) - { - boolean transchanged = false; - for (int i = 0; i < rewardsIndex.size(); i++) - if (opsAndBounds.getRewardOperator(i) == Operator.R_MIN || opsAndBounds.getRewardOperator(i) == Operator.R_LE) { - // Get non-zero reward actions - JDD.Ref(rewardsIndex.get(i)); - JDDNode actions = JDD.GreaterThan(rewardsIndex.get(i), 0.0); - if (!actions.equals(JDD.ZERO)) { - //mainLog.println("Removing non-zero reward actions in reward #" + i); - JDD.Ref(actions); - if (!transchanged) - JDD.Ref(modelProduct.getTrans()); - JDDNode tmp = JDD.ITE(actions, JDD.Constant(0), modelProduct.getTrans()); - modelProduct.trans = tmp; - if (!transchanged) - JDD.Ref(modelProduct.getTrans01()); - tmp = JDD.ITE(actions, JDD.Constant(0), modelProduct.getTrans01()); - modelProduct.trans01 = tmp; - transchanged = true; - } - } - return transchanged; - } - - // Multi-objective protected StateValues checkExpressionMultiObjective(ExpressionFunc expr) throws PrismException { // Objective/target info @@ -768,6 +325,7 @@ public class NondetModelChecker extends NonProbModelChecker // LTL/product model stuff NondetModel modelProduct, modelNew; JDDVars[] draDDRowVars, draDDColVars; + MultiObjModelChecker mcMo; LTLModelChecker mcLtl; Expression[] ltl; DRA[] dra; @@ -827,8 +385,9 @@ public class NondetModelChecker extends NonProbModelChecker draDDRowVars = new JDDVars[numTargets]; draDDColVars = new JDDVars[numTargets]; - // For LTL model checking routines + // For LTL/multi-obj model checking routines mcLtl = new LTLModelChecker(prism); + mcMo = new MultiObjModelChecker(prism, prism); // Product is initially just the original model (we build it recursively) modelProduct = model; @@ -839,8 +398,8 @@ public class NondetModelChecker extends NonProbModelChecker if (opsAndBounds.isProbabilityObjective(i)) { draDDRowVars[i] = new JDDVars(); draDDColVars[i] = new JDDVars(); - modelNew = constructDRAandProductMulti(modelProduct, mcLtl, ltl[i], i, dra, opsAndBounds.getOperator(i), targetExprs.get(i), draDDRowVars[i], - draDDColVars[i], ddStateIndex); + modelNew = mcMo.constructDRAandProductMulti(modelProduct, mcLtl, this, ltl[i], i, dra, opsAndBounds.getOperator(i), targetExprs.get(i), + draDDRowVars[i], draDDColVars[i], ddStateIndex); // Deref old product (unless is the original model) if (i > 0 & !originalmodel) modelProduct.clear(); @@ -865,13 +424,13 @@ public class NondetModelChecker extends NonProbModelChecker // Removing actions with non-zero reward from the product for maximum cases if (hasMaxReward /*& hasLTLconstraint*/) { - removeNonZeroMecsForMax(modelProduct, mcLtl, rewardsIndex, opsAndBounds, numTargets, dra, draDDRowVars, draDDColVars); + mcMo.removeNonZeroMecsForMax(modelProduct, mcLtl, rewardsIndex, opsAndBounds, numTargets, dra, draDDRowVars, draDDColVars); } // Remove all non-zero reward from trans in order to search for zero reward end components JDDNode tmptrans = modelProduct.getTrans(); JDDNode tmptrans01 = modelProduct.getTrans01(); - boolean transchanged = removeNonZeroRewardTrans(modelProduct, rewardsIndex, opsAndBounds); + boolean transchanged = mcMo.removeNonZeroRewardTrans(modelProduct, rewardsIndex, opsAndBounds); // Compute all maximal end components ArrayList> allstatesH = new ArrayList>(numTargets); @@ -909,12 +468,12 @@ public class NondetModelChecker extends NonProbModelChecker } // Find accepting maximum end components for each LTL formula - List allecs = computeAllEcs(modelProduct, mcLtl, allstatesH, allstatesL, acceptanceVector_H, acceptanceVector_L, draDDRowVars, draDDColVars, + List allecs = mcMo.computeAllEcs(modelProduct, mcLtl, allstatesH, allstatesL, acceptanceVector_H, acceptanceVector_L, draDDRowVars, draDDColVars, opsAndBounds, numTargets); for (int i = 0; i < numTargets; i++) { if (opsAndBounds.isProbabilityObjective(i)) { - targetDDs.add(computeAcceptingEndComponent(dra[i], modelProduct, draDDRowVars[i], draDDColVars[i], allecs, allstatesH.get(i), + targetDDs.add(mcMo.computeAcceptingEndComponent(dra[i], modelProduct, draDDRowVars[i], draDDColVars[i], allecs, allstatesH.get(i), allstatesL.get(i), mcLtl, conflictformulae > 1, targetName.get(i))); } else { // Fixme: maybe not efficient @@ -931,9 +490,8 @@ public class NondetModelChecker extends NonProbModelChecker if (conflictformulae > 1) { multitargetDDs = new ArrayList(); multitargetIDs = new ArrayList(); - checkConflictsInObjectives(modelProduct, mcLtl, conflictformulae, numTargets, opsAndBounds, dra, draDDRowVars, draDDColVars, targetDDs, allstatesH, + mcMo.checkConflictsInObjectives(modelProduct, mcLtl, conflictformulae, numTargets, opsAndBounds, dra, draDDRowVars, draDDColVars, targetDDs, allstatesH, allstatesL, multitargetDDs, multitargetIDs); - Object o = multitargetDDs; } for (JDDNode ec : allecs) @@ -959,7 +517,7 @@ public class NondetModelChecker extends NonProbModelChecker modelProduct.trans01 = tmptrans01; } - Object value = computeMultiReachProbs(modelProduct, mcLtl, rewards, modelProduct.getStart(), targetDDs, multitargetDDs, multitargetIDs, opsAndBounds, + Object value = mcMo.computeMultiReachProbs(modelProduct, mcLtl, rewards, modelProduct.getStart(), targetDDs, multitargetDDs, multitargetIDs, opsAndBounds, conflictformulae > 1); // Deref, clean up @@ -1009,162 +567,162 @@ public class NondetModelChecker extends NonProbModelChecker } - protected void findTargetStates(NondetModel modelProduct, LTLModelChecker mcLtl, int numTargets, int conflictformulae, boolean reachExpr[], DRA dra[], - JDDVars draDDRowVars[], JDDVars draDDColVars[], List targetDDs, List multitargetDDs, List multitargetIDs) - throws PrismException + //takes one operand of multi-objective expression and extracts operator, values and reward functions from it. + protected void extractInfoFromMultiObjectiveOperand(Expression operand, OpsAndBoundsList opsAndBounds, List rewardsIndex, List targetName, + List targetExprs, boolean isFirst) throws PrismException { - int i, j; - long l; + int stepBound = 0; + ExpressionProb exprProb = null; + ExpressionReward exprReward = null; + ExpressionTemporal exprTemp; + RelOp relOp; + if (operand instanceof ExpressionProb) { + exprProb = (ExpressionProb) operand; + exprReward = null; + relOp = exprProb.getRelOp(); + } else if (operand instanceof ExpressionReward) { + exprReward = (ExpressionReward) operand; + exprProb = null; + relOp = exprReward.getRelOp(); + Object rs = exprReward.getRewardStructIndex(); + JDDNode transRewards = null; + JDDNode stateRewards = null; + if (model.getNumRewardStructs() == 0) + throw new PrismException("Model has no rewards specified"); + if (rs == null) { + transRewards = model.getTransRewards(0); + stateRewards = model.getStateRewards(0); + } else if (rs instanceof Expression) { + int j = ((Expression) rs).evaluateInt(constantValues); + rs = new Integer(j); // for better error reporting below + transRewards = model.getTransRewards(j - 1); + stateRewards = model.getStateRewards(j - 1); + } else if (rs instanceof String) { + transRewards = model.getTransRewards((String) rs); + stateRewards = model.getStateRewards((String) rs); + } - // Compute all maximal end components - ArrayList> allstatesH = new ArrayList>(numTargets); - ArrayList> allstatesL = new ArrayList>(numTargets); - JDDNode acceptanceVector_H = JDD.Constant(0); - JDDNode acceptanceVector_L = JDD.Constant(0); - for (i = 0; i < numTargets; i++) { - if (!reachExpr[i]) { - ArrayList statesH = new ArrayList(); - ArrayList statesL = new ArrayList(); - for (int k = 0; k < dra[i].getNumAcceptancePairs(); k++) { - JDDNode tmpH = JDD.Constant(0); - JDDNode tmpL = JDD.Constant(0); - for (j = 0; j < dra[i].size(); j++) { - if (!dra[i].getAcceptanceL(k).get(j)) { - tmpH = JDD.SetVectorElement(tmpH, draDDRowVars[i], j, 1.0); - } - if (dra[i].getAcceptanceK(k).get(j)) { - tmpL = JDD.SetVectorElement(tmpL, draDDRowVars[i], j, 1.0); - } - } - statesH.add(tmpH); - JDD.Ref(tmpH); - acceptanceVector_H = JDD.Or(acceptanceVector_H, tmpH); - statesL.add(tmpL); - JDD.Ref(tmpL); - acceptanceVector_L = JDD.Or(acceptanceVector_L, tmpL); - } - allstatesH.add(i, statesH); - allstatesL.add(i, statesL); + //check if there are state rewards and display a warning + if (stateRewards != null && !stateRewards.equals(JDD.ZERO)) + throw new PrismException("Multi-objective model checking does not support state rewards; please convert to transition rewards"); + if (transRewards == null) + throw new PrismException("Invalid reward structure index \"" + rs + "\""); + rewardsIndex.add(transRewards); + } else { + throw new PrismException("Multi-objective properties can only contain P and R operators"); + } + // Get the cumulative step bound for reward + if (exprReward != null) { + exprTemp = (ExpressionTemporal) exprReward.getExpression(); + + // We only allow C or C<=k reward operators, others such as F are not supported currently + if (exprTemp.getOperator() != ExpressionTemporal.R_C) { + throw new PrismException("Reward operators in multi-objective properties must be C or C<=k (" + exprTemp.getOperatorSymbol() + + " is not yet supported)"); + } + + if (exprTemp.getUpperBound() != null) { + //This is the case of C<=k + stepBound = exprTemp.getUpperBound().evaluateInt(constantValues); } else { - allstatesH.add(i, null); - allstatesL.add(i, null); + //Here we just have C + stepBound = -1; } + /*if (exprTemp.getOperator() != ExpressionTemporal.R_F) { + throw new PrismException("Multi-objective only supports F operator for rewards"); + }*/ } - - // Find accepting maximum end components for each LTL formula - List allecs = null; - //use acceptanceVector_H and acceptanceVector_L to speed up scc computation - /*// check number of states in each scc - allecs = mcLtl.findEndComponents(modelProduct, modelProduct.getReach()); - StateListMTBDD vl; - int totalNum = 0; - for(JDDNode set : allecs) { - vl = new StateListMTBDD(set, modelProduct); - totalNum += vl.size() - 1; - } - mainLog.println("Total number of states can be saved: " + totalNum);*/ - - JDD.Ref(acceptanceVector_H); - JDD.Ref(modelProduct.getTrans01()); - JDDNode candidateStates = JDD.Apply(JDD.TIMES, modelProduct.getTrans01(), acceptanceVector_H); - for (i = 0; i < numTargets; i++) - if (!reachExpr[i]) { - acceptanceVector_H = JDD.PermuteVariables(acceptanceVector_H, draDDRowVars[i], draDDColVars[i]); + if (exprProb != null) {// || ((ExpressionTemporal) exprReward.getExpression()).getOperator() != ExpressionTemporal.R_C) { + exprTemp = (ExpressionTemporal) exprProb.getExpression(); + //TODO we currently ignore the lower bound + if (exprTemp.getUpperBound() != null) { + stepBound = exprTemp.getUpperBound().evaluateInt(constantValues); } - candidateStates = JDD.Apply(JDD.TIMES, candidateStates, acceptanceVector_H); - candidateStates = JDD.ThereExists(candidateStates, modelProduct.getAllDDColVars()); - candidateStates = JDD.ThereExists(candidateStates, modelProduct.getAllDDNondetVars()); - // find all maximal end components - allecs = mcLtl.findMECStates(modelProduct, candidateStates, acceptanceVector_L); - JDD.Deref(candidateStates); - JDD.Deref(acceptanceVector_L); - - for (i = 0; i < numTargets; i++) { - if (!reachExpr[i]) { - //mainLog.println("\nFinding accepting end components for " + targetName[i] + "..."); - l = System.currentTimeMillis(); - // increase ref count for checking conflict formulas - if (conflictformulae > 1) { - List tmpLH = allstatesH.get(i); - for (JDDNode n : tmpLH) - JDD.Ref(n); - tmpLH = allstatesL.get(i); - for (JDDNode n : tmpLH) - JDD.Ref(n); - } - targetDDs.add(mcLtl.findMultiAcceptingStates(dra[i], modelProduct, draDDRowVars[i], draDDColVars[i], false, allecs, allstatesH.get(i), - allstatesL.get(i))); - //targetDDs.add(mcLtl.findMultiAcceptingStates(dra[i], modelProduct, draDDRowVars[i], draDDColVars[i], false)); - l = System.currentTimeMillis() - l; - mainLog.println("Time for end component identification: " + l / 1000.0 + " seconds."); - } /*else { - // Fixme: maybe not efficient - if(targetExprs.get(i) != null) { - dd = checkExpressionDD(targetExprs.get(i)); - JDD.Ref(modelProduct.getReach()); - dd = JDD.And(dd, modelProduct.getReach()); - targetDDs.add(dd); - } - }*/ - //mainLog.print("\n number of targets = " + JDD.GetNumMintermsString(targetDDs.get(i), modelProduct.getAllDDRowVars().n())); - //if(i>0) - // mainLog.print("\n total number of targets = " + - // JDD.GetNumMintermsString(JDD.Or(targetDDs.get(i), targetDDs.get(i-1)), modelProduct.getAllDDRowVars().n())); + else + stepBound = -1; + } + + // Get info from P/R operator + // Store relational operator + if (relOp.isStrict()) + throw new PrismException("Multi-objective properties can not use strict inequalities on P/R operators"); + Operator op; + if (relOp == RelOp.MAX) { + op = (exprProb != null) ? Operator.P_MAX : Operator.R_MAX; + } else if (relOp == RelOp.GEQ) { + op = (exprProb != null) ? Operator.P_GE : Operator.R_GE; + } else if (relOp == RelOp.MIN) { + op = (exprProb != null) ? Operator.P_MIN : Operator.R_MIN; + } else if (relOp == RelOp.LEQ) { + op = (exprProb != null) ? Operator.P_LE : Operator.R_LE; + } else + throw new PrismException("Multi-objective properties can only contain P/R operators with max/min=? or lower/upper probability bounds"); + // Store probability/rewards bound + Expression pb = (exprProb != null) ? exprProb.getProb() : exprReward.getReward(); + if (pb != null) { + double p = pb.evaluateDouble(constantValues); + if ((exprProb != null) && (p < 0 || p > 1)) + throw new PrismException("Invalid probability bound " + p + " in P operator"); + if ((exprProb == null) && (p < 0)) + throw new PrismException("Invalid reward bound " + p + " in P operator"); + if (exprProb != null && relOp == RelOp.LEQ) + p = 1 - p; + + opsAndBounds.add(op, p, stepBound); + } else { + opsAndBounds.add(op, -1.0, stepBound); + } + + // Now extract targets + // Also store which ones are just reachability (in reachExpr) + if (exprProb != null) { + targetExprs.add(exprProb.getExpression()); + // TODO check if the following line is unneeded: it only kept track of probs vs rewards + // reachExpr[i] = false; + targetName.add(exprProb.getExpression().toString()); + } else { + targetExprs.add(null); + // TODO check if the following line is unneeded: it only kept track of probs vs rewards + // reachExpr[i] = true; + targetName.add(""); } + } - // check if there are conflicts in objectives - if (conflictformulae > 1) { - DRA[] tmpdra = new DRA[conflictformulae]; - JDDVars[] tmpdraDDRowVars = new JDDVars[conflictformulae]; - JDDVars[] tmpdraDDColVars = new JDDVars[conflictformulae]; - List tmptargetDDs = new ArrayList(conflictformulae); - List> tmpallstatesH = new ArrayList>(conflictformulae); - List> tmpallstatesL = new ArrayList>(conflictformulae); - int count = 0; - for (i = 0; i < numTargets; i++) - if (!reachExpr[i]) { - tmpdra[count] = dra[i]; - tmpdraDDRowVars[count] = draDDRowVars[i]; - tmpdraDDColVars[count] = draDDColVars[i]; - // tricky part; double check when reachExpr is set for efficiency - tmptargetDDs.add(targetDDs.get(count)); - tmpallstatesH.add(allstatesH.get(i)); - tmpallstatesL.add(allstatesL.get(i)); - count++; - } - //multitargetDDs = new ArrayList(); - List> tmpmultitargetIDs = new ArrayList>(); - - mcLtl.findMultiConflictAcceptingStates(tmpdra, modelProduct, tmpdraDDRowVars, tmpdraDDColVars, tmptargetDDs, tmpallstatesH, tmpallstatesL, - multitargetDDs, tmpmultitargetIDs); - // again. double check when reachExpr is set - count = 0; - for (i = 0; i < numTargets; i++) - if (!reachExpr[i]) { - targetDDs.remove(count); - targetDDs.add(count, tmptargetDDs.get(count)); - count++; - } + protected void addDummyFormula(NondetModel modelProduct, LTLModelChecker mcLtl, List targetDDs, OpsAndBoundsList opsAndBounds) + throws PrismException + { + List tmpecs = mcLtl.findMECStates(modelProduct, modelProduct.getReach()); + JDDNode acceptingStates = JDD.Constant(0); + for (JDDNode set : tmpecs) + acceptingStates = JDD.Or(acceptingStates, set); + targetDDs.add(acceptingStates); + opsAndBounds.add(Operator.P_GE, 0.0, -1); + } - // deal with reachability targets - //multitargetIDs = new ArrayList(tmpmultitargetIDs.size()); - for (i = 0; i < tmpmultitargetIDs.size(); i++) { - multitargetIDs.add(changeToInteger(tmpmultitargetIDs.get(i))); - } + //Prints info about the product model in multi-objective + protected void outputProductMulti(NondetModel modelProduct) throws PrismException + { + // Print product info + mainLog.println(); + modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo()); - for (i = 0; i < numTargets; i++) - if (!reachExpr[i]) { - List tmpLH = allstatesH.get(i); - for (JDDNode n : tmpLH) - JDD.Deref(n); - tmpLH = allstatesL.get(i); - for (JDDNode n : tmpLH) - JDD.Deref(n); - } + // Output product, if required + if (prism.getExportProductTrans()) { + try { + mainLog.println("\nExporting product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"..."); + prism.exportTransToFile(modelProduct, true, Prism.EXPORT_PLAIN, new File(prism.getExportProductTransFilename())); + } catch (FileNotFoundException e) { + mainLog.printWarning("Could not export product transition matrix to file \"" + prism.getExportProductTransFilename() + "\""); + } + } + if (prism.getExportProductStates()) { + try { + mainLog.println("\nExporting product state space to file \"" + prism.getExportProductStatesFilename() + "\"..."); + prism.exportStatesToFile(modelProduct, Prism.EXPORT_PLAIN, new File(prism.getExportProductStatesFilename())); + } catch (FileNotFoundException e) { + mainLog.printWarning("Could not export product state space to file \"" + prism.getExportProductStatesFilename() + "\""); + } } - - for (JDDNode ec : allecs) - JDD.Deref(ec); } // Model checking functions @@ -1993,176 +1551,6 @@ public class NondetModelChecker extends NonProbModelChecker return probs; } - // compute (max) probabilities for multi-objective reachability - - protected Object computeMultiReachProbs(NondetModel modelProduct, LTLModelChecker mcLtl, List rewards, JDDNode st, 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 = this.engine; - - //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(); - - JDDNode labels[] = new JDDNode[n]; - String labelNames[] = new String[n]; - // Build temporary DDs for combined targets - for (i = 0; i < n; i++) { - JDD.Ref(targets.get(i)); - JDDNode tmp = targets.get(i); - if (combinations != null) { - for (j = 0; j < combinations.size(); j++) { - if ((combinationIDs.get(j) & (1 << i)) > 0) { - JDD.Ref(combinations.get(j)); - tmp = JDD.Or(tmp, combinations.get(j)); - } - } - } - labels[i] = tmp; - labelNames[i] = "target" + i; - } - - if (prism.getExportTarget()) { - try { - mainLog.print("\nExporting target states info to file \"" + prism.getExportTargetFilename() + "\"..."); - PrismMTBDD.ExportLabels(labels, labelNames, "l", modelProduct.getAllDDRowVars(), modelProduct.getODD(), Prism.EXPORT_PLAIN, - prism.getExportTargetFilename()); - } catch (FileNotFoundException e) { - mainLog.println("\nWarning: Could not export target to file \"" + prism.getExportTargetFilename() + "\""); - } - } - - // yes - union of targets (just to compute no) - yes = JDD.Constant(0); - //n = targets.size(); - for (i = 0; i < n; i++) { - JDD.Ref(targets.get(i)); - yes = JDD.Or(yes, targets.get(i)); - } - if (combinations != null) - for (i = 0; i < combinations.size(); i++) { - JDD.Ref(combinations.get(i)); - yes = JDD.Or(yes, combinations.get(i)); - } - - if (opsAndBounds.rewardSize() == 0) - no = PrismMTBDD.Prob0A(modelProduct.getTrans01(), modelProduct.getReach(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), modelProduct.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); - JDD.Deref(bottomec); - bottomec = JDD.Constant(0); - for (JDDNode ec : becs) - bottomec = JDD.Or(bottomec, ec); - } - - /*if(op1>2) { // the first query is about reward - JDDNode no_r = PrismMTBDD.Prob0A(modelProduct.getTrans01(), modelProduct.getReach(), - modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), modelProduct.getReach(), targets.get(0)); - JDD.Ref(no_r); - maybe_r = JDD.And(modelProduct.getReach(), JDD.Not(JDD.Or(targets.get(0), no_r))); - trr = modelProduct.getTransRewards(); - }*/ - - // maybe - JDD.Ref(modelProduct.getReach()); - JDD.Ref(yes); - JDD.Ref(no); - maybe = JDD.And(modelProduct.getReach(), JDD.Not(JDD.Or(yes, no))); - - for (i = 0; i < rewards.size(); i++) { - JDDNode tmp = rewards.remove(i); - JDD.Ref(no); - tmp = JDD.Apply(JDD.TIMES, tmp, JDD.Not(no)); - rewards.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"); - - // compute probabilities - mainLog.println("\nComputing remaining probabilities..."); - // 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) - throw new PrismException("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 PrismException("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); - } else { - value = PrismSparse.NondetMultiReachReward(modelProduct.getTrans(), modelProduct.getTransActions(), modelProduct.getSynchs(), - modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), - targets, opsAndBounds, maybe, st, rewards, 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); - } else { - value = PrismSparse.NondetMultiReach(modelProduct.getTrans(), modelProduct.getTransActions(), modelProduct.getSynchs(), - modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), - targets, opsAndBounds, maybe, st); - } - } - } 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); - 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); - } - } catch (PrismException e) { - throw e; - } finally { - // derefs - if (opsAndBounds.rewardSize() > 0) - JDD.Deref(bottomec); - JDD.Deref(yes); - JDD.Deref(no); - 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)); - } - } - - return value; - } - // compute cumulative rewards protected StateValues computeCumulRewards(JDDNode tr, JDDNode sr, JDDNode trr, int time, boolean min) throws PrismException @@ -2407,525 +1795,6 @@ public class NondetModelChecker extends NonProbModelChecker return result; } - private int changeToInteger(List ids) - { - int k = 0; - for (int i = 0; i < ids.size(); i++) { - int j = 1; - if (ids.get(i) > 0) - j = j << ids.get(i); - k += j; - } - return k; - } - - protected Object weightedMultiReachProbs(NondetModel modelProduct, JDDNode yes_ones, JDDNode maybe, JDDNode st, 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 3"); - - 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"); - - 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 - { - int numberOfPoints = 0; - 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; - - //convert minimizing rewards to maximizing - for (int i = 0; i < opsAndBounds.rewardSize(); i++) { - if (opsAndBounds.getRewardOperator(i) == Operator.R_LE) { - JDDNode negated = JDD.Apply(JDD.TIMES, JDD.Constant(-1), rewards.get(i)); - //JDD.Ref(negated); - 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); - rewards.set(i, negated); - //boundsRewards.set(i, -1 * boundsRewards.get(i)); - } - } - - double tolerance = prism.getSettings().getDouble(PrismSettings.PRISM_PARETO_EPSILON); - int maxIters = prism.getSettings().getInteger(PrismSettings.PRISM_MULTI_MAX_POINTS); - - NativeIntArray adversary = new NativeIntArray((int) modelProduct.getNumStates()); - int dimProb = targets.length; - int dimReward = rewards.size(); - Point targetPoint = new Point(dimProb + dimReward); - ArrayList computedPoints = new ArrayList(); - ArrayList computedDirections = new ArrayList(); - ArrayList pointsForInitialTile = new ArrayList(); - - //create vectors and sparse matrices for the objectives - final DoubleVector[] probDoubleVectors = new DoubleVector[dimProb]; - final NDSparseMatrix[] rewSparseMatrices = new NDSparseMatrix[dimReward]; - - JDD.Ref(modelProduct.getTrans()); - JDD.Ref(modelProduct.getReach()); - - //create a sparse matrix for transitions - JDDNode a = JDD.Apply(JDD.TIMES, modelProduct.getTrans(), modelProduct.getReach()); - - if (!min) { - JDD.Ref(a); - JDDNode tmp = JDD.And(JDD.Equals(a, 1.0), JDD.Identity(modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars())); - a = JDD.ITE(tmp, JDD.Constant(0), a); - } - - NDSparseMatrix trans_matrix = NDSparseMatrix.BuildNDSparseMatrix(a, modelProduct.getODD(), modelProduct.getAllDDRowVars(), - modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars()); - - //create double vectors for probabilistic objectives - for (int i = 0; i < dimProb; i++) { - probDoubleVectors[i] = new DoubleVector(targets[i], modelProduct.getAllDDRowVars(), modelProduct.getODD()); - } - - //create sparse matrices for reward objectives - for (int i = 0; i < dimReward; i++) { - NDSparseMatrix rew_matrix = NDSparseMatrix.BuildSubNDSparseMatrix(a, modelProduct.getODD(), modelProduct.getAllDDRowVars(), - modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), rewards.get(i)); - rewSparseMatrices[i] = rew_matrix; - } - - JDD.Deref(a); - - 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) { - //System.out.println("Doing GS"); - result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, new DoubleVector[] {probDoubleVectors[i]}, new int[] {probStepBounds[i]}, null, - new double[] { 1.0 }, null); - } else { - //System.out.println("Not doing GS"); - result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, new DoubleVector[] {probDoubleVectors[i]}, new int[] {probStepBounds[i]}, null, - new double[] { 1.0 }, null); - }*/ - 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); - } else { - 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) - throw new PrismException("The probabilistic objective number " + i + " is degenerate since the optimal value is also the least optimal value." ); - */ - targetPoint = new Point(result); - pointsForInitialTile.add(targetPoint); - } - - for (int i = 0; i < dimReward; i++) { - if (verbose) { - mainLog.println("Getting an upper bound on maximizing objective " + i); - } - - double[] result; - double[] weights = new double[dimProb + dimReward]; - weights[i] = 1.0; - /*System.out.println(prism.getMDPSolnMethod()); - if (prism.getMDPSolnMethod() == 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[i] }, - new double[] { 1.0 }, new int[] { rewardStepBounds[i] }); - } 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[i] }, - new double[] { 1.0 }, new int[] { rewardStepBounds[i] }); - }*/ - 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); - } else { - 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; - int output = 0; - while (iters < maxIters) { - iters++; - - //create the weights array - double[] weights = new double[dimProb + dimReward]; - for (int i = 0; i < dimProb + dimReward; i++) { - weights[i] = direction.getCoord(i); - } - - 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); - } else { - 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]); - } - } */ - - numberOfPoints++; - - //collect the numbers obtained from methods executed above. - Point newPoint = new Point(result); - - if (verbose) { - mainLog.println("\n" + numberOfPoints + ": New point is " + newPoint + "."); - mainLog.println("TileList:" + tileList); - } - - computedPoints.add(newPoint); - computedDirections.add(direction); - - tileList.addNewPoint(newPoint); - //mainLog.println("\nTiles after adding: " + tileList); - //compute new direction - direction = tileList.getCandidateHyperplane(); - - if (verbose) { - mainLog.println("New direction is " + direction); - //mainLog.println("TileList: " + tileList); - - } - - if (direction == null) { - //no tile could be improved - decided = true; - break; - } - } - - timer = System.currentTimeMillis() - timer; - mainLog.println("The value iteration(s) took " + timer / 1000.0 + " seconds altogether."); - mainLog.println("Number of weight vectors used: " + numberOfPoints); - - if (!decided) - throw new PrismException("The computation did not finish in " + maxIters - + " target point iterations, try increasing this number using the -multimaxpoints switch."); - else { - String paretoFile = prism.getSettings().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()); - - return tileList; - } - } - - protected double targetDrivenMultiReachProbs(NondetModel modelProduct, JDDNode yes_ones, JDDNode maybe, final JDDNode st, JDDNode[] targets, - List rewards, OpsAndBoundsList opsAndBounds) throws PrismException - { - int numberOfPoints = 0; - 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; - - //convert minimizing rewards to maximizing - for (int i = 0; i < opsAndBounds.rewardSize(); i++) { - if (opsAndBounds.getRewardOperator(i) == Operator.R_LE) { - JDDNode negated = JDD.Apply(JDD.TIMES, JDD.Constant(-1), rewards.get(i)); - //JDD.Ref(negated); - 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); - rewards.set(i, negated); - //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); - - int maxIters = prism.getSettings().getInteger(PrismSettings.PRISM_MULTI_MAX_POINTS); - - NativeIntArray adversary = new NativeIntArray((int) modelProduct.getNumStates()); - int dimProb = targets.length; - int dimReward = rewards.size(); - Point targetPoint = new Point(dimProb + dimReward); - ArrayList computedPoints = new ArrayList(); - ArrayList computedDirections = new ArrayList(); - - ArrayList pointsForInitialTile = new ArrayList(); - - //create vectors and sparse matrices for the objectives - final DoubleVector[] probDoubleVectors = new DoubleVector[dimProb]; - final NDSparseMatrix[] rewSparseMatrices = new NDSparseMatrix[dimReward]; - - JDD.Ref(modelProduct.getTrans()); - JDD.Ref(modelProduct.getReach()); - - //create a sparse matrix for transitions - JDDNode a = JDD.Apply(JDD.TIMES, modelProduct.getTrans(), modelProduct.getReach()); - - if (!min) { - JDD.Ref(a); - JDDNode tmp = JDD.And(JDD.Equals(a, 1.0), JDD.Identity(modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars())); - a = JDD.ITE(tmp, JDD.Constant(0), a); - } - - NDSparseMatrix trans_matrix = NDSparseMatrix.BuildNDSparseMatrix(a, modelProduct.getODD(), modelProduct.getAllDDRowVars(), - modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars()); - - //create double vectors for probabilistic objectives - for (int i = 0; i < dimProb; i++) { - probDoubleVectors[i] = new DoubleVector(targets[i], modelProduct.getAllDDRowVars(), modelProduct.getODD()); - } - - //create sparse matrices for reward objectives - for (int i = 0; i < dimReward; i++) { - NDSparseMatrix rew_matrix = NDSparseMatrix.BuildSubNDSparseMatrix(a, modelProduct.getODD(), modelProduct.getAllDDRowVars(), - modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), rewards.get(i)); - rewSparseMatrices[i] = rew_matrix; - } - - JDD.Deref(a); - - //initialize the target point - for (int i = 0; i < dimProb; i++) { - targetPoint.setCoord(i, opsAndBounds.getProbBound(i)); - } - if (maximizingProb) { - targetPoint.setCoord(0, 1.0); - } - - for (int i = 0; i < dimReward; i++) { - //multiply by -1 in case of minimizing, that converts it to maximizing. - double t = (opsAndBounds.getRewardOperator(i) == Operator.R_LE) ? -opsAndBounds.getRewardBound(i) : opsAndBounds.getRewardBound(i); - targetPoint.setCoord(i + dimProb, t); - } - if (maximizingReward) { - if (verbose) { - mainLog.println("Getting an upper bound on maximizing objective"); - } - - double[] result; - if (prism.getMDPSolnMethod() == 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] }); - } 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] }); - } - numberOfPoints++; - - targetPoint.setCoord(dimProb, result[0]); - - if (verbose) { - mainLog.println("Upper bound is " + result[0]); - } - } - - Point direction = MultiObjUtils.getWeights(targetPoint, computedPoints); - - if (verbose) { - mainLog.println("The initial target point is " + targetPoint); - mainLog.println("The initial direction is " + direction); - } - - boolean decided = false; - boolean isAchievable = false; - int iters = 0; - int output = 0; - while (iters < maxIters) { - iters++; - - //create the weights array - double[] weights = new double[dimProb + dimReward]; - for (int i = 0; i < dimProb + dimReward; i++) { - weights[i] = direction.getCoord(i); - } - - 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); - } else { - 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); - - if (verbose) { - mainLog.println("New point is " + newPoint + "."); - } - - computedPoints.add(newPoint); - computedDirections.add(direction); - - - //if (prism.getExportMultiGraphs()) - // MultiObjUtils.printGraphFileDebug(targetPoint, computedPoints, computedDirections, prism.getExportMultiGraphsDir(), output++); - - //check if the new point together with the direction shows the point is unreachable - double dNew = 0.0; - for (int i = 0; i < dimProb + dimReward; i++) { - dNew += newPoint.getCoord(i) * direction.getCoord(i); - } - - double dTarget = 0.0; - for (int i = 0; i < dimProb + dimReward; i++) { - dTarget += targetPoint.getCoord(i) * direction.getCoord(i); - } - - if (dTarget > dNew) { - if (maximizingProb || maximizingReward) { - int maximizingCoord = (maximizingProb) ? 0 : dimProb; - double rest = dNew - (dTarget - direction.getCoord(maximizingCoord) * targetPoint.getCoord(maximizingCoord)); - if ((!maximizingNegated && rest < 0) || (maximizingNegated && rest > 0)) { - //target can't be lowered - decided = true; - targetPoint.setCoord(maximizingCoord, Double.NaN); - if (verbose) - mainLog.println("Decided, target is " + targetPoint); - break; - } else { - double lowered = rest / direction.getCoord(maximizingCoord); - targetPoint.setCoord(maximizingCoord, lowered); - //HACK - if (lowered == Double.NEGATIVE_INFINITY) { - targetPoint.setCoord(maximizingCoord, Double.NaN); - mainLog.println("\nThe constraints are not achievable!\n"); - decided = true; - isAchievable = false; - break; - } - if (verbose) - mainLog.println("Target lowered to " + targetPoint); - - //if (prism.getExportMultiGraphs()) - // MultiObjUtils.printGraphFileDebug(targetPoint, computedPoints, computedDirections, prism.getExportMultiGraphsDir(), output++); - } - } else { - decided = true; - isAchievable = false; - break; - } - } - - //compute new direction - direction = MultiObjUtils.getWeights(targetPoint, computedPoints); - - if (verbose) { - mainLog.println("New direction is " + direction); - } - - if (direction == null || computedDirections.contains(direction)) //The second disjunct is for convergence - { - //there is no hyperplane strictly separating the target from computed points - //hence we can conclude that the point is reachable - decided = true; - isAchievable = true; - break; - } - } - - timer = System.currentTimeMillis() - timer; - mainLog.println("The value iteration(s) took " + timer / 1000.0 + " seconds altogether."); - mainLog.println("Number of weight vectors used: " + numberOfPoints); - - if (!decided) - throw new PrismException("The computation did not finish in " + maxIters - + " target point iterations, try increasing this number using the -multimaxpoints switch."); - if (maximizingProb || maximizingReward) { - int maximizingCoord = (maximizingProb) ? 0 : dimProb; - return (maximizingNegated) ? -targetPoint.getCoord(maximizingCoord) : targetPoint.getCoord(maximizingCoord); - } else { - return (isAchievable) ? 1.0 : 0.0; - } - } }