explicit.DTMC, refactor: remove specialized prob0step, prob1step in sub-classes in favor of default methods in DTMC

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12087 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/DTMCEmbeddedSimple.java

@@ -266,20 +266,6 @@ public class DTMCEmbeddedSimple extends DTMCExplicit
 		}
 	}
 
-	public void prob0step(BitSet subset, BitSet u, BitSet result)
-	{
-		for (int i : new IterableStateSet(subset, numStates)) {
-			result.set(i, someSuccessorsInSet(i, u));
-		}
-	}
-
-	public void prob1step(BitSet subset, BitSet u, BitSet v, BitSet result)
-	{
-		for (int i : new IterableStateSet(subset, numStates)) {
-			result.set(i, someSuccessorsInSet(i, v) && allSuccessorsInSet(i, u));
-		}
-	}
-
 	public double mvMultSingle(int s, double vect[])
 	{
 		int k;

prism/src/explicit/DTMCFromMDPAndMDStrategy.java

@@ -196,21 +196,6 @@ public class DTMCFromMDPAndMDStrategy extends DTMCExplicit
 		}
 	}
 
-	public void prob0step(BitSet subset, BitSet u, BitSet result)
-	{
-		for (int i : new IterableStateSet(subset, numStates)) {
-			result.set(i, mdp.someSuccessorsInSet(i, strat.getChoiceIndex(i), u));
-		}
-	}
-
-	public void prob1step(BitSet subset, BitSet u, BitSet v, BitSet result)
-	{
-		for (int i : new IterableStateSet(subset, numStates)) {
-			int j = strat.getChoiceIndex(i);
-			result.set(i, mdp.someSuccessorsInSet(i, j, v) && mdp.allSuccessorsInSet(i, j, u));
-		}
-	}
-
 	@Override
 	public double mvMultSingle(int s, double vect[])
 	{

prism/src/explicit/DTMCFromMDPMemorylessAdversary.java

@@ -196,21 +196,6 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit
 		}
 	}
 
-	public void prob0step(BitSet subset, BitSet u, BitSet result)
-	{
-		// TODO
-		throw new Error("Not yet supported");
-	}
-
-	public void prob1step(BitSet subset, BitSet u, BitSet v, BitSet result)
-	{
-		for (int s = 0; s < numStates; s++) {
-			if (subset.get(s)) {
-				result.set(s, mdp.prob1stepSingle(s, adv[s], u, v));
-			}
-		}
-	}
-
 	@Override
 	public double mvMultSingle(int s, double vect[])
 	{

prism/src/explicit/DTMCSimple.java

@@ -274,26 +274,6 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple
 		return trans.get(s).iterator();
 	}
 
-	@Override
-	public void prob0step(BitSet subset, BitSet u, BitSet result)
-	{
-		Distribution distr;
-		for (int i : new IterableStateSet(subset, numStates)) {
-			distr = trans.get(i);
-			result.set(i, distr.containsOneOf(u));
-		}
-	}
-
-	@Override
-	public void prob1step(BitSet subset, BitSet u, BitSet v, BitSet result)
-	{
-		Distribution distr;
-		for (int i : new IterableStateSet(subset, numStates)) {
-			distr = trans.get(i);
-			result.set(i, distr.containsOneOf(v) && distr.isSubsetOf(u));
-		}
-	}
-
 	@Override
 	public double mvMultSingle(int s, double vect[])
 	{

prism/src/explicit/DTMCUniformisedSimple.java

@@ -193,18 +193,6 @@ public class DTMCUniformisedSimple extends DTMCExplicit
 		throw new RuntimeException("Not implemented yet");
 	}
 
-	public void prob0step(BitSet subset, BitSet u, BitSet result)
-	{
-		// TODO
-		throw new Error("Not yet supported");
-	}
-
-	public void prob1step(BitSet subset, BitSet u, BitSet v, BitSet result)
-	{
-		// TODO
-		throw new Error("Not yet supported");
-	}
-
 	@Override
 	public double mvMultSingle(int s, double vect[])
 	{