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

Symbolic LTLModelChecker: Provide constructDAForLTLFormula, use in ProbModelChecker and NondetModelChecker 

Mirrors the recent refactoring in the explicit engine.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10577 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 10 years ago
parent
298266c1cd
commit
423d169552
3 changed files with 68 additions and 86 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. 61
      prism/src/prism/LTLModelChecker.java
  2. 45
      prism/src/prism/NondetModelChecker.java
  3. 48
      prism/src/prism/ProbModelChecker.java

61
prism/src/prism/LTLModelChecker.java
View File

@ -27,6 +27,7 @@
package prism;
import java.io.PrintStream;
import java.util.ArrayList;
import java.util.BitSet;
import java.util.List;
@ -37,7 +38,9 @@ import acceptance.AcceptanceOmega;
import acceptance.AcceptanceOmegaDD;
import acceptance.AcceptanceRabin;
import acceptance.AcceptanceRabinDD;
import acceptance.AcceptanceType;
import automata.DA;
import automata.LTL2DA;
import jdd.JDD;
import jdd.JDDNode;
import jdd.JDDVars;
@ -154,6 +157,64 @@ public class LTLModelChecker extends PrismComponent
return expr;
}
/**
* Construct a deterministic automaton (DA) for an LTL formula, having first extracted maximal state formulas
* and model checked them with the passed in model checker. The maximal state formulas are assigned labels
* (L0, L1, etc.) which become the atomic propositions in the resulting DA. JDDNodes giving the states which
* satisfy each label are put into the vector {@code labelBS}, which should be empty when this function is called.
*
* @param mc a ModelChecker, used for checking maximal state formulas
* @param model the model
* @param expr a path expression, i.e. the LTL formula
* @param labelBS empty vector to be filled with JDDNodes for subformulas
* @param allowedAcceptance the allowed acceptance types
* @return the DA
*/
public DA<BitSet,? extends AcceptanceOmega> constructDAForLTLFormula(ModelChecker mc, Model model, Expression expr, Vector<JDDNode> labelDDs, AcceptanceType... allowedAcceptance) throws PrismException
{
if (Expression.containsTemporalTimeBounds(expr)) {
if (model.getModelType().continuousTime()) {
throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
}
if (expr.isSimplePathFormula()) {
// Convert simple path formula to canonical form,
// DRA is then generated by LTL2RabinLibrary.
//
// The conversion to canonical form has to happen here, because once
// checkMaximalStateFormulas has been called, the formula should not be modified
// anymore, as converters may expect that the generated labels for maximal state
// formulas only appear positively
expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
} else {
throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
}
}
// Model check maximal state formulas
Expression ltl = checkMaximalStateFormulas(mc, model, expr.deepCopy(), labelDDs);
// Convert LTL formula to deterministic automaton (DA)
mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")...");
long time = System.currentTimeMillis();
LTL2DA ltl2da = new LTL2DA(this);
DA<BitSet, ? extends AcceptanceOmega> da = ltl2da.convertLTLFormulaToDA(ltl, mc.getConstantValues(), allowedAcceptance);
da.checkForCanonicalAPs(labelDDs.size());
mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + ".");
time = System.currentTimeMillis() - time;
mainLog.println("Time for deterministic automaton translation: " + time / 1000.0 + " seconds.");
// If required, export DA
if (getSettings().getExportPropAut()) {
mainLog.println("Exporting DA to file \"" + getSettings().getExportPropAutFilename() + "\"...");
PrintStream out = PrismUtils.newPrintStream(getSettings().getExportPropAutFilename());
da.print(out, getSettings().getExportPropAutType());
out.close();
}
return da;
}
/**
* Construct the product of a DA and a DTMC/CTMC.
* @param da The DA

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

@ -1116,8 +1116,7 @@ public class NondetModelChecker extends NonProbModelChecker
{
LTLModelChecker mcLtl;
StateValues probsProduct = null, probs = null;
Expression ltl;
Vector<JDDNode> labelDDs;
Vector<JDDNode> labelDDs = new Vector<JDDNode>();
DA<BitSet, ? extends AcceptanceOmega> da;
NondetModel modelProduct;
NondetModelChecker mcProduct;
@ -1133,25 +1132,6 @@ public class NondetModelChecker extends NonProbModelChecker
expr = Expression.Not(Expression.Parenth(expr));
}
if (Expression.containsTemporalTimeBounds(expr)) {
if (model.getModelType().continuousTime()) {
throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
}
if (expr.isSimplePathFormula()) {
// Convert simple path formula to canonical form,
// DA is then generated by LTL2RabinLibrary.
//
// The conversion to canonical form has to happen here, because once
// checkMaximalStateFormulas has been called, the formula should not be modified
// anymore, as converters may expect that the generated labels for maximal state
// formulas only appear positively
expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
} else {
throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
}
}
// 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");
@ -1159,34 +1139,17 @@ public class NondetModelChecker extends NonProbModelChecker
// 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 automaton (DA)
mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")...");
l = System.currentTimeMillis();
LTL2DA ltl2da = new LTL2DA(prism);
AcceptanceType[] allowedAcceptance = {
AcceptanceType.RABIN,
AcceptanceType.GENERALIZED_RABIN,
AcceptanceType.REACH
};
da = ltl2da.convertLTLFormulaToDA(ltl, constantValues, allowedAcceptance);
da.checkForCanonicalAPs(labelDDs.size());
mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics()+".");
l = System.currentTimeMillis() - l;
mainLog.println("Time for deterministic automaton translation: " + l / 1000.0 + " seconds.");
// If required, export DA
if (prism.getSettings().getExportPropAut()) {
mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"...");
PrintStream out = PrismUtils.newPrintStream(prism.getSettings().getExportPropAutFilename());
da.print(out, prism.getSettings().getExportPropAutType());
out.close();
}
da = mcLtl.constructDAForLTLFormula(this, model, expr, labelDDs, allowedAcceptance);
// Build product of MDP and automaton
l = System.currentTimeMillis();
mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product...");
daDDRowVars = new JDDVars();
daDDColVars = new JDDVars();

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

@ -506,63 +506,21 @@ public class ProbModelChecker extends NonProbModelChecker
{
LTLModelChecker mcLtl;
StateValues probsProduct = null, probs = null;
Expression ltl;
Vector<JDDNode> labelDDs;
Vector<JDDNode> labelDDs = new Vector<JDDNode>();
DA<BitSet, ? extends AcceptanceOmega> da;
ProbModel modelProduct;
ProbModelChecker mcProduct;
JDDNode startMask;
JDDVars daDDRowVars, daDDColVars;
int i;
long l;
if (Expression.containsTemporalTimeBounds(expr)) {
if (model.getModelType().continuousTime()) {
throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
}
if (expr.isSimplePathFormula()) {
// Convert simple path formula to canonical form,
// DRA is then generated by LTL2RabinLibrary.
//
// The conversion to canonical form has to happen here, because once
// checkMaximalStateFormulas has been called, the formula should not be modified
// anymore, as converters may expect that the generated labels for maximal state
// formulas only appear positively
expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
} else {
throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
}
}
// 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 automaton (DA)
mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")...");
l = System.currentTimeMillis();
LTL2DA ltl2da = new LTL2DA(prism);
AcceptanceType[] allowedAcceptance = {
AcceptanceType.RABIN,
AcceptanceType.REACH,
AcceptanceType.GENERIC
};
da = ltl2da.convertLTLFormulaToDA(ltl, constantValues, allowedAcceptance);
da.checkForCanonicalAPs(labelDDs.size());
mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + ".");
l = System.currentTimeMillis() - l;
mainLog.println("Time for deterministic automaton translation: " + l / 1000.0 + " seconds.");
// If required, export DA
if (prism.getSettings().getExportPropAut()) {
mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"...");
PrintStream out = PrismUtils.newPrintStream(prism.getSettings().getExportPropAutFilename());
da.print(out, prism.getSettings().getExportPropAutType());
out.close();
}
mcLtl = new LTLModelChecker(prism);
da = mcLtl.constructDAForLTLFormula(this, model, expr, labelDDs, allowedAcceptance);
// Build product of Markov chain and automaton
// (note: might be a CTMC - StochModelChecker extends this class)

Write Preview
Loading…
Cancel
Save