diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index c0188de50..9a0408a3c 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -67,7 +67,12 @@ namespace storm { } template - ExplicitPrismModelBuilder::InternalStateInformation::InternalStateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), numberOfStates() { + ExplicitPrismModelBuilder::InternalStateInformation::InternalStateInformation() : stateStorage(64, 10), initialStateIndices(), bitsPerState(64), numberOfStates() { + // Intentionally left empty. + } + + template + ExplicitPrismModelBuilder::InternalStateInformation::InternalStateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), initialStateIndices(), bitsPerState(bitsPerState), numberOfStates() { // Intentionally left empty. } @@ -349,7 +354,7 @@ namespace storm { StateType currentIndex = internalStateInformation.stateStorage.getValue(currentState); statesToExplore.pop_front(); - STORM_LOG_TRACE("Exploring state with id " << index << "."); + STORM_LOG_TRACE("Exploring state with id " << currentIndex << "."); storm::generator::StateBehavior behavior = generator.expand(currentState, stateToIdCallback); @@ -423,7 +428,6 @@ namespace storm { ++choiceRewardIt; ++builderIt; } - ++currentRow; } } @@ -435,11 +439,7 @@ namespace storm { template typename ExplicitPrismModelBuilder::ModelComponents ExplicitPrismModelBuilder::buildModelComponents(std::vector> const& selectedRewardModels) { ModelComponents modelComponents; - - // Create the structure for storing the reachable state space. - uint64_t bitsPerState = ((variableInformation.getTotalBitOffset() / 64) + 1) * 64; - InternalStateInformation internalStateInformation(bitsPerState); - + // Determine whether we have to combine different choices to one or whether this model can have more than // one choice per state. bool deterministicModel = program.isDeterministicModel(); diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index a5e09bfae..3e5614854 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -45,7 +45,11 @@ namespace storm { public: // A structure holding information about the reachable state space while building it. struct InternalStateInformation { - InternalStateInformation(uint64_t bitsPerState = 64); + // Builds an empty state information. + InternalStateInformation(); + + // Creates a state information structure for storing states of the given bit width. + InternalStateInformation(uint64_t bitsPerState); // This member stores all the states and maps them to their unique indices. storm::storage::BitVectorHashMap stateStorage; diff --git a/src/utility/storm.h b/src/utility/storm.h index d4a042bc6..ef2e7ac7a 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -106,8 +106,8 @@ namespace storm { options.buildCommandLabels = true; } - storm::builder::ExplicitPrismModelBuilder builder; - result.model = builder.translateProgram(program, options); + storm::builder::ExplicitPrismModelBuilder builder(program, options); + result.model = builder.translate(); translatedProgram = builder.getTranslatedProgram(); } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { typename storm::builder::DdPrismModelBuilder::Options options;