diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 122920d30..e33299f90 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -130,8 +130,9 @@ void SparseDtmcParameterLiftingModelChecker 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive."); diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp index 22d948e1e..e7712ba3d 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp @@ -91,8 +91,9 @@ void SparseMdpParameterLiftingModelChecker::speci // get the step bound STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported."); STORM_LOG_THROW(checkTask.getFormula().hasUpperBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with an upper bound."); - STORM_LOG_THROW(checkTask.getFormula().getTimeBoundReference().isStepBound(), storm::exceptions::NotSupportedException, - "Expected a bounded until formula with step bounds."); + STORM_LOG_THROW(checkTask.getFormula().getTimeBoundReference().isStepBound() || checkTask.getFormula().getTimeBoundReference().isTimeBound(), + storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); + STORM_LOG_WARN_COND(!checkTask.getFormula().getTimeBoundReference().isTimeBound(), "Time bound on discrete-time model will be handled as step bound."); stepBound = checkTask.getFormula().getUpperBound().evaluateAsInt(); STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive."); diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 0da5f8dfb..47dfe4284 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -87,6 +87,7 @@ std::unique_ptr SparseDtmcPrctlModelChecker::c auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeRewardBoundedValues(env, this->getModel(), formula); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } else { + STORM_LOG_WARN_COND(!pathFormula.getTimeBoundReference().isTimeBound(), "Time bound on discrete-time model will be handled as step bound."); STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound."); STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete/integral."); STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper step bound."); @@ -192,7 +193,8 @@ std::unique_ptr SparseDtmcPrctlModelChecker::c auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeRewardBoundedValues(env, this->getModel(), formula); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } else { - STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + STORM_LOG_WARN_COND(!rewardPathFormula.getTimeBoundReference().isTimeBound(), "Time bound on discrete-time model will be handled as step bound."); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete step bound."); auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(), @@ -211,7 +213,8 @@ template std::unique_ptr SparseDtmcPrctlModelChecker::computeDiscountedCumulativeRewards( Environment const& env, CheckTask const& checkTask) { storm::logic::DiscountedCumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); - STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + STORM_LOG_WARN_COND(!rewardPathFormula.getTimeBoundReference().isTimeBound(), "Time bound on discrete-time model will be handled as step bound."); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete step bound."); auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeDiscountedCumulativeRewards( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(), @@ -223,7 +226,7 @@ template std::unique_ptr SparseDtmcPrctlModelChecker::computeInstantaneousRewards( Environment const& env, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); - STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete step bound."); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeInstantaneousRewards( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 16ce6c7bb..0533728eb 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -132,11 +132,12 @@ std::unique_ptr SparseMdpPrctlModelChecker::com env, checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } else { + STORM_LOG_WARN_COND(!pathFormula.getTimeBoundReference().isTimeBound(), "Time bound on discrete-time model will be handled as step bound."); STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound."); STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete/integral."); STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, - "Formula needs to have discrete upper time bound."); + "Formula needs to have discrete upper step bound."); std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); @@ -313,7 +314,8 @@ std::unique_ptr SparseMdpPrctlModelChecker::com return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } } else { - STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + STORM_LOG_WARN_COND(!rewardPathFormula.getTimeBoundReference().isTimeBound(), "Time bound on discrete-time model will be handled as step bound."); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete step bound."); auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(), @@ -334,7 +336,8 @@ std::unique_ptr SparseMdpPrctlModelChecker::com storm::logic::DiscountedCumulativeRewardFormula 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."); - STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + STORM_LOG_WARN_COND(!rewardPathFormula.getTimeBoundReference().isTimeBound(), "Time bound on discrete-time model will be handled as step bound."); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete step bound."); auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeDiscountedCumulativeRewards( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(), @@ -348,7 +351,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::com storm::logic::InstantaneousRewardFormula 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."); - STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete step bound."); std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeInstantaneousRewards( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), diff --git a/src/test/storm/parser/FormulaParserTest.cpp b/src/test/storm/parser/FormulaParserTest.cpp index 7fb548da8..bc5c6ccc6 100644 --- a/src/test/storm/parser/FormulaParserTest.cpp +++ b/src/test/storm/parser/FormulaParserTest.cpp @@ -128,31 +128,45 @@ TEST(FormulaParserTest, UntilOperatorTest) { EXPECT_TRUE(nested2.asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); EXPECT_EQ(3, nested2.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); - input = "P<0.9 [\"a\" U{\"rewardname\"}<=3 \"b\"]"; + input = "P<0.9 [\"a\" Utime<=3 \"b\"]"; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula(); EXPECT_TRUE(nested3.isBoundedUntilFormula()); - EXPECT_TRUE(nested3.asBoundedUntilFormula().getTimeBoundReference().isRewardBound()); - EXPECT_TRUE(nested3.asBoundedUntilFormula().getTimeBoundReference().hasRewardModelName()); - EXPECT_EQ("rewardname", nested3.asBoundedUntilFormula().getTimeBoundReference().getRewardName()); + EXPECT_TRUE(nested3.asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); EXPECT_EQ(3, nested3.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); - input = "P<0.9 [\"a\" Urew{\"rewardname\"}<=3 \"b\"]"; + input = "P<0.9 [\"a\" Usteps<=3 \"b\"]"; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); auto const &nested4 = formula->asProbabilityOperatorFormula().getSubformula(); EXPECT_TRUE(nested4.isBoundedUntilFormula()); - EXPECT_TRUE(nested4.asBoundedUntilFormula().getTimeBoundReference().isRewardBound()); - EXPECT_TRUE(nested4.asBoundedUntilFormula().getTimeBoundReference().hasRewardModelName()); - EXPECT_EQ("rewardname", nested4.asBoundedUntilFormula().getTimeBoundReference().getRewardName()); + EXPECT_TRUE(nested4.asBoundedUntilFormula().getTimeBoundReference().isStepBound()); EXPECT_EQ(3, nested4.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); - input = "P<0.9 [\"a\" Urew<=3 \"b\"]"; + input = "P<0.9 [\"a\" U{\"rewardname\"}<=3 \"b\"]"; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); auto const &nested5 = formula->asProbabilityOperatorFormula().getSubformula(); EXPECT_TRUE(nested5.isBoundedUntilFormula()); EXPECT_TRUE(nested5.asBoundedUntilFormula().getTimeBoundReference().isRewardBound()); - EXPECT_FALSE(nested5.asBoundedUntilFormula().getTimeBoundReference().hasRewardModelName()); + EXPECT_TRUE(nested5.asBoundedUntilFormula().getTimeBoundReference().hasRewardModelName()); + EXPECT_EQ("rewardname", nested5.asBoundedUntilFormula().getTimeBoundReference().getRewardName()); EXPECT_EQ(3, nested5.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); + + input = "P<0.9 [\"a\" Urew{\"rewardname\"}<=3 \"b\"]"; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const &nested6 = formula->asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(nested6.isBoundedUntilFormula()); + EXPECT_TRUE(nested6.asBoundedUntilFormula().getTimeBoundReference().isRewardBound()); + EXPECT_TRUE(nested6.asBoundedUntilFormula().getTimeBoundReference().hasRewardModelName()); + EXPECT_EQ("rewardname", nested6.asBoundedUntilFormula().getTimeBoundReference().getRewardName()); + EXPECT_EQ(3, nested6.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); + + input = "P<0.9 [\"a\" Urew<=3 \"b\"]"; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const &nested7 = formula->asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(nested7.isBoundedUntilFormula()); + EXPECT_TRUE(nested7.asBoundedUntilFormula().getTimeBoundReference().isRewardBound()); + EXPECT_FALSE(nested7.asBoundedUntilFormula().getTimeBoundReference().hasRewardModelName()); + EXPECT_EQ(3, nested7.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); } TEST(FormulaParserTest, RewardOperatorTest) {