Skip to content

Warn when using time bound on discrete-time models #855

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
volkm wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Warn when using time bound on discrete-time models #855

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
4ffe527
Extended test for parsing bounded until formulas
volkm Jan 23, 2026
6108f33
Allow time-bounded until for ParameterLiftingModelChecker on discrete…
volkm Jan 23, 2026
ff6310e
Warn when using time-bound instead of step-bound on discrete-time models
volkm Jan 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,8 +130,9 @@ void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType, Robus
// 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.");
Expand Down
5 changes: 3 additions & 2 deletions src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,8 +91,9 @@ void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::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.");
Expand Down
9 changes: 6 additions & 3 deletions src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,7 @@ std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::c
auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeRewardBoundedValues(env, this->getModel(), formula);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(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.");
Expand Down Expand Up @@ -192,7 +193,8 @@ std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::c
auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeRewardBoundedValues(env, this->getModel(), formula);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(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<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeCumulativeRewards(
env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(),
Expand All @@ -211,7 +213,8 @@ template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeDiscountedCumulativeRewards(
Environment const& env, CheckTask<storm::logic::DiscountedCumulativeRewardFormula, ValueType> 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<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeDiscountedCumulativeRewards(
env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(),
Expand All @@ -223,7 +226,7 @@ template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeInstantaneousRewards(
Environment const& env, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> 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<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeInstantaneousRewards(
env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""),
Expand Down
11 changes: 7 additions & 4 deletions src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -132,11 +132,12 @@ std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::com
env, checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates());
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(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<CheckResult> leftResultPointer = this->check(env, pathFormula.getLeftSubformula());
std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula());
ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
Expand Down Expand Up @@ -313,7 +314,8 @@ std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::com
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(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<SolutionType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType, SolutionType>::computeCumulativeRewards(
env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(),
Expand All @@ -334,7 +336,8 @@ std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::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<SolutionType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType, SolutionType>::computeDiscountedCumulativeRewards(
env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(),
Expand All @@ -348,7 +351,7 @@ std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::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<SolutionType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType, SolutionType>::computeInstantaneousRewards(
env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""),
Expand Down
34 changes: 24 additions & 10 deletions src/test/storm/parser/FormulaParserTest.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down