Initialize closed for MA

Former-commit-id: 292352f258

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;

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;