From e5b19643e82c0fc097bd07be2aef0b0a763baccb Mon Sep 17 00:00:00 2001
From: hannah <hannah.mertens@rwth-aachen.de>
Date: Wed, 11 Aug 2021 16:45:45 +0200
Subject: [PATCH] dontCareStates can now be (non)deterministic and (un)defined

 Conflicts:
	src/storm/storage/Scheduler.h
---
 src/storm/storage/Scheduler.cpp | 46 ++++++++++++++-------------------
 src/storm/storage/Scheduler.h   |  9 ++++---
 2 files changed, 25 insertions(+), 30 deletions(-)

diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp
index 964346afc..c177747de 100644
--- a/src/storm/storage/Scheduler.cpp
+++ b/src/storm/storage/Scheduler.cpp
@@ -35,26 +35,25 @@ namespace storm {
             STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index");
 
             auto& schedulerChoice = schedulerChoices[memoryState][modelState];
-            if (!dontCareStates[memoryState].get(modelState)) {
-                if (schedulerChoice.isDefined()) {
-                    if (!choice.isDefined()) {
-                        ++numOfUndefinedChoices;
-                    }
-                } else {
-                    if (choice.isDefined()) {
-                        assert(numOfUndefinedChoices > 0);
-                        --numOfUndefinedChoices;
-                    }
+
+            if (schedulerChoice.isDefined()) {
+                if (!choice.isDefined()) {
+                    ++numOfUndefinedChoices;
                 }
-                if (schedulerChoice.isDeterministic()) {
-                    if (!choice.isDeterministic()) {
-                        assert(numOfDeterministicChoices > 0);
-                        --numOfDeterministicChoices;
-                    }
-                } else {
-                    if (choice.isDeterministic()) {
-                        ++numOfDeterministicChoices;
-                    }
+            } else {
+                if (choice.isDefined()) {
+                    assert(numOfUndefinedChoices > 0);
+                    --numOfUndefinedChoices;
+                }
+            }
+            if (schedulerChoice.isDeterministic()) {
+                if (!choice.isDeterministic()) {
+                    assert(numOfDeterministicChoices > 0);
+                    --numOfDeterministicChoices;
+                }
+            } else {
+                if (choice.isDeterministic()) {
+                    ++numOfDeterministicChoices;
                 }
             }
 
@@ -87,13 +86,13 @@ namespace storm {
         }
 
         template <typename ValueType>
-        void Scheduler<ValueType>::setDontCare(uint_fast64_t modelState, uint_fast64_t memoryState) {
+        void Scheduler<ValueType>::setDontCare(uint_fast64_t modelState, uint_fast64_t memoryState, bool setArbitraryChoice) {
             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()) {
+                if (!schedulerChoice.isDefined() && setArbitraryChoice) {
                     // Set an arbitrary choice
                     this->setChoice(0, modelState, memoryState);
                 }
@@ -108,13 +107,8 @@ namespace storm {
             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;
-                }
                 dontCareStates[memoryState].set(modelState, false);
                 --numOfDontCareStates;
-
             }
         }
 
diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h
index e953e21b7..d6bdb9efd 100644
--- a/src/storm/storage/Scheduler.h
+++ b/src/storm/storage/Scheduler.h
@@ -62,12 +62,13 @@ namespace storm {
 
             /*!
              * Set the combination of model state and memoryStructure state to dontCare.
-             * Set an arbitrary choice an arbitrary choice if no choice exists.
+             * If not specified otherwise, an arbitrary choice is set if no choice exists.
              *
              * @param modelState The state of the model.
              * @param memoryState The state of the memoryStructure.
+             * @param memoryState A flag indicating whether to set an arbitrary choice.
              */
-            void setDontCare(uint_fast64_t modelState, uint_fast64_t memoryState = 0);
+            void setDontCare(uint_fast64_t modelState, uint_fast64_t memoryState = 0, bool setArbitraryChoice = true);
 
             /*!
              * Unset the combination of model state and memoryStructure state to dontCare.
@@ -152,8 +153,8 @@ namespace storm {
             bool printUndefinedChoices = false;
 
             std::vector<storm::storage::BitVector> reachableStates;
-            uint_fast64_t numOfUndefinedChoices; // Only consider reachable ones
-            std::vector<storm::storage::BitVector> dontCareStates; // Their choices are neither considered deterministic nor undefined
+            std::vector<storm::storage::BitVector> dontCareStates;
+            uint_fast64_t numOfUndefinedChoices;
             uint_fast64_t numOfDeterministicChoices;
             uint_fast64_t numOfDontCareStates;
         };