diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 43e1e795c..8e41c96eb 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -62,7 +62,15 @@ namespace storm { template GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision() * 2, storm::settings::getModule().getRelativeTerminationCriterion()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule().getSolveMode()), debug(storm::settings::getModule().isDebugSet()) { - STORM_LOG_WARN_COND(!model.hasUndefinedConstants(), "Model contains undefined constants. Game-based abstraction can treat such models, but you should make sure that you did not simply forget to define these constants. In particular, it may be necessary to constrain the values of the undefined constants."); + if (model.hasUndefinedConstants()) { + auto undefinedConstants = model.getUndefinedConstants(); + std::vector undefinedConstantNames; + for (auto undefinedConstant : undefinedConstants) { + undefinedConstantNames.emplace_back(undefinedConstant.getName()); + } + + STORM_LOG_WARN_COND(!model.hasUndefinedConstants(), "Model contains undefined constants (" << boost::algorithm::join(undefinedConstantNames, ",") << "). Game-based abstraction can treat such models, but you should make sure that you did not simply forget to define these constants. In particular, it may be necessary to constrain the values of the undefined constants."); + } if (model.isPrismProgram()) { storm::prism::Program const& originalProgram = model.asPrismProgram(); @@ -664,7 +672,7 @@ namespace storm { // In this case, we know the result for the initial states for both player 2 minimizing and maximizing. STORM_LOG_TRACE("No initial state is a 'maybe' state."); - STORM_LOG_INFO("Obtained qualitative bounds [0, 1] on the actual value for the initial states. Refining abstraction based on qualitative check."); + STORM_LOG_INFO("Obtained qualitative bounds [0, 1] on the actual value for the initial states (after " << totalWatch.getTimeInMilliseconds() << "ms in iteration " << this->iteration << "). Refining abstraction based on qualitative check."); // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine. @@ -708,9 +716,9 @@ namespace storm { ValueType minVal = quantitativeResult.min.getInitialStatesRange().first; ValueType maxVal = quantitativeResult.max.getInitialStatesRange().second; if (std::is_same::value) { - STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms."); + STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms (after " << totalWatch.getTimeInMilliseconds() << "ms in iteration " << this->iteration << ")."); } else { - STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] (approx. [" << storm::utility::convertNumber(minVal) << ", " << storm::utility::convertNumber(maxVal) << "]) on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms."); + STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] (approx. [" << storm::utility::convertNumber(minVal) << ", " << storm::utility::convertNumber(maxVal) << "]) on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms (after " << totalWatch.getTimeInMilliseconds() << "ms in iteration " << this->iteration << ")."); } @@ -1259,7 +1267,7 @@ namespace storm { // In this case, we know the result for the initial states for both player 2 minimizing and maximizing. STORM_LOG_TRACE("No initial state is a 'maybe' state."); - STORM_LOG_INFO("Obtained qualitative bounds [0, 1] on the actual value for the initial states. Refining abstraction based on qualitative check."); + STORM_LOG_INFO("Obtained qualitative bounds [0, 1] on the actual value for the initial states (after " << totalWatch.getTimeInMilliseconds() << "ms in iteration " << this->iteration << "). Refining abstraction based on qualitative check."); // Post-process strategies for better refinements. storm::utility::Stopwatch strategyProcessingWatch(true); @@ -1312,9 +1320,9 @@ namespace storm { ValueType minVal = quantitativeResult.getMin().getRange(initialStates).first; ValueType maxVal = quantitativeResult.getMax().getRange(initialStates).second; if (std::is_same::value) { - STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms."); + STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms (after " << totalWatch.getTimeInMilliseconds() << "ms in iteration " << this->iteration << ")."); } else { - STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] (approx. [" << storm::utility::convertNumber(minVal) << ", " << storm::utility::convertNumber(maxVal) << "]) on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms."); + STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] (approx. [" << storm::utility::convertNumber(minVal) << ", " << storm::utility::convertNumber(maxVal) << "]) on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms (after " << totalWatch.getTimeInMilliseconds() << "ms in iteration " << this->iteration << ")."); } // (9) Check whether the lower and upper bounds are close enough to terminate with an answer. diff --git a/src/storm/solver/GmmxxLinearEquationSolver.cpp b/src/storm/solver/GmmxxLinearEquationSolver.cpp index 83d5b6ef6..e20a47280 100644 --- a/src/storm/solver/GmmxxLinearEquationSolver.cpp +++ b/src/storm/solver/GmmxxLinearEquationSolver.cpp @@ -106,7 +106,7 @@ namespace storm { STORM_LOG_INFO("Iterative solver converged after " << iter.get_iteration() << " iterations."); return true; } else { - STORM_LOG_WARN("Iterative solver did not converge."); + STORM_LOG_WARN("Iterative solver did not converge after " << iter.get_iteration() << " iterations."); return false; } } diff --git a/src/storm/utility/Stopwatch.cpp b/src/storm/utility/Stopwatch.cpp index 8c6f008a4..f694df496 100644 --- a/src/storm/utility/Stopwatch.cpp +++ b/src/storm/utility/Stopwatch.cpp @@ -10,11 +10,19 @@ namespace storm { } Stopwatch::SecondType Stopwatch::getTimeInSeconds() const { - return std::chrono::duration_cast(accumulatedTime).count(); + auto time = accumulatedTime; + if (!this->stopped()) { + time += std::chrono::high_resolution_clock::now() - startOfCurrentMeasurement; + } + return std::chrono::duration_cast(time).count(); } Stopwatch::MilisecondType Stopwatch::getTimeInMilliseconds() const { - return std::chrono::duration_cast(accumulatedTime).count(); + auto time = accumulatedTime; + if (!this->stopped()) { + time += std::chrono::high_resolution_clock::now() - startOfCurrentMeasurement; + } + return std::chrono::duration_cast(time).count(); } Stopwatch::NanosecondType Stopwatch::getTimeInNanoseconds() const {