From fdf237ca679e1f3f4e40d270e19172e5ca8c88c6 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 30 Nov 2015 19:35:44 +0100
Subject: [PATCH] added support to create measure driven initial partition for
 bisimulation for MDPs from formula that does not specify an optimization
 direction

Former-commit-id: 0d3970456b284aebfcc77cda7b65f01e5e2ae52a
---
 src/storage/bisimulation/BisimulationDecomposition.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp
index 820cd0596..ae9b61e3a 100644
--- a/src/storage/bisimulation/BisimulationDecomposition.cpp
+++ b/src/storage/bisimulation/BisimulationDecomposition.cpp
@@ -86,6 +86,13 @@ namespace storm {
             if (formula.isProbabilityOperatorFormula()) {
                 if (formula.asProbabilityOperatorFormula().hasOptimalityType()) {
                     optimalityType = formula.asProbabilityOperatorFormula().getOptimalityType();
+                } else if (formula.asProbabilityOperatorFormula().hasBound()) {
+                    storm::logic::ComparisonType comparisonType = formula.asProbabilityOperatorFormula().getComparisonType();
+                    if (comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::LessEqual) {
+                        optimalityType = OptimizationDirection::Maximize;
+                    } else {
+                        optimalityType = OptimizationDirection::Minimize;
+                    }
                 }
                 newFormula = formula.asProbabilityOperatorFormula().getSubformula().asSharedPointer();
             } else if (formula.isRewardOperatorFormula()) {