diff --git a/src/storm/storage/memorystructure/MemoryStructure.cpp b/src/storm/storage/memorystructure/MemoryStructure.cpp
index 6103c05dd..1bcded410 100644
--- a/src/storm/storage/memorystructure/MemoryStructure.cpp
+++ b/src/storm/storage/memorystructure/MemoryStructure.cpp
@@ -11,14 +11,6 @@
namespace storm {
namespace storage {
- MemoryStructure::MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector<uint_fast64_t> const& initialMemoryStates) : transitions(transitionMatrix), stateLabeling(memoryStateLabeling), initialMemoryStates(initialMemoryStates), onlyInitialStatesRelevant(true) {
- // intentionally left empty
- }
-
- MemoryStructure::MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector<uint_fast64_t>&& initialMemoryStates) : transitions(std::move(transitionMatrix)), stateLabeling(std::move(memoryStateLabeling)), initialMemoryStates(std::move(initialMemoryStates)), onlyInitialStatesRelevant(true) {
- // intentionally left empty
- }
-
MemoryStructure::MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector<uint_fast64_t> const& initialMemoryStates, bool onlyInitialStatesRelevant) : transitions(transitionMatrix), stateLabeling(memoryStateLabeling), initialMemoryStates(initialMemoryStates), onlyInitialStatesRelevant(onlyInitialStatesRelevant) {
// intentionally left empty
}
@@ -27,7 +19,7 @@ namespace storm {
// intentionally left empty
}
- bool MemoryStructure::IsOnlyInitialStatesRelevantSet() const {
+ bool MemoryStructure::isOnlyInitialStatesRelevantSet() const {
return onlyInitialStatesRelevant;
}
diff --git a/src/storm/storage/memorystructure/MemoryStructure.h b/src/storm/storage/memorystructure/MemoryStructure.h
index 2476a4e63..e831b58cf 100644
--- a/src/storm/storage/memorystructure/MemoryStructure.h
+++ b/src/storm/storage/memorystructure/MemoryStructure.h
@@ -33,14 +33,13 @@ namespace storm {
*
* @param transitionMatrix The transition matrix
* @param memoryStateLabeling A labeling of the memory states to specify, e.g., accepting states
- * @param initialMemoryStates assigns an initial memory state to each initial state of the model.
+ * @param initialMemoryStates assigns an initial memory state to each (initial?) state of the model.
+ * @param onlyInitialStatesRelevant if true, initial memory states are only provided for each initial model state. Otherwise, an initial memory state is provided for *every* model state.
*/
- MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector<uint_fast64_t> const& initialMemoryStates);
- MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector<uint_fast64_t>&& initialMemoryStates);
- MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector<uint_fast64_t> const& initialMemoryStates, bool onlyInitialStatesRelevant);
- MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector<uint_fast64_t>&& initialMemoryStates, bool onlyInitialStatesRelevant);
+ MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector<uint_fast64_t> const& initialMemoryStates, bool onlyInitialStatesRelevant = true);
+ MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector<uint_fast64_t>&& initialMemoryStates, bool onlyInitialStatesRelevant = true);
- bool IsOnlyInitialStatesRelevantSet () const;
+ bool isOnlyInitialStatesRelevantSet () const;
TransitionMatrix const& getTransitionMatrix() const;
storm::models::sparse::StateLabeling const& getStateLabeling() const;
std::vector<uint_fast64_t> const& getInitialMemoryStates() const;
diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp
index 859a92635..54accf38a 100644
--- a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp
+++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp
@@ -9,18 +9,13 @@
namespace storm {
namespace storage {
- template <typename ValueType, typename RewardModelType>
- MemoryStructureBuilder<ValueType, RewardModelType>::MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model<ValueType, RewardModelType> const& model) : model(model), transitions(numberOfMemoryStates, std::vector<boost::optional<storm::storage::BitVector>>(numberOfMemoryStates)), stateLabeling(numberOfMemoryStates), initialMemoryStates(model.getInitialStates().getNumberOfSetBits(), 0), onlyInitialStatesRelevant(true) {
- // Intentionally left empty
- }
-
template <typename ValueType, typename RewardModelType>
MemoryStructureBuilder<ValueType, RewardModelType>::MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model<ValueType, RewardModelType> const& model, bool onlyInitialStatesRelevant) : model(model), transitions(numberOfMemoryStates, std::vector<boost::optional<storm::storage::BitVector>>(numberOfMemoryStates)), stateLabeling(numberOfMemoryStates), initialMemoryStates(onlyInitialStatesRelevant ? model.getInitialStates().getNumberOfSetBits() : model.getNumberOfStates(), 0), onlyInitialStatesRelevant(onlyInitialStatesRelevant) {
// Intentionally left empty
}
template <typename ValueType, typename RewardModelType>
- MemoryStructureBuilder<ValueType, RewardModelType>::MemoryStructureBuilder(MemoryStructure const& memoryStructure, storm::models::sparse::Model<ValueType, RewardModelType> const& model) : model(model), transitions(memoryStructure.getTransitionMatrix()), stateLabeling(memoryStructure.getStateLabeling()), initialMemoryStates(memoryStructure.getInitialMemoryStates()), onlyInitialStatesRelevant(true) {
+ MemoryStructureBuilder<ValueType, RewardModelType>::MemoryStructureBuilder(MemoryStructure const& memoryStructure, storm::models::sparse::Model<ValueType, RewardModelType> const& model) : model(model), transitions(memoryStructure.getTransitionMatrix()), stateLabeling(memoryStructure.getStateLabeling()), initialMemoryStates(memoryStructure.getInitialMemoryStates()), onlyInitialStatesRelevant(memoryStructure.isOnlyInitialStatesRelevantSet()) {
// Intentionally left empty
}
diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.h b/src/storm/storage/memorystructure/MemoryStructureBuilder.h
index 1d067a4bc..b038fb98f 100644
--- a/src/storm/storage/memorystructure/MemoryStructureBuilder.h
+++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.h
@@ -14,18 +14,12 @@ namespace storm {
class MemoryStructureBuilder {
public:
- /*!
- * Initializes a new builder for a memory structure
- * @param numberOfMemoryStates The number of states the resulting memory structure should have
- */
- MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model<ValueType, RewardModelType> const& model);
-
- /*!
+ /*!
* Initializes a new builder with the data from the provided memory structure
* @param numberOfMemoryStates The number of states the resulting memory structure should have
- * @param allModelStatesRelevant Consider non-initial model states
+ * @param onlyInitialStatesRelevant If true, assume that we only consider the fragment reachable from initial model states. If false, initial memory states need to be provided for *all* model states.
*/
- MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model<ValueType, RewardModelType> const& model, bool onlyInitialStatesRelevant);
+ MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model<ValueType, RewardModelType> const& model, bool onlyInitialStatesRelevant = true);
/*!
* Initializes a new builder with the data from the provided memory structure
@@ -33,11 +27,11 @@ namespace storm {
MemoryStructureBuilder(MemoryStructure const& memoryStructure, storm::models::sparse::Model<ValueType, RewardModelType> const& model);
/*!
- * Specifies for the given initial state of the model the corresponding initial memory state.
+ * Specifies for the given state of the model the corresponding initial memory state.
*
* @note The default initial memory state is 0.
*
- * @param initialModelState the index of an initial state of the model.
+ * @param initialModelState the index of a state of the model. Has to be an initial state iff `onlyInitialStatesRelevant` is true.
* @param initialMemoryState the initial memory state associated to the corresponding model state.
*/
void setInitialMemoryState(uint_fast64_t initialModelState, uint_fast64_t initialMemoryState);
diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
index b80910704..76fa593ba 100644
--- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
+++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
@@ -38,7 +38,7 @@ namespace storm {
// Get the initial states and reachable states. A stateIndex s corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount)
storm::storage::BitVector initialStates(modelStateCount * memoryStateCount, false);
auto memoryInitIt = memory.getInitialMemoryStates().begin();
- if (memory.IsOnlyInitialStatesRelevantSet()) {
+ if (memory.isOnlyInitialStatesRelevantSet()) {
for (auto modelInit : model.getInitialStates()) {
initialStates.set(modelInit * memoryStateCount + *memoryInitIt, true);
++memoryInitIt;