diff --git a/src/storm/storage/PostScheduler.cpp b/src/storm/storage/PostScheduler.cpp index 30c306abc..2208abb36 100644 --- a/src/storm/storage/PostScheduler.cpp +++ b/src/storm/storage/PostScheduler.cpp @@ -100,62 +100,66 @@ namespace storm { uint_fast64_t numOfSkippedStatesWithUniqueChoice = 0; out << std::setw(widthOfStates) << "model state:" << " " << (isMemorylessScheduler() ? "" : " memory: ") << "choice(s)" << std::endl; for (uint_fast64_t state = 0; state < schedulerChoiceMapping.front().size(); ++state) { - // Print the state info - if (stateValuationsGiven) { - out << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state)); + std::stringstream stateString; + // Print the state info + if (stateValuationsGiven) { + stateString << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state)); + } else { + stateString << std::setw(widthOfStates) << state; + } + stateString << " "; + + bool firstChoiceIndex = true; + for(uint choiceIndex = 0; choiceIndex < schedulerChoiceMapping[0][state].size(); choiceIndex++) { + SchedulerChoice const& choice = schedulerChoiceMapping[0][state][choiceIndex]; + if(firstChoiceIndex) { + firstChoiceIndex = false; + stateString << std::to_string(choiceIndex) << ": "; } else { - out << std::setw(widthOfStates) << state; + stateString << std::setw(widthOfStates + 5) << std::to_string(choiceIndex) << ": "; } - out << " "; - - bool firstChoiceIndex = true; - for(uint choiceIndex = 0; choiceIndex < schedulerChoiceMapping[0][state].size(); choiceIndex++) { - SchedulerChoice const& choice = schedulerChoiceMapping[0][state][choiceIndex]; - if(firstChoiceIndex) { - firstChoiceIndex = false; - out << std::to_string(choiceIndex) << ": "; + if (choice.isDefined()) { + if (choice.isDeterministic()) { + if (choiceOriginsGiven) { + stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); + } else { + stateString << choice.getDeterministicChoice(); + } + if (choiceLabelsGiven) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); + stateString << " {" << boost::join(choiceLabels, ", ") << "}"; + } } else { - out << std::setw(widthOfStates + 5) << std::to_string(choiceIndex) << ": "; - } - if (choice.isDefined()) { - if (choice.isDeterministic()) { + bool firstChoice = true; + for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { + if (firstChoice) { + firstChoice = false; + } else { + stateString << " + "; + } + stateString << choiceProbPair.second << ": ("; if (choiceOriginsGiven) { - out << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); + stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); } else { - out << choice.getDeterministicChoice(); + stateString << choiceProbPair.first; } if (choiceLabelsGiven) { auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); - out << " {" << boost::join(choiceLabels, ", ") << "}"; - } - } else { - bool firstChoice = true; - for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { - if (firstChoice) { - firstChoice = false; - } else { - out << " + "; - } - out << choiceProbPair.second << ": ("; - if (choiceOriginsGiven) { - out << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); - } else { - out << choiceProbPair.first; - } - if (choiceLabelsGiven) { - auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); - out << " {" << boost::join(choiceLabels, ", ") << "}"; - } - out << ")"; + stateString << " {" << boost::join(choiceLabels, ", ") << "}"; } + stateString << ")"; } - } else { - out << "undefined."; } - - // Todo: print memory updates - out << std::endl; + } else { + if(!this->printUndefinedChoices) goto skipStatesWithUndefinedChoices; + stateString << "undefined."; } + // Todo: print memory updates + stateString << std::endl; + } + out << stateString.str(); + // jump to label if we find one undefined choice. + skipStatesWithUndefinedChoices:; } } diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 59db79429..72b87234a 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -8,7 +8,7 @@ namespace storm { namespace storage { - + template Scheduler::Scheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure) : memoryStructure(memoryStructure) { uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1; @@ -16,7 +16,7 @@ namespace storm { numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates; numOfDeterministicChoices = 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; @@ -24,7 +24,7 @@ namespace storm { numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates; numOfDeterministicChoices = 0; } - + template void Scheduler::setChoice(SchedulerChoice const& choice, uint_fast64_t modelState, uint_fast64_t memoryState) { STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index"); @@ -50,7 +50,7 @@ namespace storm { ++numOfDeterministicChoices; } } - + schedulerChoice = choice; } @@ -71,7 +71,7 @@ namespace storm { STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index"); setChoice(SchedulerChoice(), modelState, memoryState); } - + template SchedulerChoice const& Scheduler::getChoice(uint_fast64_t modelState, uint_fast64_t memoryState) const { STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index"); @@ -96,17 +96,17 @@ namespace storm { } return result; } - + template bool Scheduler::isPartialScheduler() const { return numOfUndefinedChoices != 0; } - + template bool Scheduler::isDeterministicScheduler() const { return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices; } - + template bool Scheduler::isMemorylessScheduler() const { return getNumberOfMemoryStates() == 1; @@ -125,7 +125,7 @@ namespace storm { template void Scheduler::printToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { 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(); bool const choiceLabelsGiven = model != nullptr && model->hasChoiceLabeling(); bool const choiceOriginsGiven = model != nullptr && model->hasChoiceOrigins(); @@ -135,7 +135,7 @@ namespace storm { } widthOfStates = std::max(widthOfStates, (uint_fast64_t)12); uint_fast64_t numOfSkippedStatesWithUniqueChoice = 0; - + out << "___________________________________________________________________" << std::endl; out << (isPartialScheduler() ? "Partially" : "Fully") << " defined "; out << (isMemorylessScheduler() ? "memoryless " : ""); @@ -146,76 +146,79 @@ namespace storm { out << ":" << std::endl; STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); out << std::setw(widthOfStates) << "model state:" << " " << (isMemorylessScheduler() ? "" : " memory: ") << "choice(s)" << std::endl; - for (uint_fast64_t state = 0; state < schedulerChoices.front().size(); ++state) { - // Check whether the state is skipped - if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) { - ++numOfSkippedStatesWithUniqueChoice; - continue; - } - - // Print the state info - if (stateValuationsGiven) { - out << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state)); + for (uint_fast64_t state = 0; state < schedulerChoices.front().size(); ++state) { + std::stringstream stateString; + // Check whether the state is skipped + if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) { + ++numOfSkippedStatesWithUniqueChoice; + continue; + } + + // Print the state info + if (stateValuationsGiven) { + stateString << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state)); + } else { + stateString << std::setw(widthOfStates) << state; + } + stateString << " "; + + bool firstMemoryState = true; + for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) { + // Indent if this is not the first memory state + if (firstMemoryState) { + firstMemoryState = false; } else { - out << std::setw(widthOfStates) << state; + stateString << std::setw(widthOfStates) << ""; + stateString << " "; } - out << " "; - - bool firstMemoryState = true; - for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) { - // Indent if this is not the first memory state - if (firstMemoryState) { - firstMemoryState = false; + // Print the memory state info + if (!isMemorylessScheduler()) { + stateString << "m" << std::setw(8) << memoryState; + } + + // Print choice info + SchedulerChoice const& choice = schedulerChoices[memoryState][state]; + if (choice.isDefined()) { + if (choice.isDeterministic()) { + if (choiceOriginsGiven) { + stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); + } else { + stateString << choice.getDeterministicChoice(); + } + if (choiceLabelsGiven) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); + stateString << " {" << boost::join(choiceLabels, ", ") << "}"; + } } else { - out << std::setw(widthOfStates) << ""; - out << " "; - } - // Print the memory state info - if (!isMemorylessScheduler()) { - out << "m" << std::setw(8) << memoryState; - } - - // Print choice info - SchedulerChoice const& choice = schedulerChoices[memoryState][state]; - if (choice.isDefined()) { - if (choice.isDeterministic()) { + bool firstChoice = true; + for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { + if (firstChoice) { + firstChoice = false; + } else { + stateString << " + "; + } + stateString << choiceProbPair.second << ": ("; if (choiceOriginsGiven) { - out << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); + stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); } else { - out << choice.getDeterministicChoice(); + stateString << choiceProbPair.first; } if (choiceLabelsGiven) { auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); - out << " {" << boost::join(choiceLabels, ", ") << "}"; - } - } else { - bool firstChoice = true; - for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { - if (firstChoice) { - firstChoice = false; - } else { - out << " + "; - } - out << choiceProbPair.second << ": ("; - if (choiceOriginsGiven) { - out << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); - } else { - out << choiceProbPair.first; - } - if (choiceLabelsGiven) { - auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); - out << " {" << boost::join(choiceLabels, ", ") << "}"; - } - out << ")"; + stateString << " {" << boost::join(choiceLabels, ", ") << "}"; } + stateString << ")"; } - } else { - out << "undefined."; } - - // Todo: print memory updates - out << std::endl; + } else { + if(!printUndefinedChoices) continue; + stateString << "undefined."; } + + // Todo: print memory updates + out << stateString.str(); + out << std::endl; + } } if (numOfSkippedStatesWithUniqueChoice > 0) { out << "Skipped " << numOfSkippedStatesWithUniqueChoice << " deterministic states with unique choice." << std::endl; @@ -271,10 +274,15 @@ namespace storm { out << output.dump(4); } + template + void Scheduler::setPrintUndefinedChoices(bool value) { + printUndefinedChoices = value; + } + template class Scheduler; template class Scheduler; template class Scheduler; template class Scheduler; - + } } diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index 43340133d..53bbc1d2e 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -1,6 +1,8 @@ #pragma once #include +#include + #include "storm/storage/memorystructure/MemoryStructure.h" #include "storm/storage/SchedulerChoice.h" @@ -117,10 +119,14 @@ namespace storm { */ void printJsonToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; + void setPrintUndefinedChoices(bool value = true); + private: boost::optional memoryStructure; std::vector>> schedulerChoices; + + bool printUndefinedChoices = false; protected: uint_fast64_t numOfUndefinedChoices; uint_fast64_t numOfDeterministicChoices;