diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 5669ff0d..4a33a7ee 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/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[]) {