Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ExpectedTimeToExpectedRewardVisitor.cpp
Go to the documentation of this file.
2#include <boost/any.hpp>
4
6
8
9namespace storm {
10namespace logic {
11
12ExpectedTimeToExpectedRewardVisitor::ExpectedTimeToExpectedRewardVisitor(std::string const& timeRewardModelName) : timeRewardModelName(timeRewardModelName) {
13 // Intentionally left empty
14}
15
16std::shared_ptr<Formula> ExpectedTimeToExpectedRewardVisitor::substitute(Formula const& f) const {
17 boost::any result = f.accept(*this, boost::any());
18 return boost::any_cast<std::shared_ptr<Formula>>(result);
19}
20
21boost::any ExpectedTimeToExpectedRewardVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
22 STORM_LOG_THROW(f.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException,
23 "Expected eventually formula within time operator. Got " << f << " instead.");
24 std::shared_ptr<Formula> subsubformula =
25 boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data));
26 STORM_LOG_THROW(f.getSubformula().isReachabilityTimeFormula(), storm::exceptions::InvalidPropertyException,
27 "Expected time path formula within time operator. Got " << f << " instead.");
28 std::shared_ptr<Formula> subformula = std::make_shared<EventuallyFormula>(subsubformula, storm::logic::FormulaContext::Reward);
29 return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, timeRewardModelName, f.getOperatorInformation()));
30}
31} // namespace logic
32} // namespace storm
virtual boost::any visit(TimeOperatorFormula const &f, boost::any const &data) const override
ExpectedTimeToExpectedRewardVisitor(std::string const &timeRewardModelName)
std::shared_ptr< Formula > substitute(Formula const &f) const
virtual bool isReachabilityTimeFormula() const
Definition Formula.cpp:164
EventuallyFormula & asEventuallyFormula()
Definition Formula.cpp:333
virtual bool isEventuallyFormula() const
Definition Formula.cpp:88
boost::any accept(FormulaVisitor const &visitor) const
Definition Formula.cpp:16
OperatorInformation const & getOperatorInformation() const
Formula const & getSubformula() const
Formula const & getSubformula() const
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
LabParser.cpp.
Definition cli.cpp:18