s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Re-rename new predecessor option (-nocachepre to -noprerel, etc.) 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10197 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
01aaf56ca3
commit
88eb9ae71a
4 changed files with 20 additions and 19 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 6
      prism/src/explicit/DTMCModelChecker.java
  2. 16
      prism/src/explicit/ProbModelChecker.java
  3. 4
      prism/src/prism/Prism.java
  4. 13
      prism/src/prism/PrismSettings.java

6
prism/src/explicit/DTMCModelChecker.java
View File

@ -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);

16
prism/src/explicit/ProbModelChecker.java
View File

@ -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()

4
prism/src/prism/Prism.java
View File

@ -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()

13
prism/src/prism/PrismSettings.java
View File

@ -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]");

Write Preview
Loading…
Cancel
Save