Browse Source

Bug fix: reward structure indices start from 1 on export.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@907 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 17 years ago
parent
commit
46edabc574
  1. 8
      prism/src/prism/NondetModel.java
  2. 10
      prism/src/prism/ProbModel.java

8
prism/src/prism/NondetModel.java

@ -310,10 +310,10 @@ public class NondetModel extends ProbModel
for (i = 0; i < numRewardStructs; i++) {
filename = (file != null) ? file.getPath() : null;
if (filename != null && numRewardStructs > 1) {
filename = PrismUtils.addCounterSuffixToFilename(filename, i);
filename = PrismUtils.addCounterSuffixToFilename(filename, i+1);
allFilenames += ((i > 0) ? ", " : "") + filename;
}
PrismMTBDD.ExportVector(stateRewards[i], "c" + i, allDDRowVars, odd, exportType, filename);
PrismMTBDD.ExportVector(stateRewards[i], "c" + (i+1), allDDRowVars, odd, exportType, filename);
}
return (allFilenames.length() > 0) ? allFilenames : null;
}
@ -332,13 +332,13 @@ public class NondetModel extends ProbModel
for (i = 0; i < numRewardStructs; i++) {
filename = (file != null) ? file.getPath() : null;
if (filename != null && numRewardStructs > 1) {
filename = PrismUtils.addCounterSuffixToFilename(filename, i);
filename = PrismUtils.addCounterSuffixToFilename(filename, i+1);
allFilenames += ((i > 0) ? ", " : "") + filename;
}
if (!explicit) {
// can only do explicit (sparse matrix based) export for mdps
} else {
PrismSparse.ExportSubMDP(trans, transRewards[i], "C" + i, allDDRowVars, allDDColVars, allDDNondetVars,
PrismSparse.ExportSubMDP(trans, transRewards[i], "C" + (i+1), allDDRowVars, allDDColVars, allDDNondetVars,
odd, exportType, filename);
}
}

10
prism/src/prism/ProbModel.java

@ -651,10 +651,10 @@ public class ProbModel implements Model
for (i = 0; i < numRewardStructs; i++) {
filename = (file != null) ? file.getPath() : null;
if (filename != null && numRewardStructs > 1) {
filename = PrismUtils.addCounterSuffixToFilename(filename, i);
filename = PrismUtils.addCounterSuffixToFilename(filename, i+1);
allFilenames += ((i > 0) ? ", " : "") + filename;
}
PrismMTBDD.ExportVector(stateRewards[i], "c" + i, allDDRowVars, odd, exportType, filename);
PrismMTBDD.ExportVector(stateRewards[i], "c" + (i+1), allDDRowVars, odd, exportType, filename);
}
return (allFilenames.length() > 0) ? allFilenames : null;
}
@ -673,14 +673,14 @@ public class ProbModel implements Model
for (i = 0; i < numRewardStructs; i++) {
filename = (file != null) ? file.getPath() : null;
if (filename != null && numRewardStructs > 1) {
filename = PrismUtils.addCounterSuffixToFilename(filename, i);
filename = PrismUtils.addCounterSuffixToFilename(filename, i+1);
allFilenames += ((i > 0) ? ", " : "") + filename;
}
if (!explicit) {
PrismMTBDD
.ExportMatrix(transRewards[i], "C" + i, allDDRowVars, allDDColVars, odd, exportType, filename);
.ExportMatrix(transRewards[i], "C" + (i+1), allDDRowVars, allDDColVars, odd, exportType, filename);
} else {
PrismSparse.ExportMatrix(transRewards[i], "C" + i, allDDRowVars, allDDColVars, odd, exportType,
PrismSparse.ExportMatrix(transRewards[i], "C" + (i+1), allDDRowVars, allDDColVars, odd, exportType,
filename);
}
}

Loading…
Cancel
Save