From ef09fab7168987a377c91b6da9794b52cf7de0a0 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 8 Jan 2019 17:12:45 +0100
Subject: [PATCH] Better check if element name is already used

---
 src/storm-dft/builder/DFTBuilder.cpp |  7 +++---
 src/storm-dft/builder/DFTBuilder.h   | 36 ++++++++++++++++++----------
 2 files changed, 28 insertions(+), 15 deletions(-)

diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp
index d3e635636..87bd5f407 100644
--- a/src/storm-dft/builder/DFTBuilder.cpp
+++ b/src/storm-dft/builder/DFTBuilder.cpp
@@ -140,7 +140,8 @@ namespace storm {
             if (children.size() <= 1) {
                 STORM_LOG_ERROR("Sequence enforcers require at least two children");
             }
-            if (mElements.count(name) != 0) {
+            if (nameInUse(name)) {
+                STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
                 return false;
             }
             DFTRestrictionPointer restr;
@@ -166,8 +167,8 @@ namespace storm {
         template<typename ValueType>
         bool DFTBuilder<ValueType>::addStandardGate(std::string const& name, std::vector<std::string> const& children, storm::storage::DFTElementType tp) {
             STORM_LOG_ASSERT(children.size() > 0, "No child for " << name);
-            if(mElements.count(name) != 0) {
-                // Element with that name already exists.
+            if (nameInUse(name)) {
+                STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
                 return false;
             }
             DFTElementPointer element;
diff --git a/src/storm-dft/builder/DFTBuilder.h b/src/storm-dft/builder/DFTBuilder.h
index 4d9f2652f..479db529c 100644
--- a/src/storm-dft/builder/DFTBuilder.h
+++ b/src/storm-dft/builder/DFTBuilder.h
@@ -93,8 +93,8 @@ namespace storm {
                 if(children.size() <= 1) {
                     STORM_LOG_ERROR("Dependencies require at least two children");
                 }
-                if(mElements.count(name) != 0) {
-                    // Element with that name already exists.
+                if (nameInUse(name)) {
+                    STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
                     return false;
                 }
 
@@ -122,13 +122,11 @@ namespace storm {
                     if(binaryDependencies) {
                         for (size_t i = 1; i < children.size(); ++i) {
                             std::string nameDep = name + "_" + std::to_string(i);
-                            if (mElements.count(nameDep) != 0) {
-                                // Element with that name already exists.
-                                STORM_LOG_ERROR("Element with name: " << nameDep << " already exists.");
+                            if (nameInUse(nameDep)) {
+                                STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
                                 return false;
                             }
-                            STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2,
-                                             "PDep with multiple children supported.");
+                            STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2, "PDep with multiple children supported.");
                             DFTDependencyPointer element = std::make_shared<storm::storage::DFTDependency<ValueType>>(mNextId++, nameDep, probability);
                             mElements[element->name()] = element;
                             mDependencyChildNames[element] = {trigger, children[i]};
@@ -146,8 +144,8 @@ namespace storm {
 
             bool addVotElement(std::string const& name, unsigned threshold, std::vector<std::string> const& children) {
                 STORM_LOG_ASSERT(children.size() > 0, "Has no child.");
-                if(mElements.count(name) != 0) {
-                    STORM_LOG_ERROR("Element with name: " << name << " already exists.");
+                if (nameInUse(name)) {
+                    STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
                     return false;
                 }
                 // It is an and-gate
@@ -174,19 +172,33 @@ namespace storm {
                 //TODO Matthias: collect constraints for SMT solving
                 //failureRate > 0
                 //0 <= dormancyFactor <= 1
-                STORM_LOG_ASSERT(mElements.find(name) == mElements.end(), "Element '" << name << "' already exists.");
+                if (nameInUse(name)) {
+                    STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
+                    return false;
+                }
                 mElements[name] = std::make_shared<storm::storage::DFTBE<ValueType>>(mNextId++, name, failureRate, dormancyFactor, transient);
                 return true;
             }
 
             void addLayoutInfo(std::string const& name, double x, double y) {
-                STORM_LOG_ASSERT(mElements.count(name) > 0, "Element '" << name << "' not found.");
+                if (!nameInUse(name)) {
+                    STORM_LOG_ERROR("Element with name '" << name << "' not found.");
+                }
                 mLayoutInfo[name] = storm::storage::DFTLayoutInfo(x, y);
             }
             
             bool setTopLevel(std::string const& tle) {
                 mTopLevelIdentifier = tle;
-                return mElements.count(tle) > 0;
+                return nameInUse(tle);
+            }
+
+            /**
+             * Check whether the name is already used.
+             * @param name Element name.
+             * @return True iff name is already in use.
+             */
+            bool nameInUse(std::string const& name) {
+                return mElements.find(name) != mElements.end();
             }
             
             std::string getUniqueName(std::string name);