diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index b7e7f05f..659cea85 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -28,14 +28,20 @@ package explicit; import java.io.File; import java.util.BitSet; +import java.util.LinkedList; import java.util.List; import java.util.Map; +import java.util.Vector; import parser.ast.Expression; import parser.ast.ExpressionTemporal; import parser.ast.ExpressionUnaryOp; import parser.type.TypeDouble; +import parser.visitor.ASTTraverse; +import prism.DRA; +import prism.Pair; import prism.PrismException; +import prism.PrismLangException; import prism.PrismUtils; import explicit.rewards.MCRewards; @@ -56,7 +62,7 @@ public class DTMCModelChecker extends ProbModelChecker if (expr.isSimplePathFormula()) { return checkProbPathFormulaSimple(model, expr); } else { - throw new PrismException("Explicit engine does not yet handle LTL-style path formulas"); + return checkProbPathFormulaLTL(model, expr, false); } } @@ -187,6 +193,96 @@ public class DTMCModelChecker extends ProbModelChecker return probs; } + /** + * LTL-like path formula for P operator + */ + protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual) throws PrismException + { + LTLModelChecker mcLtl; + StateValues probsProduct, probs; + Expression ltl; + DRA dra; + Model modelProduct; + DTMCModelChecker mcProduct; + long time; + + // Can't do LTL with time-bounded variants of the temporal operators + try { + expr.accept(new ASTTraverse() + { + public void visitPre(ExpressionTemporal e) throws PrismLangException + { + if (e.getLowerBound() != null) + throw new PrismLangException(e.getOperatorSymbol()); + if (e.getUpperBound() != null) + throw new PrismLangException(e.getOperatorSymbol()); + } + }); + } catch (PrismLangException e) { + String s = "Temporal operators (like " + e.getMessage() + ")"; + s += " cannot have time bounds for LTL properties"; + throw new PrismException(s); + } + + // For LTL model checking routines + mcLtl = new LTLModelChecker(); + + // Model check maximal state formulas + Vector labelBS = new Vector(); + ltl = mcLtl.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelBS); + + // Convert LTL formula to deterministic Rabin automaton (DRA) + mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); + time = System.currentTimeMillis(); + dra = LTLModelChecker.convertLTLFormulaToDRA(ltl); + int draSize = dra.size(); + mainLog.println("\nDRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs."); + // dra.print(System.out); + time = System.currentTimeMillis() - time; + mainLog.println("\nTime for Rabin translation: " + time / 1000.0 + " seconds."); + + // Build product of Markov chain and automaton + // (note: might be a CTMC - StochModelChecker extends this class) + mainLog.println("\nConstructing MC-DRA product..."); + Pair pair = mcLtl.constructProductMC(dra, model, labelBS); + modelProduct = pair.first; + int invMap[] = pair.second; + int modelProductSize = modelProduct.getNumStates(); + + // Find accepting maximum end components + mainLog.println("\nFinding accepting end components..."); + + // Compute accepting BSCCs + BitSet acceptingBSCCs = mcLtl.findAcceptingBSCCs(dra, modelProduct, invMap, sccMethod); + mainLog.println(acceptingBSCCs); + + // Compute reachability probabilities + mainLog.println("\nComputing reachability probabilities..."); + mcProduct = new DTMCModelChecker(); + + probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((DTMC) modelProduct, acceptingBSCCs).soln, modelProduct); + + // Mapping probabilities in the original model + double[] probsProductDbl = probsProduct.getDoubleArray(); + double[] probsDbl = new double[modelProductSize]; + + LinkedList queue = new LinkedList(); + for (int s : model.getInitialStates()) + queue.add(s); + + for (int i = 0; i < invMap.length; i++) { + int j = invMap[i]; + int s = j / draSize; + // TODO: check whether this is the right way to compute probabilities in the original model + probsDbl[s] = Math.max(probsDbl[s], probsProductDbl[i]); + } + + probs = StateValues.createFromDoubleArray(probsDbl, model); + probsProduct.clear(); + + return probs; + } + /** * Compute rewards for the contents of an R operator. */ diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index 900b02aa..d9afa1e9 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/prism/src/explicit/DTMCSimple.java @@ -195,6 +195,14 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple distr.set(j, prob); } + /** + * Returns the probability for a transition + */ + public double getProbability(int i, int j) + { + return trans.get(i).get(j); + } + /** * Add to the probability for a transition. */ diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java new file mode 100644 index 00000000..3ffae59f --- /dev/null +++ b/prism/src/explicit/LTLModelChecker.java @@ -0,0 +1,237 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Alessandro Bruni (Technical University of Denmark) +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package explicit; + +import java.awt.Point; +import java.util.Arrays; +import java.util.BitSet; +import java.util.LinkedList; +import java.util.List; +import java.util.Vector; + +import parser.ast.Expression; +import parser.ast.ExpressionBinaryOp; +import parser.ast.ExpressionLabel; +import parser.ast.ExpressionTemporal; +import parser.ast.ExpressionUnaryOp; +import parser.type.TypeBool; +import parser.type.TypePathBool; +import prism.DRA; +import prism.LTL2RabinLibrary; +import prism.Pair; +import prism.PrismException; +import explicit.SCCComputer.SCCMethod; + +public class LTLModelChecker +{ + + public static DRA convertLTLFormulaToDRA(Expression ltl) throws PrismException + { + return LTL2RabinLibrary.convertLTLFormulaToDRA(ltl); + } + + public Expression checkMaximalStateFormulas(ProbModelChecker mc, Model model, Expression expr, Vector labelBS) throws PrismException + { + // A state formula + if (expr.getType() instanceof TypeBool) { + // Model check + StateValues sv = mc.checkExpression(model, expr); + if (sv.type != TypeBool.getInstance() || sv.valuesB == null) { + throw new PrismException("Excepting a boolean value here!"); + } + BitSet bs = sv.getBitSet(); + // Detect special cases (true, false) for optimisation + if (bs.isEmpty()) { + return Expression.False(); + } + BitSet tmp = (BitSet) bs.clone(); + tmp.flip(0, tmp.length()); + if (tmp.isEmpty()) { + return Expression.True(); + } + // See if we already have an identical result + // (in which case, reuse it) + int i = labelBS.indexOf(bs); + if (i != -1) { + return new ExpressionLabel("L" + i); + } + // Otherwise, add result to list, return new label + labelBS.add(bs); + return new ExpressionLabel("L" + (labelBS.size() - 1)); + } + // A path formula (recurse, modify, return) + else if (expr.getType() instanceof TypePathBool) { + if (expr instanceof ExpressionBinaryOp) { + ExpressionBinaryOp exprBinOp = (ExpressionBinaryOp) expr; + exprBinOp.setOperand1(checkMaximalStateFormulas(mc, model, exprBinOp.getOperand1(), labelBS)); + exprBinOp.setOperand2(checkMaximalStateFormulas(mc, model, exprBinOp.getOperand2(), labelBS)); + } else if (expr instanceof ExpressionUnaryOp) { + ExpressionUnaryOp exprUnOp = (ExpressionUnaryOp) expr; + exprUnOp.setOperand(checkMaximalStateFormulas(mc, model, exprUnOp.getOperand(), labelBS)); + } else if (expr instanceof ExpressionTemporal) { + ExpressionTemporal exprTemp = (ExpressionTemporal) expr; + if (exprTemp.getOperand1() != null) { + exprTemp.setOperand1(checkMaximalStateFormulas(mc, model, exprTemp.getOperand1(), labelBS)); + } + if (exprTemp.getOperand2() != null) { + exprTemp.setOperand2(checkMaximalStateFormulas(mc, model, exprTemp.getOperand2(), labelBS)); + } + } + } + return expr; + } + + /** + * Constructs the product of a DTMC and a DRA automaton + * + * @param dra the DRA representing the LTL formula + * @param model the original model + * @param labelBS a set of labels for states in the original model + * @return a Pair consisting of the product model and a map from + * (s_i * draSize + q_j) to the right state in the DRA product + * @throws PrismException + */ + public Pair constructProductMC(DRA dra, Model model, Vector labelBS) throws PrismException + { + if (!(model instanceof DTMCSimple)) { + throw new PrismException("Expecting a DTMC here"); + } + + DTMCSimple modelDTMC = (DTMCSimple) model; + DTMCSimple prodModel = new DTMCSimple(); + + int draSize = dra.size(); + int modelNumStates = modelDTMC.getNumStates(); + int prodNumStates = modelNumStates * draSize; + + // Encoding: + // each state s' = = s * draSize + q + // s(s') = s' / draSize + // q(s') = s' % draSize + + // Initial states + LinkedList queue = new LinkedList(); + int map[] = new int[prodNumStates]; + Arrays.fill(map, -1); + int q_0 = dra.getStartState(); + for (int s_0 : model.getInitialStates()) { + queue.add(new Point(s_0, q_0)); + prodModel.addState(); + prodModel.addInitialState(prodModel.getNumStates() - 1); + map[s_0 * draSize + q_0] = prodModel.getNumStates() - 1; + } + + // Product states + BitSet visited = new BitSet(prodNumStates); + int q_1 = 0, q_2 = 0, s_1 = 0, s_2 = 0; + while (!queue.isEmpty()) { + Point p = queue.pop(); + s_1 = p.x; + q_1 = p.y; + visited.set(s_1 * draSize + q_1); + int numEdges = dra.getNumEdges(q_1); + for (int j = 0; j < numEdges; j++) { + q_2 = dra.getEdgeDest(q_1, j); + BitSet label = computeLabel(dra, labelBS, modelNumStates, q_1, j); + for (s_2 = label.nextSetBit(0); s_2 != -1; s_2 = label.nextSetBit(s_2 + 1)) { + if (!visited.get(s_2 * draSize + q_2) && map[s_2 * draSize + q_2] == -1) { + queue.add(new Point(s_2, q_2)); + prodModel.addState(); + map[s_2 * draSize + q_2] = prodModel.getNumStates() - 1; + } + double prob = modelDTMC.getProbability(s_1, s_2); + prodModel.setProbability(map[s_1 * draSize + q_1], map[s_2 * draSize + q_2], prob); + } + } + } + + 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); + + return new Pair(prodModel, invMap); + } + + private BitSet computeLabel(DRA dra, Vector labelBS, int origStates, int q_1, int j) + { + int numAPs = dra.getAPList().size(); + List apList = dra.getAPList(); + BitSet label = new BitSet(origStates); + label.flip(0, origStates); + for (int k = 0; k < numAPs; k++) { + int bsID = Integer.parseInt(apList.get(k).substring(1)); + BitSet bs = labelBS.get(bsID); + if (dra.getEdgeLabel(q_1, j).get(k)) { + label.and(bs); + } else { + label.andNot(bs); + } + } + return label; + } + + public BitSet findAcceptingBSCCs(DRA dra, Model modelProduct, int invMap[], SCCMethod sccMethod) + { + // Compute bottom strongly connected components (BSCCs) + SCCComputer sccComputer = SCCComputer.createSCCComputer(sccMethod, modelProduct); + sccComputer.computeBSCCs(); + List bsccs = sccComputer.getBSCCs(); + + int draSize = dra.size(); + + BitSet result = new BitSet(); + for (BitSet bscc : bsccs) { + int numAcceptancePairs = dra.getNumAcceptancePairs(); + boolean isLEmpty = true; + boolean isKEmpty = true; + for (int acceptancePair = 0; acceptancePair < numAcceptancePairs && isLEmpty && isKEmpty; acceptancePair++) { + BitSet L = dra.getAcceptanceL(acceptancePair); + BitSet K = dra.getAcceptanceK(acceptancePair); + + for (int state = bscc.nextSetBit(0); state != -1; state = bscc.nextSetBit(state + 1)) { + int draState = invMap[state] % draSize; + isLEmpty &= !L.get(draState); + isKEmpty &= !K.get(draState); + } + } + + if (isLEmpty && !isKEmpty) { + // Acceptance condition + result.or(bscc); + } + } + + return result; + } + +} diff --git a/prism/src/prism/Pair.java b/prism/src/prism/Pair.java new file mode 100644 index 00000000..f577c140 --- /dev/null +++ b/prism/src/prism/Pair.java @@ -0,0 +1,42 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package prism; + +/** + * Simple class to store a pair of values. + */ +public class Pair +{ + public X first; + public Y second; + + public Pair(X first, Y second) + { + this.first = first; + this.second = second; + } +}