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

@@ -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:

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<Entry<Region, StateValues>>
 		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<State> 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);

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<State> 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;
+		}
+	}
+
 }