From 5855a82e800051a092a0ef46d65479c725fc1b6d Mon Sep 17 00:00:00 2001
From: Joachim Klein <joachim.klein@automata.tools>
Date: Mon, 24 Aug 2020 22:25:13 +0200
Subject: [PATCH] (MDP-LTL) CheckTask: negate()

Allow a CheckTask to be negated (e.g., useful for converting from Pmin to 1-Pmax).
---
 src/storm/modelchecker/CheckTask.h | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h
index b42e8c3f8..2143e1f30 100644
--- a/src/storm/modelchecker/CheckTask.h
+++ b/src/storm/modelchecker/CheckTask.h
@@ -101,6 +101,27 @@ namespace storm {
                 }
             }
 
+            /*!
+             * Negate the optimization direction and the bound threshold, if those exist.
+             * Suitable for switching from Pmin[phi] to 1-Pmax[!psi] computations.
+             */
+            CheckTask negate() const {
+                CheckTask result(*this);
+                if (isOptimizationDirectionSet()) {
+                    // switch from min to max and vice-versa
+                    result.setOptimizationDirection(invert(getOptimizationDirection()));
+                }
+
+                if (isBoundSet()) {
+                    // invert bound comparison type (retain strictness),
+                    // convert threshold to 1- threshold
+                    result.bound = storm::logic::Bound(storm::logic::invertPreserveStrictness(getBound().comparisonType),
+                                                       1 - getBound().threshold);
+                }
+
+                return result;
+            }
+
             /*!
              * Copies the check task from the source while replacing the considered ValueType the new one. In particular, this
              * changes the formula type of the check task object.