From 5b5bac7fe3bb15375237c368dc155f6a5eb98e99 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 31 Jan 2015 14:49:43 +0000 Subject: [PATCH] Adapt (symbolic) LTLModelChecker to support generic acceptance types for MDP. [Joachim Klein] Adapt product construction (rename dra to da) Add findAcceptingECStates() wrapper to support more acceptance types in the future. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9606 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 147 ++++++++++++++---------- prism/src/prism/NondetModelChecker.java | 51 ++++---- 2 files changed, 113 insertions(+), 85 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index c492ab2d..bc3b1610 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -35,6 +35,7 @@ import java.util.Vector; import acceptance.AcceptanceOmega; import acceptance.AcceptanceOmegaDD; import acceptance.AcceptanceRabin; +import acceptance.AcceptanceRabinDD; import jdd.JDD; import jdd.JDDNode; import jdd.JDDVars; @@ -341,43 +342,43 @@ 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 model The MDP - * @param labelDDs BDDs giving the set of states for each AP in the DRA + * @param labelDDs BDDs giving the set of states for each AP in the DA */ - public NondetModel constructProductMDP(DA dra, NondetModel model, Vector labelDDs) throws PrismException + public NondetModel constructProductMDP(DA da, NondetModel model, Vector labelDDs) throws PrismException { - return constructProductMDP(dra, model, labelDDs, null, null, true, null); + return constructProductMDP(da, model, labelDDs, null, null, true, null); } /** - * 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 model The MDP - * @param labelDDs BDDs giving the set of states for each AP in the DRA - * @param draDDRowVarsCopy (Optionally) empty JDDVars object to obtain copy of DD row vars for DRA - * @param draDDColVarsCopy (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA + * @param labelDDs BDDs giving the set of states for each AP in the DA + * @param daDDRowVarsCopy (Optionally) empty JDDVars object to obtain copy of DD row vars for DA + * @param daDDColVarsCopy (Optionally) empty JDDVars object to obtain copy of DD col vars for DA */ - public NondetModel constructProductMDP(DA dra, NondetModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy) + public NondetModel constructProductMDP(DA da, NondetModel model, Vector labelDDs, JDDVars daDDRowVarsCopy, JDDVars daDDColVarsCopy) throws PrismException { - return constructProductMDP(dra, model, labelDDs, draDDRowVarsCopy, draDDColVarsCopy, true, null); + return constructProductMDP(da, model, labelDDs, daDDRowVarsCopy, daDDColVarsCopy, true, null); } /** - * 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 model The MDP - * @param labelDDs BDDs giving the set of states for each AP in the DRA - * @param draDDRowVarsCopy (Optionally) empty JDDVars object to obtain copy of DD row vars for DRA - * @param draDDColVarsCopy (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA + * @param labelDDs BDDs giving the set of states for each AP in the DA + * @param daDDRowVarsCopy (Optionally) empty JDDVars object to obtain copy of DD row vars for DA + * @param daDDColVarsCopy (Optionally) empty JDDVars object to obtain copy of DD col vars for DA * @param allInit Do we assume that all states of the original model are initial states? * (just for the purposes of reachability) If not, the required initial states should be given * @param init The initial state(s) (of the original model) used to build the product; * if null; we just take the existing initial states from model.getStart(). */ - public NondetModel constructProductMDP(DA dra, NondetModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy, + public NondetModel constructProductMDP(DA da, NondetModel model, Vector labelDDs, JDDVars daDDRowVarsCopy, JDDVars daDDColVarsCopy, boolean allInit, JDDNode init) throws PrismException { // Existing model - dds, vars, etc. @@ -393,9 +394,9 @@ public class LTLModelChecker extends PrismComponent JDDVars newAllDDRowVars, newAllDDColVars; Vector newDDVarNames; VarList newVarList; - String draVar; - // DRA stuff - JDDVars draDDRowVars, draDDColVars; + String daVar; + // DA stuff + JDDVars daDDRowVars, daDDColVars; // Misc int i, j, n; boolean before; @@ -408,16 +409,16 @@ public class LTLModelChecker extends PrismComponent ddVarNames = model.getDDVarNames(); varList = model.getVarList(); - // Create a (new, unique) name for the variable that will represent DRA states - draVar = "_dra"; - while (varList.getIndex(draVar) != -1) { - draVar = "_" + draVar; + // Create a (new, unique) name for the variable that will represent DA states + daVar = "_da"; + while (varList.getIndex(daVar) != -1) { + daVar = "_" + daVar; } - // See how many new dd vars will be needed for DRA + // See how many new dd vars will be needed for DA // and whether there is room to put them before rather than after the existing vars - // (if DRA only has one state, we add an extra dummy state) - n = (int) Math.ceil(PrismUtils.log2(dra.size())); + // (if DA only has one state, we add an extra dummy state) + n = (int) Math.ceil(PrismUtils.log2(da.size())); n = Math.max(n, 1); before = true; if ((allDDRowVars.getMinVarIndex() - model.getAllDDNondetVars().getMaxVarIndex()) - 1 < 2 * n) { @@ -426,28 +427,28 @@ public class LTLModelChecker extends PrismComponent // If passed in var lists are null, create new lists // (which won't be accessible later in this case) - draDDRowVars = (draDDRowVarsCopy == null) ? new JDDVars() : draDDRowVarsCopy; - draDDColVars = (draDDColVarsCopy == null) ? new JDDVars() : draDDColVarsCopy; + daDDRowVars = (daDDRowVarsCopy == null) ? new JDDVars() : daDDRowVarsCopy; + daDDColVars = (daDDColVarsCopy == null) ? new JDDVars() : daDDColVarsCopy; // Create the new dd variables newDDVarNames = new Vector(); newDDVarNames.addAll(ddVarNames); j = before ? allDDRowVars.getMinVarIndex() - 2 * n : model.getAllDDColVars().getMaxVarIndex() + 1; for (i = 0; i < n; i++) { - draDDRowVars.addVar(JDD.Var(j++)); - draDDColVars.addVar(JDD.Var(j++)); + daDDRowVars.addVar(JDD.Var(j++)); + daDDColVars.addVar(JDD.Var(j++)); if (!before) { newDDVarNames.add(""); newDDVarNames.add(""); } - newDDVarNames.set(j - 2, draVar + "." + i); - newDDVarNames.set(j - 1, draVar + "'." + i); + newDDVarNames.set(j - 2, daVar + "." + i); + newDDVarNames.set(j - 1, daVar + "'." + i); } // Create/populate new lists newVarDDRowVars = new JDDVars[varDDRowVars.length + 1]; newVarDDColVars = new JDDVars[varDDRowVars.length + 1]; - newVarDDRowVars[before ? 0 : varDDRowVars.length] = draDDRowVars; - newVarDDColVars[before ? 0 : varDDColVars.length] = draDDColVars; + newVarDDRowVars[before ? 0 : varDDRowVars.length] = daDDRowVars; + newVarDDColVars[before ? 0 : varDDColVars.length] = daDDColVars; for (i = 0; i < varDDRowVars.length; i++) { newVarDDRowVars[before ? i + 1 : i] = new JDDVars(); newVarDDColVars[before ? i + 1 : i] = new JDDVars(); @@ -457,19 +458,19 @@ public class LTLModelChecker extends PrismComponent newAllDDRowVars = new JDDVars(); newAllDDColVars = new JDDVars(); if (before) { - newAllDDRowVars.addVars(draDDRowVars); - newAllDDColVars.addVars(draDDColVars); + newAllDDRowVars.addVars(daDDRowVars); + newAllDDColVars.addVars(daDDColVars); newAllDDRowVars.addVars(allDDRowVars); newAllDDColVars.addVars(allDDColVars); } else { newAllDDRowVars.addVars(allDDRowVars); newAllDDColVars.addVars(allDDColVars); - newAllDDRowVars.addVars(draDDRowVars); - newAllDDColVars.addVars(draDDColVars); + newAllDDRowVars.addVars(daDDRowVars); + newAllDDColVars.addVars(daDDColVars); } newVarList = (VarList) varList.clone(); - // NB: if DRA only has one state, we add an extra dummy state - Declaration decl = new Declaration(draVar, new DeclarationInt(Expression.Int(0), Expression.Int(Math.max(dra.size() - 1, 1)))); + // NB: if DA only has one state, we add an extra dummy state + Declaration decl = new Declaration(daVar, new DeclarationInt(Expression.Int(0), Expression.Int(Math.max(da.size() - 1, 1)))); newVarList.addVar(before ? 0 : varList.getNumVars(), decl, 1, model.getConstantValues()); // Extra references (because will get derefed when new model is done with) @@ -481,15 +482,15 @@ public class LTLModelChecker extends PrismComponent model.getModuleDDRowVars(i).refAll(); model.getModuleDDColVars(i).refAll(); } - draDDRowVars.refAll(); - draDDColVars.refAll(); + daDDRowVars.refAll(); + daDDColVars.refAll(); model.getAllDDSchedVars().refAll(); model.getAllDDSynchVars().refAll(); model.getAllDDChoiceVars().refAll(); model.getAllDDNondetVars().refAll(); // Build transition matrix for product - newTrans = buildTransMask(dra, labelDDs, allDDRowVars, allDDColVars, draDDRowVars, draDDColVars); + newTrans = buildTransMask(da, labelDDs, allDDRowVars, allDDColVars, daDDRowVars, daDDColVars); JDD.Ref(model.getTrans()); newTrans = JDD.Apply(JDD.TIMES, model.getTrans(), newTrans); @@ -502,7 +503,7 @@ public class LTLModelChecker extends PrismComponent // Optionally (if allInit is false), we don't do this - maybe because we only care about result for the initial state // Note that we reset the initial states after reachability, corresponding to just the initial states of the original model. // The initial state of the original model can be overridden by passing in 'init'. - newStart = buildStartMask(dra, labelDDs, draDDRowVars); + newStart = buildStartMask(da, labelDDs, daDDRowVars); JDD.Ref(allInit ? model.getReach() : init != null ? init : model.getStart()); newStart = JDD.And(allInit ? model.getReach() : init != null ? init : model.getStart(), newStart); @@ -541,11 +542,11 @@ public class LTLModelChecker extends PrismComponent modelProd.findDeadlocks(false); if (modelProd.getDeadlockStates().size() > 0) { // Assuming original model has no deadlocks, neither should product - throw new PrismException("Model-DRA product has deadlock states"); + throw new PrismException("Model-DA product has deadlock states"); } // Reset initial state - newStart = buildStartMask(dra, labelDDs, draDDRowVars); + newStart = buildStartMask(da, labelDDs, daDDRowVars); JDD.Ref(init != null ? init : model.getStart()); newStart = JDD.And(init != null ? init : model.getStart(), newStart); modelProd.setStart(newStart); @@ -553,11 +554,11 @@ public class LTLModelChecker extends PrismComponent //try { prism.exportStatesToFile(modelProd, Prism.EXPORT_PLAIN, new java.io.File("prod.sta")); } //catch (java.io.FileNotFoundException e) {} - // Reference DRA DD vars (if being returned) - if (draDDRowVarsCopy != null) - draDDRowVarsCopy.refAll(); - if (draDDColVarsCopy != null) - draDDColVarsCopy.refAll(); + // Reference DA DD vars (if being returned) + if (daDDRowVarsCopy != null) + daDDRowVarsCopy.refAll(); + if (daDDColVarsCopy != null) + daDDColVarsCopy.refAll(); return modelProd; } @@ -714,16 +715,36 @@ public class LTLModelChecker extends PrismComponent return allAcceptingStates; } + /** + * Find the set of states in accepting end components (ECs) in a nondeterministic model wrt an acceptance condition. + * @param acceptance the acceptance condition + * @param model The model + * @param daDDRowVars BDD row variables for the DA part of the model + * @param daDDColVars BDD column variables for the DA part of the model + * @param fairness Consider fairness? + * @return A referenced BDD for the union of all states in accepting MECs + */ + public JDDNode findAcceptingECStates(AcceptanceOmegaDD acceptance, NondetModel model, JDDVars daDDRowVars, JDDVars daDDColVars, boolean fairness) + throws PrismException + { + switch (acceptance.getType()) { + case RABIN: + return findAcceptingECStatesForRabin((AcceptanceRabinDD) acceptance, model, daDDRowVars, daDDColVars, fairness); + default: + throw new PrismException("Computing the accepting EC states for "+acceptance.getTypeName()+" acceptance is not yet implemented (symbolic engine)"); + } + } + /** * Find the set of states in accepting end components (ECs) in a nondeterministic model wrt a Rabin acceptance condition. - * @param dra The DRA storing the Rabin acceptance condition + * @param acceptance the Rabin acceptance condition * @param model The model * @param draDDRowVars BDD row variables for the DRA part of the model * @param draDDColVars BDD column variables for the DRA part of the model * @param fairness Consider fairness? * @return A referenced BDD for the union of all states in accepting MECs */ - public JDDNode findAcceptingECStatesForRabin(DA dra, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, boolean fairness) + public JDDNode findAcceptingECStatesForRabin(AcceptanceRabinDD acceptance, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, boolean fairness) throws PrismException { JDDNode acceptingStates = null, allAcceptingStates, acceptanceVector_L_not, acceptanceVector_K, candidateStates; @@ -731,15 +752,15 @@ public class LTLModelChecker extends PrismComponent allAcceptingStates = JDD.Constant(0); - if (dra.getAcceptance().size() > 1) { + if (acceptance.size() > 1) { acceptanceVector_L_not = JDD.Constant(0); acceptanceVector_K = JDD.Constant(0); ArrayList statesLnot = new ArrayList(); ArrayList statesK = new ArrayList(); - for (i = 0; i < dra.getAcceptance().size(); i++) { - JDDNode tmpLnot = buildLStatesForRabinPair(draDDRowVars, dra, i, true); - JDDNode tmpK = buildKStatesForRabinPair(draDDRowVars, dra, i); + for (i = 0; i < acceptance.size(); i++) { + JDDNode tmpLnot = JDD.Not(acceptance.get(i).getL()); + JDDNode tmpK = acceptance.get(i).getK(); statesLnot.add(tmpLnot); JDD.Ref(tmpLnot); acceptanceVector_L_not = JDD.Or(acceptanceVector_L_not, tmpLnot); @@ -760,7 +781,7 @@ public class LTLModelChecker extends PrismComponent JDD.Deref(acceptanceVector_K); JDD.Deref(candidateStates); - for (i = 0; i < dra.getAcceptance().size(); i++) { + for (i = 0; i < acceptance.size(); i++) { // build the acceptance vectors L_i and K_i acceptanceVector_L_not = statesLnot.get(i); acceptanceVector_K = statesK.get(i); @@ -810,10 +831,10 @@ public class LTLModelChecker extends PrismComponent JDD.Deref(ec); } else { // Go through the DRA acceptance pairs (L_i, K_i) - for (i = 0; i < dra.getAcceptance().size(); i++) { + for (i = 0; i < acceptance.size(); i++) { // Build BDDs for !L_i and K_i - JDDNode statesLi_not = buildLStatesForRabinPair(draDDRowVars, dra, i, true); - JDDNode statesK_i = buildKStatesForRabinPair(draDDRowVars, dra, i); + JDDNode statesLi_not = JDD.Not(acceptance.get(i).getL()); + JDDNode statesK_i = acceptance.get(i).getK(); // Find states in the model for which there are no transitions leaving !L_i // (this will allow us to reduce the problem to finding MECs, not ECs) // TODO: I don't think this next step is needed, diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 70d7b99a..754763ad 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -33,7 +33,11 @@ import java.io.File; import java.io.FileNotFoundException; import java.util.*; +import acceptance.AcceptanceOmega; +import acceptance.AcceptanceOmegaDD; import acceptance.AcceptanceRabin; +import acceptance.AcceptanceRabinDD; +import acceptance.AcceptanceType; import odd.ODDUtils; import jdd.*; import dv.*; @@ -950,11 +954,11 @@ public class NondetModelChecker extends NonProbModelChecker StateValues probsProduct = null, probs = null; Expression ltl; Vector labelDDs; - DA dra; + DA da; NondetModel modelProduct; NondetModelChecker mcProduct; JDDNode startMask; - JDDVars draDDRowVars, draDDColVars; + JDDVars daDDRowVars, daDDColVars; int i; long l; @@ -967,12 +971,12 @@ public class NondetModelChecker extends NonProbModelChecker if (Expression.containsTemporalTimeBounds(expr)) { if (model.getModelType().continuousTime()) { - throw new PrismException("DRA construction for time-bounded operators not supported for " + model.getModelType()+"."); + throw new PrismException("DA 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 @@ -996,28 +1000,29 @@ public class NondetModelChecker extends NonProbModelChecker labelDDs = new Vector(); ltl = mcLtl.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelDDs); - // Convert LTL formula to deterministic Rabin automaton (DRA) - mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); + // Convert LTL formula to deterministic automaton (DA) + mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")..."); l = System.currentTimeMillis(); LTL2DA ltl2da = new LTL2DA(prism); - dra = ltl2da.convertLTLFormulaToDRA(ltl, constantValues); - mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics()+"."); + AcceptanceType[] allowedAcceptance = {AcceptanceType.RABIN}; + da = ltl2da.convertLTLFormulaToDA(ltl, constantValues, allowedAcceptance); + mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics()+"."); l = System.currentTimeMillis() - l; - mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds."); - // If required, export DRA + mainLog.println("Time for deterministic automaton translation: " + l / 1000.0 + " seconds."); + // If required, export DA if (prism.getSettings().getExportPropAut()) { - mainLog.println("Exporting DRA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"..."); + mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"..."); PrismLog out = new PrismFileLog(prism.getSettings().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..."); - draDDRowVars = new JDDVars(); - draDDColVars = new JDDVars(); - modelProduct = mcLtl.constructProductMDP(dra, model, labelDDs, draDDRowVars, draDDColVars); + mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product..."); + daDDRowVars = new JDDVars(); + daDDColVars = new JDDVars(); + modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars); mainLog.println(); modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo()); // Output product, if required @@ -1038,7 +1043,9 @@ public class NondetModelChecker extends NonProbModelChecker // Find accepting MECs + compute reachability probabilities mainLog.println("\nFinding accepting end components..."); - JDDNode acc = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, draDDRowVars, draDDColVars, fairness); + AcceptanceOmegaDD acceptance = da.getAcceptance().toAcceptanceDD(daDDRowVars); + JDDNode acc = mcLtl.findAcceptingECStates(acceptance, modelProduct, daDDRowVars, daDDColVars, fairness); + acceptance.clear(); mainLog.println("\nComputing reachability probabilities..."); mcProduct = new NondetModelChecker(prism, modelProduct, null); probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual, min && fairness); @@ -1050,12 +1057,12 @@ public class NondetModelChecker extends NonProbModelChecker // Convert probability vector to original model // First, filter over DRA start states - startMask = mcLtl.buildStartMask(dra, labelDDs, draDDRowVars); + startMask = mcLtl.buildStartMask(da, labelDDs, daDDRowVars); JDD.Ref(model.getReach()); startMask = JDD.And(model.getReach(), startMask); probsProduct.filter(startMask); // Then sum over DD vars for the DRA state - probs = probsProduct.sumOverDDVars(draDDRowVars, model); + probs = probsProduct.sumOverDDVars(daDDRowVars, model); // Deref, clean up probsProduct.clear(); @@ -1065,8 +1072,8 @@ public class NondetModelChecker extends NonProbModelChecker } JDD.Deref(acc); JDD.Deref(startMask); - draDDRowVars.derefAll(); - draDDColVars.derefAll(); + daDDRowVars.derefAll(); + daDDColVars.derefAll(); return probs; }