added output of first 3 deadlock states in symbolic model builder

Former-commit-id: e33a984593

src/builder/DdPrismModelBuilder.cpp

@@ -1055,7 +1055,12 @@ 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.");
+                    STORM_LOG_WARN("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states. For example in");
+                    
+                    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);
+                    }
 
                     if (program.getModelType() == storm::prism::Program::ModelType::DTMC) {
                         // For DTMCs, we can simply add the identity of the global module for all deadlock states.

src/storage/expressions/SimpleValuation.cpp

@@ -1,10 +1,14 @@
 #include "src/storage/expressions/SimpleValuation.h"
 
 #include <boost/functional/hash.hpp>
+#include <boost/algorithm/string/join.hpp>
 
 #include "src/storage/expressions/ExpressionManager.h"
 #include "src/storage/expressions/Variable.h"
 
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidTypeException.h"
+
 namespace storm {
     namespace expressions {
         SimpleValuation::SimpleValuation() : Valuation(nullptr) {
@@ -87,6 +91,25 @@ namespace storm {
             rationalValues[rationalVariable.getOffset()] = value;
         }
         
+        std::string SimpleValuation::toPrettyString() const {
+            std::vector<std::string> assignments;
+            for (auto const& variable : this->getManager()) {
+                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);
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type.");
+                }
+                assignments.push_back(stream.str());
+            }
+            return "[" + boost::join(assignments, ", ") + "]";
+        }
+        
         std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation) {
             out << "valuation {" << std::endl;
             out << valuation.getManager() << std::endl;

src/storage/expressions/SimpleValuation.h

@@ -54,6 +54,8 @@ namespace storm {
             virtual double getRationalValue(Variable const& rationalVariable) const override;
             virtual void setRationalValue(Variable const& rationalVariable, double value) override;
             
+            virtual std::string toPrettyString() const;
+            
             friend std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation);
             
         private: