From 8a420d6a3663a8ea3c2157327ba16a0327628033 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 25 Aug 2017 17:03:52 +0200
Subject: [PATCH] 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.
---
 prism/src/param/ParamModelChecker.java | 1 +
 1 file changed, 1 insertion(+)

diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java
index 594d545d..51e5d0e8 100644
--- a/prism/src/param/ParamModelChecker.java
+++ b/prism/src/param/ParamModelChecker.java
@@ -903,6 +903,7 @@ final public class ParamModelChecker extends PrismComponent
 		if (expr instanceof ExpressionUnaryOp &&
 		    ((ExpressionUnaryOp)expr).getOperator() == ExpressionUnaryOp.NOT) {
 			negated = true;
+			min = !min;
 			expr = ((ExpressionUnaryOp)expr).getOperand();
 		}