diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index 4a7c62da..48dd8e44 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/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; diff --git a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java index d0c48ad2..dbb6c616 100644 --- a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java +++ b/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[]) { diff --git a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java index 6c011199..6f24cab8 100644 --- a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java +++ b/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[]) { diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index 19d9c4c8..ec2f67d5 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/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[]) { diff --git a/prism/src/explicit/DTMCUniformisedSimple.java b/prism/src/explicit/DTMCUniformisedSimple.java index 62be8c84..b5bf79ac 100644 --- a/prism/src/explicit/DTMCUniformisedSimple.java +++ b/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[]) {