From cab3339ad64fa00f8e2149c2d8260536f87dd7e0 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Mon, 19 Apr 2021 11:43:20 +0200 Subject: [PATCH] added OptimalShield --- src/storm/storage/OptimalScheduler.cpp | 112 +++++++++++++++++++++++++ src/storm/storage/OptimalScheduler.h | 42 ++++++++++ 2 files changed, 154 insertions(+) create mode 100644 src/storm/storage/OptimalScheduler.cpp create mode 100644 src/storm/storage/OptimalScheduler.h diff --git a/src/storm/storage/OptimalScheduler.cpp b/src/storm/storage/OptimalScheduler.cpp new file mode 100644 index 000000000..982c2e6fa --- /dev/null +++ b/src/storm/storage/OptimalScheduler.cpp @@ -0,0 +1,112 @@ +#include "storm/utility/vector.h" +#include "storm/storage/OptimalScheduler.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotImplementedException.h" +#include + +namespace storm { + namespace storage { + template + OptimalScheduler::OptimalScheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure) : Scheduler(numberOfModelStates, memoryStructure) { + } + + template + OptimalScheduler::OptimalScheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure) : Scheduler(numberOfModelStates, std::move(memoryStructure)) { + } + + template + void OptimalScheduler::printToStream(std::ostream& out, std::shared_ptr shieldingExpression, std::shared_ptr> model, bool skipUniqueChoices) const { + STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == this->schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); + 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(); + bool const choiceOriginsGiven = model != nullptr && model->hasChoiceOrigins(); + uint_fast64_t widthOfStates = std::to_string(this->schedulerChoices.front().size()).length(); + if (stateValuationsGiven) { + widthOfStates += model->getStateValuations().getStateInfo(this->schedulerChoices.front().size() - 1).length() + 5; + } + widthOfStates = std::max(widthOfStates, (uint_fast64_t)12); + uint_fast64_t numOfSkippedStatesWithUniqueChoice = 0; + + 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:" << " " << "choice"; + if(choiceLabelsGiven) { + out << " [: (]"; + } else { + out << " [: ()}"; + } + out << ":" << std::endl; + for (uint_fast64_t state = 0; state < this->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 < this->getNumberOfMemoryStates(); ++memoryState) { + // Indent if this is not the first memory state + if (firstMemoryState) { + firstMemoryState = false; + } else { + stateString << std::setw(widthOfStates) << ""; + stateString << " "; + } + + // Print choice info + SchedulerChoice const& choice = this->schedulerChoices[memoryState][state]; + if (choice.isDefined()) { + 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 << ")"; + } + } else { + if(!this->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; + } + out << "___________________________________________________________________" << std::endl; + } + + template class OptimalScheduler; +#ifdef STORM_HAVE_CARL + template class OptimalScheduler; +#endif + } +} diff --git a/src/storm/storage/OptimalScheduler.h b/src/storm/storage/OptimalScheduler.h new file mode 100644 index 000000000..827676bbd --- /dev/null +++ b/src/storm/storage/OptimalScheduler.h @@ -0,0 +1,42 @@ +#pragma once + +#include +#include +#include +#include "storm/storage/SchedulerChoice.h" +#include "storm/storage/Scheduler.h" +#include "storm/logic/ShieldExpression.h" + +namespace storm { + namespace storage { + + /* + * TODO needs obvious changes in all comment blocks + * This class defines which action is chosen in a particular state of a non-deterministic model. More concretely, a scheduler maps a state s to i + * if the scheduler takes the i-th action available in s (i.e. the choices are relative to the states). + * A Choice can be undefined, deterministic + */ + template + class OptimalScheduler : public Scheduler { + public: + typedef uint_fast64_t OldChoice; + /*! + * Initializes a scheduler for the given number of model states. + * + * @param numberOfModelStates number of model states + * @param memoryStructure the considered memory structure. If not given, the scheduler is considered as memoryless. + */ + OptimalScheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure = boost::none); + OptimalScheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure); + + /*! + * Prints the scheduler to the given output stream. + * @param out The output stream + * @param model If given, provides additional information for printing (e.g., displaying the state valuations instead of state indices) + * @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 shieldingExpression, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; + }; + } +}