From 48bddc29b77441c12ecc29ee56efa3a2bec0ed54 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 23 Oct 2019 20:43:54 +0200
Subject: [PATCH] NondeterministicMemoryProduct: Disabled support for Markov
 automata since Nondeterminism was added to Markovian states.

---
 .../SparseModelNondeterministicMemoryProduct.cpp         | 9 +++++++--
 .../SparseModelNondeterministicMemoryProduct.h           | 6 +++---
 2 files changed, 10 insertions(+), 5 deletions(-)

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<typename SparseModelType>
             std::shared_ptr<SparseModelType> SparseModelNondeterministicMemoryProduct<SparseModelType>::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<ValueType> 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<SparseModelType, storm::models::sparse::MarkovAutomaton<ValueType>>::value), "Model has unexpected type.");
                     auto ma = model.template as<storm::models::sparse::MarkovAutomaton<ValueType>>();
                     components.exitRates = buildExitRateVector(*ma, reachableStates);
                     components.markovianStates = buildMarkovianStateLabeling(*ma, reachableStates);
-                }
+                } */
                 return std::make_shared<SparseModelType>(std::move(components));
             }
         
@@ -132,6 +136,7 @@ namespace storm {
                 return storm::models::sparse::StandardRewardModel<ValueType>(std::move(stateRewards), std::move(actionRewards));
             }
         
+            /* Markov Automata currently not supported.
             template<typename SparseModelType>
             std::vector<typename SparseModelNondeterministicMemoryProduct<SparseModelType>::ValueType> SparseModelNondeterministicMemoryProduct<SparseModelType>::buildExitRateVector(storm::models::sparse::MarkovAutomaton<ValueType> const& modelAsMA, storm::storage::BitVector const& reachableStates) const {
                 std::vector<ValueType> res;
@@ -162,7 +167,7 @@ namespace storm {
                 }
                 assert(currReachableState == reachableStates.getNumberOfSetBits());
                 return res;
-            }
+            }*/
 
             template<typename SparseModelType>
             uint64_t SparseModelNondeterministicMemoryProduct<SparseModelType>::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<ValueType> buildRewardModel(storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel, storm::storage::BitVector const& reachableStates) const;
             
-            // Markov automaton specific components
-            std::vector<ValueType> buildExitRateVector(storm::models::sparse::MarkovAutomaton<ValueType> const& modelAsMA, storm::storage::BitVector const& reachableStates) const;
-            storm::storage::BitVector buildMarkovianStateLabeling(storm::models::sparse::MarkovAutomaton<ValueType> const& modelAsMA, storm::storage::BitVector const& reachableStates) const;
+            // Disabled because Markov automata currently not supported
+            // std::vector<ValueType> buildExitRateVector(storm::models::sparse::MarkovAutomaton<ValueType> const& modelAsMA, storm::storage::BitVector const& reachableStates) const;
+            // storm::storage::BitVector buildMarkovianStateLabeling(storm::models::sparse::MarkovAutomaton<ValueType> 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;