diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index d211c8fb8..8d2537598 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -86,8 +86,7 @@ namespace storm { std::string color = ""; auto val = first.getValue(); auto vars = val.gatherVariables(); - for (auto itr = vars.begin(); itr != vars.end(); ++itr) { - if (varsMonotone.find(*itr) == varsMonotone.end()) { + for (auto itr = vars.begin(); itr != vars.end(); ++itr) { if (varsMonotone.find(*itr) == varsMonotone.end()) { varsMonotone[*itr].first = true; varsMonotone[*itr].second = true; } @@ -97,7 +96,6 @@ namespace storm { for (auto itr2 = transitions.begin(); itr2 != transitions.end(); ++itr2) { for (auto itr3 = transitions.begin(); itr3 != transitions.end(); ++itr3) { // TODO improve - auto derivative2 = (*itr2).second.derivative(*itr); auto derivative3 = (*itr3).second.derivative(*itr); STORM_LOG_THROW(derivative2.isConstant() && derivative3.isConstant(), storm::exceptions::NotSupportedException, "Expecting derivative to be constant"); @@ -108,8 +106,8 @@ namespace storm { value->first &=derivative2.constantPart() >= 0; value->second &=derivative2.constantPart() <= 0; } else if (compare == storm::analysis::Lattice::BELOW) { - value->first &=derivative3.constantPart() <= 0; - value->second &=derivative3.constantPart() >= 0; + value->first &=derivative3.constantPart() >= 0; + value->second &=derivative3.constantPart() <= 0; } else if (compare == storm::analysis::Lattice::SAME) { // Behaviour doesn't matter, as they are at the same level } else {