diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index e8218cc4e..2a92d59e1 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -397,10 +397,15 @@ namespace storm { storm::logic::OperatorInformation opInfo; opInfo.optimalityType = opString == "Smin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; opInfo.bound = bound; - + STORM_LOG_THROW(propertyStructure.count("accumulate") > 0, storm::exceptions::InvalidJaniException, "Expected an accumulate array at steady state property at " << scope.description); + storm::logic::RewardAccumulation rewardAccumulation = parseRewardAccumulation(propertyStructure.at("accumulate"), scope.description); STORM_LOG_THROW(propertyStructure.count("exp") > 0, storm::exceptions::InvalidJaniException, "Expected an expression at steady state property at " << scope.description); auto rewExpr = parseExpression(propertyStructure["exp"], scope.refine("steady-state operator"), true); - if (!rewExpr.isInitialized() || rewExpr.hasBooleanType()) { + if (!rewExpr.isInitialized()) { + STORM_LOG_THROW(!rewardAccumulation.isStepsSet(), storm::exceptions::InvalidJaniException, "Nested long-run average properties are not allowed to accumulate on steps at" << scope.description); + STORM_LOG_THROW(!rewardAccumulation.isExitSet() || !rewardAccumulation.isTimeSet(), storm::exceptions::InvalidJaniException, "Nested long-run average properties are not allowed to accumulate both on exit and time at" << scope.description); + STORM_LOG_THROW(propertyStructure.count("exp") > 0, storm::exceptions::InvalidJaniException, "Expected an expression at steady state property at " << scope.description); + STORM_LOG_WARN("Reward Accumulations on nested long-run average properties is not respected."); std::shared_ptr subformula = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, scope.refine("Steady-state operator"))[0]; return std::make_shared(subformula, opInfo); } @@ -409,7 +414,7 @@ namespace storm { if (!rewExpr.isVariable()) { nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); } - auto subformula = std::make_shared(); + auto subformula = std::make_shared(rewardAccumulation); return std::make_shared(subformula, rewardName, opInfo); } else if (opString == "U" || opString == "F") { diff --git a/src/storm/logic/LongRunAverageRewardFormula.cpp b/src/storm/logic/LongRunAverageRewardFormula.cpp index fc7edd7fe..c36dab8a9 100644 --- a/src/storm/logic/LongRunAverageRewardFormula.cpp +++ b/src/storm/logic/LongRunAverageRewardFormula.cpp @@ -4,7 +4,7 @@ namespace storm { namespace logic { - LongRunAverageRewardFormula::LongRunAverageRewardFormula() { + LongRunAverageRewardFormula::LongRunAverageRewardFormula(boost::optional rewardAccumulation) : rewardAccumulation(rewardAccumulation) { // Intentionally left empty. } @@ -16,12 +16,25 @@ namespace storm { return true; } + bool LongRunAverageRewardFormula::hasRewardAccumulation() const { + return rewardAccumulation.is_initialized(); + } + + RewardAccumulation const& LongRunAverageRewardFormula::getRewardAccumulation() const { + return rewardAccumulation.get(); + } + boost::any LongRunAverageRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } std::ostream& LongRunAverageRewardFormula::writeToStream(std::ostream& out) const { - return out << "LRA"; + out << "LRA"; + if (hasRewardAccumulation()) { + out << "[" << getRewardAccumulation() << "]"; + } + return out; } + } } diff --git a/src/storm/logic/LongRunAverageRewardFormula.h b/src/storm/logic/LongRunAverageRewardFormula.h index 545dd0b57..03f1c3684 100644 --- a/src/storm/logic/LongRunAverageRewardFormula.h +++ b/src/storm/logic/LongRunAverageRewardFormula.h @@ -1,13 +1,15 @@ #ifndef STORM_LOGIC_LONGRUNAVERAGEREWARDFORMULA_H_ #define STORM_LOGIC_LONGRUNAVERAGEREWARDFORMULA_H_ +#include #include "storm/logic/PathFormula.h" +#include "storm/logic/RewardAccumulation.h" namespace storm { namespace logic { class LongRunAverageRewardFormula : public PathFormula { public: - LongRunAverageRewardFormula(); + LongRunAverageRewardFormula(boost::optional rewardAccumulation = boost::none); virtual ~LongRunAverageRewardFormula() { // Intentionally left empty. @@ -15,11 +17,15 @@ namespace storm { virtual bool isLongRunAverageRewardFormula() const override; virtual bool isRewardPathFormula() const override; + bool hasRewardAccumulation() const; + RewardAccumulation const& getRewardAccumulation() const; virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::ostream& writeToStream(std::ostream& out) const override; - + + private: + boost::optional rewardAccumulation; }; } } diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp index 374e49f94..9169b89f4 100644 --- a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp @@ -91,6 +91,16 @@ namespace storm { return std::static_pointer_cast(std::make_shared(bounds, timeBoundReferences, rewAcc)); } + boost::any RewardAccumulationEliminationVisitor::visit(LongRunAverageRewardFormula 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."); + auto rewName = boost::any_cast>(data); + if (!f.hasRewardAccumulation() || canEliminate(f.getRewardAccumulation(), rewName)) { + return std::static_pointer_cast(std::make_shared()); + } else { + return std::static_pointer_cast(std::make_shared(f.getRewardAccumulation())); + } + } + boost::any RewardAccumulationEliminationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); if (f.hasRewardAccumulation()) { diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.h b/src/storm/logic/RewardAccumulationEliminationVisitor.h index 59dbc330d..e5e78c04e 100644 --- a/src/storm/logic/RewardAccumulationEliminationVisitor.h +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.h @@ -26,6 +26,7 @@ namespace storm { virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override; + virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override;