Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
RewardModelNameSubstitutionVisitor.cpp
Go to the documentation of this file.
2#include <boost/any.hpp>
4
7
10
11namespace storm {
12namespace logic {
13
14RewardModelNameSubstitutionVisitor::RewardModelNameSubstitutionVisitor(std::map<std::string, std::string> const& rewardModelNameMapping)
15 : rewardModelNameMapping(rewardModelNameMapping) {
16 // Intentionally left empty
17}
18
19std::shared_ptr<Formula> RewardModelNameSubstitutionVisitor::substitute(Formula const& f) const {
20 boost::any result = f.accept(*this, boost::any());
21 return boost::any_cast<std::shared_ptr<Formula>>(result);
22}
23
24boost::any RewardModelNameSubstitutionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
25 std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds;
26 std::vector<TimeBoundReference> timeBoundReferences;
27 for (uint64_t i = 0; i < f.getDimension(); ++i) {
28 if (f.hasLowerBound(i)) {
29 lowerBounds.emplace_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i)));
30 } else {
31 lowerBounds.emplace_back();
32 }
33 if (f.hasUpperBound(i)) {
34 upperBounds.emplace_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i)));
35 } else {
36 upperBounds.emplace_back();
37 }
38 auto const& tbr = f.getTimeBoundReference(i);
39 if (tbr.isRewardBound()) {
40 timeBoundReferences.emplace_back(getNewName(tbr.getRewardName()), tbr.getOptionalRewardAccumulation());
41 } else {
42 timeBoundReferences.push_back(tbr);
43 }
44 }
46 std::vector<std::shared_ptr<Formula const>> leftSubformulas, rightSubformulas;
47 for (uint64_t i = 0; i < f.getDimension(); ++i) {
48 leftSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula(i).accept(*this, data)));
49 rightSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula(i).accept(*this, data)));
50 }
51 return std::static_pointer_cast<Formula>(
52 std::make_shared<BoundedUntilFormula>(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences));
53 } else {
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));
57 }
58}
59
60boost::any RewardModelNameSubstitutionVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const {
61 // Data is unused; no children to pass this on.
62 std::vector<TimeBound> bounds;
63 std::vector<TimeBoundReference> timeBoundReferences;
64 for (uint64_t i = 0; i < f.getDimension(); ++i) {
65 bounds.emplace_back(TimeBound(f.isBoundStrict(i), f.getBound(i)));
67 if (tbr.isRewardBound()) {
69 }
70 timeBoundReferences.push_back(std::move(tbr));
71 }
72 if (f.hasRewardAccumulation()) {
73 return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences, f.getRewardAccumulation()));
74 } else {
75 return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences));
76 }
77}
78
79boost::any RewardModelNameSubstitutionVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const {
80 std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
81 if (f.hasRewardModelName()) {
82 return std::static_pointer_cast<Formula>(
83 std::make_shared<RewardOperatorFormula>(subformula, getNewName(f.getRewardModelName()), f.getOperatorInformation()));
84 } else {
85 return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, boost::none, f.getOperatorInformation()));
86 }
87}
88
89std::string const& RewardModelNameSubstitutionVisitor::getNewName(std::string const& oldName) const {
90 auto nameIt = rewardModelNameMapping.find(oldName);
91 if (nameIt == rewardModelNameMapping.end()) {
92 return oldName;
93 } else {
94 return nameIt->second;
95 }
96}
97
98} // namespace logic
99} // namespace storm
TimeBoundReference const & getTimeBoundReference(unsigned i=0) const
bool isLowerBoundStrict(unsigned i=0) const
storm::expressions::Expression const & getUpperBound(unsigned i=0) const
storm::expressions::Expression const & getLowerBound(unsigned i=0) const
bool isUpperBoundStrict(unsigned i=0) const
TimeBoundReference const & getTimeBoundReference() const
RewardAccumulation const & getRewardAccumulation() const
storm::expressions::Expression const & getBound() const
boost::any accept(FormulaVisitor const &visitor) const
Definition Formula.cpp:16
OperatorInformation const & getOperatorInformation() const
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 & getRewardModelName() const
Retrieves the name of the reward model this property refers to (if any).
bool hasRewardModelName() const
Retrieves whether the reward model refers to a specific reward model.
std::string const & getRewardName() const
boost::optional< RewardAccumulation > const & getOptionalRewardAccumulation() const
Formula const & getSubformula() const
LabParser.cpp.
Definition cli.cpp:18