From 64f3673c6c6bc06259ed4e31a958cfb2b1924c9a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 20 Nov 2009 20:14:22 +0000 Subject: [PATCH] Improvements to StateProbs classes: additional export methods + clone. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1572 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/StateProbs.java | 7 +- prism/src/prism/StateProbsDV.java | 209 ++++++++++++++++++--------- prism/src/prism/StateProbsMTBDD.java | 79 ++++++++-- 3 files changed, 212 insertions(+), 83 deletions(-) diff --git a/prism/src/prism/StateProbs.java b/prism/src/prism/StateProbs.java index a3e4a8c7..24567125 100644 --- a/prism/src/prism/StateProbs.java +++ b/prism/src/prism/StateProbs.java @@ -51,6 +51,9 @@ public interface StateProbs StateProbs sumOverDDVars(JDDVars sumVars, Model newModel) throws PrismException; JDDNode getBDDFromInterval(String relOp, double bound); JDDNode getBDDFromInterval(double lo, double hi); - void print(PrismLog log); - void printFiltered(PrismLog log, JDDNode filter); + 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; + void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException; + StateProbs deepCopy() throws PrismException; } diff --git a/prism/src/prism/StateProbsDV.java b/prism/src/prism/StateProbsDV.java index d12c8490..24ce7823 100644 --- a/prism/src/prism/StateProbsDV.java +++ b/prism/src/prism/StateProbsDV.java @@ -34,6 +34,10 @@ import parser.type.*;; // state probability vector (double vector) +/** + * @author dxp + * + */ public class StateProbsDV implements StateProbs { // prob vector @@ -55,6 +59,11 @@ public class StateProbsDV implements StateProbs // log for output from print method PrismLog outputLog; + + // flags + boolean printSparse = true; + boolean printMatlab = false; + boolean printStates = true; // CONSTRUCTORS @@ -234,14 +243,36 @@ public class StateProbsDV implements StateProbs // PRINTING STUFF - // print vector (non zeros only) + /** + * Print vector to a log/file (non-zero entries only) + */ + public void print(PrismLog log) throws PrismException + { + print(log, true, false, true); + } - public void print(PrismLog log) + /** + * Print vector to a log/file. + * @param log: The log + * @param printSparse: Print non-zero elements only? + * @param printMatlab: Print in Matlab format? + * @param printStates: Print states (variable values) for each element? + */ +public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException { int i; + // store flags + this.printSparse = printSparse; + this.printMatlab = printMatlab; + this.printStates = printStates; + + // header for matlab format + if (printMatlab) + log.println(!printSparse ? "v = [" : "v = sparse(" + probs.getSize() + ",1);"); + // check if all zero - if (probs.getNNZ() == 0) { + if (printSparse && !printMatlab && probs.getNNZ() == 0) { log.println("(all zero)"); return; } @@ -254,48 +285,36 @@ public class StateProbsDV implements StateProbs currentVar = 0; currentVarLevel = 0; printRec(0, odd, 0); - } - - // recursive bit of print - - // (nb: this would be very easy - i.e. not even - // any recursion - if we didn't want to print - // out the values of the module variables as well - // which requires traversal of the odd as well - // as the vector) - // (nb2: traversal of vector/odd is still quite simple, - // tricky bit is keeping track of variable values - // throughout traversal - we want to be efficient - // and not compute the values from scratch each - // time, but we also want to avoid passing arrays - // into the resursive method) + + // footer for matlab format + if (printMatlab && !printSparse) + log.println("];"); +} + /** + * Recursive part of print method. + * + * (NB: this would be very easy - i.e. not even + * any recursion - if we didn't want to print + * out the values of the module variables as well + * which requires traversal of the odd as well + * as the vector) + * (NB2: traversal of vector/odd is still quite simple; + * tricky bit is keeping track of variable values + * throughout traversal - we want to be efficient + * and not compute the values from scratch each + * time, but we also want to avoid passing arrays + * into the recursive method) + */ private void printRec(int level, ODDNode o, int n) { - int i, j; double d; // base case - at bottom if (level == numVars) { d = probs.getElement(n); - if (d != 0) { - outputLog.print(n + ":("); - j = varList.getNumVars(); - for (i = 0; i < j; i++) { - // integer variable - if (varList.getType(i) instanceof TypeInt) { - outputLog.print(varValues[i]+varList.getLow(i)); - } - // boolean variable - else { - outputLog.print(varValues[i] == 1); - } - if (i < j-1) outputLog.print(","); - } - outputLog.print(")=" + d + " "); - outputLog.println(); - return; - } + printLine(n, d); + return; } // recurse else { @@ -313,20 +332,39 @@ public class StateProbsDV implements StateProbs } } } - - // print filtered vector (non zeros only) - public void printFiltered(PrismLog log, JDDNode filter) + /** + * Print part of a vector to a log/file (non-zero entries only). + * @param log: The log + * @param filter: A BDD specifying which states to print for. + */ + public void printFiltered(PrismLog log, JDDNode filter) throws PrismException + { + printFiltered(log, filter, true, false, true); + } + + /** + * Print part of a vector to a log/file (non-zero entries only). + * @param log: The log + * @param filter: A BDD specifying which states to print for. + * @param printSparse: Print non-zero elements only? + * @param printMatlab: Print in Matlab format? + * @param printStates: Print states (variable values) for each element? + */ + public void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException { int i; - // check if all zero - if (probs.getNNZ() == 0) { - log.println("(all zero)"); - return; - } - // still might be though, depending on filter - // so we kep an explicit counter + // store flags + this.printSparse = printSparse; + this.printMatlab = printMatlab; + this.printStates = printStates; + + // header for matlab format + if (printMatlab) + log.println(!printSparse ? "v = [" : "v = sparse(" + probs.getSize() + ",1);"); + + // set up a counter so we can check if there were no non-zero elements counter = 0; // set up and call recursive print @@ -338,21 +376,25 @@ public class StateProbsDV implements StateProbs currentVarLevel = 0; printFilteredRec(0, odd, 0, filter); - // check again if all zero - if (counter == 0) { + // check if all zero + if (printSparse && !printMatlab && counter == 0) { log.println("(all zero)"); return; } + + // footer for matlab format + if (printMatlab && !printSparse) + log.println("];"); } - // recursive bit of printFiltered - - // same as recursive bit of print (above) - // but we also traverse filter - + /** + * Recursive part of printFiltered method. + * + * So we need to traverse filter too. + * See also notes above for printRec. + */ private void printFilteredRec(int level, ODDNode o, int n, JDDNode filter) { - int i; double d; JDDNode newFilter; @@ -364,18 +406,8 @@ public class StateProbsDV implements StateProbs // base case - at bottom if (level == numVars) { d = probs.getElement(n); - if (d != 0) { - outputLog.print(n + ":("); - for (i = 0; i < varList.getNumVars()-1; i++) { - outputLog.print((varValues[i]+varList.getLow(i)) + ","); - } - i = varList.getNumVars()-1; - outputLog.print((varValues[i]+varList.getLow(i))); - outputLog.print(")=" + d + " "); - outputLog.println(); - counter++; - return; - } + printLine(n, d); + return; } // recurse else { @@ -399,4 +431,47 @@ public class StateProbsDV implements StateProbs } } } + + private void printLine(int n, double d) + { + int i, j; + if (!printSparse || d != 0) { + if (printSparse) + outputLog.print(printMatlab ? "v(" + (n + 1) + ")" : n); + if (printStates && !printMatlab) { + outputLog.print(":("); + j = varList.getNumVars(); + for (i = 0; i < j; i++) { + // integer variable + if (varList.getType(i) instanceof TypeInt) { + outputLog.print(varValues[i]+varList.getLow(i)); + } + // boolean variable + else { + outputLog.print(varValues[i] == 1); + } + if (i < j-1) outputLog.print(","); + } + outputLog.print(")"); + } + if (printSparse) + outputLog.print("="); + outputLog.print(d); + if (printMatlab && printSparse) + outputLog.print(";"); + outputLog.println(); + } + } + + /** + * Make a (deep) copy of this vector + */ + public StateProbsDV deepCopy() throws PrismException + { + // Clone vector + DoubleVector dv = new DoubleVector(probs.getSize()); + dv.add(probs); + // Return copy + return new StateProbsDV(dv, model); + } } diff --git a/prism/src/prism/StateProbsMTBDD.java b/prism/src/prism/StateProbsMTBDD.java index 62a299aa..97488103 100644 --- a/prism/src/prism/StateProbsMTBDD.java +++ b/prism/src/prism/StateProbsMTBDD.java @@ -330,9 +330,10 @@ public class StateProbsMTBDD implements StateProbs // PRINTING STUFF - // print vector (non zeros only) - - public void print(PrismLog log) + /** + * Print vector to a log/file (non-zero entries only) + */ + public void print(PrismLog log) throws PrismException { int i; @@ -353,14 +354,36 @@ public class StateProbsMTBDD implements StateProbs //log.println(); } - // recursive bit of print - // (nb: traversal of mtbdd/odd is quite simple, - // tricky bit is keeping track of variable values - // throughout traversal - we want to be efficient - // and not compute the values from scratch each - // time, but we also want to avoid passing arrays - // into the resursive method) + /** + * Print vector to a log/file. + * @param log: The log + * @param printSparse: Print non-zero elements only? + * @param printMatlab: Print in Matlab format? + * @param printStates: Print states (variable values) for each element? + */ + public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException + { + // Because non-sparse output from MTBDD requires a bit more effort... + if (printSparse) print(log); + else throw new PrismException("Not supported"); + // Note we also ignore printMatlab/printStates due to laziness + } + /** + * Recursive part of print method. + * + * (NB: this would be very easy - i.e. not even + * any recursion - if we didn't want to print + * out the values of the module variables as well + * which requires traversal of the odd as well + * as the vector) + * (NB2: traversal of vector/odd is still quite simple; + * tricky bit is keeping track of variable values + * throughout traversal - we want to be efficient + * and not compute the values from scratch each + * time, but we also want to avoid passing arrays + * into the recursive method) + */ private void printRec(JDDNode dd, int level, ODDNode o, long n) { int i, j; @@ -410,10 +433,13 @@ public class StateProbsMTBDD implements StateProbs varValues[currentVar] -= (1 << (varSizes[currentVar]-1-currentVarLevel)); } - // print filtered vector (non zeros only) - - public void printFiltered(PrismLog log, JDDNode filter) - { + /** + * Print part of a vector to a log/file (non-zero entries only). + * @param log: The log + * @param filter: A BDD specifying which states to print for. + */ + public void printFiltered(PrismLog log, JDDNode filter) throws PrismException + { int i; JDDNode tmp; @@ -440,4 +466,29 @@ public class StateProbsMTBDD implements StateProbs //log.println(); JDD.Deref(tmp); } + + /** + * Print part of a vector to a log/file (non-zero entries only). + * @param log: The log + * @param filter: A BDD specifying which states to print for. + * @param printSparse: Print non-zero elements only? + * @param printMatlab: Print in Matlab format? + * @param printStates: Print states (variable values) for each element? + */ + public void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException + { + // Because non-sparse output from MTBDD requires a bit more effort... + if (printSparse) printFiltered(log, filter); + else throw new PrismException("Not supported"); + // Note we also ignore printMatlab/printStates due to laziness + } + + /** + * Make a (deep) copy of this vector + */ + public StateProbsMTBDD deepCopy() throws PrismException + { + JDD.Ref(probs); + return new StateProbsMTBDD(probs, model); + } }