From 957148215ef58beff9592eff439084cd0a911815 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 16 Jul 2015 16:07:41 +0000 Subject: [PATCH] Support (symbolic/explicit) for expected reward to satisfy a co-safe LTL formula. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10334 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MDPModelChecker.java | 66 ++++ prism/src/explicit/ProbModelChecker.java | 30 +- prism/src/explicit/Product.java | 34 ++ prism/src/parser/PrismParser.java | 393 ++++++++++++----------- prism/src/parser/PrismParser.jj | 18 +- prism/src/parser/visitor/TypeCheck.java | 3 +- prism/src/prism/NondetModelChecker.java | 218 ++++++++++++- 7 files changed, 558 insertions(+), 204 deletions(-) diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 3931ec70..00b15af0 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -49,6 +49,7 @@ import acceptance.AcceptanceType; import explicit.rewards.MCRewards; import explicit.rewards.MCRewardsFromMDPRewards; import explicit.rewards.MDPRewards; +import explicit.rewards.Rewards; /** * Explicit-state model checker for Markov decision processes (MDPs). @@ -135,6 +136,71 @@ public class MDPModelChecker extends ProbModelChecker return probs; } + /** + * Compute rewards for a co-safe LTL reward operator. + */ + protected StateValues checkRewardCoSafeLTL(Model model, Rewards modelRewards, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException + { + LTLModelChecker mcLtl; + MDPRewards productRewards; + StateValues rewardsProduct, rewards; + MDPModelChecker mcProduct; + LTLModelChecker.LTLProduct product; + + // For LTL model checking routines + mcLtl = new LTLModelChecker(this); + + AcceptanceType[] allowedAcceptance = { + AcceptanceType.RABIN, + AcceptanceType.REACH + }; + + product = mcLtl.constructProductMDP(this, (MDP)model, expr, statesOfInterest, allowedAcceptance); + + // Adapt reward info to product model + productRewards = product.liftFromModel((MDPRewards) modelRewards); + + // Output product, if required + if (getExportProductTrans()) { + mainLog.println("\nExporting product transition matrix to file \"" + getExportProductTransFilename() + "\"..."); + product.getProductModel().exportToPrismExplicitTra(getExportProductTransFilename()); + } + if (getExportProductStates()) { + mainLog.println("\nExporting product state space to file \"" + getExportProductStatesFilename() + "\"..."); + PrismFileLog out = new PrismFileLog(getExportProductStatesFilename()); + VarList newVarList = (VarList) modulesFile.createVarList().clone(); + String daVar = "_da"; + while (newVarList.getIndex(daVar) != -1) { + daVar = "_" + daVar; + } + newVarList.addVar(0, new Declaration(daVar, new DeclarationIntUnbounded()), 1, null); + product.getProductModel().exportStates(Prism.EXPORT_PLAIN, newVarList, out); + out.close(); + } + + // Find accepting states + compute reachability rewards + BitSet acc; + if (product.getAcceptance() instanceof AcceptanceReach) { + // For a DFA, just collect the accept states + mainLog.println("\nSkipping end component detection since DRA is a DFA..."); + acc = ((AcceptanceReach)product.getAcceptance()).getGoalStates(); + } else { + // Usually, we have to detect end components in the product + mainLog.println("\nFinding accepting end components..."); + acc = mcLtl.findAcceptingECStates(product.getProductModel(), product.getAcceptance()); + } + mainLog.println("\nComputing reachability rewards..."); + mcProduct = new MDPModelChecker(this); + mcProduct.inheritSettings(this); + rewardsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachRewards((MDP)product.getProductModel(), productRewards, acc, false).soln, product.getProductModel()); + + // Mapping rewards in the original model + rewards = product.projectToOriginalModel(rewardsProduct); + rewardsProduct.clear(); + + return rewards; + } + // Numerical computation functions /** diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 43fcba5a..02e7d3f6 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -37,7 +37,10 @@ import parser.ast.ExpressionStrategy; import parser.ast.ExpressionTemporal; import parser.ast.ExpressionUnaryOp; import parser.ast.RewardStruct; +import parser.type.TypeBool; import parser.type.TypeDouble; +import parser.type.TypePathBool; +import parser.type.TypePathDouble; import prism.IntegerBound; import prism.OpRelOpBound; import prism.PrismComponent; @@ -884,7 +887,7 @@ public class ProbModelChecker extends NonProbModelChecker { StateValues rewards = null; - if (expr instanceof ExpressionTemporal) { + if (expr.getType() instanceof TypePathDouble) { ExpressionTemporal exprTemp = (ExpressionTemporal) expr; switch (exprTemp.getOperator()) { case ExpressionTemporal.R_F: @@ -903,6 +906,8 @@ public class ProbModelChecker extends NonProbModelChecker default: throw new PrismNotSupportedException("Explicit engine does not yet handle the " + exprTemp.getOperatorSymbol() + " reward operator"); } + } else if (expr.getType() instanceof TypePathBool || expr.getType() instanceof TypeBool) { + rewards = checkRewardPathFormula(model, modelRewards, expr, minMax, statesOfInterest); } if (rewards == null) @@ -1044,6 +1049,29 @@ public class ProbModelChecker extends NonProbModelChecker return StateValues.createFromDoubleArray(res.soln, model); } + /** + * Compute rewards for a path formula in a reward operator. + */ + protected StateValues checkRewardPathFormula(Model model, Rewards modelRewards, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException + { + if (expr instanceof ExpressionTemporal && ((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_F){ + return checkRewardReach(model, modelRewards, (ExpressionTemporal) expr, minMax, statesOfInterest); + } + else if (Expression.isCoSafeLTLSyntactic(expr)) { + return checkRewardCoSafeLTL(model, modelRewards, expr, minMax, statesOfInterest); + } + throw new PrismException("Invalid contents for an R operator: " + expr); + } + + /** + * Compute rewards for a co-safe LTL reward operator. + */ + protected StateValues checkRewardCoSafeLTL(Model model, Rewards modelRewards, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException + { + // To be overridden by subclasses + throw new PrismException("Computation not implemented yet"); + } + /** * Model check an S operator expression and return the values for all states. */ diff --git a/prism/src/explicit/Product.java b/prism/src/explicit/Product.java index b595d98a..74aac87e 100644 --- a/prism/src/explicit/Product.java +++ b/prism/src/explicit/Product.java @@ -29,6 +29,9 @@ package explicit; import java.util.BitSet; +import explicit.rewards.MDPRewards; +import explicit.rewards.MDPRewardsSimple; +import explicit.rewards.StateRewardsConstant; import parser.type.TypeBool; import parser.type.TypeDouble; import parser.type.TypeInt; @@ -142,6 +145,37 @@ public abstract class Product implements ModelTransformation ) begin = expr = Expression(false, false) { ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); ret.setUpperBound(expr); } - | begin = { ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); } - | begin = expr = Expression(false, false) { ret = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); ret.setUpperBound(expr); } - | begin = expr = Expression(prop, pathprop) { ret = new ExpressionTemporal(ExpressionTemporal.R_F, null, expr); } - | begin = { ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null); } ) + { begin = getToken(1); } + ( + // Normal reward operators + LOOKAHEAD( ) begin = expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); exprTemp.setUpperBound(expr); ret = exprTemp; } + | { ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); } + | expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); exprTemp.setUpperBound(expr); ret = exprTemp; } + | { ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null); } + // Path formula (including F "target") + | expr = Expression(prop, true) { ret = expr; } + ) { ret.setPosition(begin, getToken(0)); return ret; } } diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index 6b8b11e9..98e28ae8 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/prism/src/parser/visitor/TypeCheck.java @@ -516,7 +516,8 @@ public class TypeCheck extends ASTTraverse } } // Check argument - if (!(e.getExpression().getType() instanceof TypePathDouble)) { + Type typeArg = e.getExpression().getType(); + if (!(typeArg instanceof TypePathDouble || typeArg instanceof TypePathBool || typeArg instanceof TypeBool)) { throw new PrismLangException("Type error: Contents of R operator is invalid", e.getExpression()); } // Set type diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 1c8e1f6e..1db0630f 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -29,27 +29,44 @@ package prism; +import hybrid.PrismHybrid; + import java.io.File; import java.io.FileNotFoundException; -import java.util.*; - +import java.util.ArrayList; +import java.util.BitSet; +import java.util.List; +import java.util.Vector; + +import jdd.JDD; +import jdd.JDDNode; +import jdd.JDDVars; +import mtbdd.PrismMTBDD; +import odd.ODDUtils; +import parser.ast.Expression; +import parser.ast.ExpressionFunc; +import parser.ast.ExpressionProb; +import parser.ast.ExpressionQuant; +import parser.ast.ExpressionReward; +import parser.ast.ExpressionTemporal; +import parser.ast.ExpressionUnaryOp; +import parser.ast.PropertiesFile; +import parser.ast.RelOp; +import parser.type.TypeBool; +import parser.type.TypePathBool; +import parser.type.TypePathDouble; +import sparse.PrismSparse; +import strat.MDStrategyIV; import acceptance.AcceptanceOmega; import acceptance.AcceptanceOmegaDD; import acceptance.AcceptanceRabin; -import acceptance.AcceptanceRabinDD; import acceptance.AcceptanceReachDD; import acceptance.AcceptanceType; import automata.DA; import automata.LTL2DA; -import odd.ODDUtils; -import jdd.*; -import dv.*; +import dv.DoubleVector; +import dv.IntegerVector; import explicit.MinMax; -import mtbdd.*; -import sparse.*; -import strat.MDStrategyIV; -import hybrid.*; -import parser.ast.*; /* * Model checker for MDPs @@ -219,7 +236,7 @@ public class NondetModelChecker extends NonProbModelChecker // Compute rewards StateValues rewards = null; Expression expr2 = expr.getExpression(); - if (expr2 instanceof ExpressionTemporal) { + if (expr2.getType() instanceof TypePathDouble) { ExpressionTemporal exprTemp = (ExpressionTemporal) expr2; switch (exprTemp.getOperator()) { case ExpressionTemporal.R_C: @@ -236,7 +253,10 @@ public class NondetModelChecker extends NonProbModelChecker rewards = checkRewardReach(exprTemp, stateRewards, transRewards, minMax.isMin()); break; } + } else if (expr2.getType() instanceof TypePathBool || expr2.getType() instanceof TypeBool) { + rewards = checkRewardPathFormula(expr2, stateRewards, transRewards, minMax.isMin()); } + if (rewards == null) throw new PrismException("Unrecognised operator in R operator"); @@ -339,6 +359,7 @@ public class NondetModelChecker extends NonProbModelChecker modelProduct = model; // Go through probabilistic objectives and construct product MDP. + long l = System.currentTimeMillis(); boolean originalmodel = true; for (int i = 0; i < numObjectives; i++) { if (opsAndBounds.isProbabilityObjective(i)) { @@ -354,6 +375,8 @@ public class NondetModelChecker extends NonProbModelChecker originalmodel = false; } } + l = System.currentTimeMillis() - l; + mainLog.println("Total time for product construction: " + l / 1000.0 + " seconds."); // TODO: move this above // Replace min by max and <= by >= @@ -1030,6 +1053,8 @@ public class NondetModelChecker extends NonProbModelChecker daDDRowVars = new JDDVars(); daDDColVars = new JDDVars(); modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars); + l = System.currentTimeMillis() - l; + mainLog.println("Time for product construction: " + l / 1000.0 + " seconds."); mainLog.println(); modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo()); // Output product, if required @@ -1159,6 +1184,19 @@ public class NondetModelChecker extends NonProbModelChecker /** * Compute rewards for a reachability reward operator. */ + protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException + { + if (expr instanceof ExpressionTemporal && ((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_F){ + return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards, min); + } + else if (Expression.isCoSafeLTLSyntactic(expr)) { + return checkRewardCoSafeLTL(expr, stateRewards, transRewards, min); + } + throw new PrismException("Invalid contents for an R operator: " + expr); + } + + // reach reward + protected StateValues checkRewardReach(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException { JDDNode b; @@ -1185,6 +1223,150 @@ public class NondetModelChecker extends NonProbModelChecker return rewards; } + // co-safe LTL reward + + protected StateValues checkRewardCoSafeLTL(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException + { + LTLModelChecker mcLtl; + StateValues rewardsProduct = null, rewards = null; + Expression ltl; + Vector labelDDs; + DA da; + NondetModel modelProduct; + NondetModelChecker mcProduct; + JDDNode startMask; + JDDVars daDDRowVars, daDDColVars; + int i; + long l; + + if (Expression.containsTemporalTimeBounds(expr)) { + if (model.getModelType().continuousTime()) { + throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+"."); + } + + if (expr.isSimplePathFormula()) { + // Convert simple path formula to canonical form, + // 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 + // anymore, as converters may expect that the generated labels for maximal state + // formulas only appear positively + expr = Expression.convertSimplePathFormulaToCanonicalForm(expr); + } else { + 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")) { + 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); + + // 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 (prism.getSettings().getExportPropAut()) { + mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"..."); + PrismLog out = new PrismFileLog(prism.getSettings().getExportPropAutFilename()); + da.print(out, prism.getSettings().getExportPropAutType()); + out.close(); + //da.printDot(new java.io.PrintStream("da.dot")); + } + + // 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); + l = System.currentTimeMillis() - l; + mainLog.println("Time for product construction: " + l / 1000.0 + " seconds."); + mainLog.println(); + modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo()); + // 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())); + } catch (FileNotFoundException e) { + mainLog.printWarning("Could not export product transition matrix to file \"" + prism.getExportProductTransFilename() + "\""); + } + } + 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); + 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()); + + // 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(); + } 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(); + mainLog.println("\nComputing reachability rewards..."); + mcProduct = new NondetModelChecker(prism, modelProduct, null); + rewardsProduct = mcProduct.computeReachRewards(modelProduct.getTrans(), modelProduct.getTransActions(), modelProduct.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); + + // 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; + } + // ----------------------------------------------------------------------------------- // probability computation methods // ----------------------------------------------------------------------------------- @@ -1683,6 +1865,18 @@ public class NondetModelChecker extends NonProbModelChecker List zeroCostEndComponents = null; + // If required, export info about target states + if (prism.getExportTarget()) { + JDDNode labels[] = { model.getStart(), b }; + String labelNames[] = { "init", "target" }; + try { + mainLog.println("\nExporting target states info to file \"" + prism.getExportTargetFilename() + "\"..."); + PrismMTBDD.ExportLabels(labels, labelNames, "l", model.getAllDDRowVars(), model.getODD(), Prism.EXPORT_PLAIN, prism.getExportTargetFilename()); + } catch (FileNotFoundException e) { + mainLog.printWarning("Could not export target to file \"" + prism.getExportTargetFilename() + "\""); + } + } + // compute states which can't reach goal with probability 1 if (b.equals(JDD.ZERO)) { JDD.Ref(reach);