From ac759d267190d87566031375aedcead5826b857c Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 3 Nov 2017 14:06:39 +0100 Subject: [PATCH] minor performance improvements to model building --- src/storm/builder/ExplicitModelBuilder.cpp | 16 +++++++++------- src/storm/generator/JaniNextStateGenerator.cpp | 4 ++-- src/storm/generator/JaniNextStateGenerator.h | 2 +- src/storm/generator/NextStateGenerator.cpp | 6 ++++-- src/storm/generator/NextStateGenerator.h | 6 +++--- src/storm/generator/PrismNextStateGenerator.cpp | 4 ++-- src/storm/generator/PrismNextStateGenerator.h | 2 +- src/storm/storage/sparse/StateStorage.h | 2 +- 8 files changed, 23 insertions(+), 19 deletions(-) diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index d6096e750..ac4b554d5 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -89,20 +89,22 @@ namespace storm { // Check, if the state was already registered. std::pair actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex); - if (actualIndexBucketPair.first == newIndex) { + StateType actualIndex = actualIndexBucketPair.first; + + if (actualIndex == newIndex) { if (options.explorationOrder == ExplorationOrder::Dfs) { - statesToExplore.emplace_front(state, actualIndexBucketPair.first); + statesToExplore.emplace_front(state, actualIndex); // Reserve one slot for the new state in the remapping. stateRemapping.get().push_back(storm::utility::zero()); } else if (options.explorationOrder == ExplorationOrder::Bfs) { - statesToExplore.emplace_back(state, actualIndexBucketPair.first); + statesToExplore.emplace_back(state, actualIndex); } else { STORM_LOG_ASSERT(false, "Invalid exploration order."); } } - return actualIndexBucketPair.first; + return actualIndex; } template @@ -306,7 +308,7 @@ namespace storm { buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates); - // initialize the model components with the obtained information. + // Initialize the model components with the obtained information. storm::storage::sparse::ModelComponents modelComponents(transitionMatrixBuilder.build(), buildStateLabeling(), std::unordered_map(), !generator->isDiscreteTimeModel(), std::move(markovianStates)); // Now finalize all reward models. @@ -316,7 +318,7 @@ namespace storm { // Build the choice labeling modelComponents.choiceLabeling = choiceInformationBuilder.buildChoiceLabeling(modelComponents.transitionMatrix.getRowCount()); - // if requested, build the state valuations and choice origins + // If requested, build the state valuations and choice origins if (generator->getOptions().isBuildStateValuationsSet()) { std::vector valuations(modelComponents.transitionMatrix.getRowGroupCount()); for (auto const& bitVectorIndexPair : stateStorage.stateToId) { @@ -334,7 +336,7 @@ namespace storm { template storm::models::sparse::StateLabeling ExplicitModelBuilder::buildStateLabeling() { - return generator->label(stateStorage.stateToId, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices); + return generator->label(stateStorage, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices); } // Explicitly instantiate the class. diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index f7d86e914..40481fd83 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -608,7 +608,7 @@ namespace storm { } template - storm::models::sparse::StateLabeling JaniNextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices) { + storm::models::sparse::StateLabeling JaniNextStateGenerator::label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices) { // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to // create a list of boolean transient variables and the expressions that define them. std::unordered_map transientVariableToExpressionMap; @@ -625,7 +625,7 @@ namespace storm { transientVariableExpressions.push_back(std::make_pair(element.first.getName(), element.second)); } - return NextStateGenerator::label(states, initialStateIndices, deadlockStateIndices, transientVariableExpressions); + return NextStateGenerator::label(stateStorage, initialStateIndices, deadlockStateIndices, transientVariableExpressions); } template diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index 3fcfc2777..594efc91c 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -30,7 +30,7 @@ namespace storm { virtual std::size_t getNumberOfRewardModels() const override; virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override; - virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) override; + virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) override; private: /*! diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index 15c6048c3..f69014364 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -53,7 +53,7 @@ namespace storm { } template - storm::models::sparse::StateLabeling NextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices, std::vector> labelsAndExpressions) { + storm::models::sparse::StateLabeling NextStateGenerator::label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices, std::vector> labelsAndExpressions) { for (auto const& expression : this->options.getExpressionLabels()) { std::stringstream stream; @@ -67,12 +67,14 @@ namespace storm { labelsAndExpressions.resize(std::distance(labelsAndExpressions.begin(), it)); // Prepare result. - storm::models::sparse::StateLabeling result(states.size()); + storm::models::sparse::StateLabeling result(stateStorage.getNumberOfStates()); // Initialize labeling. for (auto const& label : labelsAndExpressions) { result.addLabel(label.first); } + + storm::storage::BitVectorHashMap const& states = stateStorage.stateToId; for (auto const& stateIndexPair : states) { unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, *this->evaluator); diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index 25335dbfc..54f7f1024 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -7,7 +7,7 @@ #include #include "storm/storage/expressions/Expression.h" -#include "storm/storage/BitVectorHashMap.h" +#include "storm/storage/sparse/StateStorage.h" #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm/storage/sparse/ChoiceOrigins.h" @@ -61,7 +61,7 @@ namespace storm { storm::expressions::SimpleValuation toValuation(CompressedState const& state) const; - virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) = 0; + virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) = 0; NextStateGeneratorOptions const& getOptions() const; @@ -71,7 +71,7 @@ namespace storm { /*! * Creates the state labeling for the given states using the provided labels and expressions. */ - storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices, std::vector> labelsAndExpressions); + storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices, std::vector> labelsAndExpressions); void postprocess(StateBehavior& result); diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index bf9d73876..db74175c0 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -575,7 +575,7 @@ namespace storm { } template - storm::models::sparse::StateLabeling PrismNextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices) { + storm::models::sparse::StateLabeling PrismNextStateGenerator::label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices) { // Gather a vector of labels and their expressions. std::vector> labels; if (this->options.isBuildAllLabelsSet()) { @@ -592,7 +592,7 @@ namespace storm { } } - return NextStateGenerator::label(states, initialStateIndices, deadlockStateIndices, labels); + return NextStateGenerator::label(stateStorage, initialStateIndices, deadlockStateIndices, labels); } template diff --git a/src/storm/generator/PrismNextStateGenerator.h b/src/storm/generator/PrismNextStateGenerator.h index 0097e7055..5cc8ce9ba 100644 --- a/src/storm/generator/PrismNextStateGenerator.h +++ b/src/storm/generator/PrismNextStateGenerator.h @@ -28,7 +28,7 @@ namespace storm { virtual std::size_t getNumberOfRewardModels() const override; virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override; - virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) override; + virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) override; virtual std::shared_ptr generateChoiceOrigins(std::vector& dataForChoiceOrigins) const override; diff --git a/src/storm/storage/sparse/StateStorage.h b/src/storm/storage/sparse/StateStorage.h index 789e16c88..65b592cb5 100644 --- a/src/storm/storage/sparse/StateStorage.h +++ b/src/storm/storage/sparse/StateStorage.h @@ -27,7 +27,7 @@ namespace storm { // The number of bits of each state. uint64_t bitsPerState; - // The number of states that were found in the exploration so far. + // Get the number of states that were found in the exploration so far. uint_fast64_t getNumberOfStates() const; };