diff --git a/src/storm/storage/memorystructure/MemoryStructure.h b/src/storm/storage/memorystructure/MemoryStructure.h index 64bd7aaa9..6f5caa015 100644 --- a/src/storm/storage/memorystructure/MemoryStructure.h +++ b/src/storm/storage/memorystructure/MemoryStructure.h @@ -24,16 +24,16 @@ namespace storm { typedef std::vector>> TransitionMatrix; /*! - * Creates a memory structure with the given transition matrix and the given memory state labeling. - * The initial state is always the state with index 0. - * The transition matrix is assumed to contain propositional state formulas. The entry - * transitionMatrix[m][n] specifies the set of model states which trigger a transition from memory - * state m to memory state n. - * Transitions are assumed to be deterministic and complete, i.e., the formulas in - * transitionMatrix[m] form a partition of the state space of the considered model. + * Creates a memory structure with the given transition matrix, the given memory state labeling, and + * the given initial states. + * The entry transitionMatrix[m][n] specifies the set of model transitions which trigger a transition + * from memory state m to memory state n. + * Transitions are assumed to be deterministic and complete, i.e., the sets in in + * transitionMatrix[m] form a partition of the transitions of the considered model. * * @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. */ MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector const& initialMemoryStates); MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector&& initialMemoryStates); diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp index 148cbf2ca..e51e85239 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp @@ -14,6 +14,11 @@ namespace storm { // Intentionally left empty } + template + MemoryStructureBuilder::MemoryStructureBuilder(MemoryStructure const& memoryStructure, storm::models::sparse::Model const& model) : model(model), transitions(memoryStructure.getTransitionMatrix()), stateLabeling(memoryStructure.getStateLabeling()), initialMemoryStates(memoryStructure.getInitialMemoryStates()) { + // Intentionally left empty + } + template void MemoryStructureBuilder::setInitialMemoryState(uint_fast64_t initialModelState, uint_fast64_t initialMemoryState) { STORM_LOG_THROW(model.getInitialStates().get(initialModelState), storm::exceptions::InvalidOperationException, "Invalid index of initial model state: " << initialMemoryState << ". This is not an initial state of the model."); diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.h b/src/storm/storage/memorystructure/MemoryStructureBuilder.h index 1cb51f384..bb310ccf3 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.h +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.h @@ -20,6 +20,11 @@ namespace storm { */ MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model const& model); + /*! + * Initializes a new builder with the data from the provided memory structure + */ + MemoryStructureBuilder(MemoryStructure const& memoryStructure, storm::models::sparse::Model const& model); + /*! * Specifies for the given initial state of the model the corresponding initial memory state. *