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(data); bool result = inherited.getSpecification().areHOAPathFormulasAllowed(); - // TODO: check for (auto& mapped : f.getAPMapping()) { result = result && boost::any_cast(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(f.getLeftSubformula().accept(*this, data)) && boost::any_cast(f.getRightSubformula().accept(*this, data)); } boost::any LiftableTransitionRewardsVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const { - return boost::any_cast(f.getLeftSubformula().accept(*this, data)) && boost::any_cast(f.getRightSubformula().accept(*this)); + return boost::any_cast(f.getLeftSubformula().accept(*this, data)) && boost::any_cast(f.getRightSubformula().accept(*this, data)); }