From a18d28a17bb90585cf6a068be65843476b87ae92 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 23 Jan 2015 01:46:31 +0000 Subject: [PATCH] Refactor: use IterableStateSet to simplify loops [Joachim Klein]. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9543 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCEmbeddedSimple.java | 16 +- prism/src/explicit/DTMCExplicit.java | 67 ++----- prism/src/explicit/DTMCSimple.java | 20 +- prism/src/explicit/MDPExplicit.java | 84 ++------ prism/src/explicit/MDPSimple.java | 121 ++++++------ prism/src/explicit/MDPSparse.java | 220 ++++++++++----------- prism/src/explicit/STPGAbstrSimple.java | 138 +++++-------- 7 files changed, 258 insertions(+), 408 deletions(-) diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index 0009766c..3fad7719 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/prism/src/explicit/DTMCEmbeddedSimple.java @@ -29,6 +29,8 @@ package explicit; import java.util.*; import java.util.Map.Entry; +import common.IterableStateSet; + import explicit.rewards.MCRewards; import parser.State; import parser.Values; @@ -258,21 +260,15 @@ public class DTMCEmbeddedSimple extends DTMCExplicit public void prob0step(BitSet subset, BitSet u, BitSet result) { - int i; - for (i = 0; i < numStates; i++) { - if (subset.get(i)) { - result.set(i, someSuccessorsInSet(i, u)); - } + for (int i : new IterableStateSet(subset, numStates)) { + result.set(i, someSuccessorsInSet(i, u)); } } public void prob1step(BitSet subset, BitSet u, BitSet v, BitSet result) { - int i; - for (i = 0; i < numStates; i++) { - if (subset.get(i)) { - result.set(i, someSuccessorsInSet(i, v) && allSuccessorsInSet(i, u)); - } + for (int i : new IterableStateSet(subset, numStates)) { + result.set(i, someSuccessorsInSet(i, v) && allSuccessorsInSet(i, u)); } } diff --git a/prism/src/explicit/DTMCExplicit.java b/prism/src/explicit/DTMCExplicit.java index b11e70c4..7efb5ec2 100644 --- a/prism/src/explicit/DTMCExplicit.java +++ b/prism/src/explicit/DTMCExplicit.java @@ -33,8 +33,9 @@ import java.util.Iterator; import java.util.Map; import java.util.TreeMap; -import explicit.rewards.MCRewards; +import common.IterableStateSet; +import explicit.rewards.MCRewards; import prism.ModelType; import prism.PrismException; import prism.PrismLog; @@ -152,74 +153,38 @@ public abstract class DTMCExplicit extends ModelExplicit implements DTMC @Override public void mvMult(double vect[], double result[], BitSet subset, boolean complement) { - int s; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) - result[s] = mvMultSingle(s, vect); - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) - result[s] = mvMultSingle(s, vect); - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) - result[s] = mvMultSingle(s, vect); + for (int s : new IterableStateSet(subset, numStates, complement)) { + result[s] = mvMultSingle(s, vect); } } @Override public double mvMultGS(double vect[], BitSet subset, boolean complement, boolean absolute) { - int s; double d, diff, maxDiff = 0.0; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) { - d = mvMultJacSingle(s, vect); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) { - d = mvMultJacSingle(s, vect); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) { + for (int s : new IterableStateSet(subset, numStates, complement)) { + d = mvMultJacSingle(s, vect); + diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); + maxDiff = diff > maxDiff ? diff : maxDiff; + vect[s] = d; + } + // Use this code instead for backwards Gauss-Seidel + /*for (s = numStates - 1; s >= 0; s--) { + if (subset.get(s)) { d = mvMultJacSingle(s, vect); diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); maxDiff = diff > maxDiff ? diff : maxDiff; vect[s] = d; } - // Use this code instead for backwards Gauss-Seidel - /*for (s = numStates - 1; s >= 0; s--) { - if (subset.get(s)) { - d = mvMultJacSingle(s, vect); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } - }*/ - } + }*/ return maxDiff; } @Override public void mvMultRew(double vect[], MCRewards mcRewards, double result[], BitSet subset, boolean complement) { - int s; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) - result[s] = mvMultRewSingle(s, vect, mcRewards); - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) - result[s] = mvMultRewSingle(s, vect, mcRewards); - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) - result[s] = mvMultRewSingle(s, vect, mcRewards); + for (int s : new IterableStateSet(subset, numStates, complement)) { + result[s] = mvMultRewSingle(s, vect, mcRewards); } } } diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index 4fe17445..3e0d5c15 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/prism/src/explicit/DTMCSimple.java @@ -30,6 +30,8 @@ import java.util.*; import java.util.Map.Entry; import java.io.*; +import common.IterableStateSet; + import explicit.rewards.*; import prism.PrismException; @@ -276,26 +278,20 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple @Override public void prob0step(BitSet subset, BitSet u, BitSet result) { - int i; Distribution distr; - for (i = 0; i < numStates; i++) { - if (subset.get(i)) { - distr = trans.get(i); - result.set(i, distr.containsOneOf(u)); - } + 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) { - int i; Distribution distr; - for (i = 0; i < numStates; i++) { - if (subset.get(i)) { - distr = trans.get(i); - result.set(i, distr.containsOneOf(v) && distr.isSubsetOf(u)); - } + for (int i : new IterableStateSet(subset, numStates)) { + distr = trans.get(i); + result.set(i, distr.containsOneOf(v) && distr.isSubsetOf(u)); } } diff --git a/prism/src/explicit/MDPExplicit.java b/prism/src/explicit/MDPExplicit.java index 27ea93f2..53a5276f 100644 --- a/prism/src/explicit/MDPExplicit.java +++ b/prism/src/explicit/MDPExplicit.java @@ -35,6 +35,8 @@ import java.util.Iterator; import java.util.Map; import java.util.TreeMap; +import common.IterableStateSet; + import prism.ModelType; import prism.PrismException; import prism.PrismLog; @@ -233,47 +235,20 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP @Override public void mvMultMinMax(double vect[], boolean min, double result[], BitSet subset, boolean complement, int strat[]) { - int s; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) - result[s] = mvMultMinMaxSingle(s, vect, min, strat); - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) - result[s] = mvMultMinMaxSingle(s, vect, min, strat); - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) - result[s] = mvMultMinMaxSingle(s, vect, min, strat); + for (int s : new IterableStateSet(subset, numStates, complement)) { + result[s] = mvMultMinMaxSingle(s, vect, min, strat); } } @Override public double mvMultGSMinMax(double vect[], boolean min, BitSet subset, boolean complement, boolean absolute, int strat[]) { - int s; double d, diff, maxDiff = 0.0; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) { - d = mvMultJacMinMaxSingle(s, vect, min, strat); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) { - d = mvMultJacMinMaxSingle(s, vect, min, strat); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) { - d = mvMultJacMinMaxSingle(s, vect, min, strat); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } + for (int s : new IterableStateSet(subset, numStates, complement)) { + d = mvMultJacMinMaxSingle(s, vect, min, strat); + diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); + maxDiff = diff > maxDiff ? diff : maxDiff; + vect[s] = d; } // Use this code instead for backwards Gauss-Seidel /*for (s = numStates - 1; s >= 0; s--) { @@ -290,47 +265,20 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP @Override public void mvMultRewMinMax(double vect[], MDPRewards mdpRewards, boolean min, double result[], BitSet subset, boolean complement, int strat[]) { - int s; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) - result[s] = mvMultRewMinMaxSingle(s, vect, mdpRewards, min, strat); - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) - result[s] = mvMultRewMinMaxSingle(s, vect, mdpRewards, min, strat); - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) - result[s] = mvMultRewMinMaxSingle(s, vect, mdpRewards, min, strat); + for (int s : new IterableStateSet(subset, numStates, complement)) { + result[s] = mvMultRewMinMaxSingle(s, vect, mdpRewards, min, strat); } } @Override public double mvMultRewGSMinMax(double vect[], MDPRewards mdpRewards, boolean min, BitSet subset, boolean complement, boolean absolute, int strat[]) { - int s; double d, diff, maxDiff = 0.0; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) { - d = mvMultRewJacMinMaxSingle(s, vect, mdpRewards, min, strat); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) { - d = mvMultRewJacMinMaxSingle(s, vect, mdpRewards, min, strat); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) { - d = mvMultRewJacMinMaxSingle(s, vect, mdpRewards, min, strat); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } + for (int s : new IterableStateSet(subset, numStates, complement)) { + d = mvMultRewJacMinMaxSingle(s, vect, mdpRewards, min, strat); + diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); + maxDiff = diff > maxDiff ? diff : maxDiff; + vect[s] = d; } // Use this code instead for backwards Gauss-Seidel /*for (s = numStates - 1; s >= 0; s--) { diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 41ce34bf..97d1bf32 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -39,6 +39,8 @@ import java.util.List; import java.util.Map; import java.util.Map.Entry; +import common.IterableStateSet; + import prism.PrismException; import prism.PrismUtils; import explicit.rewards.MCRewards; @@ -578,103 +580,92 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple @Override public void prob0step(BitSet subset, BitSet u, boolean forall, BitSet result) { - int i; boolean b1, b2; - for (i = 0; i < numStates; i++) { - if (subset.get(i)) { - b1 = forall; // there exists or for all - for (Distribution distr : trans.get(i)) { - b2 = distr.containsOneOf(u); - if (forall) { - if (!b2) { - b1 = false; - continue; - } - } else { - if (b2) { - b1 = true; - continue; - } + 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; + continue; + } + } else { + if (b2) { + b1 = true; + continue; } } - result.set(i, b1); } + result.set(i, b1); } } @Override public void prob1Astep(BitSet subset, BitSet u, BitSet v, BitSet result) { - int i; boolean b1; - for (i = 0; i < numStates; i++) { - if (subset.get(i)) { - b1 = true; - for (Distribution distr : trans.get(i)) { - if (!(distr.isSubsetOf(u) && distr.containsOneOf(v))) { - b1 = false; - continue; - } + for (int i : new IterableStateSet(subset, numStates)) { + b1 = true; + for (Distribution distr : trans.get(i)) { + if (!(distr.isSubsetOf(u) && distr.containsOneOf(v))) { + b1 = false; + continue; } - result.set(i, b1); } + result.set(i, b1); } } @Override public void prob1Estep(BitSet subset, BitSet u, BitSet v, BitSet result, int strat[]) { - int i, j, stratCh = -1; + int j, stratCh = -1; boolean b1; - for (i = 0; i < numStates; i++) { - if (subset.get(i)) { - 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; - continue; - } - 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; + 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; + continue; } - // Store result - result.set(i, b1); + 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) { - int i; boolean b1, b2; - for (i = 0; i < numStates; i++) { - if (subset.get(i)) { - 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; - continue; - } - } else { - if (b2) { - b1 = true; - continue; - } + 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; + continue; + } + } else { + if (b2) { + b1 = true; + continue; } } - result.set(i, b1); } + result.set(i, b1); } } diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index 0dd86b54..a137bc2a 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -40,6 +40,8 @@ import java.util.Map; import java.util.Map.Entry; import java.util.TreeMap; +import common.IterableStateSet; + import parser.State; import prism.PrismException; import prism.PrismUtils; @@ -612,158 +614,150 @@ public class MDPSparse extends MDPExplicit @Override public void prob0step(BitSet subset, BitSet u, boolean forall, BitSet result) { - int i, j, k, l1, h1, l2, h2; + int j, k, l1, h1, l2, h2; boolean b1, some; - for (i = 0; i < numStates; i++) { - if (subset.get(i)) { - b1 = forall; // there exists or for all - l1 = rowStarts[i]; - h1 = rowStarts[i + 1]; - for (j = l1; j < h1; j++) { - some = false; - l2 = choiceStarts[j]; - h2 = choiceStarts[j + 1]; - for (k = l2; k < h2; k++) { - // Assume that only non-zero entries are stored - if (u.get(cols[k])) { - some = true; - continue; - } + for (int i : new IterableStateSet(subset, numStates)) { + b1 = forall; // there exists or for all + l1 = rowStarts[i]; + h1 = rowStarts[i + 1]; + for (j = l1; j < h1; j++) { + some = false; + l2 = choiceStarts[j]; + h2 = choiceStarts[j + 1]; + for (k = l2; k < h2; k++) { + // Assume that only non-zero entries are stored + if (u.get(cols[k])) { + some = true; + continue; } - if (forall) { - if (!some) { - b1 = false; - continue; - } - } else { - if (some) { - b1 = true; - continue; - } + } + if (forall) { + if (!some) { + b1 = false; + continue; + } + } else { + if (some) { + b1 = true; + continue; } } - result.set(i, b1); } + result.set(i, b1); } } @Override public void prob1Astep(BitSet subset, BitSet u, BitSet v, BitSet result) { - int i, j, k, l1, h1, l2, h2; + int j, k, l1, h1, l2, h2; boolean b1, some, all; - for (i = 0; i < numStates; i++) { - if (subset.get(i)) { - b1 = true; - l1 = rowStarts[i]; - h1 = rowStarts[i + 1]; - for (j = l1; j < h1; j++) { - some = false; - all = true; - l2 = choiceStarts[j]; - h2 = choiceStarts[j + 1]; - for (k = l2; k < h2; k++) { - // Assume that only non-zero entries are stored - if (!u.get(cols[k])) { - all = false; - continue; // Stop early (already know b1 will be set to false) - } - if (v.get(cols[k])) { - some = true; - } + for (int i : new IterableStateSet(subset, numStates)) { + b1 = true; + l1 = rowStarts[i]; + h1 = rowStarts[i + 1]; + for (j = l1; j < h1; j++) { + some = false; + all = true; + l2 = choiceStarts[j]; + h2 = choiceStarts[j + 1]; + for (k = l2; k < h2; k++) { + // Assume that only non-zero entries are stored + if (!u.get(cols[k])) { + all = false; + continue; // Stop early (already know b1 will be set to false) } - if (!(some && all)) { - b1 = false; - continue; + if (v.get(cols[k])) { + some = true; } } - result.set(i, b1); + if (!(some && all)) { + b1 = false; + continue; + } } + result.set(i, b1); } } @Override public void prob1Estep(BitSet subset, BitSet u, BitSet v, BitSet result, int strat[]) { - int i, j, k, l1, h1, l2, h2, stratCh = -1; + int j, k, l1, h1, l2, h2, stratCh = -1; boolean b1, some, all; - for (i = 0; i < numStates; i++) { - if (subset.get(i)) { - b1 = false; - l1 = rowStarts[i]; - h1 = rowStarts[i + 1]; - for (j = l1; j < h1; j++) { - some = false; - all = true; - l2 = choiceStarts[j]; - h2 = choiceStarts[j + 1]; - for (k = l2; k < h2; k++) { - // Assume that only non-zero entries are stored - if (!u.get(cols[k])) { - all = false; - continue; // Stop early (already know b1 will not be set to true) - } - if (v.get(cols[k])) { - some = true; - } + for (int i : new IterableStateSet(subset, numStates)) { + b1 = false; + l1 = rowStarts[i]; + h1 = rowStarts[i + 1]; + for (j = l1; j < h1; j++) { + some = false; + all = true; + l2 = choiceStarts[j]; + h2 = choiceStarts[j + 1]; + for (k = l2; k < h2; k++) { + // Assume that only non-zero entries are stored + if (!u.get(cols[k])) { + all = false; + continue; // Stop early (already know b1 will not be set to true) } - if (some && all) { - b1 = true; - // If strategy generation is enabled, remember optimal choice - if (strat != null) - stratCh = j - l1; - continue; + if (v.get(cols[k])) { + some = true; } } - // 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; + if (some && all) { + b1 = true; + // If strategy generation is enabled, remember optimal choice + if (strat != null) + stratCh = j - l1; + continue; } - // Store result - result.set(i, b1); } + // 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) { - int i, j, k, l1, h1, l2, h2; + int j, k, l1, h1, l2, h2; boolean b1, some, all; - for (i = 0; i < numStates; i++) { - if (subset.get(i)) { - b1 = forall; // there exists or for all - l1 = rowStarts[i]; - h1 = rowStarts[i + 1]; - for (j = l1; j < h1; j++) { - some = false; - all = true; - l2 = choiceStarts[j]; - h2 = choiceStarts[j + 1]; - for (k = l2; k < h2; k++) { - // Assume that only non-zero entries are stored - if (v.get(cols[k])) { - some = true; - } - if (!u.get(cols[k])) { - all = false; - } + for (int i : new IterableStateSet(subset, numStates)) { + b1 = forall; // there exists or for all + l1 = rowStarts[i]; + h1 = rowStarts[i + 1]; + for (j = l1; j < h1; j++) { + some = false; + all = true; + l2 = choiceStarts[j]; + h2 = choiceStarts[j + 1]; + for (k = l2; k < h2; k++) { + // Assume that only non-zero entries are stored + if (v.get(cols[k])) { + some = true; } - if (forall) { - if (!(some && all)) { - b1 = false; - continue; - } - } else { - if (some && all) { - b1 = true; - continue; - } + if (!u.get(cols[k])) { + all = false; + } + } + if (forall) { + if (!(some && all)) { + b1 = false; + continue; + } + } else { + if (some && all) { + b1 = true; + continue; } } - result.set(i, b1); } + result.set(i, b1); } } diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index 0a67faa5..4706ef02 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/prism/src/explicit/STPGAbstrSimple.java @@ -31,6 +31,8 @@ import java.util.*; import java.util.Map.Entry; import java.io.*; +import common.IterableStateSet; + import explicit.rewards.STPGRewards; import prism.ModelType; import prism.PrismException; @@ -596,83 +598,68 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS @Override public void prob0step(BitSet subset, BitSet u, boolean forall1, boolean forall2, BitSet result) { - int i; boolean b1, b2, b3; - for (i = 0; i < numStates; i++) { - if (subset.get(i)) { - b1 = forall1; // there exists or for all player 1 choices - for (DistributionSet distrs : trans.get(i)) { - b2 = forall2; // there exists or for all player 2 choices - for (Distribution distr : distrs) { - b3 = distr.containsOneOf(u); - if (forall2) { - if (!b3) - b2 = false; - } else { - if (b3) - b2 = true; - } - } - if (forall1) { - if (!b2) - b1 = false; + for (int i : new IterableStateSet(subset, numStates)) { + b1 = forall1; // there exists or for all player 1 choices + for (DistributionSet distrs : trans.get(i)) { + b2 = forall2; // there exists or for all player 2 choices + for (Distribution distr : distrs) { + b3 = distr.containsOneOf(u); + if (forall2) { + if (!b3) + b2 = false; } else { - if (b2) - b1 = true; + if (b3) + b2 = true; } } - result.set(i, b1); + if (forall1) { + if (!b2) + b1 = false; + } else { + if (b2) + b1 = true; + } } + result.set(i, b1); } } @Override public void prob1step(BitSet subset, BitSet u, BitSet v, boolean forall1, boolean forall2, BitSet result) { - int i; boolean b1, b2, b3; - for (i = 0; i < numStates; i++) { - if (subset.get(i)) { - b1 = forall1; // there exists or for all player 1 choices - for (DistributionSet distrs : trans.get(i)) { - b2 = forall2; // there exists or for all player 2 choices - for (Distribution distr : distrs) { - b3 = distr.containsOneOf(v) && distr.isSubsetOf(u); - if (forall2) { - if (!b3) - b2 = false; - } else { - if (b3) - b2 = true; - } - } - if (forall1) { - if (!b2) - b1 = false; + for (int i : new IterableStateSet(subset, numStates)) { + b1 = forall1; // there exists or for all player 1 choices + for (DistributionSet distrs : trans.get(i)) { + b2 = forall2; // there exists or for all player 2 choices + for (Distribution distr : distrs) { + b3 = distr.containsOneOf(v) && distr.isSubsetOf(u); + if (forall2) { + if (!b3) + b2 = false; } else { - if (b2) - b1 = true; + if (b3) + b2 = true; } } - result.set(i, b1); + if (forall1) { + if (!b2) + b1 = false; + } else { + if (b2) + b1 = true; + } } + result.set(i, b1); } } @Override public void mvMultMinMax(double vect[], boolean min1, boolean min2, double result[], BitSet subset, boolean complement, int adv[]) { - int s; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) - result[s] = mvMultMinMaxSingle(s, vect, min1, min2); - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) - result[s] = mvMultMinMaxSingle(s, vect, min1, min2); - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) - result[s] = mvMultMinMaxSingle(s, vect, min1, min2); + for (int s : new IterableStateSet(subset, numStates, complement)) { + result[s] = mvMultMinMaxSingle(s, vect, min1, min2); } } @@ -757,30 +744,12 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS @Override public double mvMultGSMinMax(double vect[], boolean min1, boolean min2, BitSet subset, boolean complement, boolean absolute) { - int s; double d, diff, maxDiff = 0.0; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) { - d = mvMultJacMinMaxSingle(s, vect, min1, min2); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) { - d = mvMultJacMinMaxSingle(s, vect, min1, min2); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) { - d = mvMultJacMinMaxSingle(s, vect, min1, min2); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } + for (int s : new IterableStateSet(subset, numStates, complement)) { + d = mvMultJacMinMaxSingle(s, vect, min1, min2); + diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); + maxDiff = diff > maxDiff ? diff : maxDiff; + vect[s] = d; } return maxDiff; } @@ -831,17 +800,8 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS @Override public void mvMultRewMinMax(double vect[], STPGRewards rewards, boolean min1, boolean min2, double result[], BitSet subset, boolean complement, int adv[]) { - int s; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) - result[s] = mvMultRewMinMaxSingle(s, vect, rewards, min1, min2, adv); - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) - result[s] = mvMultRewMinMaxSingle(s, vect, rewards, min1, min2, adv); - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) - result[s] = mvMultRewMinMaxSingle(s, vect, rewards, min1, min2, adv); + for (int s : new IterableStateSet(subset, numStates, complement)) { + result[s] = mvMultRewMinMaxSingle(s, vect, rewards, min1, min2, adv); } }