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

Some re-factoring of LTL model checking in the explicit engine. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9921 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
5e92fabe95
commit
6e1cf75a8e
1 changed files with 48 additions and 69 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. 115
      prism/src/explicit/LTLModelChecker.java

115
prism/src/explicit/LTLModelChecker.java
View File

@ -65,7 +65,8 @@ import common.IterableStateSet;
public class LTLModelChecker extends PrismComponent
{
/** Make LTL product accessible as a Product */
public class LTLProduct<M extends Model> extends Product<M> {
public class LTLProduct<M extends Model> extends Product<M>
{
private int daSize;
private int invMap[];
private AcceptanceOmega acceptance;
@ -99,7 +100,6 @@ public class LTLModelChecker extends PrismComponent
}
}
/**
* Create a new LTLModelChecker, inherit basic state from parent (unless null).
*/
@ -186,31 +186,32 @@ public class LTLModelChecker extends PrismComponent
}
/**
* Generate a deterministic automaton for the given LTL expression and construct the product.
* 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. BitSets 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 ProbModelChecker, used for checking maximal state formulas
* @param dtmc the model
* @param expr a path expression
* @param statesOfInterest the set of states for which values should be calculated (null = all states)
* @param model the model
* @param expr a path expression, i.e. the LTL formula
* @param labelBS empty vector to be filled with BitSets for subformulas
* @param allowedAcceptance the allowed acceptance types
* @return the product with the DA
* @return the DA
*/
public LTLProduct<DTMC> constructProductMC(ProbModelChecker mc, DTMC dtmc, Expression expr, BitSet statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException
public DA<BitSet,? extends AcceptanceOmega> constructDAForLTLFormula(ProbModelChecker mc, Model model, Expression expr, Vector<BitSet> labelBS, AcceptanceType... allowedAcceptance) throws PrismException
{
Expression ltl;
DA<BitSet,? extends AcceptanceOmega> da;
LTLProduct<DTMC> product;
long time;
if (Expression.containsTemporalTimeBounds(expr)) {
if (dtmc.getModelType().continuousTime()) {
throw new PrismException("DRA construction for time-bounded operators not supported for " + dtmc.getModelType()+".");
if (model.getModelType().continuousTime()) {
throw new PrismException("Automaton 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.
//
// 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
@ -222,8 +223,7 @@ public class LTLModelChecker extends PrismComponent
}
// Model check maximal state formulas
Vector<BitSet> labelBS = new Vector<BitSet>();
ltl = checkMaximalStateFormulas(mc, dtmc, expr.deepCopy(), labelBS);
ltl = checkMaximalStateFormulas(mc, model, expr.deepCopy(), labelBS);
// Convert LTL formula to deterministic automaton
mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")...");
@ -233,20 +233,39 @@ public class LTLModelChecker extends PrismComponent
mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + ".");
time = System.currentTimeMillis() - time;
mainLog.println("Time for "+da.getAutomataType()+" translation: " + time / 1000.0 + " seconds.");
// If required, export DRA
// If required, export DA
if (settings.getExportPropAut()) {
mainLog.println("Exporting DRA to file \"" + settings.getExportPropAutFilename() + "\"...");
mainLog.println("Exporting " + da.getAutomataType() + " to file \"" + settings.getExportPropAutFilename() + "\"...");
PrismLog out = new PrismFileLog(settings.getExportPropAutFilename());
out.println(da);
out.close();
//dra.printDot(new java.io.PrintStream("dra.dot"));
//dra.printDot(new java.io.PrintStream("da.dot"));
}
return da;
}
// Build product of Markov chain and automaton
mainLog.println("\nConstructing MC-"+da.getAutomataType()+" product...");
product = constructProductMC(da, dtmc, labelBS, statesOfInterest);
/**
* Generate a deterministic automaton for the given LTL formula
* and construct the product of this automaton with a Markov chain.
*
* @param mc a ProbModelChecker, used for checking maximal state formulas
* @param model the model
* @param expr a path expression
* @param statesOfInterest the set of states for which values should be calculated (null = all states)
* @param allowedAcceptance the allowed acceptance types
* @return the product with the DA
*/
public LTLProduct<DTMC> constructProductMC(ProbModelChecker mc, DTMC model, Expression expr, BitSet statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException
{
// Convert LTL formula to automaton
Vector<BitSet> labelBS = new Vector<BitSet>();
DA<BitSet,? extends AcceptanceOmega> da;
da = constructDAForLTLFormula(mc, model, expr, labelBS, allowedAcceptance);
// Build product of model and automaton
mainLog.println("\nConstructing MC-"+da.getAutomataType()+" product...");
LTLProduct<DTMC> product = constructProductMC(da, model, labelBS, statesOfInterest);
mainLog.print("\n" + product.getProductModel().infoStringTable());
return product;
@ -371,7 +390,8 @@ public class LTLModelChecker extends PrismComponent
return product;
}
/**
* Generate the DA for the given LTL expression and construct the product.
* Generate a deterministic automaton for the given LTL formula
* and construct the product of this automaton with an MDP.
*
* @param mc a ProbModelChecker, used for checking maximal state formulas
* @param model the model
@ -383,55 +403,14 @@ public class LTLModelChecker extends PrismComponent
*/
public LTLProduct<MDP> constructProductMDP(ProbModelChecker mc, MDP model, Expression expr, BitSet statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException
{
Expression ltl;
DA<BitSet, ? extends AcceptanceOmega> da;
LTLProduct<MDP> product;
long time;
if (Expression.containsTemporalTimeBounds(expr)) {
if (model.getModelType().continuousTime()) {
throw new PrismException("DRA 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
// Convert LTL formula to automaton
Vector<BitSet> labelBS = new Vector<BitSet>();
ltl = checkMaximalStateFormulas(mc, model, expr.deepCopy(), labelBS);
// Convert LTL formula to deterministic automaton
mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")...");
time = System.currentTimeMillis();
LTL2DA ltl2da = new LTL2DA(this);
da = ltl2da.convertLTLFormulaToDA(ltl, mc.getConstantValues(), allowedAcceptance);
mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + ".");
time = System.currentTimeMillis() - time;
mainLog.println("Time for "+da.getAutomataType()+" translation: " + time / 1000.0 + " seconds.");
// If required, export DA
if (settings.getExportPropAut()) {
mainLog.println("Exporting "+da.getAutomataType()+" to file \"" + settings.getExportPropAutFilename() + "\"...");
PrismLog out = new PrismFileLog(settings.getExportPropAutFilename());
out.println(da);
out.close();
//da.printDot(new java.io.PrintStream("da.dot"));
}
DA<BitSet,? extends AcceptanceOmega> da;
da = constructDAForLTLFormula(mc, model, expr, labelBS, allowedAcceptance);
// Build product of MDP and automaton
// Build product of model and automaton
mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product...");
product = constructProductMDP(da, model, labelBS, statesOfInterest);
LTLProduct<MDP> product = constructProductMDP(da, model, labelBS, statesOfInterest);
mainLog.print("\n" + product.getProductModel().infoStringTable());
return product;

Write Preview
Loading…
Cancel
Save