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

Model checkers: use DASimplify, allow AcceptanceReach in computations. [Joachim Klein] 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9610 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
ec4ddc4513
commit
f7f4bf5f51
4 changed files with 60 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. 20
      prism/src/explicit/DTMCModelChecker.java
  2. 23
      prism/src/explicit/MDPModelChecker.java
  3. 18
      prism/src/prism/NondetModelChecker.java
  4. 18
      prism/src/prism/ProbModelChecker.java

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

@ -31,6 +31,7 @@ import java.util.BitSet;
import java.util.List;
import java.util.Map;
import acceptance.AcceptanceReach;
import acceptance.AcceptanceType;
import parser.ast.Expression;
import parser.type.TypeDouble;
@ -66,16 +67,25 @@ public class DTMCModelChecker extends ProbModelChecker
mcLtl = new LTLModelChecker(this);
// Build product of Markov chain and automaton
AcceptanceType[] allowedAcceptance = {AcceptanceType.RABIN};
AcceptanceType[] allowedAcceptance = {
AcceptanceType.RABIN,
AcceptanceType.REACH
};
product = mcLtl.constructProductMC(this, (DTMC)model, expr, statesOfInterest, allowedAcceptance);
// Find accepting BSCCs + compute reachability probabilities
mainLog.println("\nFinding accepting BSCCs...");
BitSet acceptingBSCCs = mcLtl.findAcceptingBSCCs(product.getProductModel(), product.getAcceptance());
// Find accepting states + compute reachability probabilities
BitSet acc;
if (product.getAcceptance() instanceof AcceptanceReach) {
mainLog.println("\nSkipping BSCC computation since acceptance is defined via goal states...");
acc = ((AcceptanceReach)product.getAcceptance()).getGoalStates();
} else {
mainLog.println("\nFinding accepting BSCCs...");
acc = mcLtl.findAcceptingBSCCs(product.getProductModel(), product.getAcceptance());
}
mainLog.println("\nComputing reachability probabilities...");
mcProduct = new DTMCModelChecker(this);
mcProduct.inheritSettings(this);
probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs(product.getProductModel(), acceptingBSCCs).soln, product.getProductModel());
probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs(product.getProductModel(), acc).soln, product.getProductModel());
// Mapping probabilities in the original model
probs = product.projectToOriginalModel(probsProduct);

23
prism/src/explicit/MDPModelChecker.java
View File

@ -31,6 +31,7 @@ import java.util.Iterator;
import java.util.List;
import java.util.Map;
import acceptance.AcceptanceReach;
import acceptance.AcceptanceType;
import parser.ast.Expression;
import prism.PrismComponent;
@ -76,16 +77,26 @@ public class MDPModelChecker extends ProbModelChecker
// For LTL model checking routines
mcLtl = new LTLModelChecker(this);
AcceptanceType[] allowedAcceptance = {AcceptanceType.RABIN};
AcceptanceType[] allowedAcceptance = {
AcceptanceType.RABIN,
AcceptanceType.REACH
};
product = mcLtl.constructProductMDP(this, (MDP)model, expr, statesOfInterest, allowedAcceptance);
// Find accepting MECs + compute reachability probabilities
mainLog.println("\nFinding accepting MECs...");
BitSet acceptingMECs = mcLtl.findAcceptingECStates(product.getProductModel(), product.getAcceptance());
// Find accepting states + compute reachability probabilities
BitSet acc;
if (product.getAcceptance() instanceof AcceptanceReach) {
mainLog.println("\nSkipping accepting MEC computation since acceptance is defined via goal states...");
acc = ((AcceptanceReach)product.getAcceptance()).getGoalStates();
} else {
mainLog.println("\nFinding accepting MECs...");
acc = mcLtl.findAcceptingECStates(product.getProductModel(), product.getAcceptance());
}
mainLog.println("\nComputing reachability probabilities...");
mcProduct = new MDPModelChecker(this);
mcProduct.inheritSettings(this);
probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((MDP)product.getProductModel(), acceptingMECs, false).soln, product.getProductModel());
probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((MDP)product.getProductModel(), acc, false).soln, product.getProductModel());
// Subtract from 1 if we're model checking a negated formula for regular Pmin
if (minMax.isMin()) {

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

@ -37,6 +37,7 @@ import acceptance.AcceptanceOmega;
import acceptance.AcceptanceOmegaDD;
import acceptance.AcceptanceRabin;
import acceptance.AcceptanceRabinDD;
import acceptance.AcceptanceReachDD;
import acceptance.AcceptanceType;
import odd.ODDUtils;
import jdd.*;
@ -1004,7 +1005,10 @@ public class NondetModelChecker extends NonProbModelChecker
mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")...");
l = System.currentTimeMillis();
LTL2DA ltl2da = new LTL2DA(prism);
AcceptanceType[] allowedAcceptance = {AcceptanceType.RABIN};
AcceptanceType[] allowedAcceptance = {
AcceptanceType.RABIN,
AcceptanceType.REACH
};
da = ltl2da.convertLTLFormulaToDA(ltl, constantValues, allowedAcceptance);
mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics()+".");
l = System.currentTimeMillis() - l;
@ -1041,10 +1045,16 @@ public class NondetModelChecker extends NonProbModelChecker
out.close();
}
// Find accepting MECs + compute reachability probabilities
mainLog.println("\nFinding accepting end components...");
// Find accepting states + compute reachability probabilities
AcceptanceOmegaDD acceptance = da.getAcceptance().toAcceptanceDD(daDDRowVars);
JDDNode acc = mcLtl.findAcceptingECStates(acceptance, modelProduct, daDDRowVars, daDDColVars, fairness);
JDDNode acc;
if (acceptance instanceof AcceptanceReachDD) {
mainLog.println("\nSkipping accepting MEC computation since acceptance is defined via goal states...");
acc = ((AcceptanceReachDD) acceptance).getGoalStates();
} else {
mainLog.println("\nFinding accepting end components...");
acc = mcLtl.findAcceptingECStates(acceptance, modelProduct, daDDRowVars, daDDColVars, fairness);
}
acceptance.clear();
mainLog.println("\nComputing reachability probabilities...");
mcProduct = new NondetModelChecker(prism, modelProduct, null);

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

@ -36,6 +36,7 @@ import java.util.Vector;
import acceptance.AcceptanceOmega;
import acceptance.AcceptanceOmegaDD;
import acceptance.AcceptanceReachDD;
import acceptance.AcceptanceType;
import jdd.JDD;
import jdd.JDDNode;
@ -538,7 +539,10 @@ public class ProbModelChecker extends NonProbModelChecker
mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")...");
l = System.currentTimeMillis();
LTL2DA ltl2da = new LTL2DA(prism);
AcceptanceType[] allowedAcceptance = {AcceptanceType.RABIN};
AcceptanceType[] allowedAcceptance = {
AcceptanceType.RABIN,
AcceptanceType.REACH
};
da = ltl2da.convertLTLFormulaToDA(ltl, constantValues, allowedAcceptance);
mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + ".");
l = System.currentTimeMillis() - l;
@ -576,10 +580,16 @@ public class ProbModelChecker extends NonProbModelChecker
out.close();
}
// Find accepting BSCCs + compute reachability probabilities
mainLog.println("\nFinding accepting BSCCs...");
// Find accepting states + compute reachability probabilities
AcceptanceOmegaDD acceptance = da.getAcceptance().toAcceptanceDD(daDDRowVars);
JDDNode acc = mcLtl.findAcceptingBSCCs(acceptance, modelProduct);
JDDNode acc;
if (acceptance instanceof AcceptanceReachDD) {
mainLog.println("\nSkipping BSCC computation since acceptance is defined via goal states...");
acc = ((AcceptanceReachDD) acceptance).getGoalStates();
} else {
mainLog.println("\nFinding accepting BSCCs...");
acc = mcLtl.findAcceptingBSCCs(acceptance, modelProduct);
}
acceptance.clear();
mainLog.println("\nComputing reachability probabilities...");
mcProduct = createNewModelChecker(prism, modelProduct, null);

Write Preview
Loading…
Cancel
Save