diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp
index f0d1db5ac..1979aea3b 100644
--- a/src/storage/dft/DFTBuilder.cpp
+++ b/src/storage/dft/DFTBuilder.cpp
@@ -123,7 +123,7 @@ namespace storm {
         }
 
         template<typename ValueType>
-        void DFTBuilder<ValueType>::topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour>& visited, DFTElementVector& L) {
+        void DFTBuilder<ValueType>::topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>>& visited, DFTElementVector& L) {
             if(visited[n] == topoSortColour::GREY) {
                 throw storm::exceptions::WrongFormatException("DFT is cyclic");
             } else if(visited[n] == topoSortColour::WHITE) {
@@ -141,7 +141,7 @@ namespace storm {
         // TODO Matthias: use typedefs
         template<typename ValueType>
         std::vector<std::shared_ptr<DFTElement<ValueType>>> DFTBuilder<ValueType>::topoSort() {
-            std::map<DFTElementPointer, topoSortColour> visited;
+            std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>> visited;
             for(auto const& e : mElements) {
                 visited.insert(std::make_pair(e.second, topoSortColour::WHITE)); 
             }
diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h
index 37c3c4eaa..17a16cb49 100644
--- a/src/storage/dft/DFTBuilder.h
+++ b/src/storage/dft/DFTBuilder.h
@@ -141,7 +141,7 @@ namespace storm {
             
             enum class topoSortColour {WHITE, BLACK, GREY}; 
             
-            void topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour>& visited, DFTElementVector& L);
+            void topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>>& visited, DFTElementVector& L);
 
             DFTElementVector topoSort();