From 07ddaa314c41f27d80f33fe3ac68fcd9d29bbaaa Mon Sep 17 00:00:00 2001
From: David_Korzeniewski <david.korzeniewski@rwth-aachen.de>
Date: Tue, 10 Feb 2015 17:12:31 +0100
Subject: [PATCH] User declared move constructor and move assignment, as they
are currently required to ensure pointer validity.
Former-commit-id: 5e239c60ccefde54de4bffb8e5d38f7570c7cba7
---
...erministicModelBisimulationDecomposition.h | 39 +++++++++++++++++--
1 file changed, 36 insertions(+), 3 deletions(-)
diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h
index eae63f442..55cc2241c 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.h
+++ b/src/storage/DeterministicModelBisimulationDecomposition.h
@@ -275,9 +275,42 @@ namespace storm {
Partition() = default;
Partition(Partition const& other) = default;
Partition& operator=(Partition const& other) = default;
-#ifndef WINDOWS
- Partition(Partition&& other) = default;
- Partition& operator=(Partition&& 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);
+ }
+ 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);
+
+ return *this;
+ }
+#else
+ Partition(Partition&& other) = default;
+ Partition& operator=(Partition&& other) = default;
#endif
/*!