Browse Source

Processed some TODOs in storm/logic

Conflicts:
	src/storm/logic/LiftableTransitionRewardsVisitor.cpp
tempestpy_adaptions
Tim Quatmann 3 years ago
committed by Stefan Pranger
parent
commit
b097a442ee
  1. 7
      src/storm/logic/FormulaInformationVisitor.cpp
  2. 1
      src/storm/logic/FragmentChecker.cpp
  3. 7
      src/storm/logic/LiftableTransitionRewardsVisitor.cpp

7
src/storm/logic/FormulaInformationVisitor.cpp

@ -134,12 +134,11 @@ namespace storm {
} }
boost::any FormulaInformationVisitor::visit(QuantileFormula const& f, boost::any const& data) const { boost::any FormulaInformationVisitor::visit(QuantileFormula const& f, boost::any const& data) const {
// TODO (joachim): check is this correct?
if (recurseIntoOperators) { if (recurseIntoOperators) {
return f.getSubformula().accept(*this, data); return f.getSubformula().accept(*this, data);
} else {
return FormulaInformation();
}
} else {
return FormulaInformation();
}
} }
boost::any FormulaInformationVisitor::visit(NextFormula const& f, boost::any const& data) const { boost::any FormulaInformationVisitor::visit(NextFormula const& f, boost::any const& data) const {

1
src/storm/logic/FragmentChecker.cpp

@ -341,7 +341,6 @@ namespace storm {
boost::any FragmentChecker::visit(HOAPathFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(HOAPathFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = inherited.getSpecification().areHOAPathFormulasAllowed(); bool result = inherited.getSpecification().areHOAPathFormulasAllowed();
// TODO: check
for (auto& mapped : f.getAPMapping()) { for (auto& mapped : f.getAPMapping()) {
result = result && boost::any_cast<bool>(mapped.second->accept(*this, data)); result = result && boost::any_cast<bool>(mapped.second->accept(*this, data));
} }

7
src/storm/logic/LiftableTransitionRewardsVisitor.cpp

@ -22,13 +22,12 @@ namespace storm {
return true; 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 { 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));
} }

Loading…
Cancel
Save