From db3c40e6d738f026b791ee47ad89924569dd8e40 Mon Sep 17 00:00:00 2001 From: Mavo Date: Sat, 12 Mar 2016 18:46:01 +0100 Subject: [PATCH] Fixed bugs Former-commit-id: d602972afc29bbdeb6c6eb338a393c60d3135ce7 --- src/storage/dft/DFTState.cpp | 10 +--------- src/storage/dft/DFTStateGenerationInfo.h | 2 +- 2 files changed, 2 insertions(+), 10 deletions(-) diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 558192678..24291b446 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -123,26 +123,18 @@ namespace storm { template void DFTState::setFailed(size_t id) { - if (mDft.isRepresentative(id)) { - // Activate failed element - activate(id); - } mStatus.set(mStateGenerationInfo.getStateIndex(id)); } template void DFTState::setFailsafe(size_t id) { - if (mDft.isRepresentative(id)) { - // Activate failed element - activate(id); - } mStatus.set(mStateGenerationInfo.getStateIndex(id)+1); } template void DFTState::setDontCare(size_t id) { if (mDft.isRepresentative(id)) { - // Activate failed element + // Activate dont care element activate(id); } mStatus.setFromInt(mStateGenerationInfo.getStateIndex(id), 2, static_cast(DFTElementState::DontCare) ); diff --git a/src/storage/dft/DFTStateGenerationInfo.h b/src/storage/dft/DFTStateGenerationInfo.h index e700d8700..513a6a7a0 100644 --- a/src/storage/dft/DFTStateGenerationInfo.h +++ b/src/storage/dft/DFTStateGenerationInfo.h @@ -98,7 +98,7 @@ namespace storm { for (size_t index = 0; index < newSymmetries.size(); ++index) { mSymmetries.insert(mSymmetries.begin() + i + 1 + index, std::make_pair(childLength, newSymmetries[index])); } - i += mSymmetries[j].second.size(); + i += newSymmetries.size(); break; } }