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

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
master
Dave Parker 14 years ago
parent
5dab19e7dc
commit
4a1163a86d
5 changed files with 53 additions and 15 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. 4
      prism/src/explicit/ProbModelChecker.java
  2. 11
      prism/src/prism/NondetModelChecker.java
  3. 16
      prism/src/prism/Prism.java
  4. 18
      prism/src/prism/PrismSettings.java
  5. 19
      prism/src/prism/ProbModelChecker.java

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

@ -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")) {

11
prism/src/prism/NondetModelChecker.java
View File

@ -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"

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

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

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

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

19
prism/src/prism/ProbModelChecker.java
View File

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

Write Preview
Loading…
Cancel
Save