diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index c1303463..964f19a9 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2403,6 +2403,99 @@ public class Prism extends PrismComponent implements PrismSettingsListener if (file != null) tmpLog.close(); } + + /** + * Export the (states of the) currently loaded model's strongly connected components (SCCs) 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 exportSCCsToFile(int exportType, File file) throws FileNotFoundException, PrismException + { + int i, n; + long l; // timer + PrismLog tmpLog; + SCCComputer sccComputer = null; + explicit.SCCComputer sccComputerExpl = null; + + // 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 SCCs + mainLog.println("\nComputing SCCs..."); + l = System.currentTimeMillis(); + if (!getExplicit()) { + sccComputer = getSCCComputer(currentModel); + sccComputer.computeSCCs(); + } else { + sccComputerExpl = getExplicitSCCComputer(currentModelExpl); + sccComputerExpl.computeSCCs(); + } + l = System.currentTimeMillis() - l; + mainLog.println("\nTime for SCC computation: " + l / 1000.0 + " seconds."); + + // print message + mainLog.print("\nExporting SCCs "); + 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 < currentModulesFile.getNumVars(); i++) { + tmpLog.print(currentModulesFile.getVarName(i)); + if (i < currentModulesFile.getNumVars() - 1) + tmpLog.print(","); + } + tmpLog.println(")"); + + // print states for each scc + if (!getExplicit()) { + n = sccComputer.getSCCs().size(); + } else { + n = sccComputerExpl.getSCCs().size(); + } + for (i = 0; i < n; i++) { + tmpLog.println(); + if (exportType == EXPORT_MATLAB) + tmpLog.print("% "); + tmpLog.println("SCC " + (i + 1) + "/" + n + ":"); + if (exportType == EXPORT_MATLAB) + tmpLog.println("scc" + (i + 1) + "=["); + if (!getExplicit()) { + if (exportType != EXPORT_MATLAB) + new StateListMTBDD(sccComputer.getSCCs().get(i), currentModel).print(tmpLog); + else + new StateListMTBDD(sccComputer.getSCCs().get(i), currentModel).printMatlab(tmpLog); + JDD.Deref(sccComputer.getSCCs().get(i)); + } else { + explicit.StateValues.createFromBitSet(sccComputerExpl.getSCCs().get(i), currentModelExpl).print(tmpLog, true, exportType == EXPORT_MATLAB, true, true); + } + if (exportType == EXPORT_MATLAB) + tmpLog.println("];"); + } + + if (!getExplicit()) { + JDD.Deref(sccComputer.getNotInSCCs()); + } + + // tidy up + if (file != null) + tmpLog.close(); + } /** * Export the states satisfying labels from the currently loaded model and a properties file to a file. diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 17fcf989..afad593c 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -75,6 +75,7 @@ public class PrismCL implements PrismModelListener private boolean exporttransdotstates = false; private boolean exportbsccs = false; private boolean exportmecs = false; + private boolean exportsccs = false; private boolean exportresults = false; private boolean exportresultsmatrix = false; private boolean exportresultscsv = false; @@ -130,6 +131,7 @@ public class PrismCL implements PrismModelListener private String exportTransDotStatesFilename = null; private String exportBSCCsFilename = null; private String exportMECsFilename = null; + private String exportSCCsFilename = null; private String exportResultsFilename = null; private String exportSteadyStateFilename = null; private String exportTransientFilename = null; @@ -787,6 +789,20 @@ public class PrismCL implements PrismModelListener error(e.getMessage()); } } + + // export SCCs to a file + if (exportsccs) { + try { + File f = (exportSCCsFilename.equals("stdout")) ? null : new File(exportSCCsFilename); + prism.exportSCCsToFile(exportType, f); + } + // in case of error, report it and proceed + catch (FileNotFoundException e) { + error("Couldn't open file \"" + exportSCCsFilename + "\" for output"); + } catch (PrismException e) { + error(e.getMessage()); + } + } } /** @@ -1259,6 +1275,15 @@ public class PrismCL implements PrismModelListener errorAndExit("No file specified for -" + sw + " switch"); } } + // export sccs to file + else if (sw.equals("exportsccs")) { + if (i < args.length - 1) { + exportsccs = true; + exportSCCsFilename = 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) {