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::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 + void Scheduler::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(0); } } + template bool Scheduler::isDontCare(uint_fast64_t modelState, uint64_t memoryState) const { return dontCareStates[memoryState].get(modelState); @@ -137,7 +149,7 @@ namespace storm { template bool Scheduler::isDeterministicScheduler() const { - return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices - numOfDontCareStates; + return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices; } template 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? */