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

Add state reward export for explicit engine; also some refactoring of reward exporting 

(in particular, move logic for splitting into multiple reward files up to prism.Prism)



git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12001 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 9 years ago
parent
fe76535b3d
commit
c4ed300c01
5 changed files with 175 additions and 57 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. 65
      prism/src/explicit/ProbModelChecker.java
  2. 22
      prism/src/prism/Model.java
  3. 31
      prism/src/prism/NondetModel.java
  4. 86
      prism/src/prism/Prism.java
  5. 28
      prism/src/prism/ProbModel.java

65
prism/src/explicit/ProbModelChecker.java
View File

@ -30,6 +30,11 @@ import java.io.File;
import java.util.BitSet;
import java.util.List;
import explicit.rewards.ConstructRewards;
import explicit.rewards.MCRewards;
import explicit.rewards.MDPRewards;
import explicit.rewards.Rewards;
import explicit.rewards.STPGRewards;
import parser.ast.Coalition;
import parser.ast.Expression;
import parser.ast.ExpressionProb;
@ -47,13 +52,10 @@ import prism.IntegerBound;
import prism.OpRelOpBound;
import prism.PrismComponent;
import prism.PrismException;
import prism.PrismLog;
import prism.PrismNotSupportedException;
import prism.PrismSettings;
import explicit.rewards.ConstructRewards;
import explicit.rewards.MCRewards;
import explicit.rewards.MDPRewards;
import explicit.rewards.Rewards;
import explicit.rewards.STPGRewards;
import prism.PrismUtils;
/**
* Super class for explicit-state probabilistic model checkers.
@ -1236,4 +1238,57 @@ public class ProbModelChecker extends NonProbModelChecker
return dist;
}
/**
* Export (non-zero) state rewards for one reward structure of a model.
* @param model The model
* @param r Index of reward structure to export (0-indexed)
* @param exportType The format in which to export
* @param out Where to export
*/
public void exportStateRewardsToFile(Model model, int r, int exportType, PrismLog out) throws PrismException
{
int numStates = model.getNumStates();
int nonZeroRews = 0;
Rewards modelRewards = constructRewards(model, r);
switch (model.getModelType()) {
case DTMC:
case CTMC:
MCRewards mcRewards = (MCRewards) modelRewards;
for (int s = 0; s < numStates; s++) {
double d = mcRewards.getStateReward(s);
if (d != 0) {
nonZeroRews++;
}
}
out.println(numStates + " " + nonZeroRews);
for (int s = 0; s < numStates; s++) {
double d = mcRewards.getStateReward(s);
if (d != 0) {
out.println(s + " " + PrismUtils.formatDouble(d));
}
}
break;
case MDP:
case STPG:
MDPRewards mdpRewards = (MDPRewards) modelRewards;
for (int s = 0; s < numStates; s++) {
double d = mdpRewards.getStateReward(s);
if (d != 0) {
nonZeroRews++;
}
}
out.println(numStates + " " + nonZeroRews);
for (int s = 0; s < numStates; s++) {
double d = mdpRewards.getStateReward(s);
if (d != 0) {
out.println(s + " " + PrismUtils.formatDouble(d));
}
}
break;
default:
throw new PrismNotSupportedException("Explicit engine does not yet export state rewards for " + model.getModelType() + "s");
}
}
}

22
prism/src/prism/Model.java
View File

@ -184,8 +184,30 @@ public interface Model
public void printTransInfo(PrismLog log);
public void printTransInfo(PrismLog log, boolean extra);
void exportToFile(int exportType, boolean explicit, File file) throws FileNotFoundException, PrismException;
/**
* Export (non-zero) state rewards for one reward structure of the model.
* @param r Index of reward structure to export (0-indexed)
* @param exportType The format in which to export
* @param file File to export to (if null, print to the log instead)
*/
void exportStateRewardsToFile(int r, int exportType, File file) throws FileNotFoundException, PrismException;
@Deprecated
String exportStateRewardsToFile(int exportType, File file) throws FileNotFoundException, PrismException;
/**
* Export (non-zero) transition rewards for one reward structure of the model.
* @param r Index of reward structure to export (0-indexed)
* @param exportType The format in which to export
* @param ordered Do the entries need to be printed in order?
* @param file File to export to (if null, print to the log instead)
*/
void exportTransRewardsToFile(int r, int exportType, boolean ordered, File file) throws FileNotFoundException, PrismException;
@Deprecated
String exportTransRewardsToFile(int exportType, boolean explicit, File file) throws FileNotFoundException, PrismException;
void exportStates(int exportType, PrismLog log);
void clear();

31
prism/src/prism/NondetModel.java
View File

@ -421,33 +421,22 @@ public class NondetModel extends ProbModel
}
}
// export state rewards vector to a file
// returns string containing files used if there were more than 1, null otherwise
public String exportStateRewardsToFile(int exportType, File file) throws FileNotFoundException, PrismException
@Override
public void exportTransRewardsToFile(int r, int exportType, boolean ordered, File file) throws FileNotFoundException, PrismException
{
if (numRewardStructs == 0)
throw new PrismException("There are no state rewards to export");
int i;
String filename, allFilenames = "";
for (i = 0; i < numRewardStructs; i++) {
filename = (file != null) ? file.getPath() : null;
if (filename != null && numRewardStructs > 1) {
filename = PrismUtils.addCounterSuffixToFilename(filename, i + 1);
allFilenames += ((i > 0) ? ", " : "") + filename;
}
PrismMTBDD.ExportVector(stateRewards[i], "c" + (i + 1), allDDRowVars, odd, exportType, filename);
if (!ordered) {
// can only do explicit (sparse matrix based) export for mdps
} else {
PrismSparse.ExportSubMDP(trans, transRewards[r], "C" + (r + 1), allDDRowVars, allDDColVars, allDDNondetVars, odd, exportType, (file == null) ? null : file.getPath());
}
return (allFilenames.length() > 0) ? allFilenames : null;
}
// export transition rewards matrix to a file
// returns string containing files used if there were more than 1, null otherwise
@Deprecated
public String exportTransRewardsToFile(int exportType, boolean explicit, File file) throws FileNotFoundException, PrismException
{
// export transition rewards matrix to a file
// returns string containing files used if there were more than 1, null otherwise
if (numRewardStructs == 0)
throw new PrismException("There are no transition rewards to export");
int i;

86
prism/src/prism/Prism.java
View File

@ -2317,7 +2317,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener
}
/**
* Export the currently loaded model's state rewards to a file
* Export the currently loaded model's state rewards to a file (or files, or stdout).
* If there is more than 1 reward structure, then multiple files are generated
* (e.g. "rew.sta" becomes "rew1.sta", "rew2.sta", ...)
* @param exportType Type of export; one of: <ul>
* <li> {@link #EXPORT_PLAIN}
* <li> {@link #EXPORT_MATLAB}
@ -2327,29 +2329,46 @@ public class Prism extends PrismComponent implements PrismSettingsListener
*/
public void exportStateRewardsToFile(int exportType, File file) throws FileNotFoundException, PrismException
{
String s;
if (getExplicit())
throw new PrismNotSupportedException("Export of state rewards not yet supported by explicit engine");
// rows format does not apply to vectors
int numRewardStructs = currentModelInfo.getNumRewardStructs();
if (numRewardStructs == 0) {
mainLog.println("\nOmitting state reward export as there are no reward structures");
}
// Rows format does not apply to vectors
if (exportType == EXPORT_ROWS)
exportType = EXPORT_PLAIN;
// Build model, if necessary
buildModelIfRequired();
// print message
mainLog.print("\nExporting state rewards vector ");
mainLog.print("\nExporting state rewards ");
mainLog.print(getStringForExportType(exportType) + " ");
mainLog.println(getDestinationStringForFile(file));
// do export
s = currentModel.exportStateRewardsToFile(exportType, file);
if (s != null)
mainLog.println("Rewards exported to files: " + s);
// Do export, writing to multiple files if necessary
List <String> files = new ArrayList<>();
for (int r = 0; r < numRewardStructs; r++) {
String filename = (file != null) ? file.getPath() : null;
if (filename != null && numRewardStructs > 1) {
filename = PrismUtils.addCounterSuffixToFilename(filename, r + 1);
files.add(filename);
}
File fileToUse = (filename == null) ? null : new File(filename);
if (!getExplicit()) {
currentModel.exportStateRewardsToFile(r, exportType, fileToUse);
} else {
PrismLog out = getPrismLogForFile(fileToUse);
explicit.StateModelChecker mcExpl = createModelCheckerExplicit(null);
((explicit.ProbModelChecker) mcExpl).exportStateRewardsToFile(currentModelExpl, r, exportType, out);
out.close();
}
}
if (files.size() > 1) {
mainLog.println("Rewards were exported to multiple files: " + PrismUtils.joinString(files, ","));
}
}
/**
* Export the currently loaded model's transition rewards to a file
* @param ordered Ensure that (source) states are in ascending order?
@ -2363,24 +2382,27 @@ public class Prism extends PrismComponent implements PrismSettingsListener
*/
public void exportTransRewardsToFile(boolean ordered, int exportType, File file) throws FileNotFoundException, PrismException
{
String s;
int numRewardStructs = currentModelInfo.getNumRewardStructs();
if (numRewardStructs == 0) {
mainLog.println("\nOmitting state reward export as there are no reward structures");
}
if (getExplicit())
throw new PrismException("Export of transition rewards not yet supported by explicit engine");
// can only do ordered version of export for MDPs
// Can only do ordered version of export for MDPs
if (currentModelType == ModelType.MDP) {
if (!ordered)
mainLog.printWarning("Cannot export unordered transition reward matrix for MDPs; using ordered.");
ordered = true;
}
// can only do ordered version of export for MRMC
// Can only do ordered version of export for MRMC
if (exportType == EXPORT_MRMC) {
if (!ordered)
mainLog.printWarning("Cannot export unordered transition reward matrix in MRMC format; using ordered.");
ordered = true;
}
// can only do ordered version of export for rows format
// Can only do ordered version of export for rows format
if (exportType == EXPORT_ROWS) {
if (!ordered)
mainLog.printWarning("Cannot export unordered transition matrix in rows format; using ordered.");
@ -2390,15 +2412,29 @@ public class Prism extends PrismComponent implements PrismSettingsListener
// Build model, if necessary
buildModelIfRequired();
// print message
mainLog.print("\nExporting transition rewards matrix ");
mainLog.print("\nExporting transition rewards ");
mainLog.print(getStringForExportType(exportType) + " ");
mainLog.println(getDestinationStringForFile(file));
// do export
s = currentModel.exportTransRewardsToFile(exportType, ordered, file);
if (s != null)
mainLog.println("Rewards exported to files: " + s);
// Do export, writing to multiple files if necessary
List <String> files = new ArrayList<>();
for (int r = 0; r < numRewardStructs; r++) {
String filename = (file != null) ? file.getPath() : null;
if (filename != null && numRewardStructs > 1) {
filename = PrismUtils.addCounterSuffixToFilename(filename, r + 1);
files.add(filename);
}
File fileToUse = (filename == null) ? null : new File(filename);
if (!getExplicit()) {
currentModel.exportTransRewardsToFile(r, exportType, ordered, fileToUse);
} else {
// Not implemented yet
}
}
if (files.size() > 1) {
mainLog.println("Rewards were exported to multiple files: " + PrismUtils.joinString(files, ","));
}
}
/**

28
prism/src/prism/ProbModel.java
View File

@ -837,12 +837,18 @@ public class ProbModel implements Model
}
}
// export state rewards vector to a file
// returns string containing files used if there were more than 1, null otherwise
@Override
public void exportStateRewardsToFile(int r, int exportType, File file) throws FileNotFoundException, PrismException
{
PrismMTBDD.ExportVector(stateRewards[r], "c" + (r + 1), allDDRowVars, odd, exportType, (file == null) ? null : file.getPath());
}
@Deprecated
public String exportStateRewardsToFile(int exportType, File file) throws FileNotFoundException, PrismException
{
// export state rewards vector to a file
// returns string containing files used if there were more than 1, null otherwise
if (numRewardStructs == 0)
throw new PrismException("There are no state rewards to export");
int i;
@ -858,12 +864,22 @@ public class ProbModel implements Model
return (allFilenames.length() > 0) ? allFilenames : null;
}
// export transition rewards matrix to a file
// returns string containing files used if there were more than 1, null otherwise
@Override
public void exportTransRewardsToFile(int r, int exportType, boolean ordered, File file) throws FileNotFoundException, PrismException
{
if (!ordered) {
PrismMTBDD.ExportMatrix(transRewards[r], "C" + (r + 1), allDDRowVars, allDDColVars, odd, exportType, (file == null) ? null : file.getPath());
} else {
PrismSparse.ExportMatrix(transRewards[r], "C" + (r + 1), allDDRowVars, allDDColVars, odd, exportType, (file == null) ? null : file.getPath());
}
}
@Deprecated
public String exportTransRewardsToFile(int exportType, boolean explicit, File file) throws FileNotFoundException, PrismException
{
// export transition rewards matrix to a file
// returns string containing files used if there were more than 1, null otherwise
if (numRewardStructs == 0)
throw new PrismException("There are no transition rewards to export");
int i;

Write Preview
Loading…
Cancel
Save