From 97b4f1f9391b697193ad5b1a820d120383e41d1b Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Mon, 19 Apr 2021 11:44:56 +0200 Subject: [PATCH] adapted PostScheduler output format --- src/storm/storage/PostScheduler.cpp | 65 +++++++++++++---------------- src/storm/storage/PostScheduler.h | 3 +- 2 files changed, 32 insertions(+), 36 deletions(-) diff --git a/src/storm/storage/PostScheduler.cpp b/src/storm/storage/PostScheduler.cpp index 74bb2983c..7256319f0 100644 --- a/src/storm/storage/PostScheduler.cpp +++ b/src/storm/storage/PostScheduler.cpp @@ -87,7 +87,8 @@ namespace storm { } template - void PostScheduler::printToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { + void PostScheduler::printToStream(std::ostream& out, std::shared_ptr shieldingExpression, std::shared_ptr> model, bool skipUniqueChoices) const { + STORM_LOG_THROW(this->isMemorylessScheduler(), storm::exceptions::InvalidOperationException, "The given scheduler is incompatible."); bool const stateValuationsGiven = model != nullptr && model->hasStateValuations(); bool const choiceLabelsGiven = model != nullptr && model->hasChoiceLabeling(); @@ -97,8 +98,17 @@ namespace storm { widthOfStates += model->getStateValuations().getStateInfo(schedulerChoiceMapping.front().size() - 1).length() + 5; } widthOfStates = std::max(widthOfStates, (uint_fast64_t)12); + out << "___________________________________________________________________" << std::endl; + out << shieldingExpression->prettify() << 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:" << " " << "correction"; + if(choiceLabelsGiven) { + out << " [ {action label}: {corrected action label}]"; + } else { + out << " [: ()}"; + } + out << ":" << std::endl; 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) { std::stringstream stateString; // Print the state info @@ -114,50 +124,35 @@ namespace storm { SchedulerChoice const& choice = schedulerChoiceMapping[0][state][choiceIndex]; if(firstChoiceIndex) { firstChoiceIndex = false; - stateString << std::to_string(choiceIndex) << ": "; } else { - stateString << std::setw(widthOfStates + 5) << std::to_string(choiceIndex) << ": "; + stateString << "; "; } 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, ", ") << "}"; - } + auto choiceProbPair = *(choice.getChoiceAsDistribution().begin()); + if(choiceLabelsGiven) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceIndex); + stateString << std::to_string(choiceIndex) << " {" << boost::join(choiceLabels, ", ") << "}: "; + } else { + stateString << std::to_string(choiceIndex) << ": "; + } + //stateString << choiceProbPair.second << ": ("; + if (choiceOriginsGiven) { + stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); } else { - bool firstChoice = true; - for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { - if (firstChoice) { - firstChoice = false; - } else { - stateString << " + "; - } - stateString << choiceProbPair.second << ": ("; - if (choiceOriginsGiven) { - stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); - } else { - stateString << choiceProbPair.first; - } - if (choiceLabelsGiven) { - auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); - stateString << " {" << boost::join(choiceLabels, ", ") << "}"; - } - stateString << ")"; - } + stateString << choiceProbPair.first; } + if (choiceLabelsGiven) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); + stateString << " {" << boost::join(choiceLabels, ", ") << "}"; + } + } else { if(!this->printUndefinedChoices) goto skipStatesWithUndefinedChoices; stateString << "undefined."; } // Todo: print memory updates - stateString << std::endl; } - out << stateString.str(); + out << stateString.str() << std::endl; // jump to label if we find one undefined choice. skipStatesWithUndefinedChoices:; } diff --git a/src/storm/storage/PostScheduler.h b/src/storm/storage/PostScheduler.h index 4a64ba756..57c194fa6 100644 --- a/src/storm/storage/PostScheduler.h +++ b/src/storm/storage/PostScheduler.h @@ -4,6 +4,7 @@ #include #include "storm/storage/SchedulerChoice.h" #include "storm/storage/Scheduler.h" +#include "storm/logic/ShieldExpression.h" namespace storm { namespace storage { @@ -89,7 +90,7 @@ 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 shieldingExpression, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; private: std::vector>>> schedulerChoiceMapping;