Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Explicit engine model export refactoring and enhancements #246

Merged
merged 17 commits into from
Jul 15, 2024
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Refactor export observations functionality in Prism.
New export method in Prism based on ModelExportOptions.

Formatting-specific code moves to Exporter classes.
davexparker committed Jul 9, 2024
commit c2ae7c232b79fa19245d1669823d893ba3a1d6eb
40 changes: 13 additions & 27 deletions prism/src/explicit/PartiallyObservableModel.java
Original file line number Diff line number Diff line change
@@ -29,6 +29,8 @@

import java.util.List;

import io.ModelExportOptions;
import io.PrismExplicitExporter;
import parser.State;
import prism.ModelInfo;
import prism.Prism;
@@ -126,34 +128,18 @@ public default double getObservationProb(int s, int o)
/**
* Export observations list.
*/
public default void exportObservations(int exportType, ModelInfo modelInfo, PrismLog log) throws PrismException
public default void exportObservations(ModelInfo modelInfo, PrismLog out, ModelExportOptions exportOptions) throws PrismException
{
// Print header: list of observables
if (exportType == Prism.EXPORT_MATLAB)
log.print("% ");
log.print("(");
int numObservables = modelInfo.getNumObservables();
for (int i = 0; i < numObservables; i++) {
log.print(modelInfo.getObservableName(i));
if (i < numObservables - 1)
log.print(",");
}
log.println(")");
if (exportType == Prism.EXPORT_MATLAB)
log.println("obs=[");

// Print states + observations
int numObservations = getNumObservations();
List<State> observationsList = getObservationsList();
for (int i = 0; i < numObservations; i++) {
if (exportType != Prism.EXPORT_MATLAB)
log.println(i + ":" + observationsList.get(i).toString());
else
log.println(observationsList.get(i).toStringNoParentheses());
}
new PrismExplicitExporter<Value>(exportOptions).exportObservations(this, modelInfo, out);
}

// Print footer
if (exportType == Prism.EXPORT_MATLAB)
log.println("];");
/**
* @deprecated
* Export observations list.
*/
@Deprecated
public default void exportObservations(int exportType, ModelInfo modelInfo, PrismLog out) throws PrismException
{
exportObservations(modelInfo, out, Prism.convertExportType(exportType));
}
}
18 changes: 18 additions & 0 deletions prism/src/explicit/StateModelChecker.java
Original file line number Diff line number Diff line change
@@ -1663,6 +1663,24 @@ public <Value> void exportStates(Model<Value> model, PrismLog out, ModelExportOp
}
}

/**
* Export the observations for a (partially observable) model.
* @param model The model
* @param out Where to export
* @param exportOptions The options for export
*/
public <Value> void exportObservations(Model<Value> model, PrismLog out, ModelExportOptions exportOptions) throws PrismException
{
switch (exportOptions.getFormat()) {
case EXPLICIT:
new PrismExplicitExporter<Value>(exportOptions).exportObservations((PartiallyObservableModel<Value>) model, modelInfo, out);
break;
case MATLAB:
new MatlabExporter<Value>(exportOptions).exportObservations((PartiallyObservableModel<Value>) model, modelInfo, out);
break;
}
}

/**
* Export a set of labels and the states that satisfy them.
* @param model The model
32 changes: 32 additions & 0 deletions prism/src/io/MatlabExporter.java
Original file line number Diff line number Diff line change
@@ -39,6 +39,7 @@
import parser.VarList;
import prism.Evaluator;
import io.ModelExportOptions;
import prism.ModelInfo;
import prism.ModelType;
import prism.Pair;
import prism.Prism;
@@ -100,6 +101,37 @@ public void exportStates(Model<Value> model, VarList varList, PrismLog out) thro
out.println("];");
}

/**
* Export the observations for a (partially observable) model.
* @param model The model
* @param modelInfo The ModelInfo for the model
* @param out Where to export
*/
public void exportObservations(PartiallyObservableModel<Value> model, ModelInfo modelInfo, PrismLog out) throws PrismException
{
List<State> observationsList = model.getObservationsList();

// Print header: list of observables
out.print("% (");
int numObservables = modelInfo.getNumObservables();
for (int i = 0; i < numObservables; i++) {
out.print(modelInfo.getObservableName(i));
if (i < numObservables - 1)
out.print(",");
}
out.println(")");

// Print states + observations
out.println("obs=[");
int numObservations = model.getNumObservations();
for (int i = 0; i < numObservations; i++) {
out.println(observationsList.get(i).toStringNoParentheses());
}

// Print footer
out.println("];");
}

/**
* Export a set of labels and the states that satisfy them.
* @param model The model
28 changes: 28 additions & 0 deletions prism/src/io/PrismExplicitExporter.java
Original file line number Diff line number Diff line change
@@ -39,6 +39,7 @@
import parser.VarList;
import prism.Evaluator;
import io.ModelExportOptions;
import prism.ModelInfo;
import prism.ModelType;
import prism.Pair;
import prism.Prism;
@@ -311,6 +312,33 @@ public void exportStates(Model<Value> model, VarList varList, PrismLog out) thro
}
}

/**
* Export the observations for a (partially observable) model.
* @param model The model
* @param modelInfo The ModelInfo for the model
* @param out Where to export
*/
public void exportObservations(PartiallyObservableModel<Value> model, ModelInfo modelInfo, PrismLog out) throws PrismException
{
List<State> observationsList = model.getObservationsList();

// Print header: list of observables
out.print("(");
int numObservables = modelInfo.getNumObservables();
for (int i = 0; i < numObservables; i++) {
out.print(modelInfo.getObservableName(i));
if (i < numObservables - 1)
out.print(",");
}
out.println(")");

// Print states + observations
int numObservations = model.getNumObservations();
for (int i = 0; i < numObservations; i++) {
out.println(i + ":" + observationsList.get(i).toString());
}
}

/**
* Export a set of labels and the states that satisfy them.
* @param model The model
89 changes: 48 additions & 41 deletions prism/src/prism/Prism.java
Original file line number Diff line number Diff line change
@@ -2524,6 +2524,41 @@ public void exportBuiltModelStates(File file, ModelExportOptions exportOptions)
out.close();
}

/**
* Export the observations of the currently loaded (partially observable) model.
* @param file File to export to (if null, print to the log instead)
* @param exportOptions The options for export
*/
public void exportBuiltModelObservations(File file, ModelExportOptions exportOptions) throws FileNotFoundException, PrismException
{
if (!currentModelType.partiallyObservable()) {
mainLog.println("\nOmitting observations export as the model is not partially observable");
return;
}

// Build model, if necessary
buildModelIfRequired();

// Print message
mainLog.print("\nExporting list of observations ");
mainLog.print(exportOptions.getFormat().description() + " ");
mainLog.println(getDestinationStringForFile(file));

// Merge export options with settings
exportOptions = newMergedModelExportOptions(exportOptions);

// Create new file log or use main log
PrismLog out = getPrismLogForFile(file);

// Export (explicit engine only)
explicit.StateModelChecker mcExpl = createModelCheckerExplicit(null);
mcExpl.exportObservations(currentModelExpl, out, exportOptions);

// Tidy up
if (file != null)
out.close();
}

/**
* Export the states satisfying labels from the currently loaded model and (optionally) a properties file to a file.
* The PropertiesFile should correspond to the currently loaded model.
@@ -2875,47 +2910,6 @@ public void exportSCCsToFile(int exportType, File file) throws FileNotFoundExcep
tmpLog.close();
}

/**
* Export the observations for the currently loaded model to a file
* @param exportType Type of export; one of: <ul>
* <li> {@link #EXPORT_PLAIN}
* <li> {@link #EXPORT_MATLAB}
* </ul>
* @param file File to export to (if null, print to the log instead)
*/
public void exportObservationsToFile(int exportType, File file) throws FileNotFoundException, PrismException
{
if (!currentModelType.partiallyObservable()) {
mainLog.println("\nOmitting observations export as the model is not partially observable");
return;
}

// No specific states format for MRMC
if (exportType == EXPORT_MRMC)
exportType = EXPORT_PLAIN;
// Rows format does not apply to states output
if (exportType == EXPORT_ROWS)
exportType = EXPORT_PLAIN;

// Build model, if necessary
buildModelIfRequired();

// Print message
mainLog.print("\nExporting list of observations ");
mainLog.print(getStringForExportType(exportType) + " ");
mainLog.println(getDestinationStringForFile(file));

// Create new file log or use main log
PrismLog tmpLog = getPrismLogForFile(file);

// Export (explicit engine only)
((PartiallyObservableModel<?>) currentModelExpl).exportObservations(exportType, currentModelInfo, tmpLog);

// Tidy up
if (file != null)
tmpLog.close();
}

/**
* Return a new {@code ModelExportOptions} object with any relevant PRISM settings applied,
* then merged with the passed ewxport options (which take precedence).
@@ -4197,6 +4191,19 @@ public void exportStatesToFile(int exportType, File file) throws FileNotFoundExc
exportBuiltModelStates(file, convertExportType(exportType));
}

/**
* Export the observations for the currently loaded model to a file
* @param exportType Type of export; one of: <ul>
* <li> {@link #EXPORT_PLAIN}
* <li> {@link #EXPORT_MATLAB}
* </ul>
* @param file File to export to (if null, print to the log instead)
*/
public void exportObservationsToFile(int exportType, File file) throws FileNotFoundException, PrismException
{
exportBuiltModelObservations(file, convertExportType(exportType));
}

/**
* @deprecated
* Export the states satisfying labels from the currently loaded model and (optionally) a properties file to a file.
5 changes: 4 additions & 1 deletion prism/src/prism/PrismCL.java
Original file line number Diff line number Diff line change
@@ -106,6 +106,7 @@ public class PrismCL implements PrismModelListener
private ModelExportOptions exportStateRewardsOptions = new ModelExportOptions();
private ModelExportOptions exportTransRewardsOptions = new ModelExportOptions();
private ModelExportOptions exportStatesOptions = new ModelExportOptions();
private ModelExportOptions exportObservationsOptions = new ModelExportOptions();
private ModelExportOptions exportLabelsOptions = new ModelExportOptions();
private ModelExportOptions exportTransDotOptions = new ModelExportOptions();
private ModelExportOptions exportTransDotStatesOptions = new ModelExportOptions();
@@ -863,7 +864,8 @@ private void doExports()
if (exportobservations) {
try {
File f = (exportObservationsFilename.equals("stdout")) ? null : new File(exportObservationsFilename);
prism.exportObservationsToFile(exportType, f);
exportObservationsOptions.applyTo(modelExportOptionsGlobal);
prism.exportBuiltModelObservations(f, exportStatesOptions);
}
// in case of error, report it and proceed
catch (FileNotFoundException e) {
@@ -2286,6 +2288,7 @@ else if (opt.equals("matlab")) {
exportStateRewardsOptions.setFormat(ModelExportFormat.MATLAB);
exportTransRewardsOptions.setFormat(ModelExportFormat.MATLAB);
exportStatesOptions.setFormat(ModelExportFormat.MATLAB);
exportObservationsOptions.setFormat(ModelExportFormat.MATLAB);
exportLabelsOptions.setFormat(ModelExportFormat.MATLAB);
} else if (opt.equals("rows")) {
exportType = Prism.EXPORT_ROWS;