From 059dbb6b248fcbe5cbcfdaa863686bd6dcea05d1 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 28 May 2020 11:24:00 +0100 Subject: [PATCH] Explicit models: Move getModelType() to default implementations in interfaces. --- prism/src/explicit/CTMC.java | 12 ++++++++++++ prism/src/explicit/CTMCSimple.java | 12 +----------- prism/src/explicit/CTMDP.java | 12 ++++++++++++ prism/src/explicit/CTMDPSimple.java | 9 --------- prism/src/explicit/DTMC.java | 11 +++++++++++ prism/src/explicit/DTMCEmbeddedSimple.java | 6 ------ prism/src/explicit/DTMCExplicit.java | 7 ------- .../src/explicit/DTMCFromMDPAndMDStrategy.java | 6 ------ .../DTMCFromMDPMemorylessAdversary.java | 6 ------ prism/src/explicit/DTMCUniformisedSimple.java | 6 ------ prism/src/explicit/LTS.java | 9 +++++++++ prism/src/explicit/LTSExplicit.java | 7 ------- prism/src/explicit/MDP.java | 11 +++++++++++ prism/src/explicit/MDPExplicit.java | 7 ------- prism/src/explicit/ModelExplicit.java | 4 ---- prism/src/explicit/STPG.java | 11 +++++++++++ prism/src/explicit/STPGAbstrSimple.java | 7 ------- prism/src/explicit/STPGExplicit.java | 5 +++-- prism/src/explicit/modelviews/DTMCView.java | 6 ------ prism/src/explicit/modelviews/MDPView.java | 17 +++++------------ 20 files changed, 75 insertions(+), 96 deletions(-) diff --git a/prism/src/explicit/CTMC.java b/prism/src/explicit/CTMC.java index 38b769a1..a8cce89c 100644 --- a/prism/src/explicit/CTMC.java +++ b/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) diff --git a/prism/src/explicit/CTMCSimple.java b/prism/src/explicit/CTMCSimple.java index fd9a31dc..a37cb18e 100644 --- a/prism/src/explicit/CTMCSimple.java +++ b/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 diff --git a/prism/src/explicit/CTMDP.java b/prism/src/explicit/CTMDP.java index 7a432527..e9d2aac8 100644 --- a/prism/src/explicit/CTMDP.java +++ b/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 /** diff --git a/prism/src/explicit/CTMDPSimple.java b/prism/src/explicit/CTMDPSimple.java index 9ecf9780..ccce0bf3 100644 --- a/prism/src/explicit/CTMDPSimple.java +++ b/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 diff --git a/prism/src/explicit/DTMC.java b/prism/src/explicit/DTMC.java index 4b58dde6..b843e876 100644 --- a/prism/src/explicit/DTMC.java +++ b/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. */ diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index fe079282..15292fb7 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/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(); diff --git a/prism/src/explicit/DTMCExplicit.java b/prism/src/explicit/DTMCExplicit.java index 79c8fed2..d4fe8505 100644 --- a/prism/src/explicit/DTMCExplicit.java +++ b/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) { diff --git a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java index 75084191..495c6f72 100644 --- a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java +++ b/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(); diff --git a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java index fd3fd51e..520afd08 100644 --- a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java +++ b/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(); diff --git a/prism/src/explicit/DTMCUniformisedSimple.java b/prism/src/explicit/DTMCUniformisedSimple.java index 4cc7a9c0..72bcdd76 100644 --- a/prism/src/explicit/DTMCUniformisedSimple.java +++ b/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(); diff --git a/prism/src/explicit/LTS.java b/prism/src/explicit/LTS.java index 8578fe55..3c0736ce 100644 --- a/prism/src/explicit/LTS.java +++ b/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; + } } diff --git a/prism/src/explicit/LTSExplicit.java b/prism/src/explicit/LTSExplicit.java index 4b1958aa..9e066287 100644 --- a/prism/src/explicit/LTSExplicit.java +++ b/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() { diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index 613d0a20..e6f51a1c 100644 --- a/prism/src/explicit/MDP.java +++ b/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 { + // 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}. */ diff --git a/prism/src/explicit/MDPExplicit.java b/prism/src/explicit/MDPExplicit.java index 8ec497da..3e7d2bd3 100644 --- a/prism/src/explicit/MDPExplicit.java +++ b/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() { diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index b498a38f..ba533a3e 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/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() { diff --git a/prism/src/explicit/STPG.java b/prism/src/explicit/STPG.java index 904ff65d..eb6b4336 100644 --- a/prism/src/explicit/STPG.java +++ b/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). */ diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index 02a23c96..e42498ef 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/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() { diff --git a/prism/src/explicit/STPGExplicit.java b/prism/src/explicit/STPGExplicit.java index df71ea54..ff41145a 100644 --- a/prism/src/explicit/STPGExplicit.java +++ b/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) diff --git a/prism/src/explicit/modelviews/DTMCView.java b/prism/src/explicit/modelviews/DTMCView.java index 563cdcd8..fd5e9abe 100644 --- a/prism/src/explicit/modelviews/DTMCView.java +++ b/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) { diff --git a/prism/src/explicit/modelviews/MDPView.java b/prism/src/explicit/modelviews/MDPView.java index f5295447..dc193bde 100644 --- a/prism/src/explicit/modelviews/MDPView.java +++ b/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) {