diff --git a/src/storm/api/export.h b/src/storm/api/export.h index b1dbb6d21..6f4b82f77 100644 --- a/src/storm/api/export.h +++ b/src/storm/api/export.h @@ -56,9 +56,9 @@ namespace storm { storm::utility::openFile(filename, stream); std::string jsonFileExtension = ".json"; if (filename.size() > 4 && std::equal(jsonFileExtension.rbegin(), jsonFileExtension.rend(), filename.rbegin())) { - scheduler.printJsonToStream(stream, model); + scheduler.printJsonToStream(stream, model, false, true); } else { - scheduler.printToStream(stream, model); + scheduler.printToStream(stream, model, false, true); } storm::utility::closeFile(stream); } diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index c177747de..3d2c5a697 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -162,7 +162,7 @@ namespace storm { } template - void Scheduler::printToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { + void Scheduler::printToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices, bool skipDontCareStates) 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(); @@ -214,6 +214,15 @@ namespace storm { if (!isMemorylessScheduler()) { stateString << "m" << std::setw(8) << memoryState; } + stateString << " "; + + bool firstMemoryState = true; + for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) { + + // Ignore dontCare states + if(skipDontCareStates && isDontCare(state, memoryState)) { + continue; + } // Print choice info SchedulerChoice const& choice = schedulerChoices[memoryState][state]; @@ -254,44 +263,46 @@ namespace storm { stateString << "undefined."; } - // Print memory updates - if(!isMemorylessScheduler()) { - out << std::setw(widthOfStates) << ""; - for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { - uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first; - bool firstUpdate = true; - for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) { - if (firstUpdate) { - firstUpdate = false; - } else { - stateString << ", "; + // Print memory updates + if(!isMemorylessScheduler()) { + stateString << std::setw(widthOfStates) << ""; + // The memory updates do not depend on the actual choice, they only depend on the current model- and memory state as well as the successor model state. + for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { + uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first; + bool firstUpdate = true; + for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) { + if (firstUpdate) { + firstUpdate = false; + } else { + stateString << ", "; + } + stateString << "model state' = " << entryIt->getColumn() << ": -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; + // out << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; } - stateString << "model state' = " << entryIt->getColumn() << ": -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; - // out << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; } } stateString << std::endl; } - out << stateString.str(); - out << std::endl; + stateString << stateString.str(); + stateString << std::endl; } } if (numOfSkippedStatesWithUniqueChoice > 0) { - out << "Skipped " << numOfSkippedStatesWithUniqueChoice << " deterministic states with unique choice." << std::endl; + stateString << "Skipped " << numOfSkippedStatesWithUniqueChoice << " deterministic states with unique choice." << std::endl; } - out << "___________________________________________________________________" << std::endl; + stateString << "___________________________________________________________________" << std::endl; } template <> - void Scheduler::printJsonToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { + void Scheduler::printJsonToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices, bool skipDontCareStates) const { STORM_LOG_THROW(isMemorylessScheduler(), storm::exceptions::NotImplementedException, "Json export of schedulers not implemented for this value type."); } template - void Scheduler::printJsonToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { + void Scheduler::printJsonToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices, bool skipDontCareStates) const { STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); storm::json output; @@ -303,7 +314,7 @@ namespace storm { for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) { // Ignore dontCare states - if ((!isMemorylessScheduler()) && isDontCare(state, memoryState)) { + if (skipDontCareStates && isDontCare(state, memoryState)) { continue; } diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index d6bdb9efd..91681511f 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -135,18 +135,15 @@ namespace storm { * @param skipUniqueChoices If true, the (unique) choice for deterministic states (i.e., states with only one enabled choice) is not printed explicitly. * Requires a model to be given. */ - void printToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; + void printToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false, bool skipDontCareStates = false) const; /*! * Prints the scheduler in json format to the given output stream. */ - void printJsonToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; - - void setPrintUndefinedChoices(bool value = true); - - protected: + void printJsonToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false, bool skipDontCareStates = false) const; + private: boost::optional memoryStructure; std::vector>> schedulerChoices;