Jani: Accumulations for Smin/Smax properties.

src/storm-parsers/parser/JaniParser.cpp

@@ -397,15 +397,17 @@ 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);
+                    // Reward accumulation is optional as it was not available in the early days...
+                    boost::optional<storm::logic::RewardAccumulation> rewardAccumulation;
+                    if (propertyStructure.count("accumulate") > 0) {
+                         rewardAccumulation = parseRewardAccumulation(propertyStructure.at("accumulate"), scope.description);
+                    }
+                    //STORM_LOG_THROW(, storm::exceptions::InvalidJaniException, "Expected an accumulate array at steady state property at " << 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()) {
-                        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(!rewardAccumulation.is_initialized(), storm::exceptions::InvalidJaniException, "Long-run average probabilities are not allowed to have a reward accumulation 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);
                     }

src/storm/logic/FragmentChecker.cpp

@@ -206,9 +206,10 @@ namespace storm {
             return result;
         }
         
-        boost::any FragmentChecker::visit(LongRunAverageRewardFormula const&, boost::any const& data) const {
+        boost::any FragmentChecker::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
-            return inherited.getSpecification().areLongRunAverageRewardFormulasAllowed();
+            bool result = (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed());
+            return result && inherited.getSpecification().areLongRunAverageRewardFormulasAllowed();
         }
         
         boost::any FragmentChecker::visit(MultiObjectiveFormula const& f, boost::any const& data) const {