diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 3e6bb8570..b26b16972 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/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()); } diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index be66bc2a0..86cd79400 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/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; diff --git a/src/storm-dft/storage/dft/DFTStateGenerationInfo.h b/src/storm-dft/storage/dft/DFTStateGenerationInfo.h index 7055d6682..626591768 100644 --- a/src/storm-dft/storage/dft/DFTStateGenerationInfo.h +++ b/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(); }