From b51d997d5b545acb0d3a6fff9b1ffc83250907c2 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Wed, 17 Feb 2016 14:31:35 +0100
Subject: [PATCH] Detect error with more than one spare in a module

Former-commit-id: a0812aa201fce62906f0d1ac054678476f101377
---
 src/storage/dft/DFT.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp
index 83e287b3b..a23a70f71 100644
--- a/src/storage/dft/DFT.cpp
+++ b/src/storage/dft/DFT.cpp
@@ -1,6 +1,7 @@
 #include <boost/container/flat_set.hpp>
 
 #include "DFT.h"
+#include "src/exceptions/NotSupportedException.h"
 
 namespace storm {
     namespace storage {
@@ -28,7 +29,12 @@ namespace storm {
                         std::set<size_t> module = {spareReprs->id()};
                         spareReprs->extendSpareModule(module);
                         std::vector<size_t> sparesAndBes;
+                        bool secondSpare = false;
                         for(auto const& modelem : module) {
+                            if (mElements[modelem]->isSpareGate()) {
+                                STORM_LOG_THROW(!secondSpare, storm::exceptions::NotSupportedException, "Module for '" << spareReprs->name() << "' contains more than one spare.");
+                                secondSpare = true;
+                            }
                             if(mElements[modelem]->isSpareGate() || mElements[modelem]->isBasicElement()) {
                                 sparesAndBes.push_back(modelem);
                                 mRepresentants.insert(std::make_pair(modelem, spareReprs->id()));