From abbfb2c596319d4adc7ff7e1733aadab7c331945 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 7 Jan 2010 21:28:15 +0000 Subject: [PATCH] Tweaks, tidies + addition for State{Probs,List} classes. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1678 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/StateListMTBDD.java | 5 ++ prism/src/prism/StateProbs.java | 3 ++ prism/src/prism/StateProbsDV.java | 60 +++++++++++++++++++----- prism/src/prism/StateProbsMTBDD.java | 68 +++++++++++++++++++++++++--- 4 files changed, 118 insertions(+), 18 deletions(-) diff --git a/prism/src/prism/StateListMTBDD.java b/prism/src/prism/StateListMTBDD.java index 8834dfa7..638fad22 100644 --- a/prism/src/prism/StateListMTBDD.java +++ b/prism/src/prism/StateListMTBDD.java @@ -115,6 +115,8 @@ public class StateListMTBDD implements StateList limit = false; outputLog = log; doPrint(); + if (count == 0) + outputLog.println("(none)"); } public void printMatlab(PrismLog log) { @@ -148,7 +150,10 @@ public class StateListMTBDD implements StateList numToPrint = n; outputLog = log; doPrint(); + if (count == 0) + outputLog.println("(none)"); } + public void printMatlab(PrismLog log, int n) { outputFormat = OutputFormat.MATLAB; diff --git a/prism/src/prism/StateProbs.java b/prism/src/prism/StateProbs.java index 32bfd76d..937d4171 100644 --- a/prism/src/prism/StateProbs.java +++ b/prism/src/prism/StateProbs.java @@ -54,6 +54,9 @@ public interface StateProbs StateProbs sumOverDDVars(JDDVars sumVars, Model newModel) throws PrismException; JDDNode getBDDFromInterval(String relOp, double bound); JDDNode getBDDFromInterval(double lo, double hi); + JDDNode getBDDFromCloseValue(double val, double epsilon, boolean abs); + JDDNode getBDDFromCloseValueAbs(double val, double epsilon); + JDDNode getBDDFromCloseValueRel(double val, double epsilon); void print(PrismLog log) throws PrismException; void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException; void printFiltered(PrismLog log, JDDNode filter) throws PrismException; diff --git a/prism/src/prism/StateProbsDV.java b/prism/src/prism/StateProbsDV.java index 8bdbf861..aa0d9a20 100644 --- a/prism/src/prism/StateProbsDV.java +++ b/prism/src/prism/StateProbsDV.java @@ -223,6 +223,8 @@ public class StateProbsDV implements StateProbs return "" + getNNZ(); } + // Filter operations + /** * Get the value of first vector element that is in the (BDD) filter. */ @@ -255,18 +257,20 @@ public class StateProbsDV implements StateProbs return probs.sumOverBDD(filter, vars, odd); } - // do a weighted sum of the elements of the vector and the values the mtbdd passed in - // (used for csl reward steady state operator) - + /** + * Do a weighted sum of the elements of the vector and the values the mtbdd passed in + * (used for CSL reward steady state operator). + */ public double sumOverMTBDD(JDDNode mult) { return probs.sumOverMTBDD(mult, vars, odd); } - // sum up the elements of the vector, over a subset of its dd vars - // store the result in a new StateProbsDV (for newModel) - // throws PrismException on out-of-memory - + /** + * Sum up the elements of the vector, over a subset of its DD vars + * store the result in a new StateProbs (for newModel) + * @throws PrismException (on out-of-memory) + */ public StateProbs sumOverDDVars(JDDVars sumVars, Model newModel) throws PrismException { DoubleVector tmp; @@ -276,20 +280,54 @@ public class StateProbsDV implements StateProbs return new StateProbsDV(tmp, newModel); } - // generate bdd from an interval (relative operator and bound) - + /** + * Generate BDD for states in the given interval + * (interval specified as relational operator and bound) + */ public JDDNode getBDDFromInterval(String relOp, double bound) { return probs.getBDDFromInterval(relOp, bound, vars, odd); } - // generate bdd from an interval (lower/upper bound) - + /** + * Generate BDD for states in the given interval + * (interval specified as lower/upper bound) + */ public JDDNode getBDDFromInterval(double lo, double hi) { return probs.getBDDFromInterval(lo, hi, vars, odd); } + /** + * Generate BDD for states whose value is close to 'value' + * (within either absolute or relative error 'epsilon') + */ + public JDDNode getBDDFromCloseValue(double value, double epsilon, boolean abs) + { + if (abs) + return probs.getBDDFromCloseValueAbs(value, epsilon, vars, odd); + else + return probs.getBDDFromCloseValueRel(value, epsilon, vars, odd); + } + + /** + * Generate BDD for states whose value is close to 'value' + * (within absolute error 'epsilon') + */ + public JDDNode getBDDFromCloseValueAbs(double value, double epsilon) + { + return probs.getBDDFromCloseValueAbs(value, epsilon, vars, odd); + } + + /** + * Generate BDD for states whose value is close to 'value' + * (within relative error 'epsilon') + */ + public JDDNode getBDDFromCloseValueRel(double value, double epsilon) + { + return probs.getBDDFromCloseValueRel(value, epsilon, vars, odd); + } + // PRINTING STUFF /** diff --git a/prism/src/prism/StateProbsMTBDD.java b/prism/src/prism/StateProbsMTBDD.java index 4bc119ba..2f9fe863 100644 --- a/prism/src/prism/StateProbsMTBDD.java +++ b/prism/src/prism/StateProbsMTBDD.java @@ -346,9 +346,10 @@ public class StateProbsMTBDD implements StateProbs return d; } - // do a weighted sum of the elements of a double array and the values the mtbdd passed in - // (used for csl reward steady state operator) - + /** + * Do a weighted sum of the elements of the vector and the values the mtbdd passed in + * (used for CSL reward steady state operator). + */ public double sumOverMTBDD(JDDNode mult) { JDDNode tmp; @@ -364,6 +365,11 @@ public class StateProbsMTBDD implements StateProbs return d; } + /** + * Sum up the elements of the vector, over a subset of its DD vars + * store the result in a new StateProbs (for newModel) + * @throws PrismException (on out-of-memory) + */ public StateProbs sumOverDDVars(JDDVars sumVars, Model newModel) { JDDNode tmp; @@ -374,8 +380,10 @@ public class StateProbsMTBDD implements StateProbs return new StateProbsMTBDD(tmp, newModel); } - // generate bdd (from an interval: relative operator and bound) - + /** + * Generate BDD for states in the given interval + * (interval specified as relational operator and bound) + */ public JDDNode getBDDFromInterval(String relOp, double bound) { JDDNode sol = null; @@ -397,8 +405,10 @@ public class StateProbsMTBDD implements StateProbs return sol; } - // generate bdd from an interval (lower/upper bound) - + /** + * Generate BDD for states in the given interval + * (interval specified as lower/upper bound) + */ public JDDNode getBDDFromInterval(double lo, double hi) { JDDNode sol; @@ -409,6 +419,50 @@ public class StateProbsMTBDD implements StateProbs return sol; } + /** + * Generate BDD for states whose value is close to 'value' + * (within either absolute or relative error 'epsilon') + */ + public JDDNode getBDDFromCloseValue(double value, double epsilon, boolean abs) + { + if (abs) + return getBDDFromCloseValueAbs(value, epsilon); + else + return getBDDFromCloseValueRel(value, epsilon); + } + + /** + * Generate BDD for states whose value is close to 'value' + * (within absolute error 'epsilon') + */ + public JDDNode getBDDFromCloseValueAbs(double value, double epsilon) + { + JDDNode sol; + + // TODO: infinite cases + + JDD.Ref(probs); + sol = JDD.Interval(probs, value - epsilon, value + epsilon); + + return sol; + } + + /** + * Generate BDD for states whose value is close to 'value' + * (within relative error 'epsilon') + */ + public JDDNode getBDDFromCloseValueRel(double value, double epsilon) + { + JDDNode sol; + + // TODO: wrong + + JDD.Ref(probs); + sol = JDD.Interval(probs, value - epsilon, value + epsilon); + + return sol; + } + // PRINTING STUFF /**