From 662bbd73d7a434d4c5a846cf35b46560ab86ea9c Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Mon, 18 Jul 2016 17:17:24 +0200
Subject: [PATCH] CompressedStateType as template argument for
 NextStateGenerator

Former-commit-id: 145182a9180b4d2f13f67f964086cf40e51528e6
---
 src/builder/ExplicitDFTModelBuilder.h   | 2 +-
 src/generator/NextStateGenerator.h      | 6 +++---
 src/generator/PrismNextStateGenerator.h | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h
index 71bfada61..eae19cb61 100644
--- a/src/builder/ExplicitDFTModelBuilder.h
+++ b/src/builder/ExplicitDFTModelBuilder.h
@@ -60,7 +60,7 @@ namespace storm {
             size_t initialStateIndex = 0;
 
         public:
-              struct LabelOptions {
+            struct LabelOptions {
                 bool buildFailLabel = true;
                 bool buildFailSafeLabel = false;
                 std::set<std::string> beLabels = {};
diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h
index 7dab9f470..67fd5f9f6 100644
--- a/src/generator/NextStateGenerator.h
+++ b/src/generator/NextStateGenerator.h
@@ -11,15 +11,15 @@
 
 namespace storm {
     namespace generator {
-        template<typename ValueType, typename StateType = uint32_t>
+        template<typename ValueType, typename CompressedStateType, typename StateType = uint32_t>
         class NextStateGenerator {
         public:
-            typedef std::function<StateType (CompressedState const&)> StateToIdCallback;
+            typedef std::function<StateType (CompressedStateType const&)> StateToIdCallback;
 
             virtual bool isDeterministicModel() const = 0;
             virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) = 0;
             
-            virtual void load(CompressedState const& state) = 0;
+            virtual void load(CompressedStateType const& state) = 0;
             virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) = 0;
             virtual bool satisfies(storm::expressions::Expression const& expression) const = 0;
         };
diff --git a/src/generator/PrismNextStateGenerator.h b/src/generator/PrismNextStateGenerator.h
index fe997d73a..fc1411aa0 100644
--- a/src/generator/PrismNextStateGenerator.h
+++ b/src/generator/PrismNextStateGenerator.h
@@ -13,9 +13,9 @@ namespace storm {
     namespace generator {
         
         template<typename ValueType, typename StateType = uint32_t>
-        class PrismNextStateGenerator : public NextStateGenerator<ValueType, StateType> {
+        class PrismNextStateGenerator : public NextStateGenerator<ValueType, CompressedState, StateType> {
         public:
-            typedef typename NextStateGenerator<ValueType, StateType>::StateToIdCallback StateToIdCallback;
+            typedef typename NextStateGenerator<ValueType, CompressedState, StateType>::StateToIdCallback StateToIdCallback;
             
             PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling);