From 7f4fa270088b1adc8ea11346d7ce5af810cf5865 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Tue, 1 Mar 2016 10:21:21 +0100
Subject: [PATCH] Initialize closed for MA

Former-commit-id: 292352f2580315b8e5c48d0736bfb9314c96b146
---
 src/models/sparse/MarkovAutomaton.cpp | 19 ++++++++++++++++---
 src/models/sparse/MarkovAutomaton.h   |  7 +++++++
 2 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp
index 8276f519d..aa5ffc5e2 100644
--- a/src/models/sparse/MarkovAutomaton.cpp
+++ b/src/models/sparse/MarkovAutomaton.cpp
@@ -19,8 +19,9 @@ namespace storm {
                                                         std::vector<ValueType> const& exitRates,
                                                         std::unordered_map<std::string, RewardModelType> const& rewardModels,
                                                         boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
-            : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::MarkovAutomaton, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(false) {
+            : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::MarkovAutomaton, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates) {
                 this->turnRatesToProbabilities();
+                closed = !hasHybridState();
             }
             
             template <typename ValueType, typename RewardModelType>
@@ -30,8 +31,9 @@ namespace storm {
                                                         std::vector<ValueType> const& exitRates,
                                                         std::unordered_map<std::string, RewardModelType>&& rewardModels,
                                                         boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
-            : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(false) {
+            : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)) {
                 this->turnRatesToProbabilities();
+                closed = !hasHybridState();
             }
             
             template <typename ValueType, typename RewardModelType>
@@ -42,9 +44,10 @@ namespace storm {
                                                                          bool probabilities,
                                                                          std::unordered_map<std::string, RewardModelType>&& rewardModels,
                                                                          boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
-            : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(false) {
+            : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)) {
                 assert(probabilities);
                 assert(this->getTransitionMatrix().isProbabilistic());
+                closed = !hasHybridState();
             }
             
             template <typename ValueType, typename RewardModelType>
@@ -67,6 +70,16 @@ namespace storm {
                 return !this->markovianStates.get(state);
             }
             
+            template <typename ValueType, typename RewardModelType>
+            bool MarkovAutomaton<ValueType, RewardModelType>::hasHybridState() const {
+                for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
+                    if (this->isHybridState(state)) {
+                        return true;
+                    }
+                }
+                return false;
+            }
+            
             template <typename ValueType, typename RewardModelType>
             std::vector<ValueType> const& MarkovAutomaton<ValueType, RewardModelType>::getExitRates() const {
                 return this->exitRates;
diff --git a/src/models/sparse/MarkovAutomaton.h b/src/models/sparse/MarkovAutomaton.h
index e335f5050..d97ff1517 100644
--- a/src/models/sparse/MarkovAutomaton.h
+++ b/src/models/sparse/MarkovAutomaton.h
@@ -157,6 +157,13 @@ namespace storm {
                  */
                 void turnRatesToProbabilities();
                 
+                /*!
+                 * Check if at least one hybrid state exists.
+                 *
+                 * @return True, if at least one hybrid state exists, false if none exists.
+                 */
+                bool hasHybridState() const;
+                
                 // A bit vector representing the set of Markovian states.
                 storm::storage::BitVector markovianStates;