From 1e0dff70d2ded7cebdfd5cc834733fafcf2d918a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 17 Feb 2012 12:53:02 +0000 Subject: [PATCH] Separate setting explicit engine for linear equation system solution method. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4649 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCModelChecker.java | 31 ++++++---- prism/src/explicit/ProbModelChecker.java | 76 ++++++++++++++++++++---- 2 files changed, 87 insertions(+), 20 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 50aaa32f..7efa1e62 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -291,12 +291,15 @@ public class DTMCModelChecker extends ProbModelChecker BitSet no, yes; int i, n, numYes, numNo; long timer, timerProb0, timerProb1; + // Local copy of setting + LinEqMethod linEqMethod = this.linEqMethod; - // Check for some unsupported combinations - if (solnMethod == SolnMethod.VALUE_ITERATION && valIterDir == ValIterDir.ABOVE && !(precomp && prob0)) { - throw new PrismException("Precomputation (Prob0) must be enabled for value iteration from above"); + // Switch to a supported method, if necessary + if (!(linEqMethod == LinEqMethod.POWER || linEqMethod == LinEqMethod.GAUSS_SEIDEL)) { + linEqMethod = LinEqMethod.GAUSS_SEIDEL; + mainLog.printWarning("Switching to linear equation solution method \"" + linEqMethod.fullName() + "\""); } - + // Start probabilistic reachability timer = System.currentTimeMillis(); mainLog.println("Starting probabilistic reachability..."); @@ -338,15 +341,15 @@ public class DTMCModelChecker extends ProbModelChecker mainLog.println("target=" + target.cardinality() + ", yes=" + numYes + ", no=" + numNo + ", maybe=" + (n - (numYes + numNo))); // Compute probabilities - switch (solnMethod) { - case VALUE_ITERATION: + switch (linEqMethod) { + case POWER: res = computeReachProbsValIter(dtmc, no, yes, init, known); break; case GAUSS_SEIDEL: res = computeReachProbsGaussSeidel(dtmc, no, yes, init, known); break; default: - throw new PrismException("Unknown DTMC solution method " + solnMethod); + throw new PrismException("Unknown linear equation solution method " + linEqMethod.fullName()); } // Finished probabilistic reachability @@ -808,6 +811,14 @@ public class DTMCModelChecker extends ProbModelChecker BitSet inf; int i, n, numTarget, numInf; long timer, timerProb1; + // Local copy of setting + LinEqMethod linEqMethod = this.linEqMethod; + + // Switch to a supported method, if necessary + if (!(linEqMethod == LinEqMethod.POWER)) { + linEqMethod = LinEqMethod.POWER; + mainLog.printWarning("Switching to linear equation solution method \"" + linEqMethod.fullName() + "\""); + } // Start expected reachability timer = System.currentTimeMillis(); @@ -840,12 +851,12 @@ public class DTMCModelChecker extends ProbModelChecker mainLog.println("target=" + numTarget + ", inf=" + numInf + ", rest=" + (n - (numTarget + numInf))); // Compute rewards - switch (solnMethod) { - case VALUE_ITERATION: + switch (linEqMethod) { + case POWER: res = computeReachRewardsValIter(dtmc, mcRewards, target, inf, init, known); break; default: - throw new PrismException("Unknown DTMC solution method " + solnMethod); + throw new PrismException("Unknown linear equation solution method " + linEqMethod.fullName()); } // Finished expected reachability diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 78fcf5fc..58589106 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -47,6 +47,8 @@ public class ProbModelChecker extends StateModelChecker { // Flags/settings + // Method used to solve linear equation systems + protected LinEqMethod linEqMethod = LinEqMethod.GAUSS_SEIDEL; // Iterative numerical method termination criteria protected TermCrit termCrit = TermCrit.RELATIVE; // Parameter for iterative numerical method termination criteria @@ -67,6 +69,32 @@ public class ProbModelChecker extends StateModelChecker // Enums for flags/settings + // Method used for numerical solution + public enum LinEqMethod { + POWER, JACOBI, GAUSS_SEIDEL, BACKWARDS_GAUSS_SEIDEL, JOR, SOR, BACKWARDS_SOR; + public String fullName() + { + switch (this) { + case POWER: + return "Power method"; + case JACOBI: + return "Jacobi"; + case GAUSS_SEIDEL: + return "Gauss-Seidel"; + case BACKWARDS_GAUSS_SEIDEL: + return "Backwards Gauss-Seidel"; + case JOR: + return "JOR"; + case SOR: + return "SOR"; + case BACKWARDS_SOR: + return "Backwards SOR"; + default: + return this.toString(); + } + } + }; + // Iterative numerical method termination criteria public enum TermCrit { ABSOLUTE, RELATIVE @@ -83,13 +111,33 @@ public class ProbModelChecker extends StateModelChecker }; // Settings methods - + /** * Set settings from a PRISMSettings object. */ - public void setSettings(PrismSettings settings) + public void setSettings(PrismSettings settings) throws PrismException { String s; + // PRISM_LIN_EQ_METHOD + s = settings.getString(PrismSettings.PRISM_LIN_EQ_METHOD); + if (s.equals("Power")) { + setLinEqMethod(LinEqMethod.POWER); + } else if (s.equals("Jacobi")) { + setLinEqMethod(LinEqMethod.JACOBI); + } else if (s.equals("Gauss-Seidel")) { + setLinEqMethod(LinEqMethod.GAUSS_SEIDEL); + } else if (s.equals("Backwards Gauss-Seidel")) { + setLinEqMethod(LinEqMethod.BACKWARDS_GAUSS_SEIDEL); + } else if (s.equals("JOR")) { + setLinEqMethod(LinEqMethod.JOR); + } else if (s.equals("SOR")) { + setLinEqMethod(LinEqMethod.SOR); + } else if (s.equals("Backwards SOR")) { + setLinEqMethod(LinEqMethod.BACKWARDS_SOR); + } else { + throw new PrismException("Explicit engine does not support linear equation solution method \"" + s + "\""); + } + s = settings.getString(PrismSettings.PRISM_TERM_CRIT); if (s.equals("Absolute")) { setTermCrit(TermCrit.ABSOLUTE); @@ -102,12 +150,6 @@ public class ProbModelChecker extends StateModelChecker setProb0(settings.getBoolean(PrismSettings.PRISM_PROB0)); setProb1(settings.getBoolean(PrismSettings.PRISM_PROB1)); // valiterdir - s = settings.getString(PrismSettings.PRISM_LIN_EQ_METHOD); - if (s.equals("Gauss-Seidel")) { - setSolnMethod(SolnMethod.GAUSS_SEIDEL); - } else { - setSolnMethod(SolnMethod.VALUE_ITERATION); - } s = settings.getString(PrismSettings.PRISM_MDP_SOLN_METHOD); if (s.equals("Gauss-Seidel")) { setSolnMethod(SolnMethod.GAUSS_SEIDEL); @@ -146,6 +188,7 @@ public class ProbModelChecker extends StateModelChecker public void printSettings() { super.printSettings(); + mainLog.print("linEqMethod = " + linEqMethod + " "); mainLog.print("termCrit = " + termCrit + " "); mainLog.print("termCritParam = " + termCritParam + " "); mainLog.print("maxIters = " + maxIters + " "); @@ -166,6 +209,14 @@ public class ProbModelChecker extends StateModelChecker this.verbosity = verbosity; } + /** + * Set method used to solve linear equation systems. + */ + public void setLinEqMethod(LinEqMethod linEqMethod) + { + this.linEqMethod = linEqMethod; + } + /** * Set termination criteria type for numerical iterative methods. */ @@ -237,6 +288,11 @@ public class ProbModelChecker extends StateModelChecker return verbosity; } + public LinEqMethod getLinEqMethod() + { + return linEqMethod; + } + public TermCrit getTermCrit() { return termCrit; @@ -377,7 +433,7 @@ public class ProbModelChecker extends StateModelChecker return StateValues.createFromBitSet(sol, model); } } - + /** * Model check an R operator expression and return the values for all states. */ @@ -448,7 +504,7 @@ public class ProbModelChecker extends StateModelChecker default: throw new PrismException("Cannot build rewards for " + modelType + "s"); } - + // Compute rewards mainLog.println("Building reward structure..."); switch (modelType) {