From 995cdd360033d954775a422095d4b27b092140f7 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 6 Sep 2011 14:37:42 +0000 Subject: [PATCH] More printing options in StateValues (incl. state lists) + rest of filter stuff. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3594 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/PrismExplicit.java | 4 +- prism/src/explicit/StateModelChecker.java | 28 +++---- prism/src/explicit/StateValues.java | 93 ++++++++++++++++------- 3 files changed, 80 insertions(+), 45 deletions(-) diff --git a/prism/src/explicit/PrismExplicit.java b/prism/src/explicit/PrismExplicit.java index 4747ea39..c48cf9ea 100644 --- a/prism/src/explicit/PrismExplicit.java +++ b/prism/src/explicit/PrismExplicit.java @@ -277,7 +277,7 @@ public class PrismExplicit } // print out or export probabilities - probs.print(tmpLog, fileOut == null, exportType == Prism.EXPORT_MATLAB, fileOut == null); + probs.print(tmpLog, fileOut == null, exportType == Prism.EXPORT_MATLAB, fileOut == null, true); // print out computation time mainLog.println("\nTime for steady-state probability computation: " + l/1000.0 + " seconds."); @@ -351,7 +351,7 @@ public class PrismExplicit } // print out or export probabilities - probs.print(tmpLog, fileOut == null, exportType == Prism.EXPORT_MATLAB, fileOut == null); + probs.print(tmpLog, fileOut == null, exportType == Prism.EXPORT_MATLAB, fileOut == null, true); // print out computation time mainLog.println("\nTime for transient probability computation: " + l/1000.0 + " seconds."); diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 495a44dd..a86026e3 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -534,13 +534,12 @@ public class StateModelChecker Expression filter; FilterOperator op; String filterStatesString; - /*StateListMTBDD statesFilter;*/ boolean filterInit, filterInitSingle, filterTrue; BitSet bsFilter = null; // Result info StateValues vals = null, resVals = null; BitSet bsMatch = null, bs; - /*StateListMTBDD states;*/ + StateValues states; boolean b = false; int count = 0; String resultExpl = null; @@ -558,7 +557,6 @@ public class StateModelChecker // Store some more info filterStatesString = filterTrue ? "all states" : "states satisfying filter"; bsFilter = checkExpression(model, filter).getBitSet(); - /*statesFilter = new StateListMTBDD(bsFilter, model);*/ // Check if filter state set is empty; we treat this as an error if (bsFilter.isEmpty()) { throw new PrismException("Filter satisfies no states"); @@ -567,8 +565,8 @@ public class StateModelChecker filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).getName().equals("init")); filterInitSingle = filterInit & model.getNumInitialStates() == 1; // Print out number of states satisfying filter - /*if (!filterInit) - mainLog.println("\nStates satisfying filter " + filter + ": " + statesFilter.sizeString());*/ + if (!filterInit) + mainLog.println("\nStates satisfying filter " + filter + ": " + bsFilter.cardinality()); // Compute result according to filter type op = expr.getOperatorType(); @@ -577,11 +575,9 @@ public class StateModelChecker // Format of print-out depends on type if (expr.getType() instanceof TypeBool) { // NB: 'usual' case for filter(print,...) on Booleans is to use no filter - /*mainLog.print("\nSatisfying states"); + mainLog.print("\nSatisfying states"); mainLog.println(filterTrue ? ":" : " that are also in filter " + filter + ":"); - dd = vals.deepCopy().convertToStateValuesMTBDD().getJDDNode(); - new StateListMTBDD(dd, model).print(mainLog); - JDD.Deref(dd);*/ + vals.printFiltered(mainLog, bsFilter); } else { mainLog.println("\nResults (non-zero only) for filter " + filter + ":"); vals.printFiltered(mainLog, bsFilter); @@ -771,19 +767,19 @@ public class StateModelChecker } // For some operators, print out some matching states - /*if (bsMatch != null) { - states = new StateListMTBDD(bsMatch, model); - mainLog.print("\nThere are " + states.sizeString() + " states with "); + if (bsMatch != null) { + states = StateValues.createFromBitSet(bsMatch, model); + mainLog.print("\nThere are " + bsMatch.cardinality() + " states with "); mainLog.print(expr.getType() instanceof TypeDouble ? "(approximately) " : "" + "this value"); - if (!verbose && (states.size() == -1 || states.size() > 10)) { + boolean verbose = verbosity > 0; // TODO + if (!verbose && bsMatch.cardinality() > 10) { mainLog.print(".\nThe first 10 states are displayed below. To view them all, enable verbose mode or use a print filter.\n"); states.print(mainLog, 10); } else { mainLog.print(":\n"); states.print(mainLog); } - JDD.Deref(bsMatch); - }*/ + } // Store result result.setResult(resObj); @@ -794,7 +790,7 @@ public class StateModelChecker result.setExplanation(null); } - // Derefs, clears + // Clear up if (vals != null) vals.clear(); diff --git a/prism/src/explicit/StateValues.java b/prism/src/explicit/StateValues.java index 388e0a9f..18a47872 100644 --- a/prism/src/explicit/StateValues.java +++ b/prism/src/explicit/StateValues.java @@ -519,65 +519,96 @@ public class StateValues // PRINTING STUFF /** - * Print vector to a log/file (non-zero entries only). + * Print vector to a log/file (non-zero/non-false entries only). */ public void print(PrismLog log) throws PrismException { - printFiltered(log, null, true, false, true); + doPrinting(log, -1, null, true, false, true, true); + } + + /** + * Print up to {@code limit} entries of a vector to a log/file (non-zero/non-false entries only). + */ + public void print(PrismLog log, int limit) throws PrismException + { + doPrinting(log, limit, null, true, false, true, true); } /** * Print vector to a log/file. * @param log The log - * @param printSparse Print non-zero elements only? + * @param printSparse Print non-zero/non-false elements only? * @param printMatlab Print in Matlab format? * @param printStates Print states (variable values) for each element? + * @param printIndices Print state indices for each element? */ - public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException + public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException { - printFiltered(log, null, true, false, true); + doPrinting(log, -1, null, printSparse, printMatlab, printStates, printIndices); } /** - * Print part of vector to a log/file (non-zero entries only). + * Print part of vector to a log/file (non-zero/non-false entries only). * @param log The log * @param filter A BitSet specifying which states to print for. */ public void printFiltered(PrismLog log, BitSet filter) throws PrismException { - printFiltered(log, filter, true, false, true); + doPrinting(log, -1, filter, true, false, true, true); } /** * Print part of vector to a log/file. * @param log The log * @param filter A BitSet specifying which states to print for (null if all). - * @param printSparse Print non-zero elements only? + * @param printSparse Print non-zero/non-false elements only? * @param printMatlab Print in Matlab format? * @param printStates Print states (variable values) for each element? + * @param printIndices Print state indices for each element? */ - public void printFiltered(PrismLog log, BitSet filter, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException + public void printFiltered(PrismLog log, BitSet filter, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) + throws PrismException { - int i; - boolean some = false; + doPrinting(log, -1, filter, printSparse, printMatlab, printStates, printIndices); + } + /** + * Print part of vector to a log/file. + * @param log The log + * @param limit Maximum number of entries to print (-1 = no limit) + * @param filter A BitSet specifying which states to print for (null if all). + * @param printSparse Print non-zero/non-false elements only? + * @param printMatlab Print in Matlab format? + * @param printStates Print states (variable values) for each element? + * @param printIndices Print state indices for each element? + */ + private void doPrinting(PrismLog log, int limit, BitSet filter, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) + throws PrismException + { + int i, count = 0; + + if (limit == -1) + limit = Integer.MAX_VALUE; + // Header for Matlab format if (printMatlab) log.println(!printSparse ? "v = [" : "v = sparse(" + size + ",1);"); // Print vector if (filter == null) { - for (i = 0; i < size; i++) { - some |= printLine(log, i, printSparse, printMatlab, printStates); + for (i = 0; i < size & count < limit; i++) { + if (printLine(log, i, printSparse, printMatlab, printStates, printIndices)) + count++; } } else { - for (i = filter.nextSetBit(0); i >= 0; i = filter.nextSetBit(i + 1)) { - some |= printLine(log, i, printSparse, printMatlab, printStates); + for (i = filter.nextSetBit(0); i >= 0 && count < limit; i = filter.nextSetBit(i + 1)) { + if (printLine(log, i, printSparse, printMatlab, printStates, printIndices)) + count++; } } // Check if all zero - if (printSparse && !printMatlab && !some) { + if (printSparse && !printMatlab && count == 0) { log.println("(all zero)"); return; } @@ -587,20 +618,28 @@ public class StateValues log.println("];"); } - private boolean printLine(PrismLog log, int i, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException + private boolean printLine(PrismLog log, int i, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException { if (!printSparse || isNonZero(i)) { - if (printSparse) - log.print(printMatlab ? "v(" + (i + 1) + ")" : i); - if (printStates && !printMatlab && statesList != null) { - log.print(":" + statesList.get(i).toString()); + if (printMatlab) { + if (printSparse) { + log.println("v(" + (i + 1) + ")=" + getValue(i) + ";"); + } else { + log.println(getValue(i)); + } + } else { + if (printIndices) + log.print(i); + if (printStates && statesList != null) + log.print(":" + statesList.get(i).toString()); + if (printSparse && type instanceof TypeBool) { + log.println(); + } else { + if (printIndices || printStates) + log.print("="); + log.println(getValue(i)); + } } - if (printSparse) - log.print("="); - log.print(getValue(i)); - if (printMatlab && printSparse) - log.print(";"); - log.println(); return true; } else { return false;