Browse Source

Fixed problem with BitVector size mismatch for DFT states

tempestpy_adaptions
Matthias Volk 6 years ago
parent
commit
0e0a3dd9af
  1. 2
      src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
  2. 5
      src/storm-dft/storage/dft/DFT.h
  3. 2
      src/storm-dft/storage/dft/DFTState.cpp

2
src/storm-dft/builder/ExplicitDFTModelBuilder.cpp

@ -58,7 +58,7 @@ namespace storm {
usedHeuristic(storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().getApproximationHeuristic()),
generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates),
matrixBuilder(!generator.isDeterministicModel()),
stateStorage(((dft.stateVectorSize() / 64) + 1) * 64),
stateStorage(dft.stateBitVectorSize()),
// TODO Matthias: make choosable
//explorationQueue(dft.nrElements()+1, 0, 1)
explorationQueue(200, 0, 0.9)

5
src/storm-dft/storage/dft/DFT.h

@ -80,8 +80,9 @@ namespace storm {
void copyElements(std::vector<size_t> elements, storm::builder::DFTBuilder<ValueType> builder) const;
size_t stateVectorSize() const {
return mStateVectorSize;
size_t stateBitVectorSize() const {
// Ensure multiple of 64
return (mStateVectorSize / 64 + (mStateVectorSize % 64 != 0)) * 64;
}
size_t nrElements() const {

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

@ -6,7 +6,7 @@ namespace storm {
namespace storage {
template<typename ValueType>
DFTState<ValueType>::DFTState(DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mPseudoState(false), mDft(dft), mStateGenerationInfo(stateGenerationInfo) {
DFTState<ValueType>::DFTState(DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateBitVectorSize()), mId(id), mPseudoState(false), mDft(dft), mStateGenerationInfo(stateGenerationInfo) {
// TODO Matthias: use construct()
// Initialize uses
Loading…
Cancel
Save