From 4a1163a86d6c5d4a496b3d5a8a7b0b0fcbc88729 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 21 Oct 2011 09:21:49 +0000 Subject: [PATCH] Added ability to disable precomputation algs independently (switches -noprob0 and -noprob1). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4103 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/ProbModelChecker.java | 4 ++-- prism/src/prism/NondetModelChecker.java | 11 ++++++----- prism/src/prism/Prism.java | 16 ++++++++++++++++ prism/src/prism/PrismSettings.java | 18 ++++++++++++++++-- prism/src/prism/ProbModelChecker.java | 19 +++++++++++++------ 5 files changed, 53 insertions(+), 15 deletions(-) diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 7f5cbc89..78fcf5fc 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -99,8 +99,8 @@ public class ProbModelChecker extends StateModelChecker setTermCritParam(settings.getDouble(PrismSettings.PRISM_TERM_CRIT_PARAM)); setMaxIters(settings.getInteger(PrismSettings.PRISM_MAX_ITERS)); setPrecomp(settings.getBoolean(PrismSettings.PRISM_PRECOMPUTATION)); - // prob0 - // prob1 + 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")) { diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 763ab43e..7dbadce7 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -79,8 +79,8 @@ public class NondetModelChecker extends NonProbModelChecker // Inherit some options from parent Prism object and store locally. precomp = prism.getPrecomp(); - prob0 = true; - prob1 = true; + prob0 = prism.getProb0(); + prob1 = prism.getProb1(); fairness = prism.getFairness(); // Display warning and/or make changes for some option combinations @@ -995,7 +995,8 @@ public class NondetModelChecker extends NonProbModelChecker } else { // no // if precomputation enabled - if (precomp && prob0) { + // (nb: prob1 needs prob0) + if (precomp && (prob0 || prob1)) { // min if (min) { // no: "min prob = 0" equates to "there exists an adversary prob equals 0" @@ -1016,8 +1017,8 @@ public class NondetModelChecker extends NonProbModelChecker no = JDD.And(reach, JDD.Not(JDD.Or(b1, b2))); } // yes - // if precomputation enabled (need both prob0/prob1 to be enabled to do prob1) - if (precomp && prob0 && prob1) { + // if precomputation enabled + if (precomp && prob1) { // min if (min) { // yes: "min prob = 1" equates to "for all adversaries prob equals 1" diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 2b25d5ed..051f68e5 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -278,6 +278,16 @@ public class Prism implements PrismSettingsListener settings.set(PrismSettings.PRISM_PRECOMPUTATION, b); } + public void setProb0(boolean b) throws PrismException + { + settings.set(PrismSettings.PRISM_PROB0, b); + } + + public void setProb1(boolean b) throws PrismException + { + settings.set(PrismSettings.PRISM_PROB1, b); + } + public void setDoProbChecks(boolean b) throws PrismException { settings.set(PrismSettings.PRISM_DO_PROB_CHECKS, b); @@ -479,6 +489,12 @@ public class Prism implements PrismSettingsListener public boolean getPrecomp() { return settings.getBoolean(PrismSettings.PRISM_PRECOMPUTATION); } + public boolean getProb0() + { return settings.getBoolean(PrismSettings.PRISM_PROB0); } + + public boolean getProb1() + { return settings.getBoolean(PrismSettings.PRISM_PROB1); } + public boolean getFairness() { return settings.getBoolean(PrismSettings.PRISM_FAIRNESS); } diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 6a4677d3..90a85658 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -72,6 +72,8 @@ public class PrismSettings implements Observer public static final String PRISM_VERBOSE = "prism.verbose"; public static final String PRISM_FAIRNESS = "prism.fairness"; public static final String PRISM_PRECOMPUTATION = "prism.precomputation"; + public static final String PRISM_PROB0 = "prism.prob0"; + public static final String PRISM_PROB1 = "prism.prob1"; public static final String PRISM_DO_PROB_CHECKS = "prism.doProbChecks"; public static final String PRISM_COMPACT = "prism.compact"; public static final String PRISM_LIN_EQ_METHOD = "prism.linEqMethod";//"prism.iterativeMethod"; @@ -204,7 +206,11 @@ public class PrismSettings implements Observer "Maximum number of iterations to perform if iterative methods do not converge." }, // MODEL CHECKING OPTIONS: { BOOLEAN_TYPE, PRISM_PRECOMPUTATION, "Use precomputation", "2.1", new Boolean(true), "", - "Use model checking precomputation algorithms (Prob0, Prob1, etc.), where optional." }, + "Whether to use model checking precomputation algorithms (Prob0, Prob1, etc.), where optional." }, + { BOOLEAN_TYPE, PRISM_PROB0, "Use Prob0 precomputation", "4.0.2", new Boolean(true), "", + "Whether to use model checking precomputation algorithm Prob0 (if precomputation enabled)." }, + { BOOLEAN_TYPE, PRISM_PROB1, "Use Prob1 precomputation", "4.0.2", new Boolean(true), "", + "Whether to use model checking precomputation algorithm Prob1 (if precomputation enabled)." }, { BOOLEAN_TYPE, PRISM_FAIRNESS, "Use fairness", "2.1", new Boolean(false), "", "Constrain to fair adversaries when model checking MDPs." }, { BOOLEAN_TYPE, PRISM_DO_PROB_CHECKS, "Do probability/rate checks", "2.1", new Boolean(true), "", @@ -827,6 +833,12 @@ public class PrismSettings implements Observer else if (sw.equals("nopre")) { set(PRISM_PRECOMPUTATION, false); } + else if (sw.equals("noprob0")) { + set(PRISM_PROB0, false); + } + else if (sw.equals("noprob1")) { + set(PRISM_PROB1, false); + } // Fairness on/off else if (sw.equals("fair")) { set(PRISM_FAIRNESS, true); @@ -1050,7 +1062,9 @@ public class PrismSettings implements Observer mainLog.println("-maxiters .................. Set max number of iterations [default: 10000]"); mainLog.println(); mainLog.println("MODEL CHECKING OPTIONS:"); - mainLog.println("-nopre ......................... Skip (optional) precomputation algorithms"); + mainLog.println("-nopre ......................... Skip precomputation algorithms (where optional)"); + mainLog.println("-noprob0 ....................... Skip precomputation algorithm Prob0 (where optional)"); + mainLog.println("-noprob1 ....................... Skip precomputation algorithm Prob1 (where optional)"); mainLog.println("-fair .......................... Use fairness (for model checking of MDPs)"); mainLog.println("-nofair ........................ Don't use fairness (for model checking of MDPs) [default]"); mainLog.println("-fixdl ......................... Automatically put self-loops in deadlock states"); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index bc3ba0a4..0e242de2 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -52,6 +52,8 @@ public class ProbModelChecker extends NonProbModelChecker // Use 0,1 precomputation algorithms? protected boolean precomp; + protected boolean prob0; + protected boolean prob1; // Do BSCC computation? protected boolean bsccComp; @@ -69,6 +71,8 @@ public class ProbModelChecker extends NonProbModelChecker // Inherit some options from parent Prism object. // Store locally and/or pass onto engines. precomp = prism.getPrecomp(); + prob0 = prism.getProb0(); + prob1 = prism.getProb1(); bsccComp = prism.getBSCCComp(); switch (engine) { case Prism.MTBDD: @@ -188,7 +192,7 @@ public class ProbModelChecker extends NonProbModelChecker } // Compute probabilities - boolean qual = pb != null && ((p == 0) || (p == 1)) && precomp; + boolean qual = pb != null && ((p == 0) || (p == 1)) && precomp && prob0 && prob1; probs = checkProbPathFormula(expr.getExpression(), qual); // Print out probabilities @@ -1345,7 +1349,7 @@ public class ProbModelChecker extends NonProbModelChecker // no if (yes.equals(reach)) { no = JDD.Constant(0); - } else if (precomp) { + } else if (precomp && prob0) { no = PrismMTBDD.Prob0(tr01, reach, allDDRowVars, allDDColVars, b1, yes); } else { JDD.Ref(reach); @@ -1508,17 +1512,20 @@ public class ProbModelChecker extends NonProbModelChecker maybe = JDD.Constant(0); } else { // no/yes - if (precomp) { + if (precomp && (prob0 || prob1)) { no = PrismMTBDD.Prob0(tr01, reach, allDDRowVars, allDDColVars, b1, b2); - yes = PrismMTBDD.Prob1(tr01, reach, allDDRowVars, allDDColVars, b1, b2, no); } else { - JDD.Ref(b2); - yes = b2; JDD.Ref(reach); JDD.Ref(b1); JDD.Ref(b2); no = JDD.And(reach, JDD.Not(JDD.Or(b1, b2))); } + if (precomp && prob1) { + yes = PrismMTBDD.Prob1(tr01, reach, allDDRowVars, allDDColVars, b1, b2, no); + } else { + JDD.Ref(b2); + yes = b2; + } // maybe JDD.Ref(reach); JDD.Ref(yes);