Browse Source

Simplify: Preserve type for 0-x to -x simplification

Plus test case, fixes #34.
master
Joachim Klein 8 years ago
committed by Dave Parker
parent
commit
03d83d4abb
  1. 11
      prism-tests/bugfixes/simplify-unary-minus-issue-34.prism
  2. 5
      prism-tests/bugfixes/simplify-unary-minus-issue-34.prism.args
  3. 2
      prism-tests/bugfixes/simplify-unary-minus-issue-34.prism.props
  4. 16
      prism/src/parser/visitor/Simplify.java

11
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

5
prism-tests/bugfixes/simplify-unary-minus-issue-34.prism.args

@ -0,0 +1,5 @@
-explicit
-hybrid
-mtbdd
-sparse
-exact

2
prism-tests/bugfixes/simplify-unary-minus-issue-34.prism.props

@ -0,0 +1,2 @@
// RESULT: 1
P=?[F s=1]

16
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)

Loading…
Cancel
Save