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

Refactor LTL product construction in explicit engine. [Joachim Klein] 

LTLModelChecker: add LTLProduct, translation between product and model / automaton states.
Refactor explicit.DTMCModelChecker to use Product for DRA product
Refactor explicit.MDPModelChecker to use Product for DRA product
Switch to using AcceptanceRabin in the Product instead of passing DRA to the findAcceptingBSCC etc routines



git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9591 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
150775d09f
commit
36991a899a
3 changed files with 86 additions and 82 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. 26
      prism/src/explicit/DTMCModelChecker.java
  2. 119
      prism/src/explicit/LTLModelChecker.java
  3. 23
      prism/src/explicit/MDPModelChecker.java

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

@ -36,7 +36,6 @@ import acceptance.AcceptanceRabin;
import parser.ast.Expression; import parser.ast.Expression;
import parser.type.TypeDouble; import parser.type.TypeDouble;
import prism.DA; import prism.DA;
import prism.Pair;
import prism.PrismComponent; import prism.PrismComponent;
import prism.PrismException; import prism.PrismException;
import prism.PrismFileLog; import prism.PrismFileLog;
@ -66,7 +65,7 @@ public class DTMCModelChecker extends ProbModelChecker
StateValues probsProduct, probs; StateValues probsProduct, probs;
Expression ltl; Expression ltl;
DA<BitSet,AcceptanceRabin> dra; DA<BitSet,AcceptanceRabin> dra;
Model modelProduct;
LTLModelChecker.LTLProduct<DTMC> product;
DTMCModelChecker mcProduct; DTMCModelChecker mcProduct;
long time; long time;
@ -86,7 +85,6 @@ public class DTMCModelChecker extends ProbModelChecker
mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
time = System.currentTimeMillis(); time = System.currentTimeMillis();
dra = LTLModelChecker.convertLTLFormulaToDRA(ltl); dra = LTLModelChecker.convertLTLFormulaToDRA(ltl);
int draSize = dra.size();
mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + "."); mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + ".");
time = System.currentTimeMillis() - time; time = System.currentTimeMillis() - time;
mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds."); mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds.");
@ -101,31 +99,19 @@ public class DTMCModelChecker extends ProbModelChecker
// Build product of Markov chain and automaton // Build product of Markov chain and automaton
mainLog.println("\nConstructing MC-DRA product..."); mainLog.println("\nConstructing MC-DRA product...");
Pair<Model, int[]> pair = mcLtl.constructProductMC(dra, (DTMC) model, labelBS, statesOfInterest);
modelProduct = pair.first;
int invMap[] = pair.second;
mainLog.print("\n" + modelProduct.infoStringTable());
product = mcLtl.constructProductMC(dra, (DTMC) model, labelBS, statesOfInterest);
mainLog.print("\n" + product.getProductModel().infoStringTable());
// Find accepting BSCCs + compute reachability probabilities // Find accepting BSCCs + compute reachability probabilities
mainLog.println("\nFinding accepting BSCCs..."); mainLog.println("\nFinding accepting BSCCs...");
BitSet acceptingBSCCs = mcLtl.findAcceptingBSCCsForRabin(dra, modelProduct, invMap);
BitSet acceptingBSCCs = mcLtl.findAcceptingBSCCsForRabin(product.getProductModel(), product.getAcceptance());
mainLog.println("\nComputing reachability probabilities..."); mainLog.println("\nComputing reachability probabilities...");
mcProduct = new DTMCModelChecker(this); mcProduct = new DTMCModelChecker(this);
mcProduct.inheritSettings(this); mcProduct.inheritSettings(this);
probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((DTMC) modelProduct, acceptingBSCCs).soln, modelProduct);
probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs(product.getProductModel(), acceptingBSCCs).soln, product.getProductModel());
// Mapping probabilities in the original model // Mapping probabilities in the original model
double[] probsProductDbl = probsProduct.getDoubleArray();
double[] probsDbl = new double[model.getNumStates()];
// Get the probabilities for the original model by taking the initial states
// of the product and projecting back to the states of the original model
for (int i : modelProduct.getInitialStates()) {
int s = invMap[i] / draSize;
probsDbl[s] = probsProductDbl[i];
}
probs = StateValues.createFromDoubleArray(probsDbl, model);
probs = product.projectToOriginalModel(probsProduct);
probsProduct.clear(); probsProduct.clear();
return probs; return probs;

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

@ -4,6 +4,7 @@
// Authors: // Authors:
// * Alessandro Bruni <albr@dtu.dk> (Technical University of Denmark) // * Alessandro Bruni <albr@dtu.dk> (Technical University of Denmark)
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford) // * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
// * Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
// //
//------------------------------------------------------------------------------ //------------------------------------------------------------------------------
// //
@ -47,7 +48,6 @@ import parser.type.TypeBool;
import parser.type.TypePathBool; import parser.type.TypePathBool;
import prism.DA; import prism.DA;
import prism.LTL2RabinLibrary; import prism.LTL2RabinLibrary;
import prism.Pair;
import prism.PrismComponent; import prism.PrismComponent;
import prism.PrismException; import prism.PrismException;
@ -56,6 +56,38 @@ import prism.PrismException;
*/ */
public class LTLModelChecker extends PrismComponent public class LTLModelChecker extends PrismComponent
{ {
/** Make LTL product accessible as a Product */
public class LTLProduct<M extends Model> extends Product<M> {
private int draSize;
private int invMap[];
private AcceptanceRabin acceptance;
public LTLProduct(M productModel, M originalModel, AcceptanceRabin acceptance, int draSize, int[] invMap)
{
super(productModel, originalModel);
this.draSize = draSize;
this.invMap = invMap;
this.acceptance = acceptance;
}
@Override
public int getModelState(int productState)
{
return invMap[productState] / draSize;
}
@Override
public int getAutomatonState(int productState)
{
return invMap[productState] % draSize;
}
public AcceptanceRabin getAcceptance() {
return acceptance;
}
}
/** /**
* Create a new LTLModelChecker, inherit basic state from parent (unless null). * Create a new LTLModelChecker, inherit basic state from parent (unless null).
*/ */
@ -133,9 +165,9 @@ public class LTLModelChecker extends PrismComponent
* @param dtmc The DTMC * @param dtmc The DTMC
* @param labelBS BitSets giving the set of states for each AP in the DRA * @param labelBS BitSets giving the set of states for each AP in the DRA
* @param statesOfInterest the set of states for which values should be calculated (null = all states) * @param statesOfInterest the set of states for which values should be calculated (null = all states)
* @return The product DTMC and a list of each of its states (s,q), encoded as (s * draSize + q)
* @return The product DTMC
*/ */
public Pair<Model, int[]> constructProductMC(DA<BitSet,AcceptanceRabin> dra, DTMC dtmc, Vector<BitSet> labelBS, BitSet statesOfInterest) throws PrismException
public LTLProduct<DTMC> constructProductMC(DA<BitSet,AcceptanceRabin> dra, DTMC dtmc, Vector<BitSet> labelBS, BitSet statesOfInterest) throws PrismException
{ {
DTMCSimple prodModel = new DTMCSimple(); DTMCSimple prodModel = new DTMCSimple();
@ -145,6 +177,7 @@ public class LTLModelChecker extends PrismComponent
int prodNumStates = modelNumStates * draSize; int prodNumStates = modelNumStates * draSize;
int s_1, s_2, q_1, q_2; int s_1, s_2, q_1, q_2;
BitSet s_labels = new BitSet(numAPs); BitSet s_labels = new BitSet(numAPs);
AcceptanceRabin prodAcceptance;
// Encoding: // Encoding:
// each state s' = <s, q> = s * draSize + q // each state s' = <s, q> = s * draSize + q
@ -215,7 +248,18 @@ public class LTLModelChecker extends PrismComponent
prodModel.findDeadlocks(false); prodModel.findDeadlocks(false);
return new Pair<Model, int[]>(prodModel, invMap);
prodAcceptance = new AcceptanceRabin();
LTLProduct<DTMC> product = new LTLProduct<DTMC>(prodModel, dtmc, prodAcceptance, draSize, invMap);
// generate acceptance for the product model by lifting
for (AcceptanceRabin.RabinPair pair : dra.getAcceptance()) {
BitSet Lprod = product.liftFromAutomaton(pair.getL());
BitSet Kprod = product.liftFromAutomaton(pair.getK());
prodAcceptance.add(new AcceptanceRabin.RabinPair(Lprod, Kprod));
}
return product;
} }
/** /**
@ -224,9 +268,9 @@ public class LTLModelChecker extends PrismComponent
* @param mdp The MDP * @param mdp The MDP
* @param labelBS BitSets giving the set of states for each AP in the DRA * @param labelBS BitSets giving the set of states for each AP in the DRA
* @param statesOfInterest the set of states for which values should be calculated (null = all states) * @param statesOfInterest the set of states for which values should be calculated (null = all states)
* @return The product MDP and a list of each of its states (s,q), encoded as (s * draSize + q)
* @return The product MDP
*/ */
public Pair<NondetModel, int[]> constructProductMDP(DA<BitSet,AcceptanceRabin> dra, MDP mdp, Vector<BitSet> labelBS, BitSet statesOfInterest) throws PrismException
public LTLProduct<MDP> constructProductMDP(DA<BitSet,AcceptanceRabin> dra, MDP mdp, Vector<BitSet> labelBS, BitSet statesOfInterest) throws PrismException
{ {
MDPSimple prodModel = new MDPSimple(); MDPSimple prodModel = new MDPSimple();
@ -236,6 +280,7 @@ public class LTLModelChecker extends PrismComponent
int prodNumStates = modelNumStates * draSize; int prodNumStates = modelNumStates * draSize;
int s_1, s_2, q_1, q_2; int s_1, s_2, q_1, q_2;
BitSet s_labels = new BitSet(numAPs); BitSet s_labels = new BitSet(numAPs);
AcceptanceRabin prodAcceptance;
// Encoding: // Encoding:
// each state s' = <s, q> = s * draSize + q // each state s' = <s, q> = s * draSize + q
@ -311,45 +356,38 @@ public class LTLModelChecker extends PrismComponent
prodModel.findDeadlocks(false); prodModel.findDeadlocks(false);
return new Pair<NondetModel, int[]>(prodModel, invMap);
prodAcceptance = new AcceptanceRabin();
LTLProduct<MDP> product = new LTLProduct<MDP>(prodModel, mdp, prodAcceptance, draSize, invMap);
// generate acceptance for the product model by lifting
for (AcceptanceRabin.RabinPair pair : dra.getAcceptance()) {
BitSet Lprod = product.liftFromAutomaton(pair.getL());
BitSet Kprod = product.liftFromAutomaton(pair.getK());
prodAcceptance.add(new AcceptanceRabin.RabinPair(Lprod, Kprod));
}
return product;
} }
/** /**
* Find the set of states belong to accepting BSCCs in a model wrt a Rabin acceptance condition. * Find the set of states belong to accepting BSCCs in a model wrt a Rabin acceptance condition.
* @param dra The DRA
* @param model The model * @param model The model
* @param invMap The map returned by the constructProduct method(s)
* @param acceptance The Rabin acceptance condition
*/ */
public BitSet findAcceptingBSCCsForRabin(DA<BitSet,AcceptanceRabin> dra, Model model, int invMap[]) throws PrismException
public BitSet findAcceptingBSCCsForRabin(Model model, AcceptanceRabin acceptance) throws PrismException
{ {
// Compute bottom strongly connected components (BSCCs) // Compute bottom strongly connected components (BSCCs)
SCCComputer sccComputer = SCCComputer.createSCCComputer(this, model); SCCComputer sccComputer = SCCComputer.createSCCComputer(this, model);
sccComputer.computeBSCCs(); sccComputer.computeBSCCs();
List<BitSet> bsccs = sccComputer.getBSCCs(); List<BitSet> bsccs = sccComputer.getBSCCs();
int draSize = dra.size();
int numAcceptancePairs = dra.getAcceptance().size();
BitSet result = new BitSet(); BitSet result = new BitSet();
for (BitSet bscc : bsccs) { for (BitSet bscc : bsccs) {
for (int acceptancePair = 0; acceptancePair < numAcceptancePairs; acceptancePair++) {
// accepting for L,K <=> BSCC does not intersect L but does intersect K
boolean isLEmpty = true;
boolean isKEmpty = true;
BitSet L = dra.getAcceptance().get(acceptancePair).getL();
BitSet K = dra.getAcceptance().get(acceptancePair).getK();
for (int state = bscc.nextSetBit(0); state != -1; state = bscc.nextSetBit(state + 1)) {
int draState = invMap[state] % draSize;
isLEmpty &= !L.get(draState);
isKEmpty &= !K.get(draState);
}
if (isLEmpty && !isKEmpty) {
// this BSCC is accepting
result.or(bscc);
// we do not have to consider the other acceptance pairs, continue with next BSCC
break;
}
if (acceptance.isBSCCAccepting(bscc)) {
// this BSCC is accepting
result.or(bscc);
} }
} }
@ -358,23 +396,21 @@ public class LTLModelChecker extends PrismComponent
/** /**
* Find the set of states in accepting end components (ECs) in a nondeterministic model wrt a Rabin acceptance condition. * Find the set of states in accepting end components (ECs) in a nondeterministic model wrt a Rabin acceptance condition.
* @param dra The DRA
* @param model The model * @param model The model
* @param invMap The map returned by the constructProduct method(s)
* @param acceptance the acceptance condition
*/ */
public BitSet findAcceptingECStatesForRabin(DA<BitSet,AcceptanceRabin> dra, NondetModel model, int invMap[]) throws PrismException
public BitSet findAcceptingECStatesForRabin(NondetModel model, AcceptanceRabin acceptance) throws PrismException
{ {
BitSet allAcceptingStates = new BitSet(); BitSet allAcceptingStates = new BitSet();
int numStates = model.getNumStates(); int numStates = model.getNumStates();
int draSize = dra.size();
// Go through the DRA acceptance pairs (L_i, K_i) // Go through the DRA acceptance pairs (L_i, K_i)
for (int i = 0; i < dra.getAcceptance().size(); i++) {
for (int i = 0; i < acceptance.size(); i++) {
// Find model states *not* satisfying L_i // Find model states *not* satisfying L_i
BitSet bitsetLi = dra.getAcceptance().get(i).getL();
BitSet bitsetLi = acceptance.get(i).getL();
BitSet statesLi_not = new BitSet(); BitSet statesLi_not = new BitSet();
for (int s = 0; s < numStates; s++) { for (int s = 0; s < numStates; s++) {
if (!bitsetLi.get(invMap[s] % draSize)) {
if (!bitsetLi.get(s)) {
statesLi_not.set(s); statesLi_not.set(s);
} }
} }
@ -386,13 +422,10 @@ public class LTLModelChecker extends PrismComponent
ecComputer.computeMECStates(statesLi_not); ecComputer.computeMECStates(statesLi_not);
List<BitSet> mecs = ecComputer.getMECStates(); List<BitSet> mecs = ecComputer.getMECStates();
// Check with MECs contain a K_i state // Check with MECs contain a K_i state
BitSet bitsetKi = dra.getAcceptance().get(i).getK();
BitSet bitsetKi = acceptance.get(i).getK();
for (BitSet mec : mecs) { for (BitSet mec : mecs) {
for (int s = mec.nextSetBit(0); s != -1; s = mec.nextSetBit(s + 1)) {
if (bitsetKi.get(invMap[s] % draSize)) {
allAcceptingStates.or(mec);
break;
}
if (mec.intersects(bitsetKi)) {
allAcceptingStates.or(mec);
} }
} }
} }

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

@ -35,7 +35,6 @@ import java.util.Vector;
import acceptance.AcceptanceRabin; import acceptance.AcceptanceRabin;
import parser.ast.Expression; import parser.ast.Expression;
import prism.DA; import prism.DA;
import prism.Pair;
import prism.PrismComponent; import prism.PrismComponent;
import prism.PrismDevNullLog; import prism.PrismDevNullLog;
import prism.PrismException; import prism.PrismException;
@ -69,7 +68,6 @@ public class MDPModelChecker extends ProbModelChecker
StateValues probsProduct, probs; StateValues probsProduct, probs;
Expression ltl; Expression ltl;
DA<BitSet,AcceptanceRabin> dra; DA<BitSet,AcceptanceRabin> dra;
NondetModel modelProduct;
MDPModelChecker mcProduct; MDPModelChecker mcProduct;
long time; long time;
@ -94,7 +92,6 @@ public class MDPModelChecker extends ProbModelChecker
mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
time = System.currentTimeMillis(); time = System.currentTimeMillis();
dra = LTLModelChecker.convertLTLFormulaToDRA(ltl); dra = LTLModelChecker.convertLTLFormulaToDRA(ltl);
int draSize = dra.size();
mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + "."); mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + ".");
time = System.currentTimeMillis() - time; time = System.currentTimeMillis() - time;
mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds."); mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds.");
@ -109,17 +106,15 @@ public class MDPModelChecker extends ProbModelChecker
// Build product of MDP and automaton // Build product of MDP and automaton
mainLog.println("\nConstructing MDP-DRA product..."); mainLog.println("\nConstructing MDP-DRA product...");
Pair<NondetModel, int[]> pair = mcLtl.constructProductMDP(dra, (MDP) model, labelBS, statesOfInterest);
modelProduct = pair.first;
int invMap[] = pair.second;
LTLModelChecker.LTLProduct<MDP> product = mcLtl.constructProductMDP(dra, (MDP) model, labelBS, statesOfInterest);
// Find accepting MECs + compute reachability probabilities // Find accepting MECs + compute reachability probabilities
mainLog.println("\nFinding accepting MECs..."); mainLog.println("\nFinding accepting MECs...");
BitSet acceptingMECs = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, invMap);
BitSet acceptingMECs = mcLtl.findAcceptingECStatesForRabin(product.getProductModel(), product.getAcceptance());
mainLog.println("\nComputing reachability probabilities..."); mainLog.println("\nComputing reachability probabilities...");
mcProduct = new MDPModelChecker(this); mcProduct = new MDPModelChecker(this);
mcProduct.inheritSettings(this); mcProduct.inheritSettings(this);
probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((MDP) modelProduct, acceptingMECs, false).soln, modelProduct);
probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((MDP)product.getProductModel(), acceptingMECs, false).soln, product.getProductModel());
// Subtract from 1 if we're model checking a negated formula for regular Pmin // Subtract from 1 if we're model checking a negated formula for regular Pmin
if (minMax.isMin()) { if (minMax.isMin()) {
@ -128,17 +123,7 @@ public class MDPModelChecker extends ProbModelChecker
} }
// Mapping probabilities in the original model // Mapping probabilities in the original model
double[] probsProductDbl = probsProduct.getDoubleArray();
double[] probsDbl = new double[model.getNumStates()];
// Get the probabilities for the original model by taking the initial states
// of the product and projecting back to the states of the original model
for (int i : modelProduct.getInitialStates()) {
int s = invMap[i] / draSize;
probsDbl[s] = probsProductDbl[i];
}
probs = StateValues.createFromDoubleArray(probsDbl, model);
probs = product.projectToOriginalModel(probsProduct);
probsProduct.clear(); probsProduct.clear();
return probs; return probs;

Write Preview
Loading…
Cancel
Save