imported patch sccmethodex-setting.patch

prism/src/explicit/SCCComputer.java

@@ -34,6 +34,7 @@ import java.util.function.IntPredicate;
 
 import prism.PrismComponent;
 import prism.PrismException;
+import prism.PrismSettings;
 
 /**
  * Abstract class for (explicit) classes that compute (B)SCCs,
@@ -46,15 +47,19 @@ public abstract class SCCComputer extends PrismComponent
 
 	// Method used for finding (B)SCCs
 	public enum SCCMethod {
-		TARJAN;
+		TARJAN("Tarjan-recursive"),
+		TARJAN_ITERATIVE("Tarjan-iterative");
+
+		private final String name;
+
+		private SCCMethod(String name)
+		{
+			this.name = name;
+		}
+
 		public String fullName()
 		{
-			switch (this) {
-			case TARJAN:
-				return "Tarjan";
-			default:
-				return this.toString();
-			}
+			return name;
 		}
 	};
 
@@ -63,8 +68,27 @@ public abstract class SCCComputer extends PrismComponent
 	 */
 	public static SCCComputer createSCCComputer(PrismComponent parent, Model model, SCCConsumer consumer) throws PrismException
 	{
-		// Only one algorithm implemented currently
-		return new SCCComputerTarjan(parent, model, consumer);
+		String methodName = parent.getSettings().getString(PrismSettings.PRISM_SCC_METHOD_EXPLICIT);
+		for (SCCMethod method : SCCMethod.values()) {
+			if (method.fullName().equals(methodName)) {
+				return createSCCComputer(parent, method, model, consumer);
+			}
+		}
+		throw new PrismException("SCC decomposition method " + methodName + " is unknown");
+	}
+
+	/**
+	 * Static method to create a new SCCComputer object, using the given SCC decomposition method.
+	 */
+	public static SCCComputer createSCCComputer(PrismComponent parent, SCCMethod method, Model model, SCCConsumer consumer) throws PrismException
+	{
+		switch (method) {
+		case TARJAN:
+			return new SCCComputerTarjan(parent, model, consumer);
+		case TARJAN_ITERATIVE:
+			return new SCCComputerTarjanIterative(parent, model, consumer);
+		}
+		throw new PrismException("SCC decomposition method " + method + " is not implemented");
 	}
 
 	/**

prism/src/prism/PrismSettings.java

@@ -109,6 +109,7 @@ public class PrismSettings implements Observer
 	public static final	String PRISM_EXTRA_DD_INFO					= "prism.extraDDInfo";
 	public static final	String PRISM_EXTRA_REACH_INFO				= "prism.extraReachInfo";
 	public static final String PRISM_SCC_METHOD						= "prism.sccMethod";
+	public static final String PRISM_SCC_METHOD_EXPLICIT			= "prism.explicitSccMethod";
 	public static final String PRISM_SYMM_RED_PARAMS					= "prism.symmRedParams";
 	public static final	String PRISM_EXACT_ENABLED					= "prism.exact.enabled";
 	public static final String PRISM_PTA_METHOD					= "prism.ptaMethod";
@@ -292,6 +293,8 @@ public class PrismSettings implements Observer
 																			"Use steady-state detection during CTMC transient probability computation." },
 			{ CHOICE_TYPE,		PRISM_SCC_METHOD,						"SCC decomposition method",				"3.2",			"Lockstep",																	"Xie-Beerel,Lockstep,SCC-Find",																
 																			"Which algorithm to use for (symbolic) decomposition of a graph into strongly connected components (SCCs)." },
+			{ CHOICE_TYPE,		PRISM_SCC_METHOD_EXPLICIT,				"SCC decomposition method (explicit engine)",				"4.4",			"Tarjan-recursive",																	"Tarjan-recursive,Tarjan-iterative",
+																			"Which algorithm to use for (explicit engine) decomposition of a graph into strongly connected components (SCCs)." },
 			{ STRING_TYPE,		PRISM_SYMM_RED_PARAMS,					"Symmetry reduction parameters",		"3.2",			"",																	"",																
 																			"Parameters for symmetry reduction (format: \"i j\" where i and j are the number of modules before and after the symmetric ones; empty string means symmetry reduction disabled)." },
 			{ STRING_TYPE,		PRISM_AR_OPTIONS,						"Abstraction refinement options",		"3.3",			"",																	"",																
@@ -1249,7 +1252,7 @@ public class PrismSettings implements Observer
 		else if (sw.equals("nossdetect")) {
 			set(PRISM_DO_SS_DETECTION, false);
 		}
-		// SCC computation algorithm
+		// SCC computation algorithm (symbolic engines)
 		else if (sw.equals("sccmethod") || sw.equals("bsccmethod")) {
 			if (i < args.length - 1) {
 				s = args[++i];
@@ -1265,6 +1268,20 @@ public class PrismSettings implements Observer
 				throw new PrismException("No parameter specified for -" + sw + " switch");
 			}
 		}
+		// SCC computation algorithm (explicit engines)
+		else if (sw.equals("sccmethodex") || sw.equals("bsccmethodex")) {
+			if (i < args.length - 1) {
+				s = args[++i];
+				if (s.equals("tarjan"))
+					set(PRISM_SCC_METHOD_EXPLICIT, "Tarjan-recursive");
+				else if (s.equals("tarjaniterative"))
+					set(PRISM_SCC_METHOD_EXPLICIT, "Tarjan-iterative");
+				else
+					throw new PrismException("Unrecognised option for -" + sw + " switch (options are: xiebeerel, lockstep, sccfind)");
+			} else {
+				throw new PrismException("No parameter specified for -" + sw + " switch");
+			}
+		}
 		// Enable symmetry reduction
 		else if (sw.equals("symm")) {
 			if (i < args.length - 2) {
@@ -1849,6 +1866,7 @@ public class PrismSettings implements Observer
 		mainLog.println("-zerorewardcheck ............... Check for absence of zero-reward loops");
 		mainLog.println("-nossdetect .................... Disable steady-state detection for CTMC transient computations");
 		mainLog.println("-sccmethod <name> .............. Specify (symbolic) SCC computation method (xiebeerel, lockstep, sccfind)");
+		mainLog.println("-sccmethodex <name> ............ Specify (explicit) SCC computation method (tarjan, tarjaniterative) [default: tarjan]");
 		mainLog.println("-symm <string> ................. Symmetry reduction options string");
 		mainLog.println("-aroptions <string> ............ Abstraction-refinement engine options string");
 		mainLog.println("-pathviaautomata ............... Handle all path formulas via automata constructions");