Added exportsccs

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7528 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/prism/Prism.java

@@ -2404,6 +2404,99 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 			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: <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 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.
 	 * The PropertiesFile should correspond to the currently loaded model. 

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) {