diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 667c8366..5b138988 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -31,6 +31,7 @@ import java.util.BitSet; import java.util.List; import java.util.Map; +import acceptance.AcceptanceType; import parser.ast.Expression; import parser.type.TypeDouble; import prism.PrismComponent; @@ -65,11 +66,12 @@ public class DTMCModelChecker extends ProbModelChecker mcLtl = new LTLModelChecker(this); // Build product of Markov chain and automaton - product = mcLtl.constructProductMC(this, (DTMC)model, expr, statesOfInterest); + AcceptanceType[] allowedAcceptance = {AcceptanceType.RABIN}; + product = mcLtl.constructProductMC(this, (DTMC)model, expr, statesOfInterest, allowedAcceptance); // Find accepting BSCCs + compute reachability probabilities mainLog.println("\nFinding accepting BSCCs..."); - BitSet acceptingBSCCs = mcLtl.findAcceptingBSCCsForRabin(product.getProductModel(), product.getAcceptance()); + BitSet acceptingBSCCs = mcLtl.findAcceptingBSCCs(product.getProductModel(), product.getAcceptance()); mainLog.println("\nComputing reachability probabilities..."); mcProduct = new DTMCModelChecker(this); mcProduct.inheritSettings(this); diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index c2ad1668..5116374a 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -38,7 +38,9 @@ import java.util.List; import java.util.Map; import java.util.Vector; +import acceptance.AcceptanceOmega; import acceptance.AcceptanceRabin; +import acceptance.AcceptanceType; import common.IterableStateSet; import parser.State; import parser.ast.Expression; @@ -64,14 +66,14 @@ public class LTLModelChecker extends PrismComponent { /** Make LTL product accessible as a Product */ public class LTLProduct extends Product { - private int draSize; + private int daSize; private int invMap[]; - private AcceptanceRabin acceptance; + private AcceptanceOmega acceptance; - public LTLProduct(M productModel, M originalModel, AcceptanceRabin acceptance, int draSize, int[] invMap) + public LTLProduct(M productModel, M originalModel, AcceptanceOmega acceptance, int daSize, int[] invMap) { super(productModel, originalModel); - this.draSize = draSize; + this.daSize = daSize; this.invMap = invMap; this.acceptance = acceptance; } @@ -79,18 +81,22 @@ public class LTLModelChecker extends PrismComponent @Override public int getModelState(int productState) { - return invMap[productState] / draSize; + return invMap[productState] / daSize; } @Override public int getAutomatonState(int productState) { - return invMap[productState] % draSize; + return invMap[productState] % daSize; } - public AcceptanceRabin getAcceptance() { + public AcceptanceOmega getAcceptance() { return acceptance; } + + public void setAcceptance(AcceptanceOmega acceptance) { + this.acceptance = acceptance; + } } @@ -180,18 +186,19 @@ public class LTLModelChecker extends PrismComponent } /** - * Generate the DRA for the given LTL expression and construct the product. + * Generate a deterministic automaton for the given LTL expression and construct the product. * * @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) - * @return the product with the DRA + * @param allowedAcceptance the allowed acceptance types + * @return the product with the DA */ - public LTLProduct constructProductMC(ProbModelChecker mc, DTMC dtmc, Expression expr, BitSet statesOfInterest) throws PrismException + public LTLProduct constructProductMC(ProbModelChecker mc, DTMC dtmc, Expression expr, BitSet statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException { Expression ltl; - DA dra; + DA da; LTLProduct product; long time; @@ -218,26 +225,27 @@ public class LTLModelChecker extends PrismComponent Vector labelBS = new Vector(); ltl = checkMaximalStateFormulas(mc, dtmc, expr.deepCopy(), labelBS); - // Convert LTL formula to deterministic Rabin automaton (DRA) - mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); + // Convert LTL formula to deterministic automaton + mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")..."); time = System.currentTimeMillis(); LTL2DA ltl2da = new LTL2DA(this); - dra = ltl2da.convertLTLFormulaToDRA(ltl, mc.getConstantValues()); - mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + "."); + 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 Rabin translation: " + time / 1000.0 + " seconds."); + mainLog.println("Time for "+da.getAutomataType()+" translation: " + time / 1000.0 + " seconds."); // If required, export DRA if (settings.getExportPropAut()) { mainLog.println("Exporting DRA to file \"" + settings.getExportPropAutFilename() + "\"..."); PrismLog out = new PrismFileLog(settings.getExportPropAutFilename()); - out.println(dra); + out.println(da); out.close(); //dra.printDot(new java.io.PrintStream("dra.dot")); } + // Build product of Markov chain and automaton - mainLog.println("\nConstructing MC-DRA product..."); - product = constructProductMC(dra, dtmc, labelBS, statesOfInterest); + mainLog.println("\nConstructing MC-"+da.getAutomataType()+" product..."); + product = constructProductMC(da, dtmc, labelBS, statesOfInterest); mainLog.print("\n" + product.getProductModel().infoStringTable()); @@ -245,30 +253,29 @@ public class LTLModelChecker extends PrismComponent } /** - * Construct the product of a DRA and a DTMC. - * @param dra The DRA + * Construct the product of a DA and a DTMC. + * @param dra The DA * @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 DA * @param statesOfInterest the set of states for which values should be calculated (null = all states) * @return The product DTMC */ - public LTLProduct constructProductMC(DA dra, DTMC dtmc, Vector labelBS, BitSet statesOfInterest) throws PrismException + public LTLProduct constructProductMC(DA da, DTMC dtmc, Vector labelBS, BitSet statesOfInterest) throws PrismException { DTMCSimple prodModel = new DTMCSimple(); - int draSize = dra.size(); - int numAPs = dra.getAPList().size(); + int daSize = da.size(); + int numAPs = da.getAPList().size(); int modelNumStates = dtmc.getNumStates(); - int prodNumStates = modelNumStates * draSize; + int prodNumStates = modelNumStates * daSize; int s_1, s_2, q_1, q_2; BitSet s_labels = new BitSet(numAPs); - AcceptanceRabin prodAcceptance; List prodStatesList = null; // Encoding: - // each state s' = = s * draSize + q - // s(s') = s' / draSize - // q(s') = s' % draSize + // each state s' = = s * daSize + q + // s(s') = s' / daSize + // q(s') = s' % daSize LinkedList queue = new LinkedList(); int map[] = new int[prodNumStates]; @@ -287,15 +294,15 @@ public class LTLModelChecker extends PrismComponent for (int s_0 : new IterableStateSet(statesOfInterest, dtmc.getNumStates())) { // Get BitSet representing APs (labels) satisfied by state s_0 for (int k = 0; k < numAPs; k++) { - s_labels.set(k, labelBS.get(Integer.parseInt(dra.getAPList().get(k).substring(1))).get(s_0)); + s_labels.set(k, labelBS.get(Integer.parseInt(da.getAPList().get(k).substring(1))).get(s_0)); } - // Find corresponding initial state in DRA - int q_0 = dra.getEdgeDestByLabel(dra.getStartState(), s_labels); + // Find corresponding initial state in DA + int q_0 = da.getEdgeDestByLabel(da.getStartState(), s_labels); // Add (initial) state to product queue.add(new Point(s_0, q_0)); prodModel.addState(); prodModel.addInitialState(prodModel.getNumStates() - 1); - map[s_0 * draSize + q_0] = prodModel.getNumStates() - 1; + map[s_0 * daSize + q_0] = prodModel.getNumStates() - 1; if (prodStatesList != null) { // store DTMC state information for the product state prodStatesList.add(dtmc.getStatesList().get(s_0)); @@ -308,7 +315,7 @@ public class LTLModelChecker extends PrismComponent Point p = queue.pop(); s_1 = p.x; q_1 = p.y; - visited.set(s_1 * draSize + q_1); + visited.set(s_1 * daSize + q_1); // Go through transitions from state s_1 in original DTMC Iterator> iter = dtmc.getTransitionsIterator(s_1); @@ -318,21 +325,21 @@ public class LTLModelChecker extends PrismComponent double prob = e.getValue(); // Get BitSet representing APs (labels) satisfied by successor state s_2 for (int k = 0; k < numAPs; k++) { - s_labels.set(k, labelBS.get(Integer.parseInt(dra.getAPList().get(k).substring(1))).get(s_2)); + s_labels.set(k, labelBS.get(Integer.parseInt(da.getAPList().get(k).substring(1))).get(s_2)); } // Find corresponding successor in DRA - q_2 = dra.getEdgeDestByLabel(q_1, s_labels); + q_2 = da.getEdgeDestByLabel(q_1, s_labels); // Add state/transition to model - if (!visited.get(s_2 * draSize + q_2) && map[s_2 * draSize + q_2] == -1) { + if (!visited.get(s_2 * daSize + q_2) && map[s_2 * daSize + q_2] == -1) { queue.add(new Point(s_2, q_2)); prodModel.addState(); - map[s_2 * draSize + q_2] = prodModel.getNumStates() - 1; + map[s_2 * daSize + q_2] = prodModel.getNumStates() - 1; if (prodStatesList != null) { // store DTMC state information for the product state prodStatesList.add(dtmc.getStatesList().get(s_2)); } } - prodModel.setProbability(map[s_1 * draSize + q_1], map[s_2 * draSize + q_2], prob); + prodModel.setProbability(map[s_1 * daSize + q_1], map[s_2 * daSize + q_2], prob); } } @@ -350,15 +357,10 @@ public class LTLModelChecker extends PrismComponent prodModel.setStatesList(prodStatesList); } - prodAcceptance = new AcceptanceRabin(); - LTLProduct product = new LTLProduct(prodModel, dtmc, prodAcceptance, draSize, invMap); + LTLProduct product = new LTLProduct(prodModel, dtmc, null, daSize, 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)); - } + product.setAcceptance(liftAcceptance(product, da.getAcceptance())); // lift the labels for (String label : dtmc.getLabels()) { @@ -369,18 +371,20 @@ public class LTLModelChecker extends PrismComponent return product; } /** - * Generate the DRA for the given LTL expression and construct the product. + * Generate the DA for the given LTL expression and construct the product. * * @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) - * @return the product with the DRA + * @param statesOfInterest the set of states for which values should be calculated (null = all states) + * @param allowedAcceptance the allowed acceptance conditions + * @return the product with the DA + * @throws PrismException */ - public LTLProduct constructProductMDP(ProbModelChecker mc, MDP model, Expression expr, BitSet statesOfInterest) throws PrismException + public LTLProduct constructProductMDP(ProbModelChecker mc, MDP model, Expression expr, BitSet statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException { Expression ltl; - DA dra; + DA da; LTLProduct product; long time; @@ -407,26 +411,26 @@ public class LTLModelChecker extends PrismComponent Vector labelBS = new Vector(); ltl = checkMaximalStateFormulas(mc, model, expr.deepCopy(), labelBS); - // Convert LTL formula to deterministic Rabin automaton (DRA) - mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); + // Convert LTL formula to deterministic automaton + mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")..."); time = System.currentTimeMillis(); LTL2DA ltl2da = new LTL2DA(this); - dra = ltl2da.convertLTLFormulaToDRA(ltl, mc.getConstantValues()); - mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + "."); + 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 Rabin translation: " + time / 1000.0 + " seconds."); - // If required, export DRA + mainLog.println("Time for "+da.getAutomataType()+" translation: " + time / 1000.0 + " seconds."); + // 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(dra); + out.println(da); out.close(); - //dra.printDot(new java.io.PrintStream("dra.dot")); + //da.printDot(new java.io.PrintStream("da.dot")); } // Build product of MDP and automaton - mainLog.println("\nConstructing MDP-DRA product..."); - product = constructProductMDP(dra, (MDP) model, labelBS, statesOfInterest); + mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product..."); + product = constructProductMDP(da, model, labelBS, statesOfInterest); mainLog.print("\n" + product.getProductModel().infoStringTable()); @@ -434,24 +438,23 @@ public class LTLModelChecker extends PrismComponent } /** - * Construct the product of a DRA and an MDP. - * @param dra The DRA + * Construct the product of a DA and an MDP. + * @param da The DA * @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 DA * @param statesOfInterest the set of states for which values should be calculated (null = all states) * @return The product MDP */ - public LTLProduct constructProductMDP(DA dra, MDP mdp, Vector labelBS, BitSet statesOfInterest) throws PrismException + public LTLProduct constructProductMDP(DA da, MDP mdp, Vector labelBS, BitSet statesOfInterest) throws PrismException { MDPSimple prodModel = new MDPSimple(); - int draSize = dra.size(); - int numAPs = dra.getAPList().size(); + int daSize = da.size(); + int numAPs = da.getAPList().size(); int modelNumStates = mdp.getNumStates(); - int prodNumStates = modelNumStates * draSize; + int prodNumStates = modelNumStates * daSize; int s_1, s_2, q_1, q_2; BitSet s_labels = new BitSet(numAPs); - AcceptanceRabin prodAcceptance; List prodStatesList = null; @@ -477,15 +480,15 @@ public class LTLModelChecker extends PrismComponent for (int s_0 : new IterableStateSet(statesOfInterest, mdp.getNumStates())) { // Get BitSet representing APs (labels) satisfied by state s_0 for (int k = 0; k < numAPs; k++) { - s_labels.set(k, labelBS.get(Integer.parseInt(dra.getAPList().get(k).substring(1))).get(s_0)); + s_labels.set(k, labelBS.get(Integer.parseInt(da.getAPList().get(k).substring(1))).get(s_0)); } // Find corresponding initial state in DRA - int q_0 = dra.getEdgeDestByLabel(dra.getStartState(), s_labels); + int q_0 = da.getEdgeDestByLabel(da.getStartState(), s_labels); // Add (initial) state to product queue.add(new Point(s_0, q_0)); prodModel.addState(); prodModel.addInitialState(prodModel.getNumStates() - 1); - map[s_0 * draSize + q_0] = prodModel.getNumStates() - 1; + map[s_0 * daSize + q_0] = prodModel.getNumStates() - 1; if (prodStatesList != null) { // store MDP state information for the product state prodStatesList.add(mdp.getStatesList().get(s_0)); @@ -498,7 +501,7 @@ public class LTLModelChecker extends PrismComponent Point p = queue.pop(); s_1 = p.x; q_1 = p.y; - visited.set(s_1 * draSize + q_1); + visited.set(s_1 * daSize + q_1); // Go through transitions from state s_1 in original DTMC int numChoices = mdp.getNumChoices(s_1); @@ -511,23 +514,23 @@ public class LTLModelChecker extends PrismComponent double prob = e.getValue(); // Get BitSet representing APs (labels) satisfied by successor state s_2 for (int k = 0; k < numAPs; k++) { - s_labels.set(k, labelBS.get(Integer.parseInt(dra.getAPList().get(k).substring(1))).get(s_2)); + s_labels.set(k, labelBS.get(Integer.parseInt(da.getAPList().get(k).substring(1))).get(s_2)); } // Find corresponding successor in DRA - q_2 = dra.getEdgeDestByLabel(q_1, s_labels); + q_2 = da.getEdgeDestByLabel(q_1, s_labels); // Add state/transition to model - if (!visited.get(s_2 * draSize + q_2) && map[s_2 * draSize + q_2] == -1) { + if (!visited.get(s_2 * daSize + q_2) && map[s_2 * daSize + q_2] == -1) { queue.add(new Point(s_2, q_2)); prodModel.addState(); - map[s_2 * draSize + q_2] = prodModel.getNumStates() - 1; + map[s_2 * daSize + q_2] = prodModel.getNumStates() - 1; if (prodStatesList != null) { // store MDP state information for the product state prodStatesList.add(mdp.getStatesList().get(s_2)); } } - prodDistr.set(map[s_2 * draSize + q_2], prob); + prodDistr.set(map[s_2 * daSize + q_2], prob); } - prodModel.addActionLabelledChoice(map[s_1 * draSize + q_1], prodDistr, mdp.getAction(s_1, j)); + prodModel.addActionLabelledChoice(map[s_1 * daSize + q_1], prodDistr, mdp.getAction(s_1, j)); } } @@ -545,15 +548,10 @@ public class LTLModelChecker extends PrismComponent prodModel.setStatesList(prodStatesList); } - prodAcceptance = new AcceptanceRabin(); - LTLProduct product = new LTLProduct(prodModel, mdp, prodAcceptance, draSize, invMap); + LTLProduct product = new LTLProduct(prodModel, mdp, null, daSize, 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)); - } + product.setAcceptance(liftAcceptance(product, da.getAcceptance())); // lift the labels for (String label : mdp.getLabels()) { @@ -565,11 +563,11 @@ public class LTLModelChecker extends PrismComponent } /** - * Find the set of states belong to accepting BSCCs in a model wrt a Rabin acceptance condition. + * Find the set of states that belong to accepting BSCCs in a model wrt an acceptance condition. * @param model The model - * @param acceptance The Rabin acceptance condition + * @param acceptance The acceptance condition */ - public BitSet findAcceptingBSCCsForRabin(Model model, AcceptanceRabin acceptance) throws PrismException + public BitSet findAcceptingBSCCs(Model model, AcceptanceOmega acceptance) throws PrismException { // Compute bottom strongly connected components (BSCCs) SCCComputer sccComputer = SCCComputer.createSCCComputer(this, model); @@ -588,10 +586,25 @@ public class LTLModelChecker extends PrismComponent return result; } + /** + * Compute the set of states in end components of the model that are accepting + * with regard to the acceptance condition. + * @param model the model + * @param acceptance the acceptance condition + * @return BitSet with the set of states that are accepting + */ + public BitSet findAcceptingECStates(NondetModel model, AcceptanceOmega acceptance) throws PrismException + { + if (acceptance instanceof AcceptanceRabin) { + return findAcceptingECStatesForRabin(model, (AcceptanceRabin) acceptance); + } + throw new PrismException("Computing end components for acceptance type '"+acceptance.getTypeName()+"' currently not supported (explicit engine)."); + } + /** * Find the set of states in accepting end components (ECs) in a nondeterministic model wrt a Rabin acceptance condition. * @param model The model - * @param acceptance the acceptance condition + * @param acceptance The acceptance condition */ public BitSet findAcceptingECStatesForRabin(NondetModel model, AcceptanceRabin acceptance) throws PrismException { @@ -626,4 +639,23 @@ public class LTLModelChecker extends PrismComponent return allAcceptingStates; } + + /** Lift the acceptance condition from the automaton to the product states. */ + private AcceptanceOmega liftAcceptance(final LTLProduct product, AcceptanceOmega acceptance) + { + // make a copy of the acceptance condition + AcceptanceOmega lifted = acceptance.clone(); + + // lift state sets + lifted.lift(new AcceptanceOmega.LiftBitSet() { + @Override + public BitSet lift(BitSet states) + { + return product.liftFromAutomaton(states); + } + }); + + return lifted; + } + } diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 9ab56d02..72d7915e 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -31,6 +31,7 @@ import java.util.Iterator; import java.util.List; import java.util.Map; +import acceptance.AcceptanceType; import parser.ast.Expression; import prism.PrismComponent; import prism.PrismDevNullLog; @@ -75,11 +76,12 @@ public class MDPModelChecker extends ProbModelChecker // For LTL model checking routines mcLtl = new LTLModelChecker(this); - product = mcLtl.constructProductMDP(this, (MDP)model, expr, statesOfInterest); + AcceptanceType[] allowedAcceptance = {AcceptanceType.RABIN}; + product = mcLtl.constructProductMDP(this, (MDP)model, expr, statesOfInterest, allowedAcceptance); // Find accepting MECs + compute reachability probabilities mainLog.println("\nFinding accepting MECs..."); - BitSet acceptingMECs = mcLtl.findAcceptingECStatesForRabin(product.getProductModel(), product.getAcceptance()); + BitSet acceptingMECs = mcLtl.findAcceptingECStates(product.getProductModel(), product.getAcceptance()); mainLog.println("\nComputing reachability probabilities..."); mcProduct = new MDPModelChecker(this); mcProduct.inheritSettings(this);