From b0a2923635d5ba06fab4800539d3caf99164281c Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:24:36 +0200 Subject: [PATCH] imported patch sccmethodex-setting.patch --- prism/src/explicit/SCCComputer.java | 42 ++++++++++++++++++++++------- prism/src/prism/PrismSettings.java | 20 +++++++++++++- 2 files changed, 52 insertions(+), 10 deletions(-) diff --git a/prism/src/explicit/SCCComputer.java b/prism/src/explicit/SCCComputer.java index 4a9da410..db4e90f4 100644 --- a/prism/src/explicit/SCCComputer.java +++ b/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"); } /** diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 95b24dd5..53c7f9a7 100644 --- a/prism/src/prism/PrismSettings.java +++ b/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 .............. Specify (symbolic) SCC computation method (xiebeerel, lockstep, sccfind)"); + mainLog.println("-sccmethodex ............ Specify (explicit) SCC computation method (tarjan, tarjaniterative) [default: tarjan]"); mainLog.println("-symm ................. Symmetry reduction options string"); mainLog.println("-aroptions ............ Abstraction-refinement engine options string"); mainLog.println("-pathviaautomata ............... Handle all path formulas via automata constructions");