From 56ea5fca147928c711560991cccd14d404be5693 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 11 Feb 2015 14:40:18 +0100
Subject: [PATCH] Included move-construction and move-assignment for partition.

Former-commit-id: 8ed399c30807617ce36b49c9dac28fe27acbfa21
---
 ...erministicModelBisimulationDecomposition.h | 49 ++++++-------------
 1 file changed, 16 insertions(+), 33 deletions(-)

diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h
index 55cc2241c..4199d39e5 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.h
+++ b/src/storage/DeterministicModelBisimulationDecomposition.h
@@ -275,43 +275,26 @@ namespace storm {
                 Partition() = default;
                 Partition(Partition const& other) = default;
                 Partition& operator=(Partition const& other) = default;
-#ifdef WINDOWS
-				Partition(Partition&& other) 
-					: blocks(), numberOfBlocks(other.numberOfBlocks), stateToBlockMapping(), statesAndValues(), positions(), keepSilentProbabilities(other.keepSilentProbabilities), silentProbabilities()
-				{
-					//std::cout << "Partition(Partition&& other)" << std::endl;
-					//std::cout.flush();
-					blocks.swap(other.blocks);
-					other.numberOfBlocks = 0;
-					stateToBlockMapping.swap(other.stateToBlockMapping);
-					statesAndValues.swap(other.statesAndValues);
-					positions.swap(other.positions);
-					silentProbabilities.swap(other.silentProbabilities);
+
+                // Define move-construct and move-assignment explicitly to make sure they exist (as they are vital to
+                // keep validity of pointers.
+				Partition(Partition&& other) : blocks(std::move(other.blocks)), numberOfBlocks(other.numberOfBlocks), stateToBlockMapping(std::move(other.stateToBlockMapping)), statesAndValues(std::move(other.statesAndValues)), positions(std::move(other.positions)), keepSilentProbabilities(other.keepSilentProbabilities), silentProbabilities(std::move(other.silentProbabilities)) {
+                    // Intentionally left empty.
 				}
-				Partition& operator=(Partition&& other)
-				{
-					//std::cout << "Partition& operator=(Partition&& other)" << std::endl;
-					//std::cout.flush();
-					blocks.clear();
-					blocks.swap(other.blocks);
-					numberOfBlocks = other.numberOfBlocks;
-					other.numberOfBlocks = 0;
-					stateToBlockMapping.clear();
-					stateToBlockMapping.swap(other.stateToBlockMapping);
-					statesAndValues.clear();
-					statesAndValues.swap(other.statesAndValues);
-					positions.clear();
-					positions.swap(other.positions);
-					keepSilentProbabilities = other.keepSilentProbabilities;
-					silentProbabilities.clear();
-					silentProbabilities.swap(other.silentProbabilities);
+                
+				Partition& operator=(Partition&& other) {
+                    if (this != &other) {
+                        blocks = std::move(other.blocks);
+                        numberOfBlocks = other.numberOfBlocks;
+                        stateToBlockMapping = std::move(other.stateToBlockMapping);
+                        statesAndValues = std::move(other.statesAndValues);
+                        positions = std::move(other.positions);
+                        keepSilentProbabilities = other.keepSilentProbabilities;
+                        silentProbabilities = std::move(other.silentProbabilities);
+                    }
 
 					return *this;
 				}
-#else
-				Partition(Partition&& other) = default;
-				Partition& operator=(Partition&& other) = default;
-#endif
                 
                 /*!
                  * Splits all blocks of the partition such that afterwards all blocks contain only states with the label