From 6b0aaeadb46721007c3be3b7fb80e3c57683fb9b Mon Sep 17 00:00:00 2001 From: hannah Date: Tue, 27 Jul 2021 11:05:41 +0200 Subject: [PATCH] ignore dontCare States while printing TODO Scheduler printing will need refactoring Conflicts: src/storm/storage/Scheduler.cpp src/storm/storage/Scheduler.h --- src/storm/storage/Scheduler.cpp | 48 +++++++++------------------------ src/storm/storage/Scheduler.h | 19 +++++-------- 2 files changed, 20 insertions(+), 47 deletions(-) diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index ab9fc40e3..51a3f40e8 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -13,20 +13,20 @@ namespace storm { Scheduler::Scheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure) : memoryStructure(memoryStructure) { uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1; schedulerChoices = std::vector>>(numOfMemoryStates, std::vector>(numberOfModelStates)); - reachableStates = std::vector(numOfMemoryStates, storm::storage::BitVector(numberOfModelStates, true)); + dontCareStates = std::vector(numOfMemoryStates, storm::storage::BitVector(numberOfModelStates, false)); numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates; numOfDeterministicChoices = 0; - numOfUnreachableStates = 0; + numOfDontCareStates = 0; } template Scheduler::Scheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure) : memoryStructure(std::move(memoryStructure)) { uint_fast64_t numOfMemoryStates = this->memoryStructure ? this->memoryStructure->getNumberOfStates() : 1; schedulerChoices = std::vector>>(numOfMemoryStates, std::vector>(numberOfModelStates)); - reachableStates = std::vector(numOfMemoryStates, storm::storage::BitVector(numberOfModelStates, true)); + dontCareStates = std::vector(numOfMemoryStates, storm::storage::BitVector(numberOfModelStates, false)); numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates; numOfDeterministicChoices = 0; - numOfUnreachableStates = 0; + numOfDontCareStates = 0; } template @@ -35,7 +35,7 @@ namespace storm { STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index"); auto& schedulerChoice = schedulerChoices[memoryState][modelState]; - if (reachableStates[memoryState].get(modelState)) { + if (!dontCareStates[memoryState].get(modelState)) { if (schedulerChoice.isDefined()) { if (!choice.isDefined()) { ++numOfUndefinedChoices; @@ -87,13 +87,13 @@ namespace storm { } template - void Scheduler::setStateUnreachable(uint_fast64_t modelState, uint_fast64_t memoryState) { + 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 (reachableStates[memoryState].get(modelState)) { - reachableStates[memoryState].set(modelState, false); - ++numOfUnreachableStates; + if (!dontCareStates[memoryState].get(modelState)) { + dontCareStates[memoryState].set(modelState, true); + ++numOfDontCareStates; // Choices for unreachable states are not considered undefined or deterministic if (!schedulerChoice.isDefined()) { @@ -106,27 +106,8 @@ namespace storm { } template - void Scheduler::setStateReachable(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 (!reachableStates[memoryState].get(modelState)) { - reachableStates[memoryState].set(modelState, true); - --numOfUnreachableStates; - - // Choices for unreachable states are not considered undefined or deterministic - if (!schedulerChoice.isDefined()) { - ++numOfUndefinedChoices; - } else if (schedulerChoice.isDeterministic()) { - ++numOfDeterministicChoices; - } - - } - } - - template - bool Scheduler::isStateReachable(uint_fast64_t modelState, uint64_t memoryState) const { - return reachableStates[memoryState].get(modelState); + bool Scheduler::isDontCare(uint_fast64_t modelState, uint64_t memoryState) const { + return dontCareStates[memoryState].get(modelState); } template @@ -154,7 +135,7 @@ namespace storm { template bool Scheduler::isDeterministicScheduler() const { - return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices - numOfUnreachableStates; + return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices - numOfDontCareStates; } template @@ -174,7 +155,6 @@ namespace storm { template void Scheduler::printToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { - // TODO ignore unreachable states STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); bool const stateValuationsGiven = model != nullptr && model->hasStateValuations(); @@ -267,9 +247,8 @@ namespace storm { } // Print memory updates - if(!isMemorylessScheduler()) { - stateString << std::setw(30); //todo set width + out << std::setw(8); for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first; bool firstUpdate = true; @@ -282,7 +261,6 @@ namespace storm { stateString << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; //out << ", model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = ?) "; } - } stateString << std::endl; diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index 18e3a8fb7..aeff2f225 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -61,25 +61,18 @@ namespace storm { SchedulerChoice const& getChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0) const; /*! - * Set the combination of model state and memoryStructure state to unreachable. + * Set the combination of model state and memoryStructure state to dontCare. + * This means the corresponding choices are neither considered undefined nor deterministic. * * @param modelState The state of the model. * @param memoryState The state of the memoryStructure. */ - void setStateUnreachable(uint_fast64_t modelState, uint_fast64_t memoryState = 0); - - /*! - * Set the combination of model state and memoryStructure state to reachable. - * - * @param modelState The state of the model. - * @param memoryState The state of the memoryStructure. - */ - void setStateReachable(uint_fast64_t modelState, uint_fast64_t memoryState = 0); + void setDontCare(uint_fast64_t modelState, uint_fast64_t memoryState = 0); /*! * Is the combination of model state and memoryStructure state to reachable? */ - bool isStateReachable(uint_fast64_t modelState, uint64_t memoryState = 0) const; + bool isDontCare(uint_fast64_t modelState, uint64_t memoryState = 0) const; /*! * Compute the Action Support: A bit vector that indicates all actions that are selected with positive probability in some memory state @@ -152,8 +145,10 @@ namespace storm { std::vector reachableStates; uint_fast64_t numOfUndefinedChoices; // Only consider reachable ones + std::vector dontCareStates; // Their choices are neither considered deterministic nor undefined + uint_fast64_t numOfUndefinedChoices; uint_fast64_t numOfDeterministicChoices; - uint_fast64_t numOfUnreachableStates; + uint_fast64_t numOfDontCareStates; }; } }