Explicit models: Move getModelType() to default implementations in interfaces.

prism/src/explicit/CTMC.java

@@ -28,11 +28,23 @@ package explicit;
 
 import java.util.BitSet;
 
+import prism.ModelType;
+
 /**
  * Interface for classes that provide (read) access to an explicit-state CTMC.
  */
 public interface CTMC extends DTMC
 {
+	// Accessors (for Model) - default implementations
+	
+	@Override
+	default ModelType getModelType()
+	{
+		return ModelType.CTMC;
+	}
+
+	// Accessors
+	
 	/**
 	 * Get the exit rate for state {@code i}.
 	 * i.e. sum_j R(i,j)

prism/src/explicit/CTMCSimple.java

@@ -26,10 +26,8 @@
 
 package explicit;
 
-import java.util.Map;
 import java.util.BitSet;
-
-import prism.ModelType;
+import java.util.Map;
 
 /**
  * Simple explicit-state representation of a CTMC.
@@ -84,14 +82,6 @@ public class CTMCSimple extends DTMCSimple implements CTMC
 		super(ctmc, permut);
 	}
 
-	// Accessors (for ModelSimple, overrides DTMCSimple)
-	
-	@Override
-	public ModelType getModelType()
-	{
-		return ModelType.CTMC;
-	}
-
 	// Accessors (for CTMC)
 	
 	@Override

prism/src/explicit/CTMDP.java

@@ -26,11 +26,23 @@
 
 package explicit;
 
+import prism.ModelType;
+
 /**
  * Interface for classes that provide (read) access to an explicit-state CTMDP.
  */
 public interface CTMDP extends MDP
 {
+	// Accessors (for Model) - default implementations
+	
+	@Override
+	default ModelType getModelType()
+	{
+		return ModelType.CTMDP;
+	}
+
+	// Accessors
+	
 	// TODO: copy/modify functions from CTMC
 	
 	/**

prism/src/explicit/CTMDPSimple.java

@@ -28,7 +28,6 @@ package explicit;
 
 import java.util.Map;
 
-import prism.ModelType;
 import prism.PrismUtils;
 
 /**
@@ -73,14 +72,6 @@ public class CTMDPSimple extends MDPSimple implements CTMDP
 		super(ctmdp, permut);
 	}
 
-	// Accessors (for ModelSimple)
-
-	@Override
-	public ModelType getModelType()
-	{
-		return ModelType.CTMDP;
-	}
-
 	// Accessors (for CTMDP)
 
 	@Override

prism/src/explicit/DTMC.java

@@ -32,6 +32,7 @@ import java.util.PrimitiveIterator.OfInt;
 
 import common.IterableStateSet;
 import common.iterable.IterableInt;
+import prism.ModelType;
 import prism.Pair;
 import prism.PrismException;
 import explicit.rewards.MCRewards;
@@ -41,6 +42,16 @@ import explicit.rewards.MCRewards;
  */
 public interface DTMC extends Model
 {
+	// Accessors (for Model) - default implementations
+	
+	@Override
+	default ModelType getModelType()
+	{
+		return ModelType.DTMC;
+	}
+
+	// Accessors
+	
 	/**
 	 * Get an iterator over the transitions from state s.
 	 */

prism/src/explicit/DTMCEmbeddedSimple.java

@@ -32,7 +32,6 @@ import java.util.Map.Entry;
 import explicit.rewards.MCRewards;
 import parser.State;
 import parser.Values;
-import prism.ModelType;
 import prism.PrismException;
 import prism.PrismNotSupportedException;
 
@@ -76,11 +75,6 @@ public class DTMCEmbeddedSimple extends DTMCExplicit
 	
 	// Accessors (for Model)
 
-	public ModelType getModelType()
-	{
-		return ModelType.DTMC;
-	}
-
 	public int getNumStates()
 	{
 		return ctmc.getNumStates();

prism/src/explicit/DTMCExplicit.java

@@ -35,7 +35,6 @@ import java.util.TreeMap;
 import java.util.Map.Entry;
 
 import explicit.graphviz.Decorator;
-import prism.ModelType;
 import prism.Pair;
 import prism.PrismException;
 import prism.PrismLog;
@@ -48,12 +47,6 @@ public abstract class DTMCExplicit extends ModelExplicit implements DTMC
 {
 	// Accessors (for Model)
 	
-	@Override
-	public ModelType getModelType()
-	{
-		return ModelType.DTMC;
-	}
-
 	@Override
 	public void exportToPrismExplicitTra(PrismLog out)
 	{

prism/src/explicit/DTMCFromMDPAndMDStrategy.java

@@ -32,7 +32,6 @@ import java.util.Map.Entry;
 import explicit.rewards.MCRewards;
 import parser.State;
 import parser.Values;
-import prism.ModelType;
 import prism.PrismException;
 import prism.PrismNotSupportedException;
 import strat.MDStrategy;
@@ -67,11 +66,6 @@ public class DTMCFromMDPAndMDStrategy extends DTMCExplicit
 
 	// Accessors (for Model)
 
-	public ModelType getModelType()
-	{
-		return ModelType.DTMC;
-	}
-
 	public int getNumStates()
 	{
 		return mdp.getNumStates();

prism/src/explicit/DTMCFromMDPMemorylessAdversary.java

@@ -34,7 +34,6 @@ import java.util.Map.Entry;
 
 import parser.State;
 import parser.Values;
-import prism.ModelType;
 import prism.Pair;
 import prism.PrismException;
 import prism.PrismNotSupportedException;
@@ -70,11 +69,6 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit
 
 	// Accessors (for Model)
 
-	public ModelType getModelType()
-	{
-		return ModelType.DTMC;
-	}
-
 	public int getNumStates()
 	{
 		return mdp.getNumStates();

prism/src/explicit/DTMCUniformisedSimple.java

@@ -35,7 +35,6 @@ import java.util.Map.Entry;
 
 import parser.State;
 import parser.Values;
-import prism.ModelType;
 import prism.PrismException;
 import prism.PrismNotSupportedException;
 import explicit.rewards.MCRewards;
@@ -89,11 +88,6 @@ public class DTMCUniformisedSimple extends DTMCExplicit
 	
 	// Accessors (for Model)
 
-	public ModelType getModelType()
-	{
-		return ModelType.DTMC;
-	}
-
 	public int getNumStates()
 	{
 		return ctmc.getNumStates();

prism/src/explicit/LTS.java

@@ -26,9 +26,18 @@
 
 package explicit;
 
+import prism.ModelType;
+
 /**
  * Interface for classes that provide (read) access to an explicit-state labelled transition system (LTS).
  */
 public interface LTS extends NondetModel
 {
+	// Accessors (for Model) - default implementations
+	
+	@Override
+	default ModelType getModelType()
+	{
+		return ModelType.LTS;
+	}
 }

prism/src/explicit/LTSExplicit.java

@@ -31,7 +31,6 @@ import java.util.ArrayList;
 import java.util.BitSet;
 import java.util.Iterator;
 
-import prism.ModelType;
 import prism.PrismException;
 import prism.PrismLog;
 import strat.MDStrategy;
@@ -160,12 +159,6 @@ public class LTSExplicit extends ModelExplicit implements LTS
 		throw new UnsupportedOperationException();
 	}
 
-	@Override
-	public ModelType getModelType()
-	{
-		return ModelType.LTS;
-	}
-
 	@Override
 	public int getNumTransitions()
 	{

prism/src/explicit/MDP.java

@@ -37,6 +37,7 @@ import java.util.PrimitiveIterator.OfInt;
 import common.IterableStateSet;
 import explicit.rewards.MCRewards;
 import explicit.rewards.MDPRewards;
+import prism.ModelType;
 import prism.PrismUtils;
 
 /**
@@ -48,6 +49,16 @@ import prism.PrismUtils;
  */
 public interface MDP extends MDPGeneric<Double>
 {
+	// Accessors (for Model) - default implementations
+	
+	@Override
+	default ModelType getModelType()
+	{
+		return ModelType.MDP;
+	}
+
+	// Accessors
+	
 	/**
 	 * Get an iterator over the transitions from choice {@code i} of state {@code s}.
 	 */

prism/src/explicit/MDPExplicit.java

@@ -35,7 +35,6 @@ import java.util.Iterator;
 import java.util.Map;
 import java.util.TreeMap;
 
-import prism.ModelType;
 import prism.PrismException;
 import prism.PrismLog;
 import prism.PrismUtils;
@@ -49,12 +48,6 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP
 {
 	// Accessors (for Model)
 
-	@Override
-	public ModelType getModelType()
-	{
-		return ModelType.MDP;
-	}
-
 	@Override
 	public String infoString()
 	{

prism/src/explicit/ModelExplicit.java

@@ -38,7 +38,6 @@ import java.util.TreeSet;
 import parser.State;
 import parser.Values;
 import parser.VarList;
-import prism.ModelType;
 import prism.Prism;
 import prism.PrismException;
 import prism.PrismFileLog;
@@ -248,9 +247,6 @@ public abstract class ModelExplicit implements Model
 
 	// Accessors (for Model interface)
 
-	@Override
-	public abstract ModelType getModelType();
-
 	@Override
 	public int getNumStates()
 	{

prism/src/explicit/STPG.java

@@ -32,6 +32,7 @@ import java.util.List;
 import java.util.Map.Entry;
 
 import explicit.rewards.STPGRewards;
+import prism.ModelType;
 
 /**
  * Interface for classes that provide (read) access to an explicit-state stochastic two-player game (STPG).
@@ -53,6 +54,16 @@ import explicit.rewards.STPGRewards;
  */
 public interface STPG extends NondetModel
 {
+	// Accessors (for Model) - default implementations
+	
+	@Override
+	default ModelType getModelType()
+	{
+		return ModelType.STPG;
+	}
+
+	// Accessors
+	
 	/**
 	 * Get the player that owns state {@code s} (1 or 2 for an STPG).
 	 */

prism/src/explicit/STPGAbstrSimple.java

@@ -34,7 +34,6 @@ import java.io.*;
 import common.IterableStateSet;
 
 import explicit.rewards.STPGRewards;
-import prism.ModelType;
 import prism.PrismException;
 import prism.PrismNotSupportedException;
 import prism.PrismLog;
@@ -274,12 +273,6 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS
 
 	// Accessors (for ModelSimple)
 
-	@Override
-	public ModelType getModelType()
-	{
-		return ModelType.STPG;
-	}
-
 	@Override
 	public int getNumTransitions()
 	{

prism/src/explicit/STPGExplicit.java

@@ -33,9 +33,9 @@ import java.util.List;
 import java.util.Map;
 import java.util.Map.Entry;
 
-import prism.ModelType;
 import explicit.rewards.MDPRewards;
 import explicit.rewards.STPGRewards;
+import prism.ModelType;
 
 /**
  * Simple explicit-state representation of a (turn-based) stochastic two-player game (STPG).
@@ -151,7 +151,8 @@ public class STPGExplicit extends MDPSimple implements STPG
 	@Override
 	public ModelType getModelType()
 	{
-		return ModelType.STPG;
+		// Resolve conflict: STPG interface does not (currently) extend MDP  
+		return STPG.super.getModelType();
 	}
 
 	// Accessors (for STPG)

prism/src/explicit/modelviews/DTMCView.java

@@ -104,12 +104,6 @@ public abstract class DTMCView extends ModelView implements DTMC, Cloneable
 
 	//--- Model ---
 
-	@Override
-	public ModelType getModelType()
-	{
-		return ModelType.DTMC;
-	}
-
 	@Override
 	public int getNumTransitions(final int s)
 	{

prism/src/explicit/modelviews/MDPView.java

@@ -33,22 +33,21 @@ import java.util.BitSet;
 import java.util.HashSet;
 import java.util.Iterator;
 import java.util.Map;
-import java.util.PrimitiveIterator;
 import java.util.Map.Entry;
+import java.util.PrimitiveIterator;
 import java.util.TreeMap;
 
 import common.IteratorTools;
-import prism.ModelType;
-import prism.PrismException;
-import prism.PrismLog;
-import prism.PrismUtils;
-import strat.MDStrategy;
 import explicit.DTMCFromMDPAndMDStrategy;
 import explicit.Distribution;
 import explicit.MDP;
 import explicit.Model;
 import explicit.SuccessorsIterator;
 import explicit.graphviz.Decorator;
+import prism.PrismException;
+import prism.PrismLog;
+import prism.PrismUtils;
+import strat.MDStrategy;
 
 /**
  * Base class for an MDP view, i.e., a virtual MDP that is obtained
@@ -102,12 +101,6 @@ public abstract class MDPView extends ModelView implements MDP, Cloneable
 
 	//--- Model ---
 
-	@Override
-	public ModelType getModelType()
-	{
-		return ModelType.MDP;
-	}
-
 	@Override
 	public int getNumTransitions(int s)
 	{