adjusted scheduler dontCare

src/storm/storage/Scheduler.cpp

@@ -90,23 +90,35 @@ namespace storm {
         void Scheduler<ValueType>::setDontCare(uint_fast64_t modelState, uint_fast64_t memoryState) {
             STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index");
             STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index");
-            auto& schedulerChoice = schedulerChoices[memoryState][modelState];
+
             if (!dontCareStates[memoryState].get(modelState)) {
+                auto& schedulerChoice = schedulerChoices[memoryState][modelState];
+                if (!schedulerChoice.isDefined()) {
+                    // Set an arbitrary choice
+                    this->setChoice(0, modelState, memoryState);
+                }
                 dontCareStates[memoryState].set(modelState, true);
                 ++numOfDontCareStates;
+            }
+        }
 
-                // Choices for dontCare states are not considered undefined or deterministic
+        template <typename ValueType>
+        void Scheduler<ValueType>::unSetDontCare(uint_fast64_t modelState, uint_fast64_t memoryState) {
+            STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index");
+            STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index");
+
+            if (dontCareStates[memoryState].get(modelState)) {
+                auto& schedulerChoice = schedulerChoices[memoryState][modelState];
                 if (!schedulerChoice.isDefined()) {
-                    --numOfUndefinedChoices;
-                } else if (schedulerChoice.isDeterministic()) {
-                    --numOfDeterministicChoices;
+                    ++numOfUndefinedChoices;
                 }
+                dontCareStates[memoryState].set(modelState, false);
+                --numOfDontCareStates;
 
-                // Set an arbitrary choice
-                schedulerChoices[memoryState][modelState] = SchedulerChoice<ValueType>(0);
             }
         }
 
+
         template <typename ValueType>
         bool Scheduler<ValueType>::isDontCare(uint_fast64_t modelState, uint64_t memoryState) const {
             return dontCareStates[memoryState].get(modelState);
@@ -137,7 +149,7 @@ namespace storm {
 
         template <typename ValueType>
         bool Scheduler<ValueType>::isDeterministicScheduler() const {
-            return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices - numOfDontCareStates;
+            return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices;
         }
 
         template <typename ValueType>

src/storm/storage/Scheduler.h

@@ -62,13 +62,21 @@ namespace storm {
 
             /*!
              * Set the combination of model state and memoryStructure state to dontCare.
-             * This means the corresponding choices are neither considered undefined nor deterministic.
+             * Set an arbitrary choice an arbitrary choice if no choice exists.
              *
              * @param modelState The state of the model.
              * @param memoryState The state of the memoryStructure.
              */
             void setDontCare(uint_fast64_t modelState, uint_fast64_t memoryState = 0);
 
+            /*!
+             * Unset the combination of model state and memoryStructure state to dontCare.
+             *
+             * @param modelState The state of the model.
+             * @param memoryState The state of the memoryStructure.
+             */
+            void unSetDontCare(uint_fast64_t modelState, uint_fast64_t memoryState = 0);
+
             /*!
             * Is the combination of model state and memoryStructure state to reachable?
             */