From ca77078a9c866cc0aee16908333ec37c138557de Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Thu, 18 Feb 2016 18:03:57 +0100
Subject: [PATCH] Deterministic Building for DFTs
Former-commit-id: bb669a034e24494ae3c88a6a353931651c0c945a
---
src/storage/dft/DFTBuilder.cpp | 4 ++--
src/storage/dft/DFTBuilder.h | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
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();