diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 328a94de..5930d6a5 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -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();