bugfixes

src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp

@@ -42,7 +42,7 @@ namespace storm {
             result &= parametricModel->supportsParameters();
             auto dtmc = parametricModel->template as<SparseModelType>();
             result &= static_cast<bool>(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;
         }
         

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() << "\"}";

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() << "\"}";

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -137,7 +137,7 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> 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());

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);
                             }

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");