From cffb887c4fa54898b3e481504c66bdb69ce6d25c Mon Sep 17 00:00:00 2001
From: ThomasH <thomas.henn@rwth-aachen.de>
Date: Sun, 10 Apr 2016 01:37:22 +0200
Subject: [PATCH] add state labeling

Former-commit-id: 892cf083c7fb20d2e07699f9dad8a0d06d9de4d7
---
 src/builder/ExplicitGspnModelBuilder.cpp | 27 +++++++++++++++++++++++-
 src/builder/ExplicitGspnModelBuilder.h   |  8 +++++++
 2 files changed, 34 insertions(+), 1 deletion(-)

diff --git a/src/builder/ExplicitGspnModelBuilder.cpp b/src/builder/ExplicitGspnModelBuilder.cpp
index 98f76ad1d..ddf7bf616 100644
--- a/src/builder/ExplicitGspnModelBuilder.cpp
+++ b/src/builder/ExplicitGspnModelBuilder.cpp
@@ -70,7 +70,7 @@ namespace storm {
             }
 
             auto matrix = builder.build();
-            const storm::models::sparse::StateLabeling labeling; // TODO
+            auto labeling = getStateLabeling();
 
             return storm::models::sparse::MarkovAutomaton<double>(matrix, labeling, markovianStates, exitRates);
         }
@@ -244,6 +244,31 @@ namespace storm {
             return index;
         }
 
+        template<typename ValueType>
+        storm::models::sparse::StateLabeling ExplicitGspnModelBuilder<ValueType>::getStateLabeling() const {
+            storm::models::sparse::StateLabeling labeling(markings.size());
+
+            std::map<uint_fast64_t , std::string> idToName;
+            for (auto& place : gspn.getPlaces()) {
+                idToName[place.getID()] = place.getName();
+                labeling.addLabel(place.getName());
+            }
+
+            auto it = markings.begin();
+            for ( ; it != markings.end() ; ++it) {
+                auto bitvector = std::get<0>(*it);
+                storm::gspn::Marking marking(gspn.getNumberOfPlaces(), numberOfBits, bitvector);
+                for (auto i = 0; i < marking.getNumberOfPlaces(); i++) {
+                    if (marking.getNumberOfTokensAt(i) > 0) {
+                        std::cout << i << std::endl;
+                        labeling.addLabelToState(idToName.at(i), i);
+                    }
+                }
+            }
+
+            return labeling;
+        }
+
         template class ExplicitGspnModelBuilder<double>;
     }
 }
diff --git a/src/builder/ExplicitGspnModelBuilder.h b/src/builder/ExplicitGspnModelBuilder.h
index 1b7fe4d8e..fa8ed75be 100644
--- a/src/builder/ExplicitGspnModelBuilder.h
+++ b/src/builder/ExplicitGspnModelBuilder.h
@@ -130,6 +130,14 @@ namespace storm {
              */
             uint_fast64_t findOrAddBitvectorToMarkings(storm::storage::BitVector const& bitvector);
 
+            /*!
+             * Computes the state labeling and returns it.
+             * Every state is labeled with its name.
+             *
+             * @return The computed state labeling.
+             */
+            storm::models::sparse::StateLabeling getStateLabeling() const;
+
 
             // contains the number of bits which are used the store the number of tokens at each place
             std::map<uint_fast64_t, uint_fast64_t> numberOfBits;