diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index 4f47f15a7..9d915e73e 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -50,25 +50,34 @@ namespace storm { for (auto const& transition : dtmc.getRows(state)) { sum += transition.getValue(); if (!storm::utility::isConstant(transition.getValue())) { + // Assert: 0 <= transition <= 1 if (transition.getValue().denominator().isConstant()) { - if (transition.getValue().denominatorAsNumber() > 0) { + if (transition.getValue().denominator().constantPart() > 0) { + // Assert: nom <= denom wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomial(), storm::CompareRelation::LEQ); + // Assert: nom >= 0 wellformedConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ); - } else if (transition.getValue().denominatorAsNumber() < 0) { + } else if (transition.getValue().denominator().constantPart() < 0) { + // Assert nom >= denom wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomial(), storm::CompareRelation::GEQ); + // Assert: nom <= 0 wellformedConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ); } else { - assert(false); // Should fail before. + STORM_LOG_ASSERT(false, "Denominator must not equal 0."); } } else { + // Assert: denom != 0 wellformedConstraintSet.emplace(transition.getValue().denominator().polynomial(), storm::CompareRelation::NEQ); - wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::GREATER), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ)); + // 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)); + // TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0 } graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomial(), 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); }