From cd8dafa6eac8c4530f978b7fe578a90fa108753c Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 31 Jul 2017 16:37:40 +0200 Subject: [PATCH 1/3] Check for absence of negative probabilities in matrix --- src/storm/storage/SparseMatrix.cpp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 1a005d2d0..905fbffa9 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1571,7 +1571,7 @@ namespace storm { typename SparseMatrix::index_type SparseMatrix::getNonconstantRowGroupCount() const { index_type nonConstRowGroups = 0; for (index_type rowGroup=0; rowGroup < this->getRowGroupCount(); ++rowGroup) { - for( auto const& entry : this->getRowGroup(rowGroup)){ + for (auto const& entry : this->getRowGroup(rowGroup)){ if(!storm::utility::isConstant(entry.getValue())){ ++nonConstRowGroups; break; @@ -1584,11 +1584,18 @@ namespace storm { template bool SparseMatrix::isProbabilistic() const { storm::utility::ConstantsComparator comparator; - for(index_type row = 0; row < this->rowCount; ++row) { + for (index_type row = 0; row < this->rowCount; ++row) { if(!comparator.isOne(getRowSum(row))) { return false; } } + for (auto const& entry : *this) { + if (comparator.isConstant(entry.getValue())) { + if (comparator.isLess(entry.getValue(), storm::utility::zero())) { + return false; + } + } + } return true; } From d1f8712542c9eae5164632985d3ce5364eb23035 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 31 Jul 2017 16:38:05 +0200 Subject: [PATCH 2/3] Check updates do not contain negative likelihoods --- src/storm/storage/prism/Update.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/storm/storage/prism/Update.cpp b/src/storm/storage/prism/Update.cpp index 86693328c..0d1fce1ce 100644 --- a/src/storm/storage/prism/Update.cpp +++ b/src/storm/storage/prism/Update.cpp @@ -2,6 +2,7 @@ #include #include +#include #include "storm/utility/macros.h" #include "storm/exceptions/OutOfRangeException.h" @@ -9,6 +10,7 @@ namespace storm { namespace prism { Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::vector const& assignments, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(likelihoodExpression), assignments(assignments), variableToAssignmentIndexMap(), globalIndex(globalIndex) { + STORM_LOG_ASSERT(likelihoodExpression.containsVariables() || likelihoodExpression.evaluateAsRational() >= 0, "Negative likelihood expressions are not allowed."); std::sort(this->assignments.begin(), this->assignments.end(), [] (storm::prism::Assignment const& assignment1, storm::prism::Assignment const& assignment2) { bool smaller = assignment1.getVariable().getType().isBooleanType() && !assignment2.getVariable().getType().isBooleanType(); if (!smaller) { @@ -64,9 +66,10 @@ namespace storm { for (auto const& assignment : this->getAssignments()) { newAssignments.emplace_back(assignment.substitute(substitution)); } - + auto newLikelihoodExpression = this->getLikelihoodExpression().substitute(substitution); + STORM_LOG_THROW(likelihoodExpression.containsVariables() || likelihoodExpression.evaluateAsRational() >= 0, storm::exceptions::IllegalArgumentException, "Substitution yielding negative probabilities in '" << this->getLikelihoodExpression() << "' are not allowed."); // FIXME: The expression could be simplified, but 1/K (where K is an int) is then resolved to 0, which is incorrect (for probabilities). - return Update(this->getGlobalIndex(), this->getLikelihoodExpression().substitute(substitution), newAssignments, this->getFilename(), this->getLineNumber()); + return Update(this->getGlobalIndex(), newLikelihoodExpression, newAssignments, this->getFilename(), this->getLineNumber()); } Update Update::removeIdentityAssignments() const { From b3a2da48d96fa3c3584e988b0dfc5235f7f8faa8 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 31 Jul 2017 16:38:51 +0200 Subject: [PATCH 3/3] storm wellformedness constraints fixed in case of negative coefficients --- src/storm/analysis/GraphConditions.cpp | 29 +++++++++++++------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index 812429dec..fb7b9e84a 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -29,14 +29,14 @@ namespace storm { if (!storm::utility::isConstant(entry)) { if (entry.denominator().isConstant()) { if (entry.denominatorAsNumber() > 0) { - wellformedConstraintSet.emplace(entry.nominator().polynomial(), storm::CompareRelation::GEQ); + wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ); } else if (entry.denominatorAsNumber() < 0) { - wellformedConstraintSet.emplace(entry.nominator().polynomial(), storm::CompareRelation::LEQ); + wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); } else { assert(false); // Should fail before. } } else { - wellformedConstraintSet.emplace(entry.denominator().polynomial(), storm::CompareRelation::NEQ); + wellformedConstraintSet.emplace(entry.denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at state rewards not yet supported."); } } @@ -52,34 +52,35 @@ namespace storm { if (!storm::utility::isConstant(transition.getValue())) { // Assert: 0 <= transition <= 1 if (transition.getValue().denominator().isConstant()) { + assert(transition.getValue().denominator().constantPart() != 0); if (transition.getValue().denominator().constantPart() > 0) { // Assert: nom <= denom - wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomial(), storm::CompareRelation::LEQ); + wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::LEQ); // Assert: nom >= 0 - wellformedConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ); + wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ); } else if (transition.getValue().denominator().constantPart() < 0) { // Assert nom >= denom - wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomial(), storm::CompareRelation::GEQ); + wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::GEQ); // Assert: nom <= 0 - wellformedConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ); + wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); } else { STORM_LOG_ASSERT(false, "Denominator must not equal 0."); } } else { // Assert: denom != 0 - wellformedConstraintSet.emplace(transition.getValue().denominator().polynomial(), storm::CompareRelation::NEQ); + wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ); // Assert: transition >= 0 <==> if denom > 0 then nom >= 0 else nom <= 0 - wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType::val(transition.getValue().denominator().polynomial(), storm::CompareRelation::GREATER), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ)); + wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType::val(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER), typename ConstraintType::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ), typename ConstraintType::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ)); // TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0 } // Assert: transition > 0 - graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::NEQ); + graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ); } } STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1."); if(!storm::utility::isConstant(sum)) { // Assert: sum == 1 - wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomial(), storm::CompareRelation::EQ); + wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomialWithCoefficient(), storm::CompareRelation::EQ); } } @@ -95,14 +96,14 @@ namespace storm { if(!entry.getValue().isConstant()) { if (entry.getValue().denominator().isConstant()) { if (entry.getValue().denominatorAsNumber() > 0) { - wellformedConstraintSet.emplace(entry.getValue().nominator().polynomial(), storm::CompareRelation::GEQ); + wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ); } else if (entry.getValue().denominatorAsNumber() < 0) { - wellformedConstraintSet.emplace(entry.getValue().nominator().polynomial(), storm::CompareRelation::LEQ); + wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); } else { assert(false); // Should fail before. } } else { - wellformedConstraintSet.emplace(entry.getValue().denominator().polynomial(), storm::CompareRelation::NEQ); + 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."); } }