From 36b67a3a38480d53b5b28a2d707dbb26cbae7dbf Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 27 Aug 2015 09:34:18 +0200 Subject: [PATCH] refined output of deadlock states a bit Former-commit-id: 4262871295a3665894549bd52dccb2eae8b2fbd3 --- src/builder/DdPrismModelBuilder.cpp | 4 ++-- src/storage/expressions/SimpleValuation.cpp | 18 +++++++++--------- src/storage/expressions/SimpleValuation.h | 10 ++++++++-- 3 files changed, 19 insertions(+), 13 deletions(-) diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index d2108f150..1c1d599a5 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -1055,11 +1055,11 @@ namespace storm { if (!deadlockStates.isZero()) { // If we need to fix deadlocks, we do so now. if (!storm::settings::generalSettings().isDontFixDeadlocksSet()) { - STORM_LOG_WARN("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states. For example in"); + STORM_LOG_INFO("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states. The first three of these states are: "); uint_fast64_t count = 0; for (auto it = deadlockStates.begin(), ite = deadlockStates.end(); it != ite && count < 3; ++it, ++count) { - STORM_LOG_WARN((*it).first.toPrettyString() << std::endl); + STORM_LOG_INFO((*it).first.toPrettyString(generationInfo.rowMetaVariables) << std::endl); } if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index 472687a2e..57035b397 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/src/storage/expressions/SimpleValuation.cpp @@ -91,17 +91,17 @@ namespace storm { rationalValues[rationalVariable.getOffset()] = value; } - std::string SimpleValuation::toPrettyString() const { + std::string SimpleValuation::toPrettyString(std::set const& selectedVariables) const { std::vector assignments; - for (auto const& variable : this->getManager()) { + for (auto const& variable : selectedVariables) { std::stringstream stream; - stream << variable.first.getName() << "="; - if (variable.second.isBooleanType()) { - stream << std::boolalpha << this->getBooleanValue(variable.first) << std::noboolalpha; - } else if (variable.second.isIntegerType()) { - stream << this->getIntegerValue(variable.first); - } else if (variable.second.isRationalType()) { - stream << this->getRationalValue(variable.first); + stream << variable.getName() << "="; + if (variable.hasBooleanType()) { + stream << std::boolalpha << this->getBooleanValue(variable) << std::noboolalpha; + } else if (variable.hasIntegerType()) { + stream << this->getIntegerValue(variable); + } else if (variable.hasRationalType()) { + stream << this->getRationalValue(variable); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type."); } diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h index 097f30138..47278e1ee 100644 --- a/src/storage/expressions/SimpleValuation.h +++ b/src/storage/expressions/SimpleValuation.h @@ -3,7 +3,7 @@ #include #include -#include +#include #include "src/storage/expressions/Valuation.h" @@ -54,7 +54,13 @@ namespace storm { virtual double getRationalValue(Variable const& rationalVariable) const override; virtual void setRationalValue(Variable const& rationalVariable, double value) override; - virtual std::string toPrettyString() const; + /*! + * Returns a string representation of the valuation of the selected variables. + * + * @param selectedVariables The variables to select. + * @return The string representation. + */ + virtual std::string toPrettyString(std::set const& selectedVariables) const; friend std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation);