diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 793205a1..6c09e4fe 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -36,7 +36,6 @@ import acceptance.AcceptanceRabin; import parser.ast.Expression; import parser.type.TypeDouble; import prism.DA; -import prism.Pair; import prism.PrismComponent; import prism.PrismException; import prism.PrismFileLog; @@ -66,7 +65,7 @@ public class DTMCModelChecker extends ProbModelChecker StateValues probsProduct, probs; Expression ltl; DA dra; - Model modelProduct; + LTLModelChecker.LTLProduct product; DTMCModelChecker mcProduct; long time; @@ -86,7 +85,6 @@ public class DTMCModelChecker extends ProbModelChecker mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); time = System.currentTimeMillis(); dra = LTLModelChecker.convertLTLFormulaToDRA(ltl); - int draSize = dra.size(); mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + "."); time = System.currentTimeMillis() - time; 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 mainLog.println("\nConstructing MC-DRA product..."); - Pair 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 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..."); mcProduct = new DTMCModelChecker(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 - 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(); return probs; diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 20b3745c..2ee9a446 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -4,6 +4,7 @@ // Authors: // * Alessandro Bruni (Technical University of Denmark) // * Dave Parker (University of Oxford) +// * Joachim Klein (TU Dresden) // //------------------------------------------------------------------------------ // @@ -47,7 +48,6 @@ import parser.type.TypeBool; import parser.type.TypePathBool; import prism.DA; import prism.LTL2RabinLibrary; -import prism.Pair; import prism.PrismComponent; import prism.PrismException; @@ -56,6 +56,38 @@ import prism.PrismException; */ public class LTLModelChecker extends PrismComponent { + /** Make LTL product accessible as a Product */ + public class LTLProduct extends Product { + 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). */ @@ -133,9 +165,9 @@ public class LTLModelChecker extends PrismComponent * @param dtmc The DTMC * @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) - * @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 constructProductMC(DA dra, DTMC dtmc, Vector labelBS, BitSet statesOfInterest) throws PrismException + public LTLProduct constructProductMC(DA dra, DTMC dtmc, Vector labelBS, BitSet statesOfInterest) throws PrismException { DTMCSimple prodModel = new DTMCSimple(); @@ -145,6 +177,7 @@ public class LTLModelChecker extends PrismComponent int prodNumStates = modelNumStates * draSize; int s_1, s_2, q_1, q_2; BitSet s_labels = new BitSet(numAPs); + AcceptanceRabin prodAcceptance; // Encoding: // each state s' = = s * draSize + q @@ -215,7 +248,18 @@ public class LTLModelChecker extends PrismComponent prodModel.findDeadlocks(false); - return new Pair(prodModel, invMap); + prodAcceptance = new AcceptanceRabin(); + LTLProduct product = new LTLProduct(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 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) - * @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 constructProductMDP(DA dra, MDP mdp, Vector labelBS, BitSet statesOfInterest) throws PrismException + public LTLProduct constructProductMDP(DA dra, MDP mdp, Vector labelBS, BitSet statesOfInterest) throws PrismException { MDPSimple prodModel = new MDPSimple(); @@ -236,6 +280,7 @@ public class LTLModelChecker extends PrismComponent int prodNumStates = modelNumStates * draSize; int s_1, s_2, q_1, q_2; BitSet s_labels = new BitSet(numAPs); + AcceptanceRabin prodAcceptance; // Encoding: // each state s' = = s * draSize + q @@ -311,45 +356,38 @@ public class LTLModelChecker extends PrismComponent prodModel.findDeadlocks(false); - return new Pair(prodModel, invMap); + prodAcceptance = new AcceptanceRabin(); + LTLProduct product = new LTLProduct(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. - * @param dra The DRA * @param model The model - * @param invMap The map returned by the constructProduct method(s) + * @param acceptance The Rabin acceptance condition */ - public BitSet findAcceptingBSCCsForRabin(DA dra, Model model, int invMap[]) throws PrismException + public BitSet findAcceptingBSCCsForRabin(Model model, AcceptanceRabin acceptance) throws PrismException { // Compute bottom strongly connected components (BSCCs) SCCComputer sccComputer = SCCComputer.createSCCComputer(this, model); sccComputer.computeBSCCs(); List bsccs = sccComputer.getBSCCs(); - int draSize = dra.size(); - int numAcceptancePairs = dra.getAcceptance().size(); BitSet result = new BitSet(); 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. - * @param dra The DRA * @param model The model - * @param invMap The map returned by the constructProduct method(s) + * @param acceptance the acceptance condition */ - public BitSet findAcceptingECStatesForRabin(DA dra, NondetModel model, int invMap[]) throws PrismException + public BitSet findAcceptingECStatesForRabin(NondetModel model, AcceptanceRabin acceptance) throws PrismException { BitSet allAcceptingStates = new BitSet(); int numStates = model.getNumStates(); - int draSize = dra.size(); // 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 - BitSet bitsetLi = dra.getAcceptance().get(i).getL(); + BitSet bitsetLi = acceptance.get(i).getL(); BitSet statesLi_not = new BitSet(); for (int s = 0; s < numStates; s++) { - if (!bitsetLi.get(invMap[s] % draSize)) { + if (!bitsetLi.get(s)) { statesLi_not.set(s); } } @@ -386,13 +422,10 @@ public class LTLModelChecker extends PrismComponent ecComputer.computeMECStates(statesLi_not); List mecs = ecComputer.getMECStates(); // 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 (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); } } } diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 2d4f2343..660c4e08 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -35,7 +35,6 @@ import java.util.Vector; import acceptance.AcceptanceRabin; import parser.ast.Expression; import prism.DA; -import prism.Pair; import prism.PrismComponent; import prism.PrismDevNullLog; import prism.PrismException; @@ -69,7 +68,6 @@ public class MDPModelChecker extends ProbModelChecker StateValues probsProduct, probs; Expression ltl; DA dra; - NondetModel modelProduct; MDPModelChecker mcProduct; long time; @@ -94,7 +92,6 @@ public class MDPModelChecker extends ProbModelChecker mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); time = System.currentTimeMillis(); dra = LTLModelChecker.convertLTLFormulaToDRA(ltl); - int draSize = dra.size(); mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + "."); time = System.currentTimeMillis() - time; 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 mainLog.println("\nConstructing MDP-DRA product..."); - Pair pair = mcLtl.constructProductMDP(dra, (MDP) model, labelBS, statesOfInterest); - modelProduct = pair.first; - int invMap[] = pair.second; + LTLModelChecker.LTLProduct product = mcLtl.constructProductMDP(dra, (MDP) model, labelBS, statesOfInterest); // Find accepting MECs + compute reachability probabilities 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..."); mcProduct = new MDPModelChecker(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 if (minMax.isMin()) { @@ -128,17 +123,7 @@ public class MDPModelChecker extends ProbModelChecker } // 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(); return probs;