s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

explicit: add support for CTL model checking 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11171 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 10 years ago
parent
802abccbce
commit
38617a9184
2 changed files with 432 additions and 3 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 54
      prism/src/explicit/CTMCModelChecker.java
  2. 381
      prism/src/explicit/NonProbModelChecker.java

54
prism/src/explicit/CTMCModelChecker.java
View File

@ -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.
*/

381
prism/src/explicit/NonProbModelChecker.java
View File

@ -3,6 +3,7 @@
// Copyright (c) 2002-
// Authors:
// * Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
// * Joachim Klein <klein@tcs.inf.tu-dresden.de> (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 ].
* <br>
* '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 ].
* <br>
* 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<Integer> 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<Integer> 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;
}
}
Write Preview
Loading…
Cancel
Save