diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 27960daac..502d1485c 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -42,7 +42,7 @@ namespace storm { result &= parametricModel->supportsParameters(); auto dtmc = parametricModel->template as(); result &= static_cast(dtmc); - result &= checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true)); + result &= checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true)); return result; } diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index e07d05b55..97c768944 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -282,7 +282,7 @@ namespace storm { } for (unsigned i = 0; i < this->getDimension(); ++i) { if (i > 0) { - out << ","; + out << ", "; } if (this->getTimeBoundReference(i).isRewardBound()) { out << "rew{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp index dd0eeb994..19a60a623 100644 --- a/src/storm/logic/CumulativeRewardFormula.cpp +++ b/src/storm/logic/CumulativeRewardFormula.cpp @@ -148,7 +148,7 @@ namespace storm { } for (unsigned i = 0; i < this->getDimension(); ++i) { if (i > 0) { - out << ","; + out << ", "; } if (this->getTimeBoundReference(i).isRewardBound()) { out << "rew{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 8d7fc1b8c..c6bf4c98c 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -137,7 +137,7 @@ namespace storm { std::unique_ptr SparseMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - if (rewardPathFormula.getTimeBoundReference().isRewardBound()) { + if (rewardPathFormula.isMultiDimensional() || rewardPathFormula.getTimeBoundReference().isRewardBound()) { STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Checking reward bounded cumulative reward formulas can only be done for the initial states of the model."); STORM_LOG_WARN_COND(!checkTask.isQualitativeSet(), "Checking reward bounded until formulas is not optimized w.r.t. qualitative queries"); storm::logic::OperatorInformation opInfo(checkTask.getOptimizationDirection()); diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp index 8b4223fd2..fa327d34e 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp @@ -407,8 +407,12 @@ namespace storm { STORM_LOG_THROW(!rewModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Reward model has transition rewards which is not expected."); bool rewardCollectedInEpoch = true; if (formula.getSubformula().isCumulativeRewardFormula()) { - assert(objectiveDimensions[objIndex].getNumberOfSetBits() == 1); - rewardCollectedInEpoch = !epochManager.isBottomDimensionEpochClass(epochClass, *objectiveDimensions[objIndex].begin()); + for (auto const& dim : objectiveDimensions[objIndex]) { + if (epochManager.isBottomDimensionEpochClass(epochClass, dim)) { + rewardCollectedInEpoch = false; + break; + } + } } else { STORM_LOG_THROW(formula.getSubformula().isTotalRewardFormula(), storm::exceptions::UnexpectedException, "Unexpected type of formula " << formula); } diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index b37e1775c..9e8191ad2 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -26,7 +26,7 @@ namespace storm { instantaneousRewardFormula = (qi::lit("I=") > expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)]; instantaneousRewardFormula.name("instantaneous reward formula"); - cumulativeRewardFormula = (qi::lit("C") >> (timeBound % qi::lit(",")))[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)]; + cumulativeRewardFormula = (qi::lit("C") >> timeBounds)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)]; cumulativeRewardFormula.name("cumulative reward formula"); totalRewardFormula = (qi::lit("C"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTotalRewardFormula, phoenix::ref(*this))]; @@ -59,7 +59,7 @@ namespace storm { notStateFormula = (unaryBooleanOperator_ >> atomicStateFormulaWithoutExpression)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)] | atomicStateFormula[qi::_val = qi::_1]; notStateFormula.name("negation formula"); - eventuallyFormula = (qi::lit("F") >> -(timeBound % qi::lit(",")) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)]; + eventuallyFormula = (qi::lit("F") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)]; eventuallyFormula.name("eventually formula"); globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)]; @@ -71,7 +71,7 @@ namespace storm { pathFormulaWithoutUntil = eventuallyFormula(qi::_r1) | globallyFormula(qi::_r1) | nextFormula(qi::_r1) | stateFormula; pathFormulaWithoutUntil.name("path formula"); - untilFormula = pathFormulaWithoutUntil(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("U") >> -(timeBound % qi::lit(",")) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; + untilFormula = pathFormulaWithoutUntil(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("U") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; untilFormula.name("until formula"); conditionalFormula = untilFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula(storm::logic::FormulaContext::Probability))[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)]; @@ -88,6 +88,9 @@ namespace storm { [qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromSingleBound, phoenix::ref(*this), qi::_2, qi::_a, qi::_b, qi::_1)]; timeBound.name("time bound"); + timeBounds = (timeBound % qi::lit(",")) | (((-qi::lit("^") >> qi::lit("{")) >> (timeBound % qi::lit(","))) >> qi::lit("}")); + timeBounds.name("time bounds"); + pathFormula = conditionalFormula(qi::_r1); pathFormula.name("path formula");