From b9cc6c2708baa8311acd4c00e6a9780fd1a31b38 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 18 Jun 2015 22:15:00 +0200
Subject: [PATCH] fixed bug in concatenating results of subformulas

Former-commit-id: 73b773480a102e4754e50c3d967207053cee8549
---
 .../results/ExplicitQualitativeCheckResult.cpp     | 14 ++++++++++----
 .../results/ExplicitQualitativeCheckResult.h       |  2 +-
 2 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp
index 79bb34885..121721846 100644
--- a/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp
+++ b/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp
@@ -29,13 +29,19 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        void ExplicitQualitativeCheckResult::performLogicalOperation(ExplicitQualitativeCheckResult& first, QualitativeCheckResult const& second, std::function<bool (bool, bool)> const& function) {
+        void ExplicitQualitativeCheckResult::performLogicalOperation(ExplicitQualitativeCheckResult& first, QualitativeCheckResult const& second, bool logicalAnd) {
             STORM_LOG_THROW(second.isExplicitQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type.");
             STORM_LOG_THROW(first.isResultForAllStates() == second.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type.");
             ExplicitQualitativeCheckResult const& secondCheckResult = static_cast<ExplicitQualitativeCheckResult const&>(second);
             if (first.isResultForAllStates()) {
-                boost::get<vector_type>(first.truthValues) &= boost::get<vector_type>(secondCheckResult.truthValues);
+                if (logicalAnd) {
+                    boost::get<vector_type>(first.truthValues) &= boost::get<vector_type>(secondCheckResult.truthValues);
+                } else {
+                    boost::get<vector_type>(first.truthValues) |= boost::get<vector_type>(secondCheckResult.truthValues);
+                }
             } else {
+                std::function<bool (bool, bool)> function = logicalAnd ? [] (bool a, bool b) { return a && b; } : [] (bool a, bool b) { return a || b; };
+                
                 map_type& map1 = boost::get<map_type>(first.truthValues);
                 map_type const& map2 = boost::get<map_type>(secondCheckResult.truthValues);
                 for (auto& element1 : map1) {
@@ -53,12 +59,12 @@ namespace storm {
         }
         
         QualitativeCheckResult& ExplicitQualitativeCheckResult::operator&=(QualitativeCheckResult const& other) {
-            performLogicalOperation(*this, other, [] (bool a, bool b) { return a && b; });
+            performLogicalOperation(*this, other, true);
             return *this;
         }
         
         QualitativeCheckResult& ExplicitQualitativeCheckResult::operator|=(QualitativeCheckResult const& other) {
-            performLogicalOperation(*this, other, [] (bool a, bool b) { return a || b; });
+            performLogicalOperation(*this, other, false);
             return *this;
         }
         
diff --git a/src/modelchecker/results/ExplicitQualitativeCheckResult.h b/src/modelchecker/results/ExplicitQualitativeCheckResult.h
index 8ab3e473d..abce327b4 100644
--- a/src/modelchecker/results/ExplicitQualitativeCheckResult.h
+++ b/src/modelchecker/results/ExplicitQualitativeCheckResult.h
@@ -51,7 +51,7 @@ namespace storm {
             virtual void filter(QualitativeCheckResult const& filter) override;
 
         private:
-            static void performLogicalOperation(ExplicitQualitativeCheckResult& first, QualitativeCheckResult const& second, std::function<bool (bool, bool)> const& function);
+            static void performLogicalOperation(ExplicitQualitativeCheckResult& first, QualitativeCheckResult const& second, bool logicalAnd);
             
             // The values of the quantitative check result.
             boost::variant<vector_type, map_type> truthValues;