diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index e040c763..ec2fcde3 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1002,6 +1002,22 @@ public class Prism implements PrismSettingsListener return sccComputer; } + /** + * Get an ECComputer object. + */ + public ECComputer getECComputer(NondetModel model) + { + return getECComputer(model.getReach(), model.getTrans(), model.getTrans01(), model.getAllDDRowVars(), model.getAllDDColVars(), model.getAllDDNondetVars()); + } + + /** + * Get an ECComputer object. + */ + public ECComputer getECComputer(JDDNode reach, JDDNode trans, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars allDDNondetVars) + { + return new ECComputerDefault(this, reach, trans, trans01, allDDRowVars, allDDColVars, allDDNondetVars); + } + //------------------------------------------------------------------------------ // Utility methods //------------------------------------------------------------------------------ @@ -2296,6 +2312,88 @@ public class Prism implements PrismSettingsListener tmpLog.close(); } + /** + * Export the (states of the) currently loaded model's maximal end components (MECs) to a file + * @param exportType Type of export; one of: + * @param file File to export to (if null, print to the log instead) + */ + public void exportMECsToFile(int exportType, File file) throws FileNotFoundException, PrismException + { + int i, n; + long l; // timer + PrismLog tmpLog; + ECComputer ecComputer; + Vector mecs; + JDDNode mec; + + if (getExplicit()) + throw new PrismException("Export of MECs not yet supported by explicit engine"); + + // 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(); + + // Compute MECs + mainLog.println("\nComputing MECs..."); + ecComputer = getECComputer((NondetModel) currentModel); + l = System.currentTimeMillis(); + ecComputer.computeECs(); + l = System.currentTimeMillis() - l; + mecs = ecComputer.getVectECs(); + mainLog.println("\nTime for MEC computation: " + l / 1000.0 + " seconds."); + + // print message + mainLog.print("\nExporting MECs "); + mainLog.print(getStringForExportType(exportType) + " "); + mainLog.println(getDestinationStringForFile(file)); + + // create new file log or use main log + tmpLog = getPrismLogForFile(file); + + // print header: list of model vars + if (exportType == EXPORT_MATLAB) + tmpLog.print("% "); + tmpLog.print("Variables: ("); + for (i = 0; i < currentModel.getNumVars(); i++) { + tmpLog.print(currentModel.getVarName(i)); + if (i < currentModel.getNumVars() - 1) + tmpLog.print(","); + } + tmpLog.println(")"); + + // print states for each mec + n = mecs.size(); + for (i = 0; i < n; i++) { + tmpLog.println(); + if (exportType == EXPORT_MATLAB) + tmpLog.print("% "); + tmpLog.println("MEC " + (i + 1) + "/" + n + ":"); + if (exportType == EXPORT_MATLAB) + tmpLog.println("mec" + (i + 1) + "=["); + mec = mecs.get(i); + if (exportType != EXPORT_MATLAB) + new StateListMTBDD(mec, currentModel).print(tmpLog); + else + new StateListMTBDD(mec, currentModel).printMatlab(tmpLog); + if (exportType == EXPORT_MATLAB) + tmpLog.println("];"); + JDD.Deref(mec); + } + + // tidy up + if (file != null) + tmpLog.close(); + } + /** * Export the states satisfying labels from the currently loaded model and a properties file to a file. * The PropertiesFile should correspond to the currently loaded model. diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 9ae68620..9d33b501 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -74,6 +74,7 @@ public class PrismCL implements PrismModelListener private boolean exporttransdot = false; private boolean exporttransdotstates = false; private boolean exportbsccs = false; + private boolean exportmecs = false; private boolean exportresults = false; private boolean exportresultsmatrix = false; private boolean exportresultscsv = false; @@ -128,6 +129,7 @@ public class PrismCL implements PrismModelListener private String exportTransDotFilename = null; private String exportTransDotStatesFilename = null; private String exportBSCCsFilename = null; + private String exportMECsFilename = null; private String exportResultsFilename = null; private String exportSteadyStateFilename = null; private String exportTransientFilename = null; @@ -771,6 +773,20 @@ public class PrismCL implements PrismModelListener error(e.getMessage()); } } + + // export MECs to a file + if (exportmecs) { + try { + File f = (exportMECsFilename.equals("stdout")) ? null : new File(exportMECsFilename); + prism.exportMECsToFile(exportType, f); + } + // in case of error, report it and proceed + catch (FileNotFoundException e) { + error("Couldn't open file \"" + exportMECsFilename + "\" for output"); + } catch (PrismException e) { + error(e.getMessage()); + } + } } /** @@ -1234,6 +1250,15 @@ public class PrismCL implements PrismModelListener errorAndExit("No file specified for -" + sw + " switch"); } } + // export mecs to file + else if (sw.equals("exportmecs")) { + if (i < args.length - 1) { + exportmecs = true; + exportMECsFilename = args[++i]; + } else { + errorAndExit("No file specified for -" + sw + " switch"); + } + } // export steady-state probs (as opposed to displaying on screen) else if (sw.equals("exportsteadystate") || sw.equals("exportss")) { if (i < args.length - 1) {