Browse Source

Merge branch 'master' into dft

tempestpy_adaptions
Matthias Volk 6 years ago
parent
commit
a631a9d210
  1. 10
      src/storm/analysis/GraphConditions.cpp

10
src/storm/analysis/GraphConditions.cpp

@ -38,9 +38,10 @@ namespace storm {
auto const& transitionVars = entry.gatherVariables(); auto const& transitionVars = entry.gatherVariables();
variableSet.insert(transitionVars.begin(), transitionVars.end()); variableSet.insert(transitionVars.begin(), transitionVars.end());
if (entry.denominator().isConstant()) { if (entry.denominator().isConstant()) {
if (entry.denominatorAsNumber() > 0) {
assert(entry.denominator().constantPart() != 0);
if (entry.denominator().constantPart() > 0) {
wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ); wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
} else if (entry.denominatorAsNumber() < 0) {
} else if (entry.denominator().constantPart() < 0) {
wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
} else { } else {
assert(false); // Should fail before. assert(false); // Should fail before.
@ -117,9 +118,10 @@ namespace storm {
for (auto const& entry : rewModelEntry.second.getTransitionRewardMatrix()) { for (auto const& entry : rewModelEntry.second.getTransitionRewardMatrix()) {
if(!entry.getValue().isConstant()) { if(!entry.getValue().isConstant()) {
if (entry.getValue().denominator().isConstant()) { if (entry.getValue().denominator().isConstant()) {
if (entry.getValue().denominatorAsNumber() > 0) {
assert(entry.getValue().denominator().constantPart() != 0);
if (entry.getValue().denominator().constantPart() > 0) {
wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ); wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
} else if (entry.getValue().denominatorAsNumber() < 0) {
} else if (entry.getValue().denominator().constantPart() < 0) {
wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
} else { } else {
assert(false); // Should fail before. assert(false); // Should fail before.

Loading…
Cancel
Save