Browse Source

actually fixed the issue with timed reachability

tempestpy_adaptions
TimQu 8 years ago
parent
commit
7dd5c9e2c5
  1. 5
      src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp

5
src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp

@ -267,8 +267,13 @@ namespace storm {
digitizationError -= std::exp(-maxRate * timeBound) * storm::utility::pow(storm::utility::one<VT>() + maxRate * digitizationConstant, digitizedBound);
errorAwayFromZero += digitizationError;
}
if (storm::solver::maximize(obj.optimizationDirection)) {
this->offsetsToLowerBound[objIndex] = -errorTowardsZero;
this->offsetsToUpperBound[objIndex] = errorAwayFromZero;
} else {
this->offsetsToLowerBound[objIndex] = errorAwayFromZero;
this->offsetsToUpperBound[objIndex] = -errorTowardsZero;
}
}
}

Loading…
Cancel
Save