diff --git a/prism/src/prism/ECComputer.java b/prism/src/prism/ECComputer.java new file mode 100644 index 00000000..e7cd552a --- /dev/null +++ b/prism/src/prism/ECComputer.java @@ -0,0 +1,83 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford, formerly University of Birmingham) +// * Carlos S. Bederian (Universidad Nacional de Cordoba) +// * Mark Kattenbelt (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.util.Vector; + +import jdd.*; + +// interface for end-component computing classes + +public abstract class ECComputer +{ + protected Prism prism; + protected PrismLog mainLog; + + // model info + protected JDDNode trans; + protected JDDNode trans01; + protected JDDNode reach; + protected JDDVars allDDRowVars; + protected JDDVars allDDColVars; + protected JDDVars allDDNondetVars; + + // stuff for ECs + protected Vector vectECs; + protected JDDNode notInECs; + + // Constructor + /** + * Find maximal EC of a sub-MDP by restricting reach and trans01. + * This sub-MDP needs to be deadlock-free. + */ + public ECComputer(Prism prism, JDDNode reach, JDDNode trans, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars allDDNondetVars) + { + this.prism = prism; + mainLog = prism.getMainLog(); + this.reach = reach; + this.trans = trans; + this.trans01 = trans01; + this.allDDRowVars = allDDRowVars; + this.allDDColVars = allDDColVars; + this.allDDNondetVars = allDDNondetVars; + } + + // Get vector of EndComponents + // NB: these BDDs aren't derefed by EndComponentComputer classes + public Vector getVectECs() { return vectECs; } + + // Get states not in any EndComponent + // NB: this BDD isn't derefed by SCCComputer classes + //public JDDNode getNotInECs() { return notInECs; } + + // End Components (EC) computation + // NB: This creates BDDs, obtainable from getVectECs() and getNotInECs(), + // which the calling code is responsible for dereferencing. + public abstract void computeECs(); +} diff --git a/prism/src/prism/ECComputerDefault.java b/prism/src/prism/ECComputerDefault.java new file mode 100644 index 00000000..33d2fec2 --- /dev/null +++ b/prism/src/prism/ECComputerDefault.java @@ -0,0 +1,187 @@ +package prism; + +import java.util.Stack; +import java.util.Vector; + +import jdd.JDD; +import jdd.JDDNode; +import jdd.JDDVars; + +public class ECComputerDefault extends ECComputer +{ + public ECComputerDefault(Prism prism, JDDNode reach, JDDNode trans, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars, + JDDVars allDDNondetVars) + { + super(prism, reach, trans, trans01, allDDRowVars, allDDColVars, allDDNondetVars); + } + + public void computeECs() + { + vectECs = new Vector(); + + boolean initialCandidate = true; + Stack candidates = new Stack(); + JDD.Ref(reach); + candidates.push(reach); + SCCComputer sccComputer; + + while (!candidates.isEmpty()) + { + System.out.println("Checking candidate"); + + JDDNode candidate = candidates.pop(); + + // Compute the stable set + JDD.Ref(candidate); + JDDNode stableSet = findMaximalStableSet(candidate); + + System.out.println("found max stable set"); + + // Drop empty sets + if (stableSet.equals(JDD.ZERO)) + { + System.out.println("empty set"); + JDD.Deref(stableSet); + JDD.Deref(candidate); + continue; + } + + if (!initialCandidate) + { + System.out.println("not initial"); + + // candidate is an SCC, check if it's stable + if (stableSet.equals(candidate)) + { + vectECs.add(maxStableSetChoices(candidate)); + JDD.Deref(stableSet); + continue; + } + } + else + { + initialCandidate = false; + } + + JDD.Deref(candidate); + + // Filter bad transitions + JDD.Ref(stableSet); + JDDNode stableSetTrans = maxStableSetTrans(stableSet); + + // now find the maximal SCCs in (stableSet, stableSetTrans) + Vector sccs; + sccComputer = prism.getSCCComputer(stableSet, stableSetTrans, allDDRowVars, allDDColVars); + sccComputer.computeSCCs(); + JDD.Deref(stableSet); + JDD.Deref(stableSetTrans); + sccs = sccComputer.getVectSCCs(); + JDD.Deref(sccComputer.getNotInSCCs()); + candidates.addAll(sccs); + } + } + + /** + * Returns a stable set of states contained in candidateStates + * + * @param candidateStates + * set of candidate states S x H_i (dereferenced after calling this function) + * @return a referenced BDD with the maximal stable set in c + */ + private JDDNode findMaximalStableSet(JDDNode candidateStates) + { + System.out.println("findMaximalStableSet"); + + + + JDDNode old = JDD.Constant(0); + JDDNode current = candidateStates; + + if (current.isConstant()) + System.out.println("current = " + current.getValue()); + + while (!current.equals(old)) + { + JDD.Deref(old); + JDD.Ref(current); + old = current; + + JDD.Ref(current); + JDD.Ref(trans); + // Select transitions starting in current + JDDNode currTrans = JDD.Apply(JDD.TIMES, trans, current); + // Select transitions starting in current and ending in current + JDDNode tmp = JDD.PermuteVariables(current, allDDRowVars, allDDColVars); + tmp = JDD.Apply(JDD.TIMES, currTrans, tmp); + // Sum all successor probabilities for each (state, action) tuple + tmp = JDD.SumAbstract(tmp, allDDColVars); + // If the sum for a (state,action) tuple is 1, + // there is an action that remains in the stable set with prob 1 + tmp = JDD.GreaterThan(tmp, 1 - prism.getSumRoundOff()); + // Without fairness, we just need one action per state + current = JDD.ThereExists(tmp, allDDNondetVars); + } + JDD.Deref(old); + return current; + } + + /** + * Returns the transition relation of a stable set + * + * @param b + * BDD of a stable set (dereferenced after calling this function) + * @return referenced BDD of the transition relation restricted to the stable set + */ + private JDDNode maxStableSetTrans(JDDNode b) + { + System.out.println("maxStableSetTrans"); + JDD.Ref(b); + JDD.Ref(trans); + // Select transitions starting in b + JDDNode currTrans = JDD.Apply(JDD.TIMES, trans, b); + JDDNode mask = JDD.PermuteVariables(b, allDDRowVars, allDDColVars); + // Select transitions starting in current and ending in current + mask = JDD.Apply(JDD.TIMES, currTrans, mask); + // Sum all successor probabilities for each (state, action) tuple + mask = JDD.SumAbstract(mask, allDDColVars); + // If the sum for a (state,action) tuple is 1, + // there is an action that remains in the stable set with prob 1 + mask = JDD.GreaterThan(mask, 1 - prism.getSumRoundOff()); + // select the transitions starting in these tuples + JDD.Ref(trans01); + JDDNode stableTrans01 = JDD.And(trans01, mask); + // Abstract over actions + return JDD.ThereExists(stableTrans01, allDDNondetVars); + } + + /** + * Returns the transition relation of a stable set + * + * @param b + * BDD of a stable set (dereferenced after calling this function) + * @return referenced BDD of the transition relation restricted to the stable set + */ + public JDDNode maxStableSetChoices(JDDNode b) + { + System.out.println("maxStableSetChoices"); + + JDD.Ref(b); + JDD.Ref(trans); + // Select transitions starting in b + JDDNode currTrans = JDD.Apply(JDD.TIMES, trans, b); + JDDNode mask = JDD.PermuteVariables(b, allDDRowVars, allDDColVars); + // Select transitions starting in current and ending in current + mask = JDD.Apply(JDD.TIMES, currTrans, mask); + // Sum all successor probabilities for each (state, action) tuple + mask = JDD.SumAbstract(mask, allDDColVars); + // If the sum for a (state,action) tuple is 1, + // there is an action that remains in the stable set with prob 1 + mask = JDD.GreaterThan(mask, 1 - prism.getSumRoundOff()); + // select the transitions starting in these tuples + JDD.Ref(trans01); + JDDNode stableTrans01 = JDD.And(trans01, mask); + // Abstract over actions + return JDD.ThereExists(stableTrans01, allDDColVars); + } + +} diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 0ccd2779..c4bd584e 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1077,6 +1077,8 @@ public class NondetModelChecker extends NonProbModelChecker DoubleVector rewardsDV; StateProbs rewards = null; + Vector zeroCostEndComponents = null; + // compute states which can't reach goal with probability 1 if (b.equals(JDD.ZERO)) { JDD.Ref(reach); @@ -1096,6 +1098,33 @@ public class NondetModelChecker extends NonProbModelChecker JDD.Ref(reach); inf = JDD.And(reach, JDD.Not(prob1)); } else { + + if (prism.getCheckZeroLoops()) + { + // find states transitions that have no cost + JDD.Ref(sr); + JDD.Ref(reach); + JDDNode zeroReach = JDD.And(reach, JDD.Apply(JDD.EQUALS, sr, JDD.Constant(0))); + JDD.Ref(b); + zeroReach = JDD.And(zeroReach, JDD.Not(b)); + JDD.Ref(trr); + JDDNode zeroTrr = JDD.Apply(JDD.EQUALS, trr, JDD.Constant(0)); + JDD.Ref(trans); + JDD.Ref(zeroTrr); + JDDNode zeroTrans = JDD.And(trans, zeroTrr); + JDD.Ref(trans01); + JDDNode zeroTrans01 = JDD.And(trans01, zeroTrr); + + ECComputer ecComp = new ECComputerDefault(prism, zeroReach, zeroTrans, zeroTrans01, model.getAllDDRowVars(), model.getAllDDColVars(), model.getAllDDNondetVars()); + ecComp.computeECs(); + + zeroCostEndComponents = ecComp.getVectECs(); + + JDD.Deref(zeroReach); + JDD.Deref(zeroTrans); + JDD.Deref(zeroTrans01); + } + // compute states for which all adversaries don't reach goal with probability 1 no = PrismMTBDD.Prob0A(tr01, reach, allDDRowVars, allDDColVars, allDDNondetVars, reach, b); prob1 = PrismMTBDD.Prob1E(tr01, reach, allDDRowVars, allDDColVars, allDDNondetVars, reach, b, no); @@ -1109,8 +1138,15 @@ public class NondetModelChecker extends NonProbModelChecker maybe = JDD.And(reach, JDD.Not(JDD.Or(inf, b))); } - // need to deal with zero loops yet - if (min) { + if (prism.getCheckZeroLoops()) + { + // need to deal with zero loops yet + if (min && zeroCostEndComponents != null && zeroCostEndComponents.size() > 0) { + mainLog.println("\nWarning: PRISM detected your model contains " + zeroCostEndComponents.size() + " zero-reward " + ((zeroCostEndComponents.size() == 1) ? "loop." : "loops.")); + mainLog.println("Your minimum rewards may be too low..."); + } + } + else if (min) { mainLog.println("\nWarning: PRISM hasn't checked for zero-reward loops."); mainLog.println("Your minimum rewards may be too low..."); } @@ -1156,6 +1192,11 @@ public class NondetModelChecker extends NonProbModelChecker throw e; } } + + if (zeroCostEndComponents != null) + for (JDDNode zcec : zeroCostEndComponents) + JDD.Deref(zcec); + // derefs JDD.Deref(inf); diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 5ae9da0e..fc52c75f 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -99,6 +99,7 @@ public class Prism implements PrismSettingsListener private boolean doReach; // do reachability? (sometimes might want to skip it) private boolean bsccComp; // do bscc computation before steady-state? + private boolean checkZeroLoops; // MTBDD construction method (NOW DEFUNCT) // 1 - use with ordering 1: nondet vars form a tree at the top @@ -143,6 +144,8 @@ public class Prism implements PrismSettingsListener //------------------------------------------------------------------------------ private boolean cuddStarted = false; + + //------------------------------------------------------------------------------ // methods @@ -179,6 +182,7 @@ public class Prism implements PrismSettingsListener // default values for miscellaneous options doReach = true; bsccComp = true; + checkZeroLoops = false; construction = 3; ordering = 1; sumRoundOff = 1e-5; @@ -1508,6 +1512,16 @@ public class Prism implements PrismSettingsListener { return settings; } + + public void setCheckZeroLoops(boolean checkZeroLoops) + { + this.checkZeroLoops = checkZeroLoops; + } + + public boolean getCheckZeroLoops() + { + return this.checkZeroLoops; + } } //------------------------------------------------------------------------------ diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 77267dc0..4b92d455 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -255,28 +255,27 @@ public class PrismCL error(e.getMessage()); } } - - // export labels/states - if (exportlabels) { - try { - if (propertiesFile != null) { - definedPFConstants = undefinedConstants.getPFConstantValues(); - propertiesFile.setUndefinedConstants(definedPFConstants); - } - File f = (exportLabelsFilename.equals("stdout")) ? null : new File(exportLabelsFilename); - prism.exportLabelsToFile(model, modulesFile, propertiesFile, exportType, f); - } - // in case of error, report it and proceed - catch (FileNotFoundException e) { - mainLog.println("Couldn't open file \"" + exportLabelsFilename + "\" for output"); - } - catch (PrismException e) { - mainLog.println("\nError: " + e.getMessage() + "."); + } + + // export labels/states + if (exportlabels) { + try { + if (propertiesFile != null) { + definedPFConstants = undefinedConstants.getPFConstantValues(); + propertiesFile.setUndefinedConstants(definedPFConstants); } + File f = (exportLabelsFilename.equals("stdout")) ? null : new File(exportLabelsFilename); + prism.exportLabelsToFile(model, modulesFile, propertiesFile, exportType, f); + } + // in case of error, report it and proceed + catch (FileNotFoundException e) { + mainLog.println("Couldn't open file \"" + exportLabelsFilename + "\" for output"); + } + catch (PrismException e) { + mainLog.println("\nError: " + e.getMessage() + "."); } } - // work through list of properties to be checked for (j = 0; j < numPropertiesToCheck; j++) { @@ -1122,6 +1121,10 @@ public class PrismCL else if (sw.equals("o2")) { prism.setOrdering(2); } + // zero-reward loops check on + else if (sw.equals("zerorewardcheck")) { + prism.setCheckZeroLoops(true); + } // reachability off else if (sw.equals("noreach")) { prism.setDoReach(false); @@ -1589,6 +1592,7 @@ public class PrismCL mainLog.println("-fixdl ......................... Automatically put self-loops in deadlock states"); mainLog.println("-nocompact ..................... Switch off \"compact\" sparse storage schemes"); mainLog.println("-noprobchecks .................. Disable checks on model probabilities/rates"); + mainLog.println("-zerorewardchecks .............. Check for absence of zero-reward loops"); mainLog.println("-nossdetect .................... Disable steady-state detection for CTMC transient computations"); mainLog.println("-sccmethod .............. Specify SCC computation method (xiebeerel, lockstep, sccfind)"); mainLog.println();