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

Code re-factoring in NondetModelChecker. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7730 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 12 years ago
parent
896048bf37
commit
5171fc804e
1 changed files with 156 additions and 141 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 297
      prism/src/prism/NondetModelChecker.java

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

@ -556,7 +556,7 @@ public class NondetModelChecker extends NonProbModelChecker
Vector<JDDNode> tmptargetDDs = new Vector<JDDNode>(); Vector<JDDNode> tmptargetDDs = new Vector<JDDNode>();
List<JDDNode> tmpmultitargetDDs = new ArrayList<JDDNode>(); List<JDDNode> tmpmultitargetDDs = new ArrayList<JDDNode>();
List<Integer> tmpmultitargetIDs = new ArrayList<Integer>(); List<Integer> tmpmultitargetIDs = new ArrayList<Integer>();
ArrayList<DRA> tmpdra = new ArrayList<DRA>();
ArrayList<DRA<BitSet>> tmpdra = new ArrayList<DRA<BitSet>>();
ArrayList<JDDVars> tmpdraDDRowVars = new ArrayList<JDDVars>(); ArrayList<JDDVars> tmpdraDDRowVars = new ArrayList<JDDVars>();
ArrayList<JDDVars> tmpdraDDColVars = new ArrayList<JDDVars>(); ArrayList<JDDVars> tmpdraDDColVars = new ArrayList<JDDVars>();
int count = 0; int count = 0;
@ -685,7 +685,7 @@ public class NondetModelChecker extends NonProbModelChecker
* @param expr A multi objective * @param expr A multi objective
* @throws PrismException * @throws PrismException
*/ */
protected void ensureNoTimeBounded(ExpressionFunc expr) throws PrismException
private void ensureNoTimeBounded(ExpressionFunc expr) throws PrismException
{ {
try { try {
expr.accept(new ASTTraverse() expr.accept(new ASTTraverse()
@ -1216,8 +1216,11 @@ public class NondetModelChecker extends NonProbModelChecker
JDD.Deref(ec); JDD.Deref(ec);
} }
// Contents of a P operator, i.e. a path formula
// Model checking functions
/**
* Compute probabilities for the contents of a P operator.
*/
protected StateValues checkProbPathFormula(Expression expr, boolean qual, boolean min) throws PrismException protected StateValues checkProbPathFormula(Expression expr, boolean qual, boolean min) throws PrismException
{ {
// Test whether this is a simple path formula (i.e. PCTL) // Test whether this is a simple path formula (i.e. PCTL)
@ -1229,8 +1232,9 @@ public class NondetModelChecker extends NonProbModelChecker
} }
} }
// Simple path formula for P operator (one temporal op, possibly negated)
/**
* Compute probabilities for a simple, non-LTL path operator.
*/
protected StateValues checkProbPathFormulaSimple(Expression expr, boolean qual, boolean min) throws PrismException protected StateValues checkProbPathFormulaSimple(Expression expr, boolean qual, boolean min) throws PrismException
{ {
StateValues probs = null; StateValues probs = null;
@ -1277,128 +1281,9 @@ public class NondetModelChecker extends NonProbModelChecker
return probs; return probs;
} }
// LTL-like path formula for P operator
protected StateValues checkProbPathFormulaLTL(Expression expr, boolean qual, boolean min) throws PrismException
{
LTLModelChecker mcLtl;
StateValues probsProduct = null, probs = null;
Expression ltl;
Vector<JDDNode> labelDDs;
DRA dra;
NondetModel modelProduct;
NondetModelChecker mcProduct;
JDDNode startMask;
JDDVars draDDRowVars, draDDColVars;
int i;
long l;
// Can't do LTL with time-bounded variants of the temporal operators
try {
expr.accept(new ASTTraverse()
{
public void visitPre(ExpressionTemporal e) throws PrismLangException
{
if (e.getLowerBound() != null)
throw new PrismLangException(e.getOperatorSymbol());
if (e.getUpperBound() != null)
throw new PrismLangException(e.getOperatorSymbol());
}
});
} catch (PrismLangException e) {
String s = "Temporal operators (like " + e.getMessage() + ")";
s += " cannot have time bounds for LTL properties";
throw new PrismException(s);
}
// Can't do "dfa" properties yet
if (expr instanceof ExpressionFunc && ((ExpressionFunc) expr).getName().equals("dfa")) {
throw new PrismException("Model checking for \"dfa\" specifications not supported yet");
}
// For LTL model checking routines
mcLtl = new LTLModelChecker(prism);
// Model check maximal state formulas
labelDDs = new Vector<JDDNode>();
ltl = mcLtl.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelDDs);
// Convert LTL formula to deterministic Rabin automaton (DRA)
// For min probabilities, need to negate the formula
// (But check fairness setting since this may affect min/max)
// (add parentheses to allow re-parsing if required)
if (min && !fairness) {
ltl = Expression.Not(Expression.Parenth(ltl));
}
mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
l = System.currentTimeMillis();
dra = LTLModelChecker.convertLTLFormulaToDRA(ltl);
mainLog.println("\nDRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs.");
/*try {
mainLog.print(dra);
dra.printDot(new java.io.PrintStream("dra.dot"));
} catch(Exception e) {}*/
l = System.currentTimeMillis() - l;
mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds.");
// Build product of MDP and automaton
mainLog.println("\nConstructing MDP-DRA product...");
draDDRowVars = new JDDVars();
draDDColVars = new JDDVars();
modelProduct = mcLtl.constructProductMDP(dra, model, labelDDs, draDDRowVars, draDDColVars);
mainLog.println();
modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo());
// Output product, if required
if (prism.getExportProductTrans()) {
try {
mainLog.println("\nExporting product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"...");
modelProduct.exportToFile(Prism.EXPORT_PLAIN, true, new File(prism.getExportProductTransFilename()));
} catch (FileNotFoundException e) {
mainLog.printWarning("Could not export product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"");
}
}
if (prism.getExportProductStates()) {
mainLog.println("\nExporting product state space to file \"" + prism.getExportProductStatesFilename() + "\"...");
modelProduct.exportStates(Prism.EXPORT_PLAIN, new PrismFileLog(prism.getExportProductStatesFilename()));
}
// Find accepting MECs + compute reachability probabilities
mainLog.println("\nFinding accepting end components...");
JDDNode acc = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, draDDRowVars, draDDColVars, fairness);
mainLog.println("\nComputing reachability probabilities...");
mcProduct = new NondetModelChecker(prism, modelProduct, null);
probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual, min && fairness);
// subtract from 1 if we're model checking a negated formula for regular Pmin
if (min && !fairness) {
probsProduct.subtractFromOne();
}
// Convert probability vector to original model
// First, filter over DRA start states
startMask = mcLtl.buildStartMask(dra, labelDDs, draDDRowVars);
JDD.Ref(model.getReach());
startMask = JDD.And(model.getReach(), startMask);
probsProduct.filter(startMask);
// Then sum over DD vars for the DRA state
probs = probsProduct.sumOverDDVars(draDDRowVars, model);
// Deref, clean up
probsProduct.clear();
modelProduct.clear();
for (i = 0; i < labelDDs.size(); i++) {
JDD.Deref(labelDDs.get(i));
}
JDD.Deref(acc);
JDD.Deref(startMask);
draDDRowVars.derefAll();
draDDColVars.derefAll();
return probs;
}
// next
/**
* Compute probabilities for a next operator.
*/
protected StateValues checkProbNext(ExpressionTemporal expr, boolean min) throws PrismException protected StateValues checkProbNext(ExpressionTemporal expr, boolean min) throws PrismException
{ {
JDDNode b; JDDNode b;
@ -1420,8 +1305,9 @@ public class NondetModelChecker extends NonProbModelChecker
return probs; return probs;
} }
// bounded until
/**
* Compute probabilities for a bounded until operator.
*/
protected StateValues checkProbBoundedUntil(ExpressionTemporal expr, boolean min) throws PrismException protected StateValues checkProbBoundedUntil(ExpressionTemporal expr, boolean min) throws PrismException
{ {
int time; int time;
@ -1476,10 +1362,10 @@ public class NondetModelChecker extends NonProbModelChecker
return probs; return probs;
} }
// until (unbounded)
// this method is split into two steps so that the LTL model checker can use the second part directly
/**
* Compute probabilities for an (unbounded) until operator.
* Note: This method is split into two steps so that the LTL model checker can use the second part directly.
*/
protected StateValues checkProbUntil(ExpressionTemporal expr, boolean qual, boolean min) throws PrismException protected StateValues checkProbUntil(ExpressionTemporal expr, boolean qual, boolean min) throws PrismException
{ {
JDDNode b1, b2; JDDNode b1, b2;
@ -1515,8 +1401,13 @@ public class NondetModelChecker extends NonProbModelChecker
return probs; return probs;
} }
// until (unbounded): b1/b2 are bdds for until operands
/**
* Compute probabilities for an (unbounded) until operator.
* @param b1 Remain in these states
* @param b2 Target states
* @param qual True if only qualititative (0/1) results are needed
* @param min Min or max probabilities (true=min, false=max)
*/
protected StateValues checkProbUntil(JDDNode b1, JDDNode b2, boolean qual, boolean min) throws PrismException protected StateValues checkProbUntil(JDDNode b1, JDDNode b2, boolean qual, boolean min) throws PrismException
{ {
JDDNode splus, newb1, newb2; JDDNode splus, newb1, newb2;
@ -1591,8 +1482,130 @@ public class NondetModelChecker extends NonProbModelChecker
return probs; return probs;
} }
// cumulative reward
/**
* Compute probabilities for an LTL path formula
*/
protected StateValues checkProbPathFormulaLTL(Expression expr, boolean qual, boolean min) throws PrismException
{
LTLModelChecker mcLtl;
StateValues probsProduct = null, probs = null;
Expression ltl;
Vector<JDDNode> labelDDs;
DRA<BitSet> dra;
NondetModel modelProduct;
NondetModelChecker mcProduct;
JDDNode startMask;
JDDVars draDDRowVars, draDDColVars;
int i;
long l;
// Can't do LTL with time-bounded variants of the temporal operators
try {
expr.accept(new ASTTraverse()
{
public void visitPre(ExpressionTemporal e) throws PrismLangException
{
if (e.getLowerBound() != null)
throw new PrismLangException(e.getOperatorSymbol());
if (e.getUpperBound() != null)
throw new PrismLangException(e.getOperatorSymbol());
}
});
} catch (PrismLangException e) {
String s = "Temporal operators (like " + e.getMessage() + ")";
s += " cannot have time bounds for LTL properties";
throw new PrismException(s);
}
// Can't do "dfa" properties yet
if (expr instanceof ExpressionFunc && ((ExpressionFunc) expr).getName().equals("dfa")) {
throw new PrismException("Model checking for \"dfa\" specifications not supported yet");
}
// For LTL model checking routines
mcLtl = new LTLModelChecker(prism);
// Model check maximal state formulas
labelDDs = new Vector<JDDNode>();
ltl = mcLtl.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelDDs);
// Convert LTL formula to deterministic Rabin automaton (DRA)
// For min probabilities, need to negate the formula
// (But check fairness setting since this may affect min/max)
// (add parentheses to allow re-parsing if required)
if (min && !fairness) {
ltl = Expression.Not(Expression.Parenth(ltl));
}
mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
l = System.currentTimeMillis();
dra = LTLModelChecker.convertLTLFormulaToDRA(ltl);
mainLog.println("\nDRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs.");
/*try {
mainLog.print(dra);
dra.printDot(new java.io.PrintStream("dra.dot"));
} catch(Exception e) {}*/
l = System.currentTimeMillis() - l;
mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds.");
// Build product of MDP and automaton
mainLog.println("\nConstructing MDP-DRA product...");
draDDRowVars = new JDDVars();
draDDColVars = new JDDVars();
modelProduct = mcLtl.constructProductMDP(dra, model, labelDDs, draDDRowVars, draDDColVars);
mainLog.println();
modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo());
// Output product, if required
if (prism.getExportProductTrans()) {
try {
mainLog.println("\nExporting product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"...");
modelProduct.exportToFile(Prism.EXPORT_PLAIN, true, new File(prism.getExportProductTransFilename()));
} catch (FileNotFoundException e) {
mainLog.printWarning("Could not export product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"");
}
}
if (prism.getExportProductStates()) {
mainLog.println("\nExporting product state space to file \"" + prism.getExportProductStatesFilename() + "\"...");
modelProduct.exportStates(Prism.EXPORT_PLAIN, new PrismFileLog(prism.getExportProductStatesFilename()));
}
// Find accepting MECs + compute reachability probabilities
mainLog.println("\nFinding accepting end components...");
JDDNode acc = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, draDDRowVars, draDDColVars, fairness);
mainLog.println("\nComputing reachability probabilities...");
mcProduct = new NondetModelChecker(prism, modelProduct, null);
probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual, min && fairness);
// subtract from 1 if we're model checking a negated formula for regular Pmin
if (min && !fairness) {
probsProduct.subtractFromOne();
}
// Convert probability vector to original model
// First, filter over DRA start states
startMask = mcLtl.buildStartMask(dra, labelDDs, draDDRowVars);
JDD.Ref(model.getReach());
startMask = JDD.And(model.getReach(), startMask);
probsProduct.filter(startMask);
// Then sum over DD vars for the DRA state
probs = probsProduct.sumOverDDVars(draDDRowVars, model);
// Deref, clean up
probsProduct.clear();
modelProduct.clear();
for (i = 0; i < labelDDs.size(); i++) {
JDD.Deref(labelDDs.get(i));
}
JDD.Deref(acc);
JDD.Deref(startMask);
draDDRowVars.derefAll();
draDDColVars.derefAll();
return probs;
}
/**
* Compute rewards for a cumulative reward operator.
*/
protected StateValues checkRewardCumul(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException protected StateValues checkRewardCumul(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
{ {
int time; // time int time; // time
@ -1624,8 +1637,9 @@ public class NondetModelChecker extends NonProbModelChecker
return rewards; return rewards;
} }
// inst reward
/**
* Compute rewards for an instantaneous reward operator.
*/
protected StateValues checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException protected StateValues checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
{ {
int time; // time bound int time; // time bound
@ -1643,8 +1657,9 @@ public class NondetModelChecker extends NonProbModelChecker
return rewards; return rewards;
} }
// reach reward
/**
* Compute rewards for a reachability reward operator.
*/
protected StateValues checkRewardReach(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException protected StateValues checkRewardReach(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
{ {
JDDNode b; JDDNode b;

Write Preview
Loading…
Cancel
Save