diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index a6018c6a..053fca08 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -60,15 +60,18 @@ import parser.type.TypeBool; import parser.type.TypeDouble; import parser.type.TypePathBool; import parser.type.TypePathDouble; +import prism.LTLModelChecker.LTLProduct; import sparse.PrismSparse; import strat.MDStrategyIV; import acceptance.AcceptanceOmega; import acceptance.AcceptanceOmegaDD; import acceptance.AcceptanceRabin; +import acceptance.AcceptanceReach; import acceptance.AcceptanceReachDD; import acceptance.AcceptanceType; import automata.DA; import automata.LTL2DA; +import automata.LTL2WDBA; import dv.DoubleVector; import dv.IntegerVector; import explicit.MinMax; @@ -1455,18 +1458,15 @@ public class NondetModelChecker extends NonProbModelChecker { LTLModelChecker mcLtl; StateValues rewardsProduct = null, rewards = null; - Expression ltl; - Vector labelDDs; - DA da; - NondetModel modelProduct; + Vector labelDDs = new Vector(); + DA da; + LTLProduct modelProduct; NondetModelChecker mcProduct; - JDDNode startMask; - JDDVars daDDRowVars, daDDColVars; - int i; long l; if (Expression.containsTemporalTimeBounds(expr)) { if (model.getModelType().continuousTime()) { + JDD.Deref(statesOfInterest); throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+"."); } @@ -1480,35 +1480,25 @@ public class NondetModelChecker extends NonProbModelChecker // formulas only appear positively expr = Expression.convertSimplePathFormulaToCanonicalForm(expr); } else { + JDD.Deref(statesOfInterest); throw new PrismException("Time-bounded operators not supported in LTL: " + expr); } } // Can't do "dfa" properties yet if (expr instanceof ExpressionFunc && ((ExpressionFunc) expr).getName().equals("dfa")) { + JDD.Deref(statesOfInterest); throw new PrismException("Model checking for \"dfa\" specifications not supported yet"); } // For LTL model checking routines mcLtl = new LTLModelChecker(prism); - // Model check maximal state formulas - labelDDs = new Vector(); - ltl = mcLtl.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelDDs); + // Model check maximal state formulas and construct DFA, with the special + // handling needed for cosafety reward translation + da = mcLtl.constructDFAForCosafetyRewardLTL(this, model, expr, labelDDs); - // Convert LTL formula to deterministic automaton (DA) - mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")..."); - l = System.currentTimeMillis(); - LTL2DA ltl2da = new LTL2DA(prism); - AcceptanceType[] allowedAcceptance = { - AcceptanceType.RABIN, - AcceptanceType.REACH - }; - 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 deterministic automaton translation: " + l / 1000.0 + " seconds."); - // If required, export DA + // If required, export DA if (prism.getSettings().getExportPropAut()) { mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"..."); PrintStream out = PrismUtils.newPrintStream(prism.getSettings().getExportPropAutFilename()); @@ -1518,20 +1508,12 @@ public class NondetModelChecker extends NonProbModelChecker } // Build product of MDP and automaton - mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product..."); - daDDRowVars = new JDDVars(); - daDDColVars = new JDDVars(); - l = System.currentTimeMillis(); - modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest); - l = System.currentTimeMillis() - l; - mainLog.println("Time for product construction: " + l / 1000.0 + " seconds."); - mainLog.println(); - modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo()); + modelProduct = mcLtl.constructProductMDP(model, da, labelDDs, statesOfInterest); // Output product, if required if (prism.getExportProductTrans()) { try { mainLog.println("\nExporting product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"..."); - modelProduct.exportToFile(Prism.EXPORT_PLAIN, true, new File(prism.getExportProductTransFilename())); + modelProduct.getProductModel().exportToFile(Prism.EXPORT_PLAIN, true, new File(prism.getExportProductTransFilename())); } catch (FileNotFoundException e) { mainLog.printWarning("Could not export product transition matrix to file \"" + prism.getExportProductTransFilename() + "\""); } @@ -1539,58 +1521,37 @@ public class NondetModelChecker extends NonProbModelChecker if (prism.getExportProductStates()) { mainLog.println("\nExporting product state space to file \"" + prism.getExportProductStatesFilename() + "\"..."); PrismFileLog out = new PrismFileLog(prism.getExportProductStatesFilename()); - modelProduct.exportStates(Prism.EXPORT_PLAIN, out); + modelProduct.getProductModel().exportStates(Prism.EXPORT_PLAIN, out); out.close(); } // Adapt reward info to product model - JDD.Ref(stateRewards); - JDD.Ref(modelProduct.getReach()); - JDDNode stateRewardsProduct = JDD.Apply(JDD.TIMES, stateRewards, modelProduct.getReach()); - JDD.Ref(transRewards); - JDD.Ref(modelProduct.getTrans01()); - JDDNode transRewardsProduct = JDD.Apply(JDD.TIMES, transRewards, modelProduct.getTrans01()); + JDDNode stateRewardsProduct = JDD.Apply(JDD.TIMES, stateRewards.copy(), modelProduct.getProductModel().getReach().copy()); + JDDNode transRewardsProduct = JDD.Apply(JDD.TIMES, transRewards.copy(), modelProduct.getProductModel().getTrans01().copy()); // Find accepting states + compute reachability rewards - AcceptanceOmegaDD acceptance = da.getAcceptance().toAcceptanceDD(daDDRowVars); - JDDNode acc = null; - if (acceptance instanceof AcceptanceReachDD) { - // For a DFA, just collect the accept states - mainLog.println("\nSkipping end component detection since DRA is a DFA..."); - acc = ((AcceptanceReachDD) acceptance).getGoalStates(); - JDD.Ref(modelProduct.getReach()); - acc = JDD.And(acc, modelProduct.getReach()); - } else { - // Usually, we have to detect end components in the product - mainLog.println("\nFinding accepting end components..."); - acc = mcLtl.findAcceptingECStates(acceptance, modelProduct, daDDRowVars, daDDColVars, fairness); - } - acceptance.clear(); + AcceptanceReachDD acceptance = (AcceptanceReachDD) modelProduct.getProductAcceptance(); + // acc is already restricted to the product model's reachable states + JDDNode acc = acceptance.getGoalStates(); + mainLog.println("\nComputing reachability rewards..."); - mcProduct = new NondetModelChecker(prism, modelProduct, null); - rewardsProduct = mcProduct.computeReachRewards(modelProduct.getTrans(), modelProduct.getTransActions(), modelProduct.getTrans01(), stateRewardsProduct, transRewardsProduct, acc, min); + mcProduct = createNewModelChecker(prism, modelProduct.getProductModel(), null); + rewardsProduct = mcProduct.computeReachRewards(modelProduct.getProductModel().getTrans(), + modelProduct.getProductModel().getTransActions(), + modelProduct.getProductModel().getTrans01(), + stateRewardsProduct, + transRewardsProduct, + acc, + min); // Convert reward vector to original model - // First, filter over DRA start states - startMask = mcLtl.buildStartMask(da, labelDDs, daDDRowVars); - JDD.Ref(model.getReach()); - startMask = JDD.And(model.getReach(), startMask); - rewardsProduct.filter(startMask); - // Then sum over DD vars for the DRA state - rewards = rewardsProduct.sumOverDDVars(daDDRowVars, model); + rewards = modelProduct.projectToOriginalModel(rewardsProduct); // Deref, clean up JDD.Deref(stateRewardsProduct); JDD.Deref(transRewardsProduct); - rewardsProduct.clear(); modelProduct.clear(); - for (i = 0; i < labelDDs.size(); i++) { - JDD.Deref(labelDDs.get(i)); - } JDD.Deref(acc); - JDD.Deref(startMask); - daDDRowVars.derefAll(); - daDDColVars.derefAll(); return rewards; }