Browse Source

fixing precision issue in sanity check and silencing min-max solver a bit

tempestpy_adaptions
dehnert 7 years ago
parent
commit
acf297a811
  1. 3
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  2. 4
      src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

3
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@ -548,9 +548,10 @@ namespace storm {
#ifndef NDEBUG
// As a sanity check, make sure our local upper bounds were in fact correct.
if (solver->hasUpperBound(storm::solver::AbstractEquationSolver<ValueType>::BoundType::Local)) {
auto precision = storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::MinMaxEquationSolverSettings>().getPrecision());
auto resultIt = x.begin();
for (auto const& entry : solver->getUpperBounds()) {
STORM_LOG_ASSERT(*resultIt <= entry, "Expecting result value for state " << std::distance(x.begin(), resultIt) << " to be <= " << entry << ", but got " << *resultIt << ".");
STORM_LOG_ASSERT(*resultIt <= entry + precision, "Expecting result value for state " << std::distance(x.begin(), resultIt) << " to be <= " << entry << ", but got " << *resultIt << ".");
++resultIt;
}
}

4
src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@ -1383,8 +1383,8 @@ namespace storm {
template<typename ValueType>
void IterativeMinMaxLinearEquationSolver<ValueType>::reportStatus(SolverStatus status, uint64_t iterations) {
switch (status) {
case SolverStatus::Converged: STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations."); break;
case SolverStatus::TerminatedEarly: STORM_LOG_INFO("Iterative solver terminated early after " << iterations << " iterations."); break;
case SolverStatus::Converged: STORM_LOG_TRACE("Iterative solver converged after " << iterations << " iterations."); break;
case SolverStatus::TerminatedEarly: STORM_LOG_TRACE("Iterative solver terminated early after " << iterations << " iterations."); break;
case SolverStatus::MaximalIterationsExceeded: STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations."); break;
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Iterative solver terminated unexpectedly.");

Loading…
Cancel
Save