diff --git a/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.cpp index 4748a03e8..16d3f7065 100644 --- a/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.cpp @@ -19,6 +19,9 @@ namespace storm { template std::shared_ptr SparseModelNondeterministicMemoryProduct::build() const { + // For Markov automata, we can not introduce nondeterminism at Markovian states. + // We could introduce new intermediate probabilistic states, however that is not supported yet. + STORM_LOG_THROW(!model.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::NotSupportedException, "Nondeterministic memory product not supported for Markov automata as this would introduce nondeterminism at Markovian states."); // For simplicity we first build the 'full' product of model and memory (with model.numStates * memory.numStates states). storm::storage::sparse::ModelComponents components; components.transitionMatrix = buildTransitions(); @@ -34,12 +37,13 @@ namespace storm { for (auto const& rewModel : model.getRewardModels()) { components.rewardModels.emplace(rewModel.first, buildRewardModel(rewModel.second, reachableStates)); } + /* Markov automata are not supported (This code would introduce nondeterminism at Markovian states...) if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) { STORM_LOG_ASSERT((std::is_same>::value), "Model has unexpected type."); auto ma = model.template as>(); components.exitRates = buildExitRateVector(*ma, reachableStates); components.markovianStates = buildMarkovianStateLabeling(*ma, reachableStates); - } + } */ return std::make_shared(std::move(components)); } @@ -132,6 +136,7 @@ namespace storm { return storm::models::sparse::StandardRewardModel(std::move(stateRewards), std::move(actionRewards)); } + /* Markov Automata currently not supported. template std::vector::ValueType> SparseModelNondeterministicMemoryProduct::buildExitRateVector(storm::models::sparse::MarkovAutomaton const& modelAsMA, storm::storage::BitVector const& reachableStates) const { std::vector res; @@ -162,7 +167,7 @@ namespace storm { } assert(currReachableState == reachableStates.getNumberOfSetBits()); return res; - } + }*/ template uint64_t SparseModelNondeterministicMemoryProduct::getProductState(uint64_t modelState, uint64_t memoryState) const { diff --git a/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.h index 664d8c63d..378b0e953 100644 --- a/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.h +++ b/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.h @@ -22,9 +22,9 @@ namespace storm { storm::models::sparse::StateLabeling buildStateLabeling() const; storm::models::sparse::StandardRewardModel buildRewardModel(storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& reachableStates) const; - // Markov automaton specific components - std::vector buildExitRateVector(storm::models::sparse::MarkovAutomaton const& modelAsMA, storm::storage::BitVector const& reachableStates) const; - storm::storage::BitVector buildMarkovianStateLabeling(storm::models::sparse::MarkovAutomaton const& modelAsMA, storm::storage::BitVector const& reachableStates) const; + // Disabled because Markov automata currently not supported + // std::vector buildExitRateVector(storm::models::sparse::MarkovAutomaton const& modelAsMA, storm::storage::BitVector const& reachableStates) const; + // storm::storage::BitVector buildMarkovianStateLabeling(storm::models::sparse::MarkovAutomaton const& modelAsMA, storm::storage::BitVector const& reachableStates) const; uint64_t getProductState(uint64_t modelState, uint64_t memoryState) const; uint64_t getModelState(uint64_t productState) const;