diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index 4149a8bf..44b86dc9 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -541,16 +541,22 @@ final public class ParamModelChecker extends PrismComponent RegionValues resVals = null; switch (op) { case PRINT: + case PRINTALL: // 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.println(filterTrue ? ":" : " that are also in filter " + filter + ":"); - mainLog.print(vals.filteredString(bsFilter)); } else { mainLog.println("\nResults (non-zero only) for filter " + filter + ":"); - mainLog.print(vals.filteredString(bsFilter)); } + + vals.printFiltered(mainLog, mode, expr.getType(), bsFilter, + model.getStatesList(), + op == FilterOperator.PRINT, // printSparse if PRINT + true, // print state values + true); // print state index + resVals = vals; break; case MIN: diff --git a/prism/src/param/RegionValues.java b/prism/src/param/RegionValues.java index 01c35cdb..e458ff59 100644 --- a/prism/src/param/RegionValues.java +++ b/prism/src/param/RegionValues.java @@ -31,8 +31,12 @@ import java.util.HashMap; import java.util.ArrayList; import java.util.HashSet; import java.util.Iterator; +import java.util.List; import java.util.Map.Entry; +import parser.State; +import prism.PrismLog; + /** * Assigns to the different regions different values over model states. * For each region for which values have been decided, an object of this @@ -420,6 +424,30 @@ public final class RegionValues implements Iterable> return builder.toString(); } + /** + * For each region, print part of vector to a log/file. + * @param log The log + * @param mode the mode + * @param filter A BitSet specifying which states to print for (null if all). + * @param printSparse Print non-zero/non-false elements only? + * @param printStates Print states (variable values) for each element? + * @param printIndices Print state indices for each element? + */ + public void printFiltered(PrismLog log, ParamMode mode, parser.type.Type type, BitSet filter, List statesList, boolean printSparse, boolean printStates, boolean printIndices) + { + if (mode == ParamMode.EXACT) { + assert(parameterIndependent()); + getStateValues().printFiltered(log, mode, type, filter, statesList, printSparse, printStates, printIndices); + } else { + for (Region region : regions) { + log.println(region + ":"); + StateValues vals = values.get(region); + vals.printFiltered(log, mode, type, filter, statesList, printSparse, printStates, printIndices); + log.println(); + } + } + } + public RegionValues unaryOp(int parserUnaryOpToRegionOp) { RegionValues result = new RegionValues(factory); diff --git a/prism/src/param/StateValues.java b/prism/src/param/StateValues.java index 3a339d75..705cf21b 100644 --- a/prism/src/param/StateValues.java +++ b/prism/src/param/StateValues.java @@ -30,6 +30,13 @@ package param; import java.util.ArrayList; import java.util.BitSet; +import java.util.List; +import java.util.function.IntPredicate; + +import common.IterableStateSet; +import parser.State; +import parser.type.TypeBool; +import prism.PrismLog; /** * Class to assign a value to each state of a model. @@ -245,4 +252,61 @@ public final class StateValues } return result; } + + /** + * Print part of vector to a log/file. + * @param log The log + * @param mode the mode + * @param filter A BitSet specifying which states to print for (null if all). + * @param printSparse Print non-zero/non-false elements only? + * @param printStates Print states (variable values) for each element? + * @param printIndices Print state indices for each element? + */ + public void printFiltered(PrismLog log, ParamMode mode, parser.type.Type type, BitSet filter, List statesList, boolean printSparse, boolean printStates, boolean printIndices) + { + int count = 0; + + IntPredicate nonZero = + (type instanceof TypeBool) + ? (int n) -> {return getStateValueAsBoolean(n);} + : (int n) -> {return !getStateValueAsFunction(n).isZero();}; + + // Print vector + for (int n : new IterableStateSet(filter, getNumStates())) { + if (!printSparse || nonZero.test(n)) { + if (printIndices) { + log.print(n); + log.print(":"); + } + + if (printStates && statesList != null) + log.print(statesList.get(n).toString()); + if (printSparse && type instanceof TypeBool) { + log.println(); + } else { + if (printIndices || printStates) + log.print("="); + + if (type instanceof TypeBool) { + log.println(getStateValueAsBoolean(n)); + } else { + if (mode == ParamMode.EXACT) { + BigRational value = getStateValueAsFunction(n).asBigRational(); + log.println(value + " (" + value.toApproximateString() + ")"); + } else { + log.println(getStateValueAsFunction(n)); + } + } + } + count++; + } + } + + // Check if all zero + if (printSparse && count == 0) { + log.println("(all zero)"); + return; + } + } + }