From b097a442eeccbf10908cd3362719600d489edc88 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 9 Aug 2021 13:48:51 +0200
Subject: [PATCH] Processed some TODOs in storm/logic

 Conflicts:
	src/storm/logic/LiftableTransitionRewardsVisitor.cpp
---
 src/storm/logic/FormulaInformationVisitor.cpp        | 7 +++----
 src/storm/logic/FragmentChecker.cpp                  | 1 -
 src/storm/logic/LiftableTransitionRewardsVisitor.cpp | 7 +++----
 3 files changed, 6 insertions(+), 9 deletions(-)

diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp
index 7a0b95f0c..0f174430b 100644
--- a/src/storm/logic/FormulaInformationVisitor.cpp
+++ b/src/storm/logic/FormulaInformationVisitor.cpp
@@ -134,12 +134,11 @@ namespace storm {
         }
         
         boost::any FormulaInformationVisitor::visit(QuantileFormula const& f, boost::any const& data) const {
-            // TODO (joachim): check is this correct?
             if (recurseIntoOperators) {
                 return f.getSubformula().accept(*this, data);
-	    } else {
-	        return FormulaInformation();
-	    }
+            } else {
+                return FormulaInformation();
+            }
         }
         
         boost::any FormulaInformationVisitor::visit(NextFormula const& f, boost::any const& data) const {
diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp
index c40d703c9..6ee707ef5 100644
--- a/src/storm/logic/FragmentChecker.cpp
+++ b/src/storm/logic/FragmentChecker.cpp
@@ -341,7 +341,6 @@ namespace storm {
         boost::any FragmentChecker::visit(HOAPathFormula const& f, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
             bool result = inherited.getSpecification().areHOAPathFormulasAllowed();
-            // TODO: check
             for (auto& mapped : f.getAPMapping()) {
                 result = result && boost::any_cast<bool>(mapped.second->accept(*this, data));
             }
diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp
index fbb215440..7c3b1da97 100644
--- a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp
+++ b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp
@@ -22,13 +22,12 @@ namespace storm {
             return true;
         }
 
-        boost::any LiftableTransitionRewardsVisitor::visit(BinaryBooleanStateFormula const&, boost::any const&) const {
-	  // TODO joachim: is this correct?
-            return true;
+        boost::any LiftableTransitionRewardsVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const {
+            return boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data)) && boost::any_cast<bool>(f.getRightSubformula().accept(*this, data));
         }
 
         boost::any LiftableTransitionRewardsVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const {
-            return boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data)) && boost::any_cast<bool>(f.getRightSubformula().accept(*this));
+            return boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data)) && boost::any_cast<bool>(f.getRightSubformula().accept(*this, data));
         }