|
|
|
@ -146,7 +146,7 @@ public class StateModelChecker implements ModelChecker |
|
|
|
|
|
|
|
// Create storage for result |
|
|
|
result = new Result(); |
|
|
|
|
|
|
|
|
|
|
|
// The final result of model checking will be a single value. If the expression to be checked does not |
|
|
|
// already yield a single value (e.g. because a filter has not been explicitly included), we need to wrap |
|
|
|
// a new (invisible) filter around it. Note that some filters (e.g. print/argmin/argmax) also do not |
|
|
|
@ -179,7 +179,7 @@ public class StateModelChecker implements ModelChecker |
|
|
|
// We stop any additional explanation being displayed to avoid confusion. |
|
|
|
exprFilter.setExplanationEnabled(false); |
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
// For any case where a new filter was created above... |
|
|
|
if (exprFilter != null) { |
|
|
|
// Make it invisible (not that it will be displayed) |
|
|
|
@ -202,7 +202,7 @@ public class StateModelChecker implements ModelChecker |
|
|
|
resultString += " (" + expr.getResultName().toLowerCase() + ")"; |
|
|
|
resultString += ": " + result.getResultString(); |
|
|
|
mainLog.print("\n" + resultString + "\n"); |
|
|
|
|
|
|
|
|
|
|
|
// Clean up |
|
|
|
vals.clear(); |
|
|
|
|
|
|
|
@ -340,8 +340,6 @@ public class StateModelChecker implements ModelChecker |
|
|
|
res1.clear(); |
|
|
|
if (res2 != null) |
|
|
|
res2.clear(); |
|
|
|
if (res3 != null) |
|
|
|
res3.clear(); |
|
|
|
throw e; |
|
|
|
} |
|
|
|
|
|
|
|
@ -391,8 +389,6 @@ public class StateModelChecker implements ModelChecker |
|
|
|
} catch (PrismException e) { |
|
|
|
if (res1 != null) |
|
|
|
res1.clear(); |
|
|
|
if (res2 != null) |
|
|
|
res2.clear(); |
|
|
|
throw e; |
|
|
|
} |
|
|
|
|
|
|
|
@ -591,8 +587,6 @@ public class StateModelChecker implements ModelChecker |
|
|
|
} catch (PrismException e) { |
|
|
|
if (res1 != null) |
|
|
|
res1.clear(); |
|
|
|
if (res2 != null) |
|
|
|
res2.clear(); |
|
|
|
throw e; |
|
|
|
} |
|
|
|
dd1 = res1.convertToStateValuesMTBDD().getJDDNode(); |
|
|
|
@ -632,13 +626,7 @@ public class StateModelChecker implements ModelChecker |
|
|
|
int i, n, op = expr.getOperator(); |
|
|
|
|
|
|
|
// Check operand recursively |
|
|
|
try { |
|
|
|
res1 = checkExpression(expr.getOperand()); |
|
|
|
} catch (PrismException e) { |
|
|
|
if (res1 != null) |
|
|
|
res1.clear(); |
|
|
|
throw e; |
|
|
|
} |
|
|
|
res1 = checkExpression(expr.getOperand()); |
|
|
|
|
|
|
|
// Parentheses are easy - nothing to do: |
|
|
|
if (op == ExpressionUnaryOp.PARENTH) |
|
|
|
@ -708,13 +696,7 @@ public class StateModelChecker implements ModelChecker |
|
|
|
int i, n, op = expr.getNameCode(); |
|
|
|
|
|
|
|
// Check operand recursively |
|
|
|
try { |
|
|
|
res1 = checkExpression(expr.getOperand(0)); |
|
|
|
} catch (PrismException e) { |
|
|
|
if (res1 != null) |
|
|
|
res1.clear(); |
|
|
|
throw e; |
|
|
|
} |
|
|
|
res1 = checkExpression(expr.getOperand(0)); |
|
|
|
// Symbolic |
|
|
|
if (res1 instanceof StateValuesMTBDD) { |
|
|
|
dd1 = ((StateValuesMTBDD) res1).getJDDNode(); |
|
|
|
@ -765,8 +747,6 @@ public class StateModelChecker implements ModelChecker |
|
|
|
} catch (PrismException e) { |
|
|
|
if (res1 != null) |
|
|
|
res1.clear(); |
|
|
|
if (res2 != null) |
|
|
|
res2.clear(); |
|
|
|
throw e; |
|
|
|
} |
|
|
|
// If both operands are symbolic, result will be symbolic |
|
|
|
@ -851,13 +831,7 @@ public class StateModelChecker implements ModelChecker |
|
|
|
boolean symbolic; |
|
|
|
|
|
|
|
// Check first operand recursively |
|
|
|
try { |
|
|
|
res1 = checkExpression(expr.getOperand(0)); |
|
|
|
} catch (PrismException e) { |
|
|
|
if (res1 != null) |
|
|
|
res1.clear(); |
|
|
|
throw e; |
|
|
|
} |
|
|
|
res1 = checkExpression(expr.getOperand(0)); |
|
|
|
// Go through remaining operands |
|
|
|
// Switch to explicit as soon as an operand is explicit |
|
|
|
n = expr.getNumOperands(); |
|
|
|
|