diff --git a/src/storm/shields/PreSafetyShield.cpp b/src/storm/shields/PreSafetyShield.cpp index 06cbb56f7..abbc50ae7 100644 --- a/src/storm/shields/PreSafetyShield.cpp +++ b/src/storm/shields/PreSafetyShield.cpp @@ -11,7 +11,7 @@ namespace tempest { } template - storm::storage::Scheduler PreSafetyShield::construct() { + storm::storage::PreScheduler PreSafetyShield::construct() { if (this->getOptimizationDirection() == storm::OptimizationDirection::Minimize) { if(this->shieldingExpression->isRelative()) { return constructWithCompareType, true>(); @@ -29,9 +29,9 @@ namespace tempest { template template - storm::storage::Scheduler PreSafetyShield::constructWithCompareType() { + storm::storage::PreScheduler PreSafetyShield::constructWithCompareType() { tempest::shields::utility::ChoiceFilter choiceFilter; - storm::storage::Scheduler shield(this->rowGroupIndices.size() - 1); + storm::storage::PreScheduler shield(this->rowGroupIndices.size() - 1); auto choice_it = this->choiceValues.begin(); if(this->coalitionStates.is_initialized()) { this->relevantStates &= this->coalitionStates.get(); diff --git a/src/storm/shields/PreSafetyShield.h b/src/storm/shields/PreSafetyShield.h index 22e758aa1..8a4667bf2 100644 --- a/src/storm/shields/PreSafetyShield.h +++ b/src/storm/shields/PreSafetyShield.h @@ -1,6 +1,7 @@ #pragma once #include "storm/shields/AbstractShield.h" +#include "storm/storage/PreScheduler.h" namespace tempest { namespace shields { @@ -10,9 +11,9 @@ namespace tempest { public: PreSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); - storm::storage::Scheduler construct(); + storm::storage::PreScheduler construct(); template - storm::storage::Scheduler constructWithCompareType(); + storm::storage::PreScheduler constructWithCompareType(); private: std::vector choiceValues; }; diff --git a/src/storm/storage/PreScheduler.cpp b/src/storm/storage/PreScheduler.cpp new file mode 100644 index 000000000..0f1cf775d --- /dev/null +++ b/src/storm/storage/PreScheduler.cpp @@ -0,0 +1,112 @@ +#include "storm/utility/vector.h" +#include "storm/storage/PreScheduler.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotImplementedException.h" +#include + +namespace storm { + namespace storage { + template + PreScheduler::PreScheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure) : Scheduler(numberOfModelStates, memoryStructure) { + } + + template + PreScheduler::PreScheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure) : Scheduler(numberOfModelStates, std::move(memoryStructure)) { + } + + template + void PreScheduler::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(s)"; + 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 PreScheduler; +#ifdef STORM_HAVE_CARL + template class PreScheduler; +#endif + } +} diff --git a/src/storm/storage/PreScheduler.h b/src/storm/storage/PreScheduler.h new file mode 100644 index 000000000..8207456e1 --- /dev/null +++ b/src/storm/storage/PreScheduler.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 PreScheduler : 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. + */ + PreScheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure = boost::none); + PreScheduler(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; + }; + } +}