From 80c8dcd09d87549021fcb6e70af7cd3d4d5f2a85 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 21 Jul 2015 11:39:31 +0000 Subject: [PATCH] Refactor explicit engine product construction. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10393 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/LTLModelChecker.java | 275 ++++++++++-------------- 1 file changed, 119 insertions(+), 156 deletions(-) diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 1de7bf32..d019723b 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -278,143 +278,42 @@ public class LTLModelChecker extends PrismComponent // Build product of model and automaton mainLog.println("\nConstructing MC-"+da.getAutomataType()+" product..."); - LTLProduct product = constructProductMC(da, model, labelBS, statesOfInterest); + LTLProduct product = constructProductModel(da, model, labelBS, statesOfInterest); mainLog.print("\n" + product.getProductModel().infoStringTable()); return product; } /** - * 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 DA + * 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 + * @param expr a path expression * @param statesOfInterest the set of states for which values should be calculated (null = all states) - * @return The product DTMC + * @param allowedAcceptance the allowed acceptance conditions + * @return the product with the DA + * @throws PrismException */ - public LTLProduct constructProductMC(DA da, DTMC dtmc, Vector labelBS, BitSet statesOfInterest) throws PrismException + public LTLProduct constructProductMDP(ProbModelChecker mc, MDP model, Expression expr, BitSet statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException { - DTMCSimple prodModel = new DTMCSimple(); - - int daSize = da.size(); - int numAPs = da.getAPList().size(); - int modelNumStates = dtmc.getNumStates(); - int prodNumStates = modelNumStates * daSize; - int s_1, s_2, q_1, q_2; - BitSet s_labels = new BitSet(numAPs); - List prodStatesList = null, daStatesList = null; - - // Encoding: - // each state s' = = s * daSize + q - // s(s') = s' / daSize - // q(s') = s' % daSize - - LinkedList queue = new LinkedList(); - int map[] = new int[prodNumStates]; - Arrays.fill(map, -1); - - if (dtmc.getStatesList() != null) { - prodStatesList = new ArrayList(); - daStatesList = new ArrayList(da.size()); - for (int i = 0; i < da.size(); i++) { - daStatesList.add(new State(1).setValue(0, i)); - } - } - - // We need results for all states of the original model in statesOfInterest - // We thus explore states of the product starting from these states. - // These are designated as initial states of the product model - // (a) to ensure reachability is done for these states; and - // (b) to later identify the corresponding product state for the original states - // of interest - 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(da.getAPList().get(k).substring(1))).get(s_0)); - } - // Find corresponding initial state in DA - int q_0 = da.getEdgeDestByLabel(da.getStartState(), s_labels); - if (q_0 < 0) { - throw new PrismException("The deterministic automaton is not complete (state " + da.getStartState() + ")"); - } - // Add (initial) state to product - queue.add(new Point(s_0, q_0)); - prodModel.addState(); - prodModel.addInitialState(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(new State(daStatesList.get(q_0), dtmc.getStatesList().get(s_0))); - } - } - - // Product states - BitSet visited = new BitSet(prodNumStates); - while (!queue.isEmpty()) { - Point p = queue.pop(); - s_1 = p.x; - q_1 = p.y; - visited.set(s_1 * daSize + q_1); - - // Go through transitions from state s_1 in original DTMC - Iterator> iter = dtmc.getTransitionsIterator(s_1); - while (iter.hasNext()) { - Map.Entry e = iter.next(); - s_2 = e.getKey(); - 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(da.getAPList().get(k).substring(1))).get(s_2)); - } - // Find corresponding successor in DRA - q_2 = da.getEdgeDestByLabel(q_1, s_labels); - if (q_2 < 0) { - throw new PrismException("The deterministic automaton is not complete (state " + q_1 + ")"); - } - // Add state/transition to model - 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 * daSize + q_2] = prodModel.getNumStates() - 1; - if (prodStatesList != null) { - // store DTMC state information for the product state - prodStatesList.add(new State(daStatesList.get(q_2), dtmc.getStatesList().get(s_2))); - } - } - prodModel.setProbability(map[s_1 * daSize + q_1], map[s_2 * daSize + q_2], prob); - } - } - - // Build a mapping from state indices to states (s,q), encoded as (s * draSize + q) - int invMap[] = new int[prodModel.getNumStates()]; - for (int i = 0; i < map.length; i++) { - if (map[i] != -1) { - invMap[map[i]] = i; - } - } - - prodModel.findDeadlocks(false); - - if (prodStatesList != null) { - prodModel.setStatesList(prodStatesList); - } - - LTLProduct product = new LTLProduct(prodModel, dtmc, null, daSize, invMap); - - // generate acceptance for the product model by lifting - product.setAcceptance(liftAcceptance(product, da.getAcceptance())); + // Convert LTL formula to automaton + Vector labelBS = new Vector(); + DA da; + da = constructDAForLTLFormula(mc, model, expr, labelBS, allowedAcceptance); - // lift the labels - for (String label : dtmc.getLabels()) { - BitSet liftedLabel = product.liftFromModel(dtmc.getLabelStates(label)); - prodModel.addLabel(label, liftedLabel); - } + // Build product of model and automaton + mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product..."); + LTLProduct product = constructProductModel(da, model, labelBS, statesOfInterest); + mainLog.print("\n" + product.getProductModel().infoStringTable()); return product; } + /** * Generate a deterministic automaton for the given LTL formula - * and construct the product of this automaton with an MDP. + * and construct the product of this automaton with a model. * * @param mc a ProbModelChecker, used for checking maximal state formulas * @param model the model @@ -424,7 +323,7 @@ public class LTLModelChecker extends PrismComponent * @return the product with the DA * @throws PrismException */ - public LTLProduct constructProductMDP(ProbModelChecker mc, MDP model, Expression expr, BitSet statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException + public LTLProduct constructProductSTPG(ProbModelChecker mc, M model, Expression expr, BitSet statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException { // Convert LTL formula to automaton Vector labelBS = new Vector(); @@ -432,44 +331,58 @@ public class LTLModelChecker extends PrismComponent da = constructDAForLTLFormula(mc, model, expr, labelBS, allowedAcceptance); // Build product of model and automaton - mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product..."); - LTLProduct product = constructProductMDP(da, model, labelBS, statesOfInterest); + mainLog.println("\nConstructing " + model.getModelType() + "-" + da.getAutomataType() + " product..."); + LTLProduct product = constructProductModel(da, model, labelBS, statesOfInterest); mainLog.print("\n" + product.getProductModel().infoStringTable()); return product; } - + /** - * Construct the product of a DA and an MDP. + * Construct the product of a DA and a model. * @param da The DA - * @param mdp The MDP + * @param model The model * @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 + * @return The product model */ - public LTLProduct constructProductMDP(DA da, MDP mdp, Vector labelBS, BitSet statesOfInterest) throws PrismException + public LTLProduct constructProductModel(DA da, M model, Vector labelBS, BitSet statesOfInterest) throws PrismException { - MDPSimple prodModel = new MDPSimple(); - + ModelType modelType = model.getModelType(); int daSize = da.size(); int numAPs = da.getAPList().size(); - int modelNumStates = mdp.getNumStates(); + int modelNumStates = model.getNumStates(); int prodNumStates = modelNumStates * daSize; int s_1, s_2, q_1, q_2; BitSet s_labels = new BitSet(numAPs); List prodStatesList = null, daStatesList = null; + // Create a (simple, mutable) model of the appropriate type + ModelSimple prodModel = null; + switch (modelType) { + case DTMC: + prodModel = new DTMCSimple(); + break; + case MDP: + prodModel = new MDPSimple(); + break; + case STPG: + prodModel = new STPGExplicit(); + break; + default: + throw new PrismNotSupportedException("Model construction not supported for " + modelType + "s"); + } // 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]; Arrays.fill(map, -1); - if (mdp.getStatesList() != null) { + if (model.getStatesList() != null) { prodStatesList = new ArrayList(); daStatesList = new ArrayList(da.size()); for (int i = 0; i < da.size(); i++) { @@ -483,24 +396,31 @@ public class LTLModelChecker extends PrismComponent // (a) to ensure reachability is done for these states; and // (b) to later identify the corresponding product state for the original states // of interest - for (int s_0 : new IterableStateSet(statesOfInterest, mdp.getNumStates())) { + for (int s_0 : new IterableStateSet(statesOfInterest, model.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(da.getAPList().get(k).substring(1))).get(s_0)); } - // Find corresponding initial state in DRA + // Find corresponding initial state in DA int q_0 = da.getEdgeDestByLabel(da.getStartState(), s_labels); if (q_0 < 0) { throw new PrismException("The deterministic automaton is not complete (state " + da.getStartState() + ")"); } // Add (initial) state to product queue.add(new Point(s_0, q_0)); - prodModel.addState(); + switch (modelType) { + case STPG: + ((STPGExplicit) prodModel).addState(((STPG) model).getPlayer(s_0)); + break; + default: + prodModel.addState(); + break; + } prodModel.addInitialState(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(new State(daStatesList.get(q_0), mdp.getStatesList().get(s_0))); + // Store state information for the product + prodStatesList.add(new State(daStatesList.get(q_0), model.getStatesList().get(s_0))); } } @@ -512,11 +432,27 @@ public class LTLModelChecker extends PrismComponent q_1 = p.y; visited.set(s_1 * daSize + q_1); - // Go through transitions from state s_1 in original MDP - int numChoices = mdp.getNumChoices(s_1); + // Go through transitions from state s_1 in original model + int numChoices = (model instanceof NondetModel) ? ((NondetModel) model).getNumChoices(s_1) : 1; for (int j = 0; j < numChoices; j++) { - Distribution prodDistr = new Distribution(); - Iterator> iter = mdp.getTransitionsIterator(s_1, j); + Iterator> iter; + switch (modelType) { + case DTMC: + iter = ((DTMC) model).getTransitionsIterator(s_1); + break; + case MDP: + iter = ((MDP) model).getTransitionsIterator(s_1, j); + break; + case STPG: + iter = ((STPG) model).getTransitionsIterator(s_1, j); + break; + default: + throw new PrismNotSupportedException("Product construction not implemented for " + modelType + "s"); + } + Distribution prodDistr = null; + if (modelType.nondeterministic()) { + prodDistr = new Distribution(); + } while (iter.hasNext()) { Map.Entry e = iter.next(); s_2 = e.getKey(); @@ -525,7 +461,7 @@ public class LTLModelChecker extends PrismComponent for (int k = 0; k < numAPs; k++) { s_labels.set(k, labelBS.get(Integer.parseInt(da.getAPList().get(k).substring(1))).get(s_2)); } - // Find corresponding successor in DRA + // Find corresponding successor in DA q_2 = da.getEdgeDestByLabel(q_1, s_labels); if (q_2 < 0) { throw new PrismException("The deterministic automaton is not complete (state " + q_1 + ")"); @@ -533,20 +469,46 @@ public class LTLModelChecker extends PrismComponent // Add state/transition to model 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(); + switch (modelType) { + case STPG: + ((STPGExplicit) prodModel).addState(((STPG) model).getPlayer(s_2)); + break; + default: + prodModel.addState(); + break; + } map[s_2 * daSize + q_2] = prodModel.getNumStates() - 1; if (prodStatesList != null) { - // store MDP state information for the product state - prodStatesList.add(new State(daStatesList.get(q_2), mdp.getStatesList().get(s_2))); + // Store state information for the product + prodStatesList.add(new State(daStatesList.get(q_2), model.getStatesList().get(s_2))); } } - prodDistr.set(map[s_2 * daSize + q_2], prob); + switch (modelType) { + case DTMC: + ((DTMCSimple) prodModel).setProbability(map[s_1 * daSize + q_1], map[s_2 * daSize + q_2], prob); + break; + case MDP: + case STPG: + prodDistr.set(map[s_2 * daSize + q_2], prob); + break; + default: + throw new PrismNotSupportedException("Product construction not implemented for " + modelType + "s"); + } + } + switch (modelType) { + case MDP: + ((MDPSimple) prodModel).addActionLabelledChoice(map[s_1 * daSize + q_1], prodDistr, ((MDP) model).getAction(s_1, j)); + break; + case STPG: + ((STPGExplicit) prodModel).addActionLabelledChoice(map[s_1 * daSize + q_1], prodDistr, ((STPG) model).getAction(s_1, j)); + break; + default: + break; } - prodModel.addActionLabelledChoice(map[s_1 * daSize + q_1], prodDistr, mdp.getAction(s_1, j)); } } - // Build a mapping from state indices to states (s,q), encoded as (s * draSize + q) + // Build a mapping from state indices to states (s,q), encoded as (s * daSize + q) int invMap[] = new int[prodModel.getNumStates()]; for (int i = 0; i < map.length; i++) { if (map[i] != -1) { @@ -560,14 +522,15 @@ public class LTLModelChecker extends PrismComponent prodModel.setStatesList(prodStatesList); } - LTLProduct product = new LTLProduct(prodModel, mdp, null, daSize, invMap); + @SuppressWarnings("unchecked") + LTLProduct product = new LTLProduct((M) prodModel, model, null, daSize, invMap); // generate acceptance for the product model by lifting product.setAcceptance(liftAcceptance(product, da.getAcceptance())); // lift the labels - for (String label : mdp.getLabels()) { - BitSet liftedLabel = product.liftFromModel(mdp.getLabelStates(label)); + for (String label : model.getLabels()) { + BitSet liftedLabel = product.liftFromModel(model.getLabelStates(label)); prodModel.addLabel(label, liftedLabel); }