From 1f5439e270fda649a63f6be8f4fdf75cad829eda Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sun, 6 Mar 2016 20:08:53 +0100
Subject: [PATCH] added state labeling generator interface

Former-commit-id: eb7668741fa1561dbb2bd3c043a7b4b5674327fe
---
 src/builder/ExplicitPrismModelBuilder.cpp     | 30 ++---------
 src/generator/NextStateGenerator.h            |  2 +-
 src/generator/PrismNextStateGenerator.h       |  2 +-
 src/generator/PrismStateLabelingGenerator.cpp | 50 +++++++++++++++++++
 src/generator/PrismStateLabelingGenerator.h   | 31 ++++++++++++
 src/generator/StateLabelingGenerator.h        | 20 ++++++++
 6 files changed, 106 insertions(+), 29 deletions(-)
 create mode 100644 src/generator/PrismStateLabelingGenerator.cpp
 create mode 100644 src/generator/PrismStateLabelingGenerator.h
 create mode 100644 src/generator/StateLabelingGenerator.h

diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index 1ef7f3ad8..ef53b9e43 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -12,6 +12,7 @@
 #include "src/settings/modules/GeneralSettings.h"
 
 #include "src/generator/PrismNextStateGenerator.h"
+#include "src/generator/PrismStateLabelingGenerator.h"
 
 #include "src/utility/prism.h"
 #include "src/utility/constants.h"
@@ -558,33 +559,8 @@ namespace storm {
         
         template <typename ValueType, typename RewardModelType, typename StateType>
         storm::models::sparse::StateLabeling ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::buildStateLabeling() {
-            std::vector<storm::prism::Label> const& labels = program.getLabels();
-            
-            storm::expressions::ExpressionEvaluator<ValueType> evaluator(program.getManager());
-            storm::models::sparse::StateLabeling result(internalStateInformation.numberOfStates);
-            
-            // Initialize labeling.
-            for (auto const& label : labels) {
-                result.addLabel(label.getName());
-            }
-            for (auto const& stateIndexPair : internalStateInformation.stateStorage) {
-                unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, evaluator);
-
-                for (auto const& label : labels) {
-                    // Add label to state, if the corresponding expression is true.
-                    if (evaluator.asBool(label.getStatePredicateExpression())) {
-                        result.addLabelToState(label.getName(), stateIndexPair.second);
-                    }
-                }
-            }
-            
-            // Also label the initial state with the special label "init".
-            result.addLabel("init");
-            for (auto index : internalStateInformation.initialStateIndices) {
-                result.addLabelToState("init", index);
-            }
-            
-            return result;
+            storm::generator::PrismStateLabelingGenerator<ValueType, StateType> generator(program, variableInformation);
+            return generator.generate(internalStateInformation.stateStorage, internalStateInformation.initialStateIndices);
         }
         
         // Explicitly instantiate the class.
diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h
index f70709779..779a49ef3 100644
--- a/src/generator/NextStateGenerator.h
+++ b/src/generator/NextStateGenerator.h
@@ -21,4 +21,4 @@ namespace storm {
     }
 }
 
-#endif
\ No newline at end of file
+#endif /* STORM_GENERATOR_NEXTSTATEGENERATOR_H_ */
\ No newline at end of file
diff --git a/src/generator/PrismNextStateGenerator.h b/src/generator/PrismNextStateGenerator.h
index e9c63502e..d8eddc0ac 100644
--- a/src/generator/PrismNextStateGenerator.h
+++ b/src/generator/PrismNextStateGenerator.h
@@ -92,7 +92,7 @@ namespace storm {
             // An optional expression that governs which states must not be explored.
             boost::optional<storm::expressions::Expression> terminalExpression;
 
-            // Information about how the variables are packed
+            // Information about how the variables are packed.
             VariableInformation const& variableInformation;
             
             // An evaluator used to evaluate expressions.
diff --git a/src/generator/PrismStateLabelingGenerator.cpp b/src/generator/PrismStateLabelingGenerator.cpp
new file mode 100644
index 000000000..6022ce063
--- /dev/null
+++ b/src/generator/PrismStateLabelingGenerator.cpp
@@ -0,0 +1,50 @@
+#include "src/generator/PrismStateLabelingGenerator.h"
+
+#include "src/generator/CompressedState.h"
+
+#include "src/storage/expressions/ExpressionEvaluator.h"
+
+namespace storm {
+    namespace generator {
+        
+        template<typename ValueType, typename StateType>
+        PrismStateLabelingGenerator<ValueType, StateType>::PrismStateLabelingGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation) : program(program), variableInformation(variableInformation) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType, typename StateType>
+        storm::models::sparse::StateLabeling PrismStateLabelingGenerator<ValueType, StateType>::generate(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices) {
+            std::vector<storm::prism::Label> const& labels = program.getLabels();
+            
+            storm::expressions::ExpressionEvaluator<ValueType> evaluator(program.getManager());
+            storm::models::sparse::StateLabeling result(states.size());
+            
+            // Initialize labeling.
+            for (auto const& label : labels) {
+                result.addLabel(label.getName());
+            }
+            for (auto const& stateIndexPair : states) {
+                unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, evaluator);
+                
+                for (auto const& label : labels) {
+                    // Add label to state, if the corresponding expression is true.
+                    if (evaluator.asBool(label.getStatePredicateExpression())) {
+                        result.addLabelToState(label.getName(), stateIndexPair.second);
+                    }
+                }
+            }
+            
+            // Also label the initial state with the special label "init".
+            result.addLabel("init");
+            for (auto index : initialStateIndices) {
+                result.addLabelToState("init", index);
+            }
+            
+            return result;
+        }
+        
+        template class PrismStateLabelingGenerator<double, uint32_t>;
+        template class PrismStateLabelingGenerator<storm::RationalFunction, uint32_t>;
+
+    }
+}
\ No newline at end of file
diff --git a/src/generator/PrismStateLabelingGenerator.h b/src/generator/PrismStateLabelingGenerator.h
new file mode 100644
index 000000000..9859453ba
--- /dev/null
+++ b/src/generator/PrismStateLabelingGenerator.h
@@ -0,0 +1,31 @@
+#ifndef STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_
+#define STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_
+
+#include "src/generator/StateLabelingGenerator.h"
+
+#include "src/generator/VariableInformation.h"
+
+#include "src/storage/prism/Program.h"
+
+namespace storm {
+    namespace generator {
+        
+        template<typename ValueType, typename StateType = uint32_t>
+        class PrismStateLabelingGenerator : public StateLabelingGenerator<StateType> {
+        public:
+            PrismStateLabelingGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation);
+            
+            virtual storm::models::sparse::StateLabeling generate(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) override;
+            
+        private:
+            // The program for which to generate the labels.
+            storm::prism::Program const& program;
+            
+            // Information about how the variables are packed.
+            VariableInformation const& variableInformation;
+        };
+        
+    }
+}
+
+#endif /* STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_ */
\ No newline at end of file
diff --git a/src/generator/StateLabelingGenerator.h b/src/generator/StateLabelingGenerator.h
new file mode 100644
index 000000000..17401c703
--- /dev/null
+++ b/src/generator/StateLabelingGenerator.h
@@ -0,0 +1,20 @@
+#ifndef STORM_GENERATOR_STATELABELINGGENERATOR_H_
+#define STORM_GENERATOR_STATELABELINGGENERATOR_H_
+
+#include "src/models/sparse/StateLabeling.h"
+
+#include "src/storage/BitVectorHashMap.h"
+
+namespace storm {
+    namespace generator {
+        
+        template<typename StateType = uint32_t>
+        class StateLabelingGenerator {
+        public:
+            virtual storm::models::sparse::StateLabeling generate(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) = 0;
+        };
+        
+    }
+}
+
+#endif /* STORM_GENERATOR_STATELABELINGGENERATOR_H_ */
\ No newline at end of file