From 093b01f0c50b470dee2820b5e70cf2388ba5dc3e Mon Sep 17 00:00:00 2001
From: hannah <hannah.mertens@rwth-aachen.de>
Date: Tue, 3 Aug 2021 13:51:41 +0200
Subject: [PATCH] adjusted scheduler dontCare

---
 src/storm/storage/Scheduler.cpp | 28 ++++++++++++++++++++--------
 src/storm/storage/Scheduler.h   | 10 +++++++++-
 2 files changed, 29 insertions(+), 9 deletions(-)

diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp
index 0c087b269..55b842d37 100644
--- a/src/storm/storage/Scheduler.cpp
+++ b/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>
diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h
index aeff2f225..cacd5b00b 100644
--- a/src/storm/storage/Scheduler.h
+++ b/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?
             */