From 03d83d4abb5a5a1047863f5afab5db4e8596bd2e Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 8 Jan 2018 19:55:17 +0100 Subject: [PATCH] Simplify: Preserve type for 0-x to -x simplification Plus test case, fixes #34. --- .../bugfixes/simplify-unary-minus-issue-34.prism | 11 +++++++++++ .../simplify-unary-minus-issue-34.prism.args | 5 +++++ .../simplify-unary-minus-issue-34.prism.props | 2 ++ prism/src/parser/visitor/Simplify.java | 16 ++++++++++++---- 4 files changed, 30 insertions(+), 4 deletions(-) create mode 100644 prism-tests/bugfixes/simplify-unary-minus-issue-34.prism create mode 100644 prism-tests/bugfixes/simplify-unary-minus-issue-34.prism.args create mode 100644 prism-tests/bugfixes/simplify-unary-minus-issue-34.prism.props diff --git a/prism-tests/bugfixes/simplify-unary-minus-issue-34.prism b/prism-tests/bugfixes/simplify-unary-minus-issue-34.prism new file mode 100644 index 00000000..90bf0f29 --- /dev/null +++ b/prism-tests/bugfixes/simplify-unary-minus-issue-34.prism @@ -0,0 +1,11 @@ +// Test case for https://github.com/prismmodelchecker/prism/issues/34 +// Expression simplification for 0-x does not preserve type +// Error during model building (explicit), simulation + +dtmc + +module M1 + s : [0..1] init 0; + + [] true -> 1/2:(s'=0) + 1/2:(s'=max(1,0-s)); +endmodule diff --git a/prism-tests/bugfixes/simplify-unary-minus-issue-34.prism.args b/prism-tests/bugfixes/simplify-unary-minus-issue-34.prism.args new file mode 100644 index 00000000..7bb2673f --- /dev/null +++ b/prism-tests/bugfixes/simplify-unary-minus-issue-34.prism.args @@ -0,0 +1,5 @@ +-explicit +-hybrid +-mtbdd +-sparse +-exact diff --git a/prism-tests/bugfixes/simplify-unary-minus-issue-34.prism.props b/prism-tests/bugfixes/simplify-unary-minus-issue-34.prism.props new file mode 100644 index 00000000..1b0c0e0e --- /dev/null +++ b/prism-tests/bugfixes/simplify-unary-minus-issue-34.prism.props @@ -0,0 +1,2 @@ +// RESULT: 1 +P=?[F s=1] diff --git a/prism/src/parser/visitor/Simplify.java b/prism/src/parser/visitor/Simplify.java index bb339268..4e12ac92 100644 --- a/prism/src/parser/visitor/Simplify.java +++ b/prism/src/parser/visitor/Simplify.java @@ -105,15 +105,23 @@ public class Simplify extends ASTTraverseModify case ExpressionBinaryOp.MINUS: if (Expression.isInt(e.getOperand2()) && e.getOperand2().evaluateInt() == 0) return e.getOperand1(); - if (Expression.isInt(e.getOperand1()) && e.getOperand1().evaluateInt() == 0) - return new ExpressionUnaryOp(ExpressionUnaryOp.MINUS, e.getOperand2()); + if (Expression.isInt(e.getOperand1()) && e.getOperand1().evaluateInt() == 0) { + ExpressionUnaryOp simplified = new ExpressionUnaryOp(ExpressionUnaryOp.MINUS, e.getOperand2()); + // preserve type + simplified.setType(e.getType()); + return simplified; + } if (Expression.isDouble(e.getOperand2()) && e.getOperand2().evaluateDouble() == 0.0) { // Need to be careful that type is preserved e.getOperand1().setType(e.getType()); return e.getOperand1(); } - if (Expression.isDouble(e.getOperand1()) && e.getOperand1().evaluateDouble() == 0.0) - return new ExpressionUnaryOp(ExpressionUnaryOp.MINUS, e.getOperand2()); + if (Expression.isDouble(e.getOperand1()) && e.getOperand1().evaluateDouble() == 0.0) { + ExpressionUnaryOp simplified = new ExpressionUnaryOp(ExpressionUnaryOp.MINUS, e.getOperand2()); + // preserve type + simplified.setType(e.getType()); + return simplified; + } break; case ExpressionBinaryOp.TIMES: if (Expression.isInt(e.getOperand2()) && e.getOperand2().evaluateInt() == 1)