sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

minor performance improvements to model building

tempestpy_adaptions
dehnert 7 years ago
parent
6501fffac3
commit
ac759d2671
8 changed files with 23 additions and 19 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 16
      src/storm/builder/ExplicitModelBuilder.cpp
  2. 4
      src/storm/generator/JaniNextStateGenerator.cpp
  3. 2
      src/storm/generator/JaniNextStateGenerator.h
  4. 6
      src/storm/generator/NextStateGenerator.cpp
  5. 6
      src/storm/generator/NextStateGenerator.h
  6. 4
      src/storm/generator/PrismNextStateGenerator.cpp
  7. 2
      src/storm/generator/PrismNextStateGenerator.h
  8. 2
      src/storm/storage/sparse/StateStorage.h

16
src/storm/builder/ExplicitModelBuilder.cpp
View File

@ -89,20 +89,22 @@ namespace storm {
// Check, if the state was already registered.
std::pair<StateType, std::size_t> 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<StateType>());
} 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 <typename ValueType, typename RewardModelType, typename StateType>
@ -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<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !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<storm::expressions::SimpleValuation> valuations(modelComponents.transitionMatrix.getRowGroupCount());
for (auto const& bitVectorIndexPair : stateStorage.stateToId) {
@ -334,7 +336,7 @@ namespace storm {
template <typename ValueType, typename RewardModelType, typename StateType>
storm::models::sparse::StateLabeling ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildStateLabeling() {
return generator->label(stateStorage.stateToId, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices);
return generator->label(stateStorage, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices);
}
// Explicitly instantiate the class.

4
src/storm/generator/JaniNextStateGenerator.cpp
View File

@ -608,7 +608,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> 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<storm::expressions::Variable, storm::expressions::Expression> transientVariableToExpressionMap;
@ -625,7 +625,7 @@ namespace storm {
transientVariableExpressions.push_back(std::make_pair(element.first.getName(), element.second));
}
return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, deadlockStateIndices, transientVariableExpressions);
return NextStateGenerator<ValueType, StateType>::label(stateStorage, initialStateIndices, deadlockStateIndices, transientVariableExpressions);
}
template<typename ValueType, typename StateType>

2
src/storm/generator/JaniNextStateGenerator.h
View File

@ -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<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override;
virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override;
private:
/*!

6
src/storm/generator/NextStateGenerator.cpp
View File

@ -53,7 +53,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling NextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions) {
storm::models::sparse::StateLabeling NextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> 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<StateType> const& states = stateStorage.stateToId;
for (auto const& stateIndexPair : states) {
unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, *this->evaluator);

6
src/storm/generator/NextStateGenerator.h
View File

@ -7,7 +7,7 @@
#include <boost/variant.hpp>
#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<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) = 0;
virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> 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<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions);
storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions);
void postprocess(StateBehavior<ValueType, StateType>& result);

4
src/storm/generator/PrismNextStateGenerator.cpp
View File

@ -575,7 +575,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
// Gather a vector of labels and their expressions.
std::vector<std::pair<std::string, storm::expressions::Expression>> labels;
if (this->options.isBuildAllLabelsSet()) {
@ -592,7 +592,7 @@ namespace storm {
}
}
return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, deadlockStateIndices, labels);
return NextStateGenerator<ValueType, StateType>::label(stateStorage, initialStateIndices, deadlockStateIndices, labels);
}
template<typename ValueType, typename StateType>

2
src/storm/generator/PrismNextStateGenerator.h
View File

@ -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<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override;
virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override;
virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const override;

2
src/storm/storage/sparse/StateStorage.h
View File

@ -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;
};

Write Preview
Loading…
Cancel
Save