Browse Source

param/exact: Fix Pmax/Pmin [ ! (F a) ] / [ !( a U b) ] computation

Switching between max and min when removing the negation was missing for MDPs.

Test case:
prism functionality/verify/mdps/ltl/simple_ltl.nm functionality/verify/mdps/ltl/simple_ltl.nm.props -exact -prop 3
from prism-tests.
master
Joachim Klein 8 years ago
parent
commit
8a420d6a36
  1. 1
      prism/src/param/ParamModelChecker.java

1
prism/src/param/ParamModelChecker.java

@ -903,6 +903,7 @@ final public class ParamModelChecker extends PrismComponent
if (expr instanceof ExpressionUnaryOp && if (expr instanceof ExpressionUnaryOp &&
((ExpressionUnaryOp)expr).getOperator() == ExpressionUnaryOp.NOT) { ((ExpressionUnaryOp)expr).getOperator() == ExpressionUnaryOp.NOT) {
negated = true; negated = true;
min = !min;
expr = ((ExpressionUnaryOp)expr).getOperand(); expr = ((ExpressionUnaryOp)expr).getOperand();
} }

Loading…
Cancel
Save