Explicit models: Move infoString methods to default implementations in interfaces.

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
 	
 	/**

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)

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

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

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

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

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)
 	{

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
 	
 	/**

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

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)

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