diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 80324a14..128da11d 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -452,14 +452,14 @@ public class DTMCModelChecker extends ProbModelChecker exportLabels(dtmc, labels, labelNames, Prism.EXPORT_PLAIN, new PrismFileLog(getExportTargetFilename())); } - if (precomp && (prob0 || prob1) && cachePre) { + if (precomp && (prob0 || prob1) && preRel) { pre = dtmc.getPredecessorRelation(this, true); } // Precomputation timerProb0 = System.currentTimeMillis(); if (precomp && prob0) { - if (cachePre) { + if (preRel) { no = prob0(dtmc, remain, target, pre); } else { no = prob0(dtmc, remain, target); @@ -470,7 +470,7 @@ public class DTMCModelChecker extends ProbModelChecker timerProb0 = System.currentTimeMillis() - timerProb0; timerProb1 = System.currentTimeMillis(); if (precomp && prob1) { - if (cachePre) { + if (preRel) { yes = prob1(dtmc, remain, target, pre); } else { yes = prob1(dtmc, remain, target); diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 020dfdfd..cb9f5b66 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -72,8 +72,8 @@ public class ProbModelChecker extends NonProbModelChecker protected boolean precomp = true; protected boolean prob0 = true; protected boolean prob1 = true; - // Cache predecessor relation? (e.g. for precomputation) - protected boolean cachePre = true; + // Use predecessor relation? (e.g. for precomputation) + protected boolean preRel = true; // Direction of convergence for value iteration (lfp/gfp) protected ValIterDir valIterDir = ValIterDir.BELOW; // Method used for numerical solution @@ -213,7 +213,7 @@ public class ProbModelChecker extends NonProbModelChecker // PRISM_PROB1 setProb1(settings.getBoolean(PrismSettings.PRISM_PROB1)); // PRISM_USE_PRE - setCachePre(settings.getBoolean(PrismSettings.PRISM_CACHE_PRE)); + setPreRel(settings.getBoolean(PrismSettings.PRISM_PRE_REL)); // PRISM_FAIRNESS if (settings.getBoolean(PrismSettings.PRISM_FAIRNESS)) { throw new PrismNotSupportedException("The explicit engine does not support model checking MDPs under fairness"); @@ -345,11 +345,11 @@ public class ProbModelChecker extends NonProbModelChecker } /** - * Set whether or not to use precomputed Pre relation + * Set whether or not to use pre-computed predecessor relation */ - public void setCachePre(boolean cachePre) + public void setPreRel(boolean preRel) { - this.cachePre = cachePre; + this.preRel = preRel; } /** @@ -433,9 +433,9 @@ public class ProbModelChecker extends NonProbModelChecker return prob1; } - public boolean getCachePre() + public boolean getPreRel() { - return cachePre; + return preRel; } public ValIterDir getValIterDir() diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 7c03d98d..8a5452c2 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -776,9 +776,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener return settings.getBoolean(PrismSettings.PRISM_PROB1); } - public boolean getCachePre() + public boolean getPreRel() { - return settings.getBoolean(PrismSettings.PRISM_CACHE_PRE); + return settings.getBoolean(PrismSettings.PRISM_PRE_REL); } public boolean getFairness() diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 73e1948e..b8ccc7ba 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -77,7 +77,7 @@ public class PrismSettings implements Observer 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_CACHE_PRE = "prism.cachePre"; + public static final String PRISM_PRE_REL = "prism.preRel"; public static final String PRISM_FIX_DEADLOCKS = "prism.fixDeadlocks"; public static final String PRISM_DO_PROB_CHECKS = "prism.doProbChecks"; public static final String PRISM_SUM_ROUND_OFF = "prism.sumRoundOff"; @@ -249,8 +249,8 @@ public class PrismSettings implements Observer "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_CACHE_PRE, "Cache predecessor relation", "4.2.1", new Boolean(true), "", - "Whether to use a precomputed predecessor relation in several algorithms." }, + { BOOLEAN_TYPE, PRISM_PRE_REL, "Use predecessor relation", "4.2.1", new Boolean(true), "", + "Whether to use a pre-computed predecessor relation in several algorithms." }, { BOOLEAN_TYPE, PRISM_FAIRNESS, "Use fairness", "2.1", new Boolean(false), "", "Constrain to fair adversaries when model checking MDPs." }, { BOOLEAN_TYPE, PRISM_FIX_DEADLOCKS, "Automatically fix deadlocks", "4.0.3", new Boolean(true), "", @@ -1018,9 +1018,9 @@ public class PrismSettings implements Observer else if (sw.equals("noprob1")) { set(PRISM_PROB1, false); } - // Caching of predecessor relation (e.g. for precomputation) - else if (sw.equals("nocachepre")) { - set(PRISM_CACHE_PRE, false); + // Use predecessor relation? (e.g. for precomputation) + else if (sw.equals("noprerel")) { + set(PRISM_PRE_REL, false); } // Fix deadlocks on/off else if (sw.equals("fixdl")) { @@ -1552,6 +1552,7 @@ public class PrismSettings implements Observer 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("-noprerel ...................... Do not pre-compute/use predecessor relation, e.g. for precomputation"); 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 [default]");