From 592be782616c8debfd24e6f4dc896260038f045f Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 28 Aug 2017 12:45:47 +0200 Subject: [PATCH] param / exact: improve filter(print, ...) output, support filter(printall, ...) In particular, align output format with other engines and treat exact mode specially (print rational numbers instead of functions, approximate values) For parametric, output results per region. Print not only the state index, but also the variable valuations for that state (similar to the other engines). Example for exact: prism prism-examples/dice/dice.pm -pf 'filter(print, P=?[ F d=1])' --exact === Previously === Results (non-zero only) for filter true: ([0.0,1.0])0:={ 1 | 6 }1:={ 1 | 3 }2:={ 0 }3:={ 2 | 3 }4:={ 0 }5:={ 0 }6:={ 0 }7:={ 1 }8:={ 0 }9:={ 0 }10:={ 0 }11:={ 0 }12:={ 0 } ================== === Now ========== Results (non-zero only) for filter true: 0:(0,0)=1/6 (~0.16666666666666666) 1:(1,0)=1/3 (~0.33333333333333337) 3:(3,0)=2/3 (~0.6666666666666666) 7:(7,1)=1 (1.0) ================== Example for parametric: === Previously === Results (non-zero only) for filter true: ([0.0,0.5])0:={ ( -1 ) p + 1 }1:={ 1 }2:={ 0 }([0.5,1.0])0:={ p }1:={ 1 }2:={ 0 } ================== === Now ========== Results (non-zero only) for filter true: ([0.0,0.5]): 0:(0)={ ( -1 ) p + 1 } 1:(1)={ 1 } ([0.5,1.0]): 0:(0)={ p } 1:(1)={ 1 } ================== --- prism/src/param/ParamModelChecker.java | 10 +++- prism/src/param/RegionValues.java | 28 +++++++++++ prism/src/param/StateValues.java | 64 ++++++++++++++++++++++++++ 3 files changed, 100 insertions(+), 2 deletions(-) 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; + } + } + }