explicit.MDPSimple: remove specializations for prob0/prob1, use default methods from explicit.MDP

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

prism/src/explicit/MDPSimple.java

@@ -573,105 +573,6 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
 		return trans.get(s).get(i).iterator();
 	}
 
-	@Override
-	public void prob0step(BitSet subset, BitSet u, boolean forall, BitSet result)
-	{
-		boolean b1, b2;
-		for (int i : new IterableStateSet(subset, numStates)) {
-			b1 = forall; // there exists or for all
-			for (Distribution distr : trans.get(i)) {
-				b2 = distr.containsOneOf(u);
-				if (forall) {
-					if (!b2) {
-						b1 = false;
-						break;
-					}
-				} else {
-					if (b2) {
-						b1 = true;
-						break;
-					}
-				}
-			}
-			result.set(i, b1);
-		}
-	}
-
-	@Override
-	public void prob1Astep(BitSet subset, BitSet u, BitSet v, BitSet result)
-	{
-		boolean b1;
-		for (int i : new IterableStateSet(subset, numStates)) {
-			b1 = true;
-			for (Distribution distr : trans.get(i)) {
-				if (!(distr.isSubsetOf(u) && distr.containsOneOf(v))) {
-					b1 = false;
-					break;
-				}
-			}
-			result.set(i, b1);
-		}
-	}
-
-	@Override
-	public void prob1Estep(BitSet subset, BitSet u, BitSet v, BitSet result, int strat[])
-	{
-		int j, stratCh = -1;
-		boolean b1;
-		for (int i : new IterableStateSet(subset, numStates)) {
-			j = 0;
-			b1 = false;
-			for (Distribution distr : trans.get(i)) {
-				if (distr.isSubsetOf(u) && distr.containsOneOf(v)) {
-					b1 = true;
-					// If strategy generation is enabled, remember optimal choice
-					if (strat != null)
-						stratCh = j;
-					break;
-				}
-				j++;
-			}
-			// If strategy generation is enabled, store optimal choice
-			// (only if this the first time we add the state to S^yes)
-			if (strat != null & b1 & !result.get(i)) {
-				strat[i] = stratCh;
-			}
-			// Store result
-			result.set(i, b1);
-		}
-	}
-
-	@Override
-	public void prob1step(BitSet subset, BitSet u, BitSet v, boolean forall, BitSet result)
-	{
-		boolean b1, b2;
-		for (int i : new IterableStateSet(subset, numStates)) {
-			b1 = forall; // there exists or for all
-			for (Distribution distr : trans.get(i)) {
-				b2 = distr.containsOneOf(v) && distr.isSubsetOf(u);
-				if (forall) {
-					if (!b2) {
-						b1 = false;
-						break;
-					}
-				} else {
-					if (b2) {
-						b1 = true;
-						break;
-					}
-				}
-			}
-			result.set(i, b1);
-		}
-	}
-
-	@Override
-	public boolean prob1stepSingle(int s, int i, BitSet u, BitSet v)
-	{
-		Distribution distr = trans.get(s).get(i);
-		return distr.containsOneOf(v) && distr.isSubsetOf(u);
-	}
-
 	@Override
 	public double mvMultMinMaxSingle(int s, double vect[], boolean min, int strat[])
 	{