Respecting reward accumulations for long-run-average properties.

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<storm::logic::Formula const> subformula = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, scope.refine("Steady-state operator"))[0];
                         return std::make_shared<storm::logic::LongRunAverageOperatorFormula>(subformula, opInfo);
                     }
@@ -409,7 +414,7 @@ namespace storm {
                     if (!rewExpr.isVariable()) {
                         nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr);
                     }
-                    auto subformula = std::make_shared<storm::logic::LongRunAverageRewardFormula>();
+                    auto subformula = std::make_shared<storm::logic::LongRunAverageRewardFormula>(rewardAccumulation);
                     return std::make_shared<storm::logic::RewardOperatorFormula>(subformula, rewardName, opInfo);
                     
                 } else if (opString == "U" || opString == "F") {

src/storm/logic/LongRunAverageRewardFormula.cpp

@@ -4,7 +4,7 @@
 
 namespace storm {
     namespace logic {
-        LongRunAverageRewardFormula::LongRunAverageRewardFormula() {
+        LongRunAverageRewardFormula::LongRunAverageRewardFormula(boost::optional<RewardAccumulation> 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;
         }
+        
     }
 }

src/storm/logic/LongRunAverageRewardFormula.h

@@ -1,13 +1,15 @@
 #ifndef STORM_LOGIC_LONGRUNAVERAGEREWARDFORMULA_H_
 #define STORM_LOGIC_LONGRUNAVERAGEREWARDFORMULA_H_
 
+#include <boost/optional.hpp>
 #include "storm/logic/PathFormula.h"
+#include "storm/logic/RewardAccumulation.h"
 
 namespace storm {
     namespace logic {
         class LongRunAverageRewardFormula : public PathFormula {
         public:
-            LongRunAverageRewardFormula();
+            LongRunAverageRewardFormula(boost::optional<RewardAccumulation> 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> rewardAccumulation;
         };
     }
 }

src/storm/logic/RewardAccumulationEliminationVisitor.cpp

@@ -91,6 +91,16 @@ namespace storm {
             return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(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<boost::optional<std::string>>(data);
+            if (!f.hasRewardAccumulation() || canEliminate(f.getRewardAccumulation(), rewName)) {
+                return std::static_pointer_cast<Formula>(std::make_shared<LongRunAverageRewardFormula>());
+            } else {
+                return std::static_pointer_cast<Formula>(std::make_shared<LongRunAverageRewardFormula>(f.getRewardAccumulation()));
+            }
+        }
+        
         boost::any RewardAccumulationEliminationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
             if (f.hasRewardAccumulation()) {

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;