From 3a86cc4391a7a80359954ade82e150eb074fed49 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 25 May 2020 16:34:20 +0200
Subject: [PATCH] CompressedState: Added a method to create a human readable
 string out of the state. Added a method to "uncompress" by extracting all
 values into corresponding value vectors

---
 src/storm/generator/CompressedState.cpp | 37 +++++++++++++++++++++++++
 src/storm/generator/CompressedState.h   | 16 +++++++++++
 2 files changed, 53 insertions(+)

diff --git a/src/storm/generator/CompressedState.cpp b/src/storm/generator/CompressedState.cpp
index b623dab72..546b8e4bc 100644
--- a/src/storm/generator/CompressedState.cpp
+++ b/src/storm/generator/CompressedState.cpp
@@ -1,5 +1,7 @@
 #include "storm/generator/CompressedState.h"
 
+#include <boost/algorithm/string/join.hpp>
+
 #include "storm/generator/VariableInformation.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 #include "storm/storage/expressions/SimpleValuation.h"
@@ -43,6 +45,41 @@ namespace storm {
             return result;
         }
 
+        void extractVariableValues(CompressedState const& state, VariableInformation const& variableInformation, std::vector<int64_t>& locationValues, std::vector<bool>& booleanValues, std::vector<int64_t>& integerValues) {
+            for (auto const& locationVariable : variableInformation.locationVariables) {
+                if (locationVariable.bitWidth != 0) {
+                    locationValues.push_back(state.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth));
+                } else {
+                    locationValues.push_back(0);
+                }
+            }
+            for (auto const& booleanVariable : variableInformation.booleanVariables) {
+                booleanValues.push_back(state.get(booleanVariable.bitOffset));
+            }
+            for (auto const& integerVariable : variableInformation.integerVariables) {
+                integerValues.push_back(state.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound);
+            }
+        }
+        
+        std::string toString(CompressedState const& state, VariableInformation const& variableInformation) {
+            std::vector<std::string> assignments;
+            for (auto const& locationVariable : variableInformation.locationVariables) {
+                assignments.push_back(locationVariable.variable.getName() + "=");
+                    assignments.back() += std::to_string(locationVariable.bitWidth == 0 ? 0 : state.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth));
+            }
+            for (auto const& booleanVariable : variableInformation.booleanVariables) {
+                if (!state.get(booleanVariable.bitOffset)) {
+                    assignments.push_back("!" + booleanVariable.variable.getName());
+                } else {
+                    assignments.push_back(booleanVariable.variable.getName());
+                }
+            }
+            for (auto const& integerVariable : variableInformation.integerVariables) {
+                assignments.push_back(integerVariable.variable.getName() + "=" + std::to_string(state.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound));
+            }
+            return boost::join(assignments, " & ");
+        }
+
         storm::storage::BitVector computeObservabilityMask(VariableInformation const& variableInformation) {
             storm::storage::BitVector result(variableInformation.getTotalBitOffset(true));
             for (auto const& locationVariable : variableInformation.locationVariables) {
diff --git a/src/storm/generator/CompressedState.h b/src/storm/generator/CompressedState.h
index 302230273..8768929ee 100644
--- a/src/storm/generator/CompressedState.h
+++ b/src/storm/generator/CompressedState.h
@@ -37,6 +37,22 @@ namespace storm {
          */
         storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager);
 
+        /*!
+         * Appends the values of the given variables in the given state to the corresponding result vectors.
+         * locationValues are inserted before integerValues (relevant if both, locationValues and integerValues actually refer to the same vector)
+         * @param state The state
+         * @param variableInformation The variables
+         * @param locationValues
+         * @param booleanValues
+         * @param integerValues
+         */
+        void extractVariableValues(CompressedState const& state, VariableInformation const& variableInformation, std::vector<int64_t>& locationValues, std::vector<bool>& booleanValues, std::vector<int64_t>& integerValues);
+        
+        /*!
+         * Returns a (human readable) string representation of the variable valuation encoded by the given state
+         */
+        std::string toString(CompressedState const& state, VariableInformation const& variableInformation);
+
         /*!
          *
          * @param variableInformation