Browse Source

added function to build a trivial memory structure

tempestpy_adaptions
TimQu 7 years ago
parent
commit
4251c9f525
  1. 4
      src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
  2. 7
      src/storm/storage/memorystructure/MemoryStructureBuilder.cpp
  3. 5
      src/storm/storage/memorystructure/MemoryStructureBuilder.h

4
src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp

@ -69,9 +69,7 @@ namespace storm {
template <typename SparseModelType>
SparseMultiObjectivePreprocessor<SparseModelType>::PreprocessorData::PreprocessorData(SparseModelType const& model) : originalModel(model) {
storm::storage::MemoryStructureBuilder<ValueType, RewardModelType> memoryBuilder(1, model);
memoryBuilder.setTransition(0,0, storm::storage::BitVector(model.getNumberOfStates(), true));
memory = std::make_shared<storm::storage::MemoryStructure>(memoryBuilder.build());
memory = std::make_shared<storm::storage::MemoryStructure>(storm::storage::MemoryStructureBuilder<ValueType, RewardModelType>::buildTrivialMemoryStructure(model));
// The memoryLabelPrefix should not be a prefix of a state label of the given model to ensure uniqueness of label names
memoryLabelPrefix = "mem";

7
src/storm/storage/memorystructure/MemoryStructureBuilder.cpp

@ -83,6 +83,13 @@ namespace storm {
return MemoryStructure(std::move(transitions), std::move(stateLabeling), std::move(initialMemoryStates));
}
template <typename ValueType, typename RewardModelType>
MemoryStructure MemoryStructureBuilder<ValueType, RewardModelType>::buildTrivialMemoryStructure(storm::models::sparse::Model<ValueType, RewardModelType> const& model) {
MemoryStructureBuilder<ValueType, RewardModelType> memoryBuilder(1, model);
memoryBuilder.setTransition(0,0, storm::storage::BitVector(model.getNumberOfStates(), true));
return memoryBuilder.build();
}
template class MemoryStructureBuilder<double>;
template class MemoryStructureBuilder<storm::RationalNumber>;
template class MemoryStructureBuilder<storm::RationalFunction>;

5
src/storm/storage/memorystructure/MemoryStructureBuilder.h

@ -57,6 +57,11 @@ namespace storm {
*/
MemoryStructure build();
/*!
* Builds a trivial memory structure for the given model (consisting of a single memory state)
*/
static MemoryStructure buildTrivialMemoryStructure(storm::models::sparse::Model<ValueType, RewardModelType> const& model);
private:
storm::models::sparse::Model<ValueType, RewardModelType> const& model;

Loading…
Cancel
Save