diff --git a/CHANGELOG.md b/CHANGELOG.md
index 40ee6caa3..5fb7d1140 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -8,10 +8,11 @@ The releases of major and minor versions contain an overview of changes since th
 Version 1.5.x
 -------------
 ## Version 1.5.x (Under development)
-- Scheduler export: Properly handle models with end components. Added export in .json format.
+- Changed default Dd library from `cudd` to `sylvan`. The Dd library can be changed back to `cudd` using the command line switch `--ddlib`.
+- Scheduler export: Properly handle models with end components. Added export in `.json` format.
 - CMake: Search for Gurobi prefers new versions
 - CMake: We no longer ship xerces-c. If xerces-c is not found on the system, storm-gspn will not be able to parse xml-based GSPN formats 
-- `Eigen' library: The source code of Eigen is no longer included but downloaded from an external repository instead. Incremented Eigen version to 3.3.7 which fixes a compilation issue with recent XCode Versions.
+- Eigen library: The source code of Eigen is no longer included but downloaded from an external repository instead. Incremented Eigen version to 3.3.7 which fixes a compilation issue with recent XCode versions.
 - Tests: Enabled tests for permissive schedulers
 - `storm-counterexamples`: fix when computing multiple counterexamples in debug mode
 - `storm-dft`: Renamed setting `--show-dft-stats` to `dft-statistics` and added approximation information to statistics.
diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp
index 0dad59191..b4be0dd6a 100644
--- a/src/storm/builder/ExplicitModelBuilder.cpp
+++ b/src/storm/builder/ExplicitModelBuilder.cpp
@@ -105,7 +105,7 @@ namespace storm {
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
-        void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianStates) {
+        void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianStates, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder) {
             
             // Create markovian states bit vector, if required.
             if (generator->getModelType() == storm::generator::ModelType::MA) {
@@ -154,6 +154,9 @@ namespace storm {
                 }
                 
                 generator->load(currentState);
+                if (stateValuationsBuilder) {
+                    generator->addStateValuation(currentIndex, stateValuationsBuilder.get());
+                }
                 storm::generator::StateBehavior<ValueType, StateType> behavior = generator->expand(stateToIdCallback);
                 
                 // If there is no behavior, we might have to introduce a self-loop.
@@ -188,7 +191,7 @@ namespace storm {
                         ++currentRow;
                         ++currentRowGroup;
                     } else {
-                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from probabilistic program: found deadlock state (" << generator->toValuation(currentState).toString(true) << "). For fixing these, please provide the appropriate option.");
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from probabilistic program: found deadlock state (" << generator->stateToString(currentState) << "). For fixing these, please provide the appropriate option.");
                     }
                 } else {
                     // Add the state rewards to the corresponding reward models.
@@ -314,7 +317,13 @@ namespace storm {
             ChoiceInformationBuilder choiceInformationBuilder;
             boost::optional<storm::storage::BitVector> markovianStates;
             
-            buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates);
+            // If we need to build state valuations, initialize them now.
+            boost::optional<storm::storage::sparse::StateValuationsBuilder> stateValuationsBuilder;
+            if (generator->getOptions().isBuildStateValuationsSet()) {
+                stateValuationsBuilder = generator->initializeStateValuationsBuilder();
+            }
+            
+            buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates, stateValuationsBuilder);
             
             // Initialize the model components with the obtained information.
             storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel(), std::move(markovianStates));
@@ -327,12 +336,8 @@ namespace storm {
             modelComponents.choiceLabeling = choiceInformationBuilder.buildChoiceLabeling(modelComponents.transitionMatrix.getRowCount());
             
             // If requested, build the state valuations and choice origins
-            if (generator->getOptions().isBuildStateValuationsSet()) {
-                std::vector<storm::expressions::SimpleValuation> valuations(modelComponents.transitionMatrix.getRowGroupCount());
-                for (auto const& bitVectorIndexPair : stateStorage.stateToId) {
-                    valuations[bitVectorIndexPair.second] = generator->toValuation(bitVectorIndexPair.first);
-                }
-                modelComponents.stateValuations = storm::storage::sparse::StateValuations(std::move(valuations));
+            if (stateValuationsBuilder) {
+                modelComponents.stateValuations = stateValuationsBuilder->build(modelComponents.transitionMatrix.getRowGroupCount());
             }
             if (generator->getOptions().isBuildChoiceOriginsSet()) {
                 auto originData = choiceInformationBuilder.buildDataOfChoiceOrigins(modelComponents.transitionMatrix.getRowCount());
diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h
index 58be400ab..4a94ad724 100644
--- a/src/storm/builder/ExplicitModelBuilder.h
+++ b/src/storm/builder/ExplicitModelBuilder.h
@@ -107,9 +107,10 @@ namespace storm {
              * @param transitionMatrixBuilder The builder of the transition matrix.
              * @param rewardModelBuilders The builders for the selected reward models.
              * @param choiceInformationBuilder The builder for the requested information of the choices
-             * @param markovianChoices is set to a bit vector storing whether a choice is markovian (is only set if the model type requires this information).
+             * @param markovianChoices is set to a bit vector storing whether a choice is Markovian (is only set if the model type requires this information).
+             * @param stateValuationsBuilder if not boost::none, we insert valuations for the corresponding states
              */
-            void buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianChoices);
+            void buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianChoices, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder);
             
             /*!
              * Explores the state space of the given program and returns the components of the model as a result.
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
diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp
index 87baa0b98..0506629f1 100644
--- a/src/storm/generator/JaniNextStateGenerator.cpp
+++ b/src/storm/generator/JaniNextStateGenerator.cpp
@@ -394,7 +394,7 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        void JaniNextStateGenerator<ValueType, StateType>::applyTransientUpdate(TransientVariableValuation<ValueType>& transientValuation, storm::jani::detail::ConstAssignments const& transientAssignments,  storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator) {
+        void JaniNextStateGenerator<ValueType, StateType>::applyTransientUpdate(TransientVariableValuation<ValueType>& transientValuation, storm::jani::detail::ConstAssignments const& transientAssignments,  storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator) const {
             
             auto assignmentIt = transientAssignments.begin();
             auto assignmentIte = transientAssignments.end();
@@ -457,15 +457,7 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        StateBehavior<ValueType, StateType> JaniNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
-            // Prepare the result, in case we return early.
-            StateBehavior<ValueType, StateType> result;
-            
-            // Retrieve the locations from the state.
-            std::vector<uint64_t> locations = getLocations(*this->state);
-            
-            // First, construct the state rewards, as we may return early if there are no choices later and we already
-            // need the state rewards then.
+        TransientVariableValuation<ValueType> JaniNextStateGenerator<ValueType, StateType>::getTransientVariableValuationAtLocations(std::vector<uint64_t> const& locations) const {
             uint64_t automatonIndex = 0;
             TransientVariableValuation<ValueType> transientVariableValuation;
             for (auto const& automatonRef : this->parallelAutomata) {
@@ -476,6 +468,84 @@ namespace storm {
                 applyTransientUpdate(transientVariableValuation, location.getAssignments().getTransientAssignments(), *this->evaluator);
                 ++automatonIndex;
             }
+            return transientVariableValuation;
+        }
+        
+        template<typename ValueType, typename StateType>
+        storm::storage::sparse::StateValuationsBuilder JaniNextStateGenerator<ValueType, StateType>::initializeStateValuationsBuilder() const {
+            auto result = NextStateGenerator<ValueType, StateType>::initializeStateValuationsBuilder();
+            // Also add information for transient variables
+            for (auto const& varInfo : transientVariableInformation.booleanVariableInformation) {
+                result.addVariable(varInfo.variable);
+            }
+            for (auto const& varInfo : transientVariableInformation.integerVariableInformation) {
+                result.addVariable(varInfo.variable);
+            }
+            for (auto const& varInfo : transientVariableInformation.rationalVariableInformation) {
+                result.addVariable(varInfo.variable);
+            }
+            return result;
+        }
+        
+        template<typename ValueType, typename StateType>
+        void JaniNextStateGenerator<ValueType, StateType>::addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const {
+            std::vector<bool> booleanValues;
+            booleanValues.reserve(this->variableInformation.booleanVariables.size() + transientVariableInformation.booleanVariableInformation.size());
+            std::vector<int64_t> integerValues;
+            integerValues.reserve(this->variableInformation.locationVariables.size() + this->variableInformation.integerVariables.size() + transientVariableInformation.integerVariableInformation.size());
+            std::vector<storm::RationalNumber> rationalValues;
+            rationalValues.reserve(transientVariableInformation.rationalVariableInformation.size());
+            
+            // Add values for non-transient variables
+            extractVariableValues(*this->state, this->variableInformation, integerValues, booleanValues, integerValues);
+            
+            // Add values for transient variables
+            auto transientVariableValuation = getTransientVariableValuationAtLocations(getLocations(*this->state));
+            {
+                auto varIt = transientVariableValuation.booleanValues.begin();
+                for (auto const& varInfo : transientVariableInformation.booleanVariableInformation) {
+                    if (varIt->first->variable == varInfo.variable) {
+                        booleanValues.push_back(varIt->second);
+                    } else {
+                        booleanValues.push_back(varInfo.defaultValue);
+                    }
+                }
+            }
+            {
+                auto varIt = transientVariableValuation.integerValues.begin();
+                for (auto const& varInfo : transientVariableInformation.integerVariableInformation) {
+                    if (varIt->first->variable == varInfo.variable) {
+                        integerValues.push_back(varIt->second);
+                    } else {
+                        integerValues.push_back(varInfo.defaultValue);
+                    }
+                }
+            }
+            {
+                auto varIt = transientVariableValuation.rationalValues.begin();
+                for (auto const& varInfo : transientVariableInformation.rationalVariableInformation) {
+                    if (varIt->first->variable == varInfo.variable) {
+                        rationalValues.push_back(storm::utility::convertNumber<storm::RationalNumber>(varIt->second));
+                    } else {
+                        rationalValues.push_back(storm::utility::convertNumber<storm::RationalNumber>(varInfo.defaultValue));
+                    }
+                }
+            }
+            
+            valuationsBuilder.addState(currentStateIndex, std::move(booleanValues), std::move(integerValues), std::move(rationalValues));
+        }
+        
+        template<typename ValueType, typename StateType>
+        StateBehavior<ValueType, StateType> JaniNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
+            // Prepare the result, in case we return early.
+            StateBehavior<ValueType, StateType> result;
+            
+            // Retrieve the locations from the state.
+            std::vector<uint64_t> locations = getLocations(*this->state);
+            
+            // First, construct the state rewards, as we may return early if there are no choices later and we already
+            // need the state rewards then.
+            auto transientVariableValuation = getTransientVariableValuationAtLocations(locations);
             transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet());
             result.addStateRewards(evaluateRewardExpressions());
             this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator);
diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h
index 74ead73e6..de4fe24ed 100644
--- a/src/storm/generator/JaniNextStateGenerator.h
+++ b/src/storm/generator/JaniNextStateGenerator.h
@@ -50,8 +50,14 @@ namespace storm {
             virtual bool isPartiallyObservable() const override;
             virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
             
+            /// Initializes a builder for state valuations by adding the appropriate variables.
+            virtual storm::storage::sparse::StateValuationsBuilder initializeStateValuationsBuilder() const override;
+            
             virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;
             
+            /// Adds the valuation for the currently loaded state to the given builder
+            virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const override;
+            
             virtual std::size_t getNumberOfRewardModels() const override;
             virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override;
                         
@@ -102,7 +108,7 @@ namespace storm {
              * @params assignmentLevel The assignmentLevel that is to be considered for the update.
              * @return The resulting state.
              */
-            void applyTransientUpdate(TransientVariableValuation<ValueType>& transientValuation, storm::jani::detail::ConstAssignments const& transientAssignments, storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator);
+            void applyTransientUpdate(TransientVariableValuation<ValueType>& transientValuation, storm::jani::detail::ConstAssignments const& transientAssignments, storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator) const;
 
             /**
              * Required method to overload, but currently throws an error as POMDPs are not yet specified in JANI.
@@ -113,6 +119,8 @@ namespace storm {
              */
             virtual storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const override;
 
+            TransientVariableValuation<ValueType> getTransientVariableValuationAtLocations(std::vector<uint64_t> const& locations) const;
+            
             /*!
              * Retrieves all choices possible from the given state.
              *
diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp
index fd4578235..e83c9338d 100644
--- a/src/storm/generator/NextStateGenerator.cpp
+++ b/src/storm/generator/NextStateGenerator.cpp
@@ -47,6 +47,21 @@ namespace storm {
             return variableInformation.getTotalBitOffset(true);
         }
         
+        template<typename ValueType, typename StateType>
+        storm::storage::sparse::StateValuationsBuilder NextStateGenerator<ValueType, StateType>::initializeStateValuationsBuilder() const {
+            storm::storage::sparse::StateValuationsBuilder result;
+            for (auto const& v : variableInformation.locationVariables) {
+                result.addVariable(v.variable);
+            }
+            for (auto const& v : variableInformation.booleanVariables) {
+                result.addVariable(v.variable);
+            }
+            for (auto const& v : variableInformation.integerVariables) {
+                result.addVariable(v.variable);
+            }
+            return result;
+        }
+        
         template<typename ValueType, typename StateType>
         void NextStateGenerator<ValueType, StateType>::load(CompressedState const& state) {
             // Since almost all subsequent operations are based on the evaluator, we load the state into it now.
@@ -64,6 +79,16 @@ namespace storm {
             return evaluator->asBool(expression);
         }
         
+        template<typename ValueType, typename StateType>
+        void NextStateGenerator<ValueType, StateType>::addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const {
+            std::vector<bool> booleanValues;
+            booleanValues.reserve(variableInformation.booleanVariables.size());
+            std::vector<int64_t> integerValues;
+            integerValues.reserve(variableInformation.locationVariables.size() + variableInformation.integerVariables.size());
+            extractVariableValues(*this->state, variableInformation, integerValues, booleanValues, integerValues);
+            valuationsBuilder.addState(currentStateIndex, std::move(booleanValues), std::move(integerValues));
+        }
+        
         template<typename ValueType, typename StateType>
         storm::models::sparse::StateLabeling NextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions) {
             
@@ -168,8 +193,8 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        storm::expressions::SimpleValuation NextStateGenerator<ValueType, StateType>::toValuation(CompressedState const& state) const {
-            return unpackStateIntoValuation(state, variableInformation, *expressionManager);
+        std::string NextStateGenerator<ValueType, StateType>::stateToString(CompressedState const& state) const {
+            return toString(state, variableInformation);
         }
         
         template<typename ValueType, typename StateType>
diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h
index fb72de23f..c329f34d6 100644
--- a/src/storm/generator/NextStateGenerator.h
+++ b/src/storm/generator/NextStateGenerator.h
@@ -10,6 +10,7 @@
 #include "storm/storage/sparse/StateStorage.h"
 #include "storm/storage/expressions/ExpressionEvaluator.h"
 #include "storm/storage/sparse/ChoiceOrigins.h"
+#include "storm/storage/sparse/StateValuations.h"
 
 #include "storm/builder/BuilderOptions.h"
 #include "storm/builder/RewardModelInformation.h"
@@ -54,14 +55,20 @@ namespace storm {
             virtual bool isPartiallyObservable() const = 0;
             virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) = 0;
             
+            /// Initializes a builder for state valuations by adding the appropriate variables.
+            virtual storm::storage::sparse::StateValuationsBuilder initializeStateValuationsBuilder() const;
+            
             void load(CompressedState const& state);
             virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) = 0;
             bool satisfies(storm::expressions::Expression const& expression) const;
             
+            /// Adds the valuation for the currently loaded state to the given builder
+            virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const;
+            
             virtual std::size_t getNumberOfRewardModels() const = 0;
             virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const = 0;
             
-            storm::expressions::SimpleValuation toValuation(CompressedState const& state) const;
+            std::string stateToString(CompressedState const& state) const;
 
             uint32_t observabilityClass(CompressedState const& state) const;
 
diff --git a/src/storm/generator/TransientVariableInformation.cpp b/src/storm/generator/TransientVariableInformation.cpp
index 391f290cd..420e2ae6e 100644
--- a/src/storm/generator/TransientVariableInformation.cpp
+++ b/src/storm/generator/TransientVariableInformation.cpp
@@ -97,21 +97,21 @@ namespace storm {
         }
         
         template <typename ValueType>
-        TransientVariableData<bool> const& TransientVariableInformation<ValueType>::getBooleanArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) {
+        TransientVariableData<bool> const& TransientVariableInformation<ValueType>::getBooleanArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) const {
             std::vector<uint64_t> const& indices = arrayVariableToElementInformations.at(arrayVariable);
             STORM_LOG_THROW(arrayIndex < indices.size(), storm::exceptions::WrongFormatException, "Array access at array " << arrayVariable.getName() << " evaluates to array index " << arrayIndex << " which is out of bounds as the array size is " << indices.size() << ".");
             return booleanVariableInformation[indices[arrayIndex]];
         }
         
         template <typename ValueType>
-        TransientVariableData<int64_t> const& TransientVariableInformation<ValueType>::getIntegerArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) {
+        TransientVariableData<int64_t> const& TransientVariableInformation<ValueType>::getIntegerArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) const {
             std::vector<uint64_t> const& indices = arrayVariableToElementInformations.at(arrayVariable);
             STORM_LOG_THROW(arrayIndex < indices.size(), storm::exceptions::WrongFormatException, "Array access at array " << arrayVariable.getName() << " evaluates to array index " << arrayIndex << " which is out of bounds as the array size is " << indices.size() << ".");
             return integerVariableInformation[indices[arrayIndex]];
         }
         
         template <typename ValueType>
-        TransientVariableData<ValueType> const& TransientVariableInformation<ValueType>::getRationalArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) {
+        TransientVariableData<ValueType> const& TransientVariableInformation<ValueType>::getRationalArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) const {
             std::vector<uint64_t> const& indices = arrayVariableToElementInformations.at(arrayVariable);
             STORM_LOG_THROW(arrayIndex < indices.size(), storm::exceptions::WrongFormatException, "Array access at array " << arrayVariable.getName() << " evaluates to array index " << arrayIndex << " which is out of bounds as the array size is " << indices.size() << ".");
             return rationalVariableInformation[indices[arrayIndex]];
diff --git a/src/storm/generator/TransientVariableInformation.h b/src/storm/generator/TransientVariableInformation.h
index c6047f470..5ea1c6342 100644
--- a/src/storm/generator/TransientVariableInformation.h
+++ b/src/storm/generator/TransientVariableInformation.h
@@ -93,9 +93,9 @@ namespace storm {
             TransientVariableInformation() = default;
             
             void registerArrayVariableReplacements(storm::jani::ArrayEliminatorData const& arrayEliminatorData);
-            TransientVariableData<bool> const& getBooleanArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index);
-            TransientVariableData<int64_t> const& getIntegerArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index);
-            TransientVariableData<ValueType> const& getRationalArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index);
+            TransientVariableData<bool> const& getBooleanArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index) const;
+            TransientVariableData<int64_t> const& getIntegerArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index) const;
+            TransientVariableData<ValueType> const& getRationalArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index) const;
             
             void setDefaultValuesInEvaluator(storm::expressions::ExpressionEvaluator<ValueType>& evaluator) const;
             
diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp
index 0f05c1aa6..d520f930b 100644
--- a/src/storm/settings/modules/CoreSettings.cpp
+++ b/src/storm/settings/modules/CoreSettings.cpp
@@ -46,7 +46,7 @@ namespace storm {
                 
                 std::vector<std::string> ddLibraries = {"cudd", "sylvan"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, ddLibraryOptionName, false, "Sets which library is preferred for decision-diagram operations.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the library to prefer.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(ddLibraries)).setDefaultValueString("cudd").build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the library to prefer.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(ddLibraries)).setDefaultValueString("sylvan").build()).build());
                 
                 std::vector<std::string> lpSolvers = {"gurobi", "glpk", "z3"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.")
diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp
index 673a64173..689917f32 100644
--- a/src/storm/storage/Scheduler.cpp
+++ b/src/storm/storage/Scheduler.cpp
@@ -241,7 +241,7 @@ namespace storm {
                 }
                 storm::json<storm::RationalNumber> stateChoicesJson;
                 if (model && model->hasStateValuations()) {
-                    stateChoicesJson["s"] = model->getStateValuations().getStateValuation(state).toJson();
+                    stateChoicesJson["s"] = model->getStateValuations().toJson(state);
                 } else {
                     stateChoicesJson["s"] = state;
                 }
diff --git a/src/storm/storage/sparse/StateValuations.cpp b/src/storm/storage/sparse/StateValuations.cpp
index 833ed9399..b1d70b81b 100644
--- a/src/storm/storage/sparse/StateValuations.cpp
+++ b/src/storm/storage/sparse/StateValuations.cpp
@@ -1,37 +1,194 @@
 #include "storm/storage/sparse/StateValuations.h"
 
+#include "storm/storage/BitVector.h"
+
 #include "storm/utility/vector.h"
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidTypeException.h"
 
 namespace storm {
     namespace storage {
         namespace sparse {
             
-            StateValuations::StateValuations(std::vector<storm::expressions::SimpleValuation> const& valuations) : valuations(valuations) {
-                // Intentionally left empty.
+            StateValuations::StateValuation::StateValuation(std::vector<bool>&& booleanValues, std::vector<int64_t>&& integerValues, std::vector<storm::RationalNumber>&& rationalValues) : booleanValues(std::move(booleanValues)), integerValues(std::move(integerValues)), rationalValues(std::move(rationalValues)) {
+                // Intentionally left empty
             }
-                        
-            StateValuations::StateValuations(std::vector<storm::expressions::SimpleValuation>&& valuations) : valuations(std::move(valuations)) {
-                // Intentionally left empty.
+            
+            typename StateValuations::StateValuation const& StateValuations::getValuation(storm::storage::sparse::state_type const& stateIndex) const {
+                STORM_LOG_ASSERT(stateIndex < valuations.size(), "Invalid state index.");
+                STORM_LOG_ASSERT(assertValuation(valuations[stateIndex]), "Invalid  state valuations");
+                return valuations[stateIndex];
             }
             
-            std::string StateValuations::getStateInfo(state_type const& state) const {
-                return getStateValuation(state).toString();
+            bool StateValuations::getBooleanValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& booleanVariable) const {
+                auto const& valuation = getValuation(stateIndex);
+                STORM_LOG_ASSERT(variableToIndexMap.count(booleanVariable) > 0, "Variable " << booleanVariable.getName() << " is not part of this valuation.");
+                return valuation.booleanValues[variableToIndexMap.at(booleanVariable)];
             }
             
-            storm::expressions::SimpleValuation const& StateValuations::getStateValuation(storm::storage::sparse::state_type const& state) const {
-                return valuations[state];
+            int64_t const& StateValuations::getIntegerValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& integerVariable) const {
+                auto const& valuation = getValuation(stateIndex);
+                STORM_LOG_ASSERT(variableToIndexMap.count(integerVariable) > 0, "Variable " << integerVariable.getName() << " is not part of this valuation.");
+                return valuation.integerValues[variableToIndexMap.at(integerVariable)];
             }
-
+            
+            storm::RationalNumber const& StateValuations::getRationalValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& rationalVariable) const {
+                auto const& valuation = getValuation(stateIndex);
+                STORM_LOG_ASSERT(variableToIndexMap.count(rationalVariable) > 0, "Variable " << rationalVariable.getName() << " is not part of this valuation.");
+                return valuation.rationalValues[variableToIndexMap.at(rationalVariable)];
+            }
+            
+            bool StateValuations::isEmpty(storm::storage::sparse::state_type const& stateIndex) const {
+                auto const& valuation = getValuation(stateIndex);
+                return valuation.booleanValues.empty() && valuation.integerValues.empty() && valuation.rationalValues.empty();
+            }
+            
+            std::string StateValuations::toString(storm::storage::sparse::state_type const& stateIndex, bool pretty, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables) const {
+                auto const& valuation = getValuation(stateIndex);
+                typename std::map<storm::expressions::Variable, uint64_t>::const_iterator mapIt = variableToIndexMap.begin();
+                typename std::set<storm::expressions::Variable>::const_iterator setIt;
+                if (selectedVariables) {
+                    setIt = selectedVariables->begin();
+                }
+                std::vector<std::string> assignments;
+                while (mapIt != variableToIndexMap.end() && (!selectedVariables || setIt != selectedVariables->end())) {
+                    
+                    // Move Map iterator to next relevant position
+                    if (selectedVariables) {
+                        while (mapIt->first != *setIt) {
+                            ++mapIt;
+                            STORM_LOG_ASSERT(mapIt != variableToIndexMap.end(), "Valuation does not consider selected variable " << setIt->getName() << ".");
+                        }
+                    }
+                    
+                    auto const& variable = mapIt->first;
+                    std::stringstream stream;
+                    if (pretty) {
+                        if (variable.hasBooleanType() && !valuation.booleanValues[mapIt->second]) {
+                            stream << "!";
+                        }
+                        stream << variable.getName();
+                        if (variable.hasIntegerType()) {
+                            stream << "=" << valuation.integerValues[mapIt->second];
+                        } else if (variable.hasRationalType()) {
+                            stream << "=" << valuation.rationalValues[mapIt->second];
+                        } else {
+                            STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidTypeException, "Unexpected variable type.");
+                        }
+                    } else {
+                        if (variable.hasBooleanType()) {
+                            stream << std::boolalpha << valuation.booleanValues[mapIt->second] << std::noboolalpha;
+                        } else if (variable.hasIntegerType()) {
+                            stream << valuation.integerValues[mapIt->second];
+                        } else if (variable.hasRationalType()) {
+                            stream << valuation.rationalValues[mapIt->second];
+                        }
+                    }
+                    assignments.push_back(stream.str());
+                    
+                    // Go to next position
+                    if (selectedVariables) {
+                        ++setIt;
+                    } else {
+                        ++mapIt;
+                    }
+                }
+                if (pretty) {
+                    return "[" + boost::join(assignments, "\t& ") + "]";
+                } else {
+                    return "[" + boost::join(assignments, "\t") + "]";
+                }
+            }
+            
+            typename StateValuations::Json StateValuations::toJson(storm::storage::sparse::state_type const& stateIndex, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables) const {
+                auto const& valuation = getValuation(stateIndex);
+                typename std::map<storm::expressions::Variable, uint64_t>::const_iterator mapIt = variableToIndexMap.begin();
+                typename std::set<storm::expressions::Variable>::const_iterator setIt;
+                if (selectedVariables) {
+                    setIt = selectedVariables->begin();
+                }
+                Json result;
+                while (mapIt != variableToIndexMap.end() && (!selectedVariables || setIt != selectedVariables->end())) {
+                    // Move Map iterator to next relevant position
+                    if (selectedVariables) {
+                        while (mapIt->first != *setIt) {
+                            ++mapIt;
+                            STORM_LOG_ASSERT(mapIt != variableToIndexMap.end(), "Valuation does not consider selected variable " << setIt->getName() << ".");
+                        }
+                    }
+                    
+                    auto const& variable = mapIt->first;
+                    if (variable.hasBooleanType()) {
+                        result[variable.getName()] = bool(valuation.booleanValues[mapIt->second]);
+                    } else if (variable.hasIntegerType()) {
+                        result[variable.getName()] = valuation.integerValues[mapIt->second];
+                    } else if (variable.hasRationalType()) {
+                        result[variable.getName()] = valuation.rationalValues[mapIt->second];
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type.");
+                    }
+                
+                    // Go to next position
+                    if (selectedVariables) {
+                        ++setIt;
+                    } else {
+                        ++mapIt;
+                    }
+                }
+                return result;
+            }
+            
+            bool StateValuations::assertValuation(StateValuation const& valuation) const {
+                storm::storage::BitVector foundBooleanValues(valuation.booleanValues.size(), false);
+                storm::storage::BitVector foundIntegerValues(valuation.integerValues.size(), false);
+                storm::storage::BitVector foundRationalValues(valuation.rationalValues.size(), false);
+                for (auto const& varIndex : variableToIndexMap) {
+                    storm::storage::BitVector* bv;
+                    if (varIndex.first.hasBooleanType()) {
+                        bv = &foundBooleanValues;
+                    } else if (varIndex.first.hasIntegerType()) {
+                        bv = &foundIntegerValues;
+                    } else if (varIndex.first.hasRationalType()) {
+                        bv = &foundRationalValues;
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type.");
+                    }
+                    if (varIndex.second < bv->size()) {
+                        if (bv->get(varIndex.second)) {
+                            STORM_LOG_ERROR("Multiple variables refer to the same value index");
+                            return false;
+                        }
+                        bv->set(varIndex.second, true);
+                    } else {
+                        STORM_LOG_ERROR("Valuation does not provide a value for all variables");
+                        return false;
+                    }
+                }
+                if (!(foundBooleanValues.full() && foundIntegerValues.full() && foundRationalValues.full())) {
+                    STORM_LOG_ERROR("Valuation has too many entries.");
+                }
+                return true;
+            }
+            
+            StateValuations::StateValuations(std::map<storm::expressions::Variable, uint64_t> const& variableToIndexMap, std::vector<StateValuation>&& valuations) : variableToIndexMap(variableToIndexMap), valuations(valuations) {
+                // Intentionally left empty
+            }
+            
+            std::string StateValuations::getStateInfo(state_type const& state) const {
+                STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index.");
+                return this->toString(state);
+            }
+            
             uint_fast64_t StateValuations::getNumberOfStates() const {
                 return valuations.size();
             }
             
             StateValuations StateValuations::selectStates(storm::storage::BitVector const& selectedStates) const {
-                return StateValuations(storm::utility::vector::filterVector(valuations, selectedStates));
+                return StateValuations(variableToIndexMap, storm::utility::vector::filterVector(valuations, selectedStates));
             }
 
             StateValuations StateValuations::selectStates(std::vector<storm::storage::sparse::state_type> const& selectedStates) const {
-                std::vector<storm::expressions::SimpleValuation> selectedValuations;
+                std::vector<StateValuation> selectedValuations;
                 selectedValuations.reserve(selectedStates.size());
                 for (auto const& selectedState : selectedStates){
                     if (selectedState < valuations.size()) {
@@ -40,7 +197,44 @@ namespace storm {
                         selectedValuations.emplace_back();
                     }
                 }
-                return StateValuations(std::move(selectedValuations));
+                return StateValuations(variableToIndexMap, std::move(selectedValuations));
+            }
+            
+            StateValuationsBuilder::StateValuationsBuilder() : booleanVarCount(0), integerVarCount(0), rationalVarCount(0) {
+                // Intentionally left empty.
+            }
+            
+            void StateValuationsBuilder::addVariable(storm::expressions::Variable const& variable) {
+                STORM_LOG_ASSERT(currentStateValuations.valuations.empty(), "Tried to add a variable, although a state has already been added before.");
+                STORM_LOG_ASSERT(currentStateValuations.variableToIndexMap.count(variable) == 0, "Variable " << variable.getName() << " already added.");
+                if (variable.hasBooleanType()) {
+                    currentStateValuations.variableToIndexMap[variable] = booleanVarCount++;
+                }
+                if (variable.hasIntegerType()) {
+                    currentStateValuations.variableToIndexMap[variable] = integerVarCount++;
+                }
+                if (variable.hasRationalType()) {
+                    currentStateValuations.variableToIndexMap[variable] = rationalVarCount++;
+                }
+            }
+            
+            void StateValuationsBuilder::addState(storm::storage::sparse::state_type const& state, std::vector<bool>&& booleanValues, std::vector<int64_t>&& integerValues, std::vector<storm::RationalNumber>&& rationalValues) {
+                if (state > currentStateValuations.valuations.size()) {
+                    currentStateValuations.valuations.resize(state);
+                }
+                if (state == currentStateValuations.valuations.size()) {
+                    currentStateValuations.valuations.emplace_back(std::move(booleanValues), std::move(integerValues), std::move(rationalValues));
+                } else {
+                    STORM_LOG_ASSERT(currentStateValuations.isEmpty(state), "Adding a valuation to the same state multiple times.");
+                    currentStateValuations.valuations[state] = typename StateValuations::StateValuation(std::move(booleanValues), std::move(integerValues), std::move(rationalValues));
+                }
+            }
+            
+            StateValuations StateValuationsBuilder::build(std::size_t totalStateCount) {
+                return std::move(currentStateValuations);
+                booleanVarCount = 0;
+                integerVarCount = 0;
+                rationalVarCount = 0;
             }
         }
     }
diff --git a/src/storm/storage/sparse/StateValuations.h b/src/storm/storage/sparse/StateValuations.h
index 84d5b7c2d..43edda895 100644
--- a/src/storm/storage/sparse/StateValuations.h
+++ b/src/storm/storage/sparse/StateValuations.h
@@ -1,35 +1,68 @@
-#ifndef STORM_STORAGE_SPARSE_STATEVALUATIONS_H_
-#define STORM_STORAGE_SPARSE_STATEVALUATIONS_H_
+#pragma once
 
 #include <cstdint>
 #include <string>
 
 #include "storm/storage/sparse/StateType.h"
 #include "storm/storage/BitVector.h"
-#include "storm/storage/expressions/SimpleValuation.h"
+#include "storm/storage/expressions/Variable.h"
 #include "storm/models/sparse/StateAnnotation.h"
+#include "storm/adapters/JsonAdapter.h"
 
 namespace storm {
     namespace storage {
         namespace sparse {
             
+            class StateValuationsBuilder;
+            
             // A structure holding information about the reachable state space that can be retrieved from the outside.
             class StateValuations : public storm::models::sparse::StateAnnotation {
-            
             public:
-                /*!
-                 * Constructs a state information object for the given number of states.
-                 */
-                StateValuations(std::vector<storm::expressions::SimpleValuation> const& valuations);
-                StateValuations(std::vector<storm::expressions::SimpleValuation>&& valuations);
+                friend class StateValuationsBuilder;
+                typedef storm::json<storm::RationalNumber> Json;
+
+                class StateValuation {
+                public:
+                    friend class StateValuations;
+                    StateValuation() = default;
+                    StateValuation(std::vector<bool>&& booleanValues, std::vector<int64_t>&& integerValues, std::vector<storm::RationalNumber>&& rationalValues);
+    
+                private:
+                    
+                    std::vector<bool> booleanValues;
+                    std::vector<int64_t> integerValues;
+                    std::vector<storm::RationalNumber> rationalValues;
+                };
                 
-                virtual ~StateValuations() = default;
+
+                StateValuations() = default;
                 
+                virtual ~StateValuations() = default;
                 virtual std::string getStateInfo(storm::storage::sparse::state_type const& state) const override;
                 
-                storm::expressions::SimpleValuation const& getStateValuation(storm::storage::sparse::state_type const& state) const;
+                bool getBooleanValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& booleanVariable) const;
+                int64_t const& getIntegerValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& integerVariable) const;
+                storm::RationalNumber const& getRationalValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& rationalVariable) const;
+                /// Returns true, if this valuation does not contain any value.
+                bool isEmpty(storm::storage::sparse::state_type const& stateIndex) const;
+                
+                /*!
+                 * Returns a string representation of the valuation.
+                 *
+                 * @param selectedVariables If given, only the informations for the variables in this set are processed.
+                 * @return The string representation.
+                 */
+                std::string toString(storm::storage::sparse::state_type const& stateIndex, bool pretty = true, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables = boost::none) const;
                 
-                // Returns the number of states that this object describes.
+                /*!
+                 * Returns a JSON representation of this valuation
+                 * @param selectedVariables If given, only the informations for the variables in this set are processed.
+                 * @return
+                 */
+                Json toJson(storm::storage::sparse::state_type const& stateIndex, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables = boost::none) const;
+
+                
+                // Returns the (current) number of states that this object describes.
                 uint_fast64_t getNumberOfStates() const;
                 
                 /*
@@ -45,14 +78,44 @@ namespace storm {
                 
                 
             private:
+                StateValuations(std::map<storm::expressions::Variable, uint64_t> const& variableToIndexMap, std::vector<StateValuation>&& valuations);
+                bool assertValuation(StateValuation const& valuation) const;
+                StateValuation const& getValuation(storm::storage::sparse::state_type const& stateIndex) const;
                 
+                std::map<storm::expressions::Variable, uint64_t> variableToIndexMap;
                 // A mapping from state indices to their variable valuations.
-                std::vector<storm::expressions::SimpleValuation> valuations;
+                std::vector<StateValuation> valuations;
                 
             };
             
+            class StateValuationsBuilder {
+            public:
+                StateValuationsBuilder();
+                
+                /*! Adds a new variable to keep track of for the state valuations.
+                 *! All variables need to be added before adding new states.
+                 */
+                void addVariable(storm::expressions::Variable const& variable);
+                
+                /*!
+                 * Adds a new state.
+                 * The variable values have to be given in the same order as the variables have been added.
+                 * The number of given variable values for each type needs to match the number of added variables.
+                 * After calling this method, no more variables should be added.
+                 */
+                 void addState(storm::storage::sparse::state_type const& state, std::vector<bool>&& booleanValues = {}, std::vector<int64_t>&& integerValues = {}, std::vector<storm::RationalNumber>&& rationalValues = {});
+                 
+                 /*!
+                  * Creates the finalized state valuations object.
+                  */
+                 StateValuations build(std::size_t totalStateCount);
+
+            private:
+                StateValuations currentStateValuations;
+                uint64_t booleanVarCount;
+                uint64_t integerVarCount;
+                uint64_t rationalVarCount;
+            };
         }
     }
 }
-
-#endif /* STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ */