From b59cbfa1de0933221b18d4ee93c5bdbbd1190e10 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 14 Feb 2019 23:24:11 +0100 Subject: [PATCH] graph conditions for rewards described by rational functions with nonconstant denominators --- src/storm/analysis/GraphConditions.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index 8fa6c194a..2152adfe7 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -48,7 +48,7 @@ namespace storm { } } else { wellformedConstraintSet.emplace(entry.denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ); - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at state rewards not yet supported."); + wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType::val(entry.denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER), typename ConstraintType::val(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ), typename ConstraintType::val(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ)); } } } @@ -151,7 +151,7 @@ namespace storm { } } else { wellformedConstraintSet.emplace(entry.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ); - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at transition rewards are not yet supported."); + wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType::val(entry.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER), typename ConstraintType::val(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ), typename ConstraintType::val(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ)); } } }