diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index ccdacd7c..ea0ebbd0 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -836,7 +836,59 @@ public class CTMCModelChecker extends ProbModelChecker mcDTMC.inheritSettings(this); return mcDTMC; } - + + // ------------------ CTL model checking ------------------------------------------------ + // + // For CTL model checking, the actual computation happens in the + // embedded DTMC (due to the possibility of a zero exit rate turning + // into a self-loop. + // So, we don't override the check... methods (so that recursive computation + // of the subformulas happens in the CTMCModelChecker), but override the + // compute... methods to use a DTMCModelChecker for the computations instead + + @Override + public BitSet computeExistsNext(Model model, BitSet target, BitSet statesOfInterest) throws PrismException + { + // Construct embedded DTMC and do CTL computation on that + mainLog.println("Building embedded DTMC..."); + DTMC dtmcEmb = ((CTMC)model).getImplicitEmbeddedDTMC(); + return createDTMCModelChecker().computeExistsNext(dtmcEmb, target, statesOfInterest); + } + + @Override + public BitSet computeForAllNext(Model model, BitSet target, BitSet statesOfInterest) throws PrismException + { + // Construct embedded DTMC and do CTL computation on that + mainLog.println("Building embedded DTMC..."); + DTMC dtmcEmb = ((CTMC)model).getImplicitEmbeddedDTMC(); + return createDTMCModelChecker().computeForAllNext(dtmcEmb, target, statesOfInterest); + } + + @Override + public BitSet computeExistsUntil(Model model, BitSet A, BitSet B) throws PrismException + { + // Construct embedded DTMC and do CTL computation on that + mainLog.println("Building embedded DTMC..."); + DTMC dtmcEmb = ((CTMC)model).getImplicitEmbeddedDTMC(); + return createDTMCModelChecker().computeExistsUntil(dtmcEmb, A, B); + } + + public BitSet computeExistsGlobally(Model model, BitSet A) throws PrismException + { + // Construct embedded DTMC and do CTL computation on that + mainLog.println("Building embedded DTMC..."); + DTMC dtmcEmb = ((CTMC)model).getImplicitEmbeddedDTMC(); + return createDTMCModelChecker().computeExistsGlobally(dtmcEmb, A); + } + + public BitSet computeExistsRelease(Model model, BitSet A, BitSet B) throws PrismException + { + // Construct embedded DTMC and do CTL computation on that + mainLog.println("Building embedded DTMC..."); + DTMC dtmcEmb = ((CTMC)model).getImplicitEmbeddedDTMC(); + return createDTMCModelChecker().computeExistsRelease(dtmcEmb, A, B); + } + /** * Simple test program. */ diff --git a/prism/src/explicit/NonProbModelChecker.java b/prism/src/explicit/NonProbModelChecker.java index 9d52c2ea..11ae4391 100644 --- a/prism/src/explicit/NonProbModelChecker.java +++ b/prism/src/explicit/NonProbModelChecker.java @@ -3,6 +3,7 @@ // Copyright (c) 2002- // Authors: // * Dave Parker (University of Birmingham/Oxford) +// * Joachim Klein (TU Dresden) // //------------------------------------------------------------------------------ // @@ -27,10 +28,15 @@ package explicit; import java.util.BitSet; +import java.util.Iterator; +import common.IterableBitSet; +import common.IterableStateSet; import parser.ast.Expression; import parser.ast.ExpressionExists; import parser.ast.ExpressionForAll; +import parser.ast.ExpressionTemporal; +import parser.ast.ExpressionUnaryOp; import prism.PrismComponent; import prism.PrismException; import prism.PrismNotSupportedException; @@ -55,11 +61,11 @@ public class NonProbModelChecker extends StateModelChecker // E operator if (expr instanceof ExpressionExists) { - throw new PrismNotSupportedException("CTL model checking is not yet supported by the explicit engine"); + return checkExpressionExists(model, ((ExpressionExists)expr).getExpression(), statesOfInterest); } // A operator else if (expr instanceof ExpressionForAll) { - throw new PrismNotSupportedException("CTL model checking is not yet supported by the explicit engine"); + return checkExpressionForAll(model, ((ExpressionForAll)expr).getExpression(), statesOfInterest); } // Otherwise, use the superclass else { @@ -68,5 +74,376 @@ public class NonProbModelChecker extends StateModelChecker return res; } + + /** + * Compute the set of states satisfying E[ expr ]. + *
+ * 'expr' has to be a simple path formula. + * + * @param model the model + * @param expr the expression for 'expr' + * @param statesOfInterest the states of interest ({@code null} = all states) + * @return a boolean StateValues, with {@code true} for all states satisfying E[ expr ] + */ + protected StateValues checkExpressionExists(Model model, Expression expr, BitSet statesOfInterest) throws PrismException + { + // Check whether this is a simple path formula (i.e. CTL, not LTL) + if (!expr.isSimplePathFormula()) { + throw new PrismNotSupportedException("(Non-probabilistic) LTL model checking is not supported"); + } + + // convert to either + // (1) a U b + // (2) !(a U b) + // (3) X a + expr = Expression.convertSimplePathFormulaToCanonicalForm(expr); + + // next-step (3) + if (expr instanceof ExpressionTemporal && + ((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_X) { + if (((ExpressionTemporal)expr).hasBounds()) { + throw new PrismNotSupportedException("Model checking of bounded CTL operators is not supported"); + } + return checkExistsNext(model, ((ExpressionTemporal) expr).getOperand2(), statesOfInterest); + } + + // until + boolean negated = false; + if (Expression.isNot(expr)) { + // (2) !(a U b) + negated = true; + expr = ((ExpressionUnaryOp)expr).getOperand(); + } + + ExpressionTemporal exprTemp = (ExpressionTemporal) expr; + assert (exprTemp.getOperator() == ExpressionTemporal.P_U); + + if (exprTemp.hasBounds()) { + throw new PrismNotSupportedException("Model checking of bounded CTL operators is not supported"); + } + + StateValues result; + + if (negated) { + // compute E[ !a R !b ] instead of E[ !(a U b) ] + result = checkExistsRelease(model, + Expression.Not(exprTemp.getOperand1()), + Expression.Not(exprTemp.getOperand2())); + } else { + // compute E[ a U b ] + result = checkExistsUntil(model, exprTemp.getOperand1(), exprTemp.getOperand2()); + } + + return result; + } + + /** + * Compute the set of states satisfying A[ expr ]. + *
+ * This is computed by determining the set of states not satisfying E[ !expr ]. + * 'expr' has to be a simple path formula. + * + * @param model the model + * @param expr the expression for 'expr' + * @param statesOfInterest the states of interest ({@code null} = all states) + * @return a boolean StateValues, with {@code true} for all states satisfying A[ expr ] + */ + protected StateValues checkExpressionForAll(Model model, Expression expr, BitSet statesOfInterest) throws PrismException + { + StateValues result = checkExpressionExists(model, Expression.Not(expr), statesOfInterest); + result.complement(); + + return result; + } + + /** + * Compute the set of states satisfying E[ X expr ]. + * @param model the model + * @param expr the expression for 'expr' + * @param statesOfInterest the states of interest ({@code null} = all states) + * @return a boolean StateValues, with {@code true} for all states satisfying E[ X expr ] + */ + protected StateValues checkExistsNext(Model model, Expression expr, BitSet statesOfInterest) throws PrismException + { + BitSet target = checkExpression(model, expr, null).getBitSet(); + BitSet result = computeExistsNext(model, target, statesOfInterest); + + return StateValues.createFromBitSet(result, model); + } + + /** + * Compute the set of states satisfying E[ X "target" ]. + * @param model the model + * @param target the BitSet of states for target + * @param statesOfInterest the states of interest ({@code null} = all states) + * @return a boolean StateValues, with {@code true} for all states satisfying E[ X "target" ] + */ + public BitSet computeExistsNext(Model model, BitSet target, BitSet statesOfInterest) throws PrismException + { + BitSet result = new BitSet(); + + for (int s : new IterableStateSet(statesOfInterest, model.getNumStates())) { + // for each state of interest, check whether there is a transition to the 'target' + if (model.someSuccessorsInSet(s, target)) { + result.set(s); + } + } + + return result; + } + + /** + * Compute the set of states satisfying A[ X expr ]. + * @param model the model + * @param expr the expression for 'expr' + * @param statesOfInterest the states of interest ({@code null} = all states) + * @return a boolean StateValues, with {@code true} for all states satisfying A[ X expr ] + */ + protected StateValues checkForAllNext(Model model, Expression expr, BitSet statesOfInterest) throws PrismException + { + BitSet target = checkExpression(model, expr, null).getBitSet(); + BitSet result = new BitSet(); + + for (int s : new IterableStateSet(statesOfInterest, model.getNumStates())) { + // for each state of interest, check whether all transitions go to 'target' + if (model.allSuccessorsInSet(s, target)) { + result.set(s); + } + } + + return StateValues.createFromBitSet(result, model); + } + + /** + * Compute the set of states satisfying A[ X "target" ]. + * @param model the model + * @param target the BitSet of states in target + * @param statesOfInterest the states of interest ({@code null} = all states) + * @return a boolean StateValues, with {@code true} for all states satisfying A[ X "target" ] + */ + public BitSet computeForAllNext(Model model, BitSet target, BitSet statesOfInterest) throws PrismException + { + BitSet result = new BitSet(); + + for (int s : new IterableStateSet(statesOfInterest, model.getNumStates())) { + // for each state of interest, check whether all transitions go to 'target' + if (model.allSuccessorsInSet(s, target)) { + result.set(s); + } + } + + return result; + } + + + /** + * Compute the set of states satisfying E[ a U b ]. + * @param model the model + * @param exprA the expression for 'a' + * @param exprB the expression for 'b' + * @return a boolean StateValues, with {@code true} for all states satisfying E[ a U b ] + */ + protected StateValues checkExistsUntil(Model model, Expression exprA, Expression exprB) throws PrismException { + // the set of states satisfying exprA + BitSet A = checkExpression(model, exprA, null).getBitSet(); + // the set of states satisfying exprB + BitSet B = checkExpression(model, exprB, null).getBitSet(); + + BitSet result = computeExistsUntil(model, A, B); + + return StateValues.createFromBitSet(result, model); + } + + /** + * Compute the set of states satisfying E[ "a" U "b" ]. + * @param model the model + * @param A the BitSet of states for "a" + * @param B the BitSet of states for "b" + * @return a boolean StateValues, with {@code true} for all states satisfying E[ "a" U "b" ] + */ + public BitSet computeExistsUntil(Model model, BitSet A, BitSet B) throws PrismException + { + PredecessorRelation pre = model.getPredecessorRelation(this, true); + return pre.calculatePreStar(A, B, B); + } + + /** + * Compute the set of states satisfying E[ G a ]. + * @param model the model + * @param exprA the expression for 'a' + * @return a boolean StateValues, with {@code true} for all states satisfying E[ G a ] + */ + protected StateValues checkExistsGlobally(Model model, Expression exprA) throws PrismException + { + return checkExistsRelease(model, Expression.False(), exprA); + } + + /** + * Compute the set of states satisfying E[ G "a" ]. + * @param model the model + * @param A the BitSet of states for "a" + * @return a boolean StateValues, with {@code true} for all states satisfying E[ G "a" ] + */ + public BitSet computeExistsGlobally(Model model, BitSet A) throws PrismException + { + return computeExistsRelease(model, new BitSet(), A); + } + + /** + * Compute the set of states satisfying E[ a R b ], i.e., from which there + * exists a path satisfying G b or b U (a&b) + * @param model the model + * @param exprA the expression for 'a' + * @param exprB the expression for 'b' + * @return a boolean StateValues, with {@code true} for all states satisfying E[ a R b ] + */ + protected StateValues checkExistsRelease(Model model, Expression exprA, Expression exprB) throws PrismException + { + // the set of states satisfying exprA + BitSet A = checkExpression(model, exprA, null).getBitSet(); + // the set of states satisfying exprB + BitSet B = checkExpression(model, exprB, null).getBitSet(); + + PredecessorRelation pre = model.getPredecessorRelation(this, true); + + // the intersection of A and B + // these states surely satisfy E[ a R b ] + BitSet AandB = (BitSet) A.clone(); + AandB.and(B); + + // The set T contains all states for which E[ a R b ] has not yet been disproven + // Initially, this contains all 'B' states + BitSet T = (BitSet) B.clone(); + + // the set E contains all states that have not yet been visited + // and for which we have proven that they do not satisfy E[ a R b ] + // Initially, it contains the complement of 'T' + BitSet E = (BitSet) T.clone(); + E.flip(0, model.getNumStates()); + + // NOTE: The correctness relies on the fact that both + // getSuccessorsIterator and pre.getPre are exactly the two sides + // of the underlying edge relation, i.e., that the number of entries + // is consistent. If the PredecessorRelation semantics are changed + // later on, we have to adapt here as well... + + // for all states s in T \ AandB, we compute count[s], the number of successors + // according to getSuccessorsIterator + int count[] = new int[model.getNumStates()]; + for (int s : IterableBitSet.getSetBits(T)) { + if (AandB.get(s)) continue; + + int i=0; + for (Iterator it = model.getSuccessorsIterator(s); it.hasNext(); it.next()) { + i++; + } + count[s]=i; + } + + while (!E.isEmpty()) { + // get the first element of E + int t = E.nextSetBit(0); + // and mark it as processed + E.clear(t); + + // We know that t does not satisfy E[ a R b ]. + // Any predecessor s of t can be shown to not satisfy E[ a R b ] + // if there are no remaining successors into T, i.e, if count[s]==0 + + // For all predecessors s of t.... + for (int s : pre.getPre(t)) { + // ... ignore if we have already proven that it does not satisfy E[ a R b ] + if (!T.get(s)) continue; + + // decrement count, because s can not use t to stay in T + count[s]--; + if (count[s] == 0 && !AandB.get(s)) { + // the count is zero and s is not safe because it's in AandB + // -> remove from T and add to E + T.clear(s); + E.set(s); + } + } + } + + return StateValues.createFromBitSet(T, model); + } + + /** + * Compute the set of states satisfying E[ "a" R "b" ], i.e., from which there + * exists a path satisfying G "b" or "b" U ("a&b") + * @param model the model + * @param A the BitSet for the states in "a" + * @param A the BitSet for the states in "a" + * @return a boolean StateValues, with {@code true} for all states satisfying E[ "a" R "b" ] + */ + public BitSet computeExistsRelease(Model model, BitSet A, BitSet B) throws PrismException + { + PredecessorRelation pre = model.getPredecessorRelation(this, true); + + // the intersection of A and B + // these states surely satisfy E[ a R b ] + BitSet AandB = (BitSet) A.clone(); + AandB.and(B); + + // The set T contains all states for which E[ a R b ] has not yet been disproven + // Initially, this contains all 'B' states + BitSet T = (BitSet) B.clone(); + + // the set E contains all states that have not yet been visited + // and for which we have proven that they do not satisfy E[ a R b ] + BitSet E = new BitSet(); + // Initially, it contains the complement of 'T' + E.set(0, model.getNumStates(), true); + E.andNot(T); + + // TODO: Important: The correctness relies on the fact that + // the number of predecessors provided by pre.getPre() + // and the number of successors provided by getSuccessorsIterator() + // mirror each other. If PredecessorRelation is changed later on, + // take this into account... + + // for all states s in T \ AandB, we compute count[s], the number of (unique) successors + int count[] = new int[model.getNumStates()]; + for (int s : IterableBitSet.getSetBits(T)) { + if (AandB.get(s)) continue; + + int i=0; + for (Iterator it = model.getSuccessorsIterator(s); it.hasNext(); it.next()) { + i++; + } + count[s]=i; + } + + while (!E.isEmpty()) { + // get the first element of E + int t = E.nextSetBit(0); + // and mark it as processed + E.clear(t); + + // We know that t does not satisfy E[ a R b ]. + // Any predecessor s of t can be shown to not satisfy E[ a R b ] + // if there are no remaining successors into T, i.e, if count[s]==0 + + // For all predecessors s of t.... + + for (int s : pre.getPre(t)) { + // ... ignore if we have already proven that it does not satisfy E[ a R b ] + if (!T.get(s)) continue; + + // decrement count, because s can not use t to stay in T + count[s]--; + if (count[s] == 0 && !AandB.get(s)) { + // the count is zero and s is not safe because it's in AandB + // -> remove from T and add to E + T.clear(s); + E.set(s); + } + } + } + + return T; + } + }