Browse Source

Fixed problem with usageInfoBits for only one element

Former-commit-id: ac52fff2d7
tempestpy_adaptions
Mavo 9 years ago
parent
commit
e12ac36249
  1. 2
      src/storage/dft/DFT.cpp
  2. 2
      src/storage/dft/DFT.h

2
src/storage/dft/DFT.cpp

@ -63,7 +63,7 @@ namespace storm {
}
mTopModule = std::vector<size_t>(topModuleSet.begin(), topModuleSet.end());
size_t usageInfoBits = storm::utility::math::uint64_log2(mElements.size()-1)+1;
size_t usageInfoBits = mElements.size() > 1 ? storm::utility::math::uint64_log2(mElements.size()-1) + 1 : 1;
mStateVectorSize = nrElements() * 2 + mNrOfSpares * usageInfoBits + nrRepresentatives;
}

2
src/storage/dft/DFT.h

@ -43,7 +43,7 @@ namespace storm {
public:
DFTStateGenerationInfo(size_t nrElements) : mUsageInfoBits(storm::utility::math::uint64_log2(nrElements-1)+1), mIdToStateIndex(nrElements) {
DFTStateGenerationInfo(size_t nrElements) : mUsageInfoBits(nrElements > 1 ? storm::utility::math::uint64_log2(nrElements-1) + 1 : 1), mIdToStateIndex(nrElements) {
}
size_t usageInfoBits() const {

Loading…
Cancel
Save