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 - void Scheduler::setDontCare(uint_fast64_t modelState, uint_fast64_t memoryState) { + void Scheduler::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 reachableStates; - uint_fast64_t numOfUndefinedChoices; // Only consider reachable ones - std::vector dontCareStates; // Their choices are neither considered deterministic nor undefined + std::vector dontCareStates; + uint_fast64_t numOfUndefinedChoices; uint_fast64_t numOfDeterministicChoices; uint_fast64_t numOfDontCareStates; };