Added assertions for better debugging

src/storm-dft/storage/dft/DFT.cpp

@@ -197,7 +197,8 @@ namespace storm {
             STORM_LOG_TRACE(generationInfo);
             STORM_LOG_ASSERT(stateIndex == mStateVectorSize, "Id incorrect.");
             STORM_LOG_ASSERT(visited.full(), "Not all elements considered.");
-            
+            generationInfo.checkSymmetries();
+
             return generationInfo;
         }
         
@@ -337,7 +338,7 @@ namespace storm {
                 // Accumulate children names
                 std::vector<std::string> childrenNames;
                 for (size_t i = 1; i < rewrites.size(); ++i) {
-                    STORM_LOG_ASSERT(mElements[rewrites[i]]->parents().front()->id() == originalParent->id(), "Children have the same father");
+                    STORM_LOG_ASSERT(mElements[rewrites[i]]->parents().front()->id() == originalParent->id(), "Children '" << *(mElements[rewrites[i]]) << "' and  '" << *(mElements[rewrites[1]]) << "' have the same father.");
                     childrenNames.push_back(mElements[rewrites[i]]->name());
                 }
                 

src/storm-dft/storage/dft/DFTState.cpp

@@ -522,6 +522,8 @@ namespace storm {
                 do {
                     tmp = 0;
                     for (size_t i = 1; i < n; ++i) {
+                        STORM_LOG_ASSERT(symmetryIndices[i-1] + length <= mStatus.size(), "Symmetry index "<< symmetryIndices[i-1] << " + length " << length << " is larger than status vector " << mStatus.size());
+                        STORM_LOG_ASSERT(symmetryIndices[i] + length <= mStatus.size(), "Symmetry index "<< symmetryIndices[i] << " + length " << length << " is larger than status vector " << mStatus.size());
                         if (mStatus.compareAndSwap(symmetryIndices[i-1], symmetryIndices[i], length)) {
                             tmp = i;
                             changed = true;

src/storm-dft/storage/dft/DFTStateGenerationInfo.h

@@ -144,6 +144,17 @@ namespace storm {
                 }
             }
 
+            void checkSymmetries() {
+                for (auto pair : mSymmetries) {
+                    STORM_LOG_ASSERT(pair.first > 0, "Empty symmetry.");
+                    STORM_LOG_ASSERT(pair.first < stateIndexSize, "Symmetry too long.");
+                    for (size_t index : pair.second) {
+                        STORM_LOG_ASSERT(index < stateIndexSize, "Symmetry starting point " << index << " invalid.");
+                        STORM_LOG_ASSERT(index + pair.first < stateIndexSize, "Symmetry ending point " << index << " invalid.");
+                    }
+                }
+            }
+
             size_t getSymmetrySize() const {
                 return mSymmetries.size();
             }