DTMC/MDP toString().

Author: davexparker

prism/src/explicit/DTMC.java

@@ -803,4 +803,36 @@ public default void vmMultPowerSteadyState(double vect[], double[] result, doubl
 		}
 	}
 
+	/**
+	 * Generate a string representation for a DTMC.
+	 */
+	default String toStringDTMC()
+	{
+		StringBuilder str = new StringBuilder("[ ");
+		int numStates = getNumStates();
+		for (int s = 0; s < numStates; s++) {
+			if (s > 0) {
+				str.append(", ");
+			}
+			str.append(s).append(": ");
+			str.append("{");
+			Iterator<Entry<Integer, Pair<Value, Object>>> iter = getTransitionsAndActionsIterator(s);
+			boolean first = true;
+			while (iter.hasNext()) {
+				if (first) {
+					first = false;
+				} else {
+					str.append(",");
+				}
+				Entry<Integer, Pair<Value, Object>> entry = iter.next();
+				str.append(entry.getValue().first).append(":").append(entry.getKey());
+				if (entry.getValue().second != null) {
+					str.append(":").append(entry.getValue().second);
+				}
+			}
+			str.append("}");
+		}
+		str.append(" ]\n");
+		return str.toString();
+	}
 }

prism/src/explicit/DTMCSimple.java

@@ -425,41 +425,7 @@ public Distribution<Value> getTransitions(int s)
 	@Override
 	public String toString()
 	{
-		int i;
-		boolean first;
-		String s = "";
-		s = "[ ";
-		first = true;
-		for (i = 0; i < numStates; i++) {
-			if (first)
-				first = false;
-			else
-				s += ", ";
-			s += i + ": " + toStringDistr(i);
-		}
-		s += " ]";
-		return s;
-	}
-
-	protected String toStringDistr(int i)
-	{
-		String s = "";
-		boolean first = true;
-		s = "{";
-		int numSucc = succ.get(i).size();
-		for (int j = 0; j < numSucc; j++) {
-			if (first)
-				first = false;
-			else
-				s += ", ";
-			s += succ.get(i).get(j) + "=" + trans.get(i).get(j);
-			Object action = actions.getAction(i, j);
-			if (action != null) {
-				s += ":" + action;
-			}
-		}
-		s += "}";
-		return s;
+		return toStringDTMC();
 	}
 
 	@Override

prism/src/explicit/DTMCSparse.java

@@ -530,33 +530,12 @@ public void vmMultPowerSteadyState(double vect[], double result[], double[] diag
 		}
 	}
 
-
-
 	//--- Object ---
 
 	@Override
 	public String toString()
 	{
-		final Function<Integer, Entry<Integer, Distribution<Double>>> getDistribution = new Function<Integer, Entry<Integer, Distribution<Double>>>()
-		{
-			@Override
-			public final Entry<Integer, Distribution<Double>> apply(final Integer state)
-			{
-				final Distribution<Double> distribution = new Distribution<>(getTransitionsIterator(state), getEvaluator());
-				return new AbstractMap.SimpleImmutableEntry<>(state, distribution);
-			}
-		};
-		String s = "trans: [ ";
-		IterableStateSet states = new IterableStateSet(numStates);
-		Iterator<Entry<Integer, Distribution<Double>>> distributions = states.iterator().map(getDistribution);
-		while (distributions.hasNext()) {
-			final Entry<Integer, Distribution<Double>> dist = distributions.next();
-			s += dist.getKey() + ": " + dist.getValue();
-			if (distributions.hasNext()) {
-				s += ", ";
-			}
-		}
-		return s + " ]";
+		return toStringDTMC();
 	}
 
 	@Override

prism/src/explicit/MDP.java

@@ -884,4 +884,44 @@ public default void mvMultRight(int[] states, int[] strat, double[] source, doub
 		}
 	}
 
+	/**
+	 * Generate a string representation for an MDP.
+	 */
+	default String toStringMDP()
+	{
+		StringBuilder str = new StringBuilder("[ ");
+		int numStates = getNumStates();
+		for (int s = 0; s < numStates; s++) {
+			if (s > 0) {
+				str.append(", ");
+			}
+			str.append(s).append(": ").append("[");
+			int numChoices = getNumChoices(s);
+			for (int i = 0; i < numChoices; i++) {
+				if (i > 0) {
+					str.append(",");
+				}
+				Object action = getAction(s, i);
+				if (action != null) {
+					str.append(action).append(":");
+				}
+				str.append("{");
+				Iterator<Entry<Integer, Value>> iter = getTransitionsIterator(s, i);
+				boolean first = true;
+				while (iter.hasNext()) {
+					if (first) {
+						first = false;
+					} else {
+						str.append(",");
+					}
+					Entry<Integer, Value> entry = iter.next();
+					str.append(entry.getValue()).append(":").append(entry.getKey());
+				}
+				str.append("}");
+			}
+			str.append("]");
+		}
+		str.append(" ]\n");
+		return str.toString();
+	}
 }

prism/src/explicit/MDPSimple.java

@@ -553,28 +553,7 @@ public int indexOfActionLabelledChoice(int s, Distribution<Value> distr, Object
 	@Override
 	public String toString()
 	{
-		int i, j, n;
-		Object o;
-		String s = "";
-		s = "[ ";
-		for (i = 0; i < numStates; i++) {
-			if (i > 0)
-				s += ", ";
-			s += i + ": ";
-			s += "[";
-			n = getNumChoices(i);
-			for (j = 0; j < n; j++) {
-				if (j > 0)
-					s += ",";
-				o = getAction(i, j);
-				if (o != null)
-					s += o + ":";
-				s += trans.get(i).get(j);
-			}
-			s += "]";
-		}
-		s += " ]\n";
-		return s;
+		return toStringMDP();
 	}
 
 	@Override

prism/src/explicit/MDPSparse.java

@@ -1134,37 +1134,7 @@ public void mvMultRight(int[] states, int[] strat, double[] source, double[] des
 	@Override
 	public String toString()
 	{
-		int i, j, k, l1, h1, l2, h2;
-		Object o;
-		String s = "";
-		s = "[ ";
-		for (i = 0; i < numStates; i++) {
-			if (i > 0)
-				s += ", ";
-			s += i + ": [";
-			l1 = rowStarts[i];
-			h1 = rowStarts[i + 1];
-			for (j = l1; j < h1; j++) {
-				if (j > l1)
-					s += ",";
-				o = getAction(i, j - l1);
-				if (o != null)
-					s += o + ":";
-				s += "{";
-				l2 = choiceStarts[j];
-				h2 = choiceStarts[j + 1];
-				for (k = l2; k < h2; k++) {
-					if (k > l2)
-						s += ", ";
-					s += cols[k] + ":" + nonZeros[k];
-				}
-				s += "}";
-			}
-			s += "]";
-		}
-		s += " ]";
-
-		return s;
+		return toStringMDP();
 	}
 
 	@Override

prism/src/explicit/ModelExplicitWrapper.java

@@ -274,4 +274,12 @@ public void exportToPrismLanguage(String filename, int precision) throws PrismEx
 	{
 		this.model.exportToPrismLanguage(filename, precision);
 	}
+
+	// Standard methods
+
+	@Override
+	public String toString()
+	{
+		return model.toString();
+	}
 }