From c43e13172fa98c6ac6f9254ec1f69e5b5f45dbff Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 5 Apr 2019 16:31:44 +0200 Subject: [PATCH] Jani: Accumulations for Smin/Smax properties. --- src/storm-parsers/parser/JaniParser.cpp | 12 +++++++----- src/storm/logic/FragmentChecker.cpp | 5 +++-- 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 2a92d59e1..bc38ac495 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/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 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 subformula = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, scope.refine("Steady-state operator"))[0]; return std::make_shared(subformula, opInfo); } diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index 4bda466c4..b669e75bd 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/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(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 {