Browse Source

fixed in reward accumulation elimination of total reward formulas

tempestpy_adaptions
TimQu 6 years ago
parent
commit
b08373ac67
  1. 2
      src/storm/logic/RewardAccumulationEliminationVisitor.cpp

2
src/storm/logic/RewardAccumulationEliminationVisitor.cpp

@ -118,7 +118,7 @@ namespace storm {
boost::any RewardAccumulationEliminationVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const { boost::any RewardAccumulationEliminationVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const {
STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator."); STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator.");
auto rewName = boost::any_cast<boost::optional<std::string>>(data); auto rewName = boost::any_cast<boost::optional<std::string>>(data);
if (f.hasRewardAccumulation() || canEliminate(f.getRewardAccumulation(), rewName)) {
if (!f.hasRewardAccumulation() || canEliminate(f.getRewardAccumulation(), rewName)) {
return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>()); return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>());
} else { } else {
return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>(f.getRewardAccumulation())); return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>(f.getRewardAccumulation()));

Loading…
Cancel
Save