2#include <boost/any.hpp>
15 : rewardModelNameMapping(rewardModelNameMapping) {
20 boost::any result = f.
accept(*
this, boost::any());
21 return boost::any_cast<std::shared_ptr<Formula>>(result);
25 std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds;
26 std::vector<TimeBoundReference> timeBoundReferences;
31 lowerBounds.emplace_back();
36 upperBounds.emplace_back();
39 if (tbr.isRewardBound()) {
40 timeBoundReferences.emplace_back(getNewName(tbr.getRewardName()), tbr.getOptionalRewardAccumulation());
42 timeBoundReferences.push_back(tbr);
46 std::vector<std::shared_ptr<Formula const>> leftSubformulas, rightSubformulas;
48 leftSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.
getLeftSubformula(i).
accept(*
this, data)));
51 return std::static_pointer_cast<Formula>(
52 std::make_shared<BoundedUntilFormula>(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences));
54 std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.
getLeftSubformula().
accept(*
this, data));
55 std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.
getRightSubformula().
accept(*
this, data));
56 return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBounds, upperBounds, timeBoundReferences));
62 std::vector<TimeBound> bounds;
63 std::vector<TimeBoundReference> timeBoundReferences;
70 timeBoundReferences.push_back(std::move(tbr));
73 return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences, f.
getRewardAccumulation()));
75 return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences));
80 std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.
getSubformula().
accept(*
this, data));
82 return std::static_pointer_cast<Formula>(
85 return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, boost::none, f.
getOperatorInformation()));
89std::string
const& RewardModelNameSubstitutionVisitor::getNewName(std::string
const& oldName)
const {
90 auto nameIt = rewardModelNameMapping.find(oldName);
91 if (nameIt == rewardModelNameMapping.end()) {
94 return nameIt->second;
std::shared_ptr< Formula > substitute(Formula const &f) const
RewardModelNameSubstitutionVisitor(std::map< std::string, std::string > const &rewardModelNameMapping)
virtual boost::any visit(BoundedUntilFormula const &f, boost::any const &data) const override
std::string const & getRewardName() const
boost::optional< RewardAccumulation > const & getOptionalRewardAccumulation() const
bool isRewardBound() const