From cce39fbd5dc7eeaff21090f850e83b0522c91573 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Tue, 23 Feb 2016 18:57:41 +0100
Subject: [PATCH] Helper function for symmetry ordering on bitvector

Former-commit-id: e98b004de6f93c4287e4a869483c0dce892f29c5
---
 src/storage/dft/DFTState.cpp | 31 +++++++++++++++++++++++++++++++
 src/storage/dft/DFTState.h   |  6 ++++++
 2 files changed, 37 insertions(+)

diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp
index 7f34e03ef..591f6f9da 100644
--- a/src/storage/dft/DFTState.cpp
+++ b/src/storage/dft/DFTState.cpp
@@ -242,6 +242,37 @@ namespace storm {
             }
             return false;
         }
+        
+        template<typename ValueType>
+        bool DFTState<ValueType>::orderBySymmetry() {
+            bool changed = false;
+            for (size_t pos = 0; pos < mStateGenerationInfo.getSymmetrySize(); ++pos) {
+                // Check each symmetry
+                size_t length = mStateGenerationInfo.getSymmetryLength(pos);
+                std::vector<size_t> symmetryIndices = mStateGenerationInfo.getSymmetryIndices(pos);
+                // Sort symmetry group in decreasing order by bubble sort
+                // TODO use better algorithm?
+                size_t tmp, elem1, elem2;
+                size_t n = symmetryIndices.size();
+                do {
+                    tmp = 0;
+                    for (size_t i = 1; i < n; ++i) {
+                        elem1 = mStatus.getAsInt(symmetryIndices[i-1], length);
+                        elem2 = mStatus.getAsInt(symmetryIndices[i], length);
+                        if (elem1 > elem2) {
+                            // Swap elements
+                            mStatus.setFromInt(symmetryIndices[i-1], length, elem2);
+                            mStatus.setFromInt(symmetryIndices[i], length, elem1);
+                            tmp = i;
+                            changed = true;
+                        }
+                    }
+                    n = tmp;
+                } while (n > 0);
+            }
+            return changed;
+        }
+
 
         // Explicitly instantiate the class.
         template class DFTState<double>;
diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h
index 7a26e10ab..eccf7f01d 100644
--- a/src/storage/dft/DFTState.h
+++ b/src/storage/dft/DFTState.h
@@ -164,6 +164,12 @@ namespace storm {
              */
             void letDependencyBeUnsuccessful(size_t index = 0);
             
+            /**
+             * Order the state in decreasing order using the symmetries.
+             * @return True, if elements were swapped, false if nothing changed.
+             */
+            bool orderBySymmetry();
+            
             std::string getCurrentlyFailableString() const {
                 std::stringstream stream;
                 if (nrFailableDependencies() > 0) {