s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

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
master
Dave Parker 11 years ago
parent
95feea13ce
commit
a18d28a17b
7 changed files with 258 additions and 408 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 16
      prism/src/explicit/DTMCEmbeddedSimple.java
  2. 67
      prism/src/explicit/DTMCExplicit.java
  3. 20
      prism/src/explicit/DTMCSimple.java
  4. 84
      prism/src/explicit/MDPExplicit.java
  5. 121
      prism/src/explicit/MDPSimple.java
  6. 220
      prism/src/explicit/MDPSparse.java
  7. 138
      prism/src/explicit/STPGAbstrSimple.java

16
prism/src/explicit/DTMCEmbeddedSimple.java
View File

@ -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));
}
}

67
prism/src/explicit/DTMCExplicit.java
View File

@ -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);
}
}
}

20
prism/src/explicit/DTMCSimple.java
View File

@ -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));
}
}

84
prism/src/explicit/MDPExplicit.java
View File

@ -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--) {

121
prism/src/explicit/MDPSimple.java
View File

@ -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);
}
}

220
prism/src/explicit/MDPSparse.java
View File

@ -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);
}
}

138
prism/src/explicit/STPGAbstrSimple.java
View File

@ -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);
}
}

Write Preview
Loading…
Cancel
Save