diff --git a/prism/src/explicit/DTMC.java b/prism/src/explicit/DTMC.java
index 9742e02a..f5909838 100644
--- a/prism/src/explicit/DTMC.java
+++ b/prism/src/explicit/DTMC.java
@@ -136,6 +136,24 @@ public interface DTMC extends Model
 		}
 	}
 
+	@Override
+	default String infoString()
+	{
+		String s = "";
+		s += getNumStates() + " states (" + getNumInitialStates() + " initial)";
+		s += ", " + getNumTransitions() + " transitions";
+		return s;
+	}
+
+	@Override
+	default String infoStringTable()
+	{
+		String s = "";
+		s += "States:      " + getNumStates() + " (" + getNumInitialStates() + " initial)\n";
+		s += "Transitions: " + getNumTransitions() + "\n";
+		return s;
+	}
+
 	// Accessors
 	
 	/**
diff --git a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java
index 495c6f72..6aa624bd 100644
--- a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java
+++ b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java
@@ -141,18 +141,6 @@ public class DTMCFromMDPAndMDStrategy extends DTMCExplicit
 		// No deadlocks by definition
 	}
 
-	@Override
-	public String infoString()
-	{
-		return mdp.infoString() + " + " + "???"; // TODO
-	}
-
-	@Override
-	public String infoStringTable()
-	{
-		return mdp.infoString() + " + " + "???\n"; // TODO
-	}
-
 	// Accessors (for DTMC)
 
 	public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s)
diff --git a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java
index 520afd08..2f328841 100644
--- a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java
+++ b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java
@@ -144,18 +144,6 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit
 		// No deadlocks by definition
 	}
 
-	@Override
-	public String infoString()
-	{
-		return mdp.infoString() + " + " + "???"; // TODO
-	}
-
-	@Override
-	public String infoStringTable()
-	{
-		return mdp.infoString() + " + " + "???\n"; // TODO
-	}
-
 	// Accessors (for DTMC)
 
 	@Override
diff --git a/prism/src/explicit/LTS.java b/prism/src/explicit/LTS.java
index dd10a085..294f9ab3 100644
--- a/prism/src/explicit/LTS.java
+++ b/prism/src/explicit/LTS.java
@@ -68,6 +68,24 @@ public interface LTS extends NondetModel
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
+	default String infoString()
+	{
+		String s = "";
+		s += getNumStates() + " states (" + getNumInitialStates() + " initial)";
+		s += ", " + getNumTransitions() + " transitions";
+		return s;
+	}
+
+	@Override
+	default String infoStringTable()
+	{
+		String s = "";
+		s += "States:      " + getNumStates() + " (" + getNumInitialStates() + " initial)\n";
+		s += "Transitions: " + getNumTransitions() + "\n";
+		return s;
+	}
+
 	// Accessors (for NondetModel) - default implementations
 	
 	@Override
diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java
index a3a4547c..fe88c41a 100644
--- a/prism/src/explicit/MDP.java
+++ b/prism/src/explicit/MDP.java
@@ -178,6 +178,30 @@ public interface MDP extends MDPGeneric<Double>
 		}
 	}
 
+	@Override
+	default String infoString()
+	{
+		final int numStates = getNumStates();
+		String s = "";
+		s += numStates + " states (" + getNumInitialStates() + " initial)";
+		s += ", " + getNumTransitions() + " transitions";
+		s += ", " + getNumChoices() + " choices";
+		s += ", dist max/avg = " + getMaxNumChoices() + "/" + PrismUtils.formatDouble2dp(((double) getNumChoices()) / numStates);
+		return s;
+	}
+
+	@Override
+	default String infoStringTable()
+	{
+		final int numStates = getNumStates();
+		String s = "";
+		s += "States:      " + numStates + " (" + getNumInitialStates() + " initial)\n";
+		s += "Transitions: " + getNumTransitions() + "\n";
+		s += "Choices:     " + getNumChoices() + "\n";
+		s += "Max/avg:     " + getMaxNumChoices() + "/" + PrismUtils.formatDouble2dp(((double) getNumChoices()) / numStates) + "\n";
+		return s;
+	}
+
 	// Accessors (for NondetModel) - default implementations
 	
 	@Override
diff --git a/prism/src/explicit/MDPExplicit.java b/prism/src/explicit/MDPExplicit.java
index bd3140af..a2226d44 100644
--- a/prism/src/explicit/MDPExplicit.java
+++ b/prism/src/explicit/MDPExplicit.java
@@ -29,7 +29,6 @@ package explicit;
 
 import java.util.HashSet;
 
-import prism.PrismUtils;
 import strat.MDStrategy;
 
 /**
@@ -37,30 +36,6 @@ import strat.MDStrategy;
  */
 public abstract class MDPExplicit extends ModelExplicit implements MDP
 {
-	// Accessors (for Model)
-
-	@Override
-	public String infoString()
-	{
-		String s = "";
-		s += numStates + " states (" + getNumInitialStates() + " initial)";
-		s += ", " + getNumTransitions() + " transitions";
-		s += ", " + getNumChoices() + " choices";
-		s += ", dist max/avg = " + getMaxNumChoices() + "/" + PrismUtils.formatDouble2dp(((double) getNumChoices()) / numStates);
-		return s;
-	}
-
-	@Override
-	public String infoStringTable()
-	{
-		String s = "";
-		s += "States:      " + numStates + " (" + getNumInitialStates() + " initial)\n";
-		s += "Transitions: " + getNumTransitions() + "\n";
-		s += "Choices:     " + getNumChoices() + "\n";
-		s += "Max/avg:     " + getMaxNumChoices() + "/" + PrismUtils.formatDouble2dp(((double) getNumChoices()) / numStates) + "\n";
-		return s;
-	}
-
 	// Accessors (for NondetModel)
 	
 	@Override
diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java
index 95e183f4..1551ebbe 100644
--- a/prism/src/explicit/ModelExplicit.java
+++ b/prism/src/explicit/ModelExplicit.java
@@ -389,24 +389,6 @@ public abstract class ModelExplicit implements Model
 			log.println("];");
 	}
 
-	@Override
-	public String infoString()
-	{
-		String s = "";
-		s += numStates + " states (" + getNumInitialStates() + " initial)";
-		s += ", " + getNumTransitions() + " transitions";
-		return s;
-	}
-
-	@Override
-	public String infoStringTable()
-	{
-		String s = "";
-		s += "States:      " + numStates + " (" + getNumInitialStates() + " initial)\n";
-		s += "Transitions: " + getNumTransitions() + "\n";
-		return s;
-	}
-	
 	@Override
 	public boolean equals(Object o)
 	{
diff --git a/prism/src/explicit/STPG.java b/prism/src/explicit/STPG.java
index 7dd61e82..d7edc814 100644
--- a/prism/src/explicit/STPG.java
+++ b/prism/src/explicit/STPG.java
@@ -102,6 +102,30 @@ public interface STPG extends NondetModel
 		throw new UnsupportedOperationException();
 	}
 	
+	@Override
+	default String infoString()
+	{
+		final int numStates = getNumStates();
+		String s = "";
+		s += numStates + " states (" + getNumInitialStates() + " initial)";
+		s += ", " + getNumTransitions() + " transitions";
+		s += ", " + getNumChoices() + " choices";
+		s += ", dist max/avg = " + getMaxNumChoices() + "/" + PrismUtils.formatDouble2dp(((double) getNumChoices()) / numStates);
+		return s;
+	}
+
+	@Override
+	default String infoStringTable()
+	{
+		final int numStates = getNumStates();
+		String s = "";
+		s += "States:      " + numStates + " (" + getNumInitialStates() + " initial)\n";
+		s += "Transitions: " + getNumTransitions() + "\n";
+		s += "Choices:     " + getNumChoices() + "\n";
+		s += "Max/avg:     " + getMaxNumChoices() + "/" + PrismUtils.formatDouble2dp(((double) getNumChoices()) / numStates) + "\n";
+		return s;
+	}
+
 	// Accessors
 	
 	/**
diff --git a/prism/src/explicit/STPGExplicit.java b/prism/src/explicit/STPGExplicit.java
index fc95ad6d..0ac81242 100644
--- a/prism/src/explicit/STPGExplicit.java
+++ b/prism/src/explicit/STPGExplicit.java
@@ -171,6 +171,20 @@ public class STPGExplicit extends MDPSimple implements STPG
 		STPG.super.exportToPrismLanguage(filename);
 	}
 
+	@Override
+	public String infoString()
+	{
+		// Resolve conflict: STPG interface does not (currently) extend MDP  
+		return STPG.super.infoString();
+	}
+
+	@Override
+	public String infoStringTable()
+	{
+		// Resolve conflict: STPG interface does not (currently) extend MDP  
+		return STPG.super.infoStringTable();
+	}
+
 	// Accessors (for STPG)
 
 	@Override
diff --git a/prism/src/explicit/modelviews/DTMCView.java b/prism/src/explicit/modelviews/DTMCView.java
index cc866236..2f953dac 100644
--- a/prism/src/explicit/modelviews/DTMCView.java
+++ b/prism/src/explicit/modelviews/DTMCView.java
@@ -105,26 +105,6 @@ public abstract class DTMCView extends ModelView implements DTMC, Cloneable
 		}, true);
 	}
 
-	@Override
-	public String infoString()
-	{
-		String s = "";
-		s += getNumStates() + " states (" + getNumInitialStates() + " initial)";
-		s += ", " + getNumTransitions() + " transitions";
-		return s;
-	}
-
-	@Override
-	public String infoStringTable()
-	{
-		String s = "";
-		s += "States:      " + getNumStates() + " (" + getNumInitialStates() + " initial)\n";
-		s += "Transitions: " + getNumTransitions() + "\n";
-		return s;
-	}
-
-
-
 	//--- DTMC ---
 
 	public static Entry<Integer, Pair<Double, Object>> attachAction(final Entry<Integer, Double> transition, final Object action)
diff --git a/prism/src/explicit/modelviews/MDPView.java b/prism/src/explicit/modelviews/MDPView.java
index b6ddd70a..fb5b2121 100644
--- a/prism/src/explicit/modelviews/MDPView.java
+++ b/prism/src/explicit/modelviews/MDPView.java
@@ -37,7 +37,6 @@ import explicit.Distribution;
 import explicit.MDP;
 import explicit.Model;
 import explicit.SuccessorsIterator;
-import prism.PrismUtils;
 import strat.MDStrategy;
 
 /**
@@ -88,34 +87,6 @@ public abstract class MDPView extends ModelView implements MDP, Cloneable
 		return s;
 	}
 
-
-
-	//--- Model ---
-
-	@Override
-	public String infoString()
-	{
-		final int numStates = getNumStates();
-		String s = "";
-		s += numStates + " states (" + getNumInitialStates() + " initial)";
-		s += ", " + getNumTransitions() + " transitions";
-		s += ", " + getNumChoices() + " choices";
-		s += ", dist max/avg = " + getMaxNumChoices() + "/" + PrismUtils.formatDouble2dp(((double) getNumChoices()) / numStates);
-		return s;
-	}
-
-	@Override
-	public String infoStringTable()
-	{
-		final int numStates = getNumStates();
-		String s = "";
-		s += "States:      " + numStates + " (" + getNumInitialStates() + " initial)\n";
-		s += "Transitions: " + getNumTransitions() + "\n";
-		s += "Choices:     " + getNumChoices() + "\n";
-		s += "Max/avg:     " + getMaxNumChoices() + "/" + PrismUtils.formatDouble2dp(((double) getNumChoices()) / numStates) + "\n";
-		return s;
-	}
-
 	//--- NondetModel ---
 
 	@Override