From 8c09a4d4418485244746a4c01fc06868128f5cac Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Mon, 20 Sep 2021 18:36:56 +0200 Subject: [PATCH] refactored safety shield choices and scheduler --- src/storm/shields/PostSafetyShield.cpp | 14 ++--- src/storm/shields/PreSafetyShield.cpp | 13 ++-- src/storm/storage/PostScheduler.cpp | 74 +++++++++-------------- src/storm/storage/PostScheduler.h | 22 +++---- src/storm/storage/PostSchedulerChoice.cpp | 63 +++++++++++++++++++ src/storm/storage/PostSchedulerChoice.h | 46 ++++++++++++++ src/storm/storage/PreScheduler.cpp | 43 ++++++++++--- src/storm/storage/PreScheduler.h | 28 ++++++--- src/storm/storage/PreSchedulerChoice.cpp | 56 +++++++++++++++++ src/storm/storage/PreSchedulerChoice.h | 42 +++++++++++++ 10 files changed, 312 insertions(+), 89 deletions(-) create mode 100644 src/storm/storage/PostSchedulerChoice.cpp create mode 100644 src/storm/storage/PostSchedulerChoice.h create mode 100644 src/storm/storage/PreSchedulerChoice.cpp create mode 100644 src/storm/storage/PreSchedulerChoice.h diff --git a/src/storm/shields/PostSafetyShield.cpp b/src/storm/shields/PostSafetyShield.cpp index 9c639c010..311da2832 100644 --- a/src/storm/shields/PostSafetyShield.cpp +++ b/src/storm/shields/PostSafetyShield.cpp @@ -43,28 +43,28 @@ namespace tempest { ValueType maxProbability = *(choice_it + maxProbabilityIndex); if(!relative && !choiceFilter(maxProbability, maxProbability, this->shieldingExpression->getValue())) { STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); - shield.setChoice(0, storm::storage::Distribution(), state); + shield.setChoice(storm::storage::PostSchedulerChoice(), state, 0); choice_it += rowGroupSize; continue; } + storm::storage::PostSchedulerChoice choiceMapping; for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { - storm::storage::Distribution actionDistribution; if(choiceFilter(*choice_it, maxProbability, this->shieldingExpression->getValue())) { - actionDistribution.addProbability(choice, 1); + choiceMapping.addChoice(choice, choice); } else { - actionDistribution.addProbability(maxProbabilityIndex, 1); + choiceMapping.addChoice(choice, maxProbabilityIndex); } - shield.setChoice(choice, storm::storage::SchedulerChoice(actionDistribution), state); } + shield.setChoice(choiceMapping, state, 0); } else { - shield.setChoice(0, storm::storage::Distribution(), state); + shield.setChoice(storm::storage::PostSchedulerChoice(), state, 0); choice_it += rowGroupSize; } } return shield; } - // Explicitly instantiate appropriate + // Explicitly instantiate appropriate classes template class PostSafetyShield::index_type>; #ifdef STORM_HAVE_CARL template class PostSafetyShield::index_type>; diff --git a/src/storm/shields/PreSafetyShield.cpp b/src/storm/shields/PreSafetyShield.cpp index abbc50ae7..f4374b929 100644 --- a/src/storm/shields/PreSafetyShield.cpp +++ b/src/storm/shields/PreSafetyShield.cpp @@ -39,29 +39,30 @@ namespace tempest { for(uint state = 0; state < this->rowGroupIndices.size() - 1; state++) { uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state]; if(this->relevantStates.get(state)) { - storm::storage::Distribution actionDistribution; + storm::storage::PreSchedulerChoice enabledChoices; ValueType maxProbability = *std::max_element(choice_it, choice_it + rowGroupSize); if(!relative && !choiceFilter(maxProbability, maxProbability, this->shieldingExpression->getValue())) { STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); - shield.setChoice(storm::storage::Distribution(), state); + shield.setChoice(storm::storage::PreSchedulerChoice(), state, 0); choice_it += rowGroupSize; continue; } for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { if(choiceFilter(*choice_it, maxProbability, this->shieldingExpression->getValue())) { - actionDistribution.addProbability(choice, *choice_it); + enabledChoices.addChoice(choice, *choice_it); } } - shield.setChoice(storm::storage::SchedulerChoice(actionDistribution), state); + shield.setChoice(enabledChoices, state, 0); } else { - shield.setChoice(storm::storage::Distribution(), state); + shield.setChoice(storm::storage::PreSchedulerChoice(), state, 0); choice_it += rowGroupSize; } + } return shield; } - // Explicitly instantiate appropriate + // Explicitly instantiate appropriate classes template class PreSafetyShield::index_type>; #ifdef STORM_HAVE_CARL template class PreSafetyShield::index_type>; diff --git a/src/storm/storage/PostScheduler.cpp b/src/storm/storage/PostScheduler.cpp index 92a81b434..11d0a7aed 100644 --- a/src/storm/storage/PostScheduler.cpp +++ b/src/storm/storage/PostScheduler.cpp @@ -9,14 +9,10 @@ namespace storm { namespace storage { template - PostScheduler::PostScheduler(uint_fast64_t numberOfModelStates, std::vector numberOfChoicesPerState, boost::optional const& memoryStructure) : Scheduler(numberOfModelStates, memoryStructure) { - STORM_LOG_DEBUG(numberOfChoicesPerState.size() << " " << numberOfModelStates); - STORM_LOG_ASSERT(numberOfChoicesPerState.size() == numberOfModelStates, "Need to know amount of choices per model state"); + PostScheduler::PostScheduler(uint_fast64_t numberOfModelStates, std::vector numberOfChoicesPerState, boost::optional const& memoryStructure) : memoryStructure(memoryStructure) { + //STORM_LOG_ASSERT(numberOfChoicesPerState.size() == numberOfModelStates, "Need to know amount of choices per model state"); uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1; - schedulerChoiceMapping = std::vector>>>(numOfMemoryStates, std::vector>>(numberOfModelStates)); - for(uint state = 0; state < numberOfModelStates; state++) { - schedulerChoiceMapping[0][state].resize(numberOfChoicesPerState[state]); - } + schedulerChoiceMapping = std::vector>>(numOfMemoryStates, std::vector>(numberOfModelStates)); numberOfChoices = 0; for(std::vector::iterator it = numberOfChoicesPerState.begin(); it != numberOfChoicesPerState.end(); ++it) numberOfChoices += *it; @@ -25,13 +21,10 @@ namespace storm { } template - PostScheduler::PostScheduler(uint_fast64_t numberOfModelStates, std::vector numberOfChoicesPerState, boost::optional&& memoryStructure) : Scheduler(numberOfModelStates, std::move(memoryStructure)) { + PostScheduler::PostScheduler(uint_fast64_t numberOfModelStates, std::vector numberOfChoicesPerState, boost::optional&& memoryStructure) : memoryStructure(std::move(memoryStructure)) { STORM_LOG_ASSERT(numberOfChoicesPerState.size() == numberOfModelStates, "Need to know amount of choices per model state"); uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1; - schedulerChoiceMapping = std::vector>>>(numOfMemoryStates, std::vector>>(numberOfModelStates)); - for(uint state = 0; state < numberOfModelStates; state++) { - schedulerChoiceMapping[0][state].resize(numberOfChoicesPerState[state]); - } + schedulerChoiceMapping = std::vector>>(numOfMemoryStates, std::vector>(numberOfModelStates)); numberOfChoices = 0; for(std::vector::iterator it = numberOfChoicesPerState.begin(); it != numberOfChoicesPerState.end(); ++it) numberOfChoices += *it; @@ -40,21 +33,13 @@ namespace storm { } template - void PostScheduler::setChoice(OldChoice const& oldChoice, SchedulerChoice const& newChoice, uint_fast64_t modelState, uint_fast64_t memoryState) { + void PostScheduler::setChoice(PostSchedulerChoice const& choice, uint_fast64_t modelState, uint_fast64_t memoryState) { STORM_LOG_ASSERT(memoryState == 0, "Currently we do not support PostScheduler with memory"); STORM_LOG_ASSERT(modelState < schedulerChoiceMapping[memoryState].size(), "Illegal model state index"); - schedulerChoiceMapping[memoryState][modelState][oldChoice] = newChoice; - } - - template - SchedulerChoice const& PostScheduler::getChoice(uint_fast64_t modelState, OldChoice oldChoice, uint_fast64_t memoryState) { - STORM_LOG_ASSERT(memoryState < this->getNumberOfMemoryStates(), "Illegal memory state index"); - STORM_LOG_ASSERT(modelState < schedulerChoiceMapping[memoryState].size(), "Illegal model state index"); - return schedulerChoiceMapping[memoryState][modelState][oldChoice]; + schedulerChoiceMapping[memoryState][modelState] = choice; } - template bool PostScheduler::isDeterministicScheduler() const { return true; @@ -89,7 +74,11 @@ namespace storm { out << ":" << std::endl; uint_fast64_t numOfSkippedStatesWithUniqueChoice = 0; for (uint_fast64_t state = 0; state < schedulerChoiceMapping.front().size(); ++state) { + PostSchedulerChoice const& choices = schedulerChoiceMapping[0][state]; + if(choices.isEmpty() && !printUndefinedChoices) continue; + std::stringstream stateString; + // Print the state info if (stateValuationsGiven) { stateString << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state)); @@ -98,42 +87,37 @@ namespace storm { } stateString << " "; + bool firstChoiceIndex = true; - for(uint choiceIndex = 0; choiceIndex < schedulerChoiceMapping[0][state].size(); choiceIndex++) { - SchedulerChoice const& choice = schedulerChoiceMapping[0][state][choiceIndex]; + for(auto const& choiceMap : choices.getChoiceMap()) { if(firstChoiceIndex) { firstChoiceIndex = false; } else { stateString << "; "; } - if (choice.isDefined()) { - 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 { - stateString << choiceProbPair.first; - } - if (choiceLabelsGiven) { - auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); - stateString << " {" << boost::join(choiceLabels, ", ") << "}"; - } + if(choiceLabelsGiven) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + std::get<0>(choiceMap)); + stateString << std::to_string(std::get<0>(choiceMap)) << " {" << boost::join(choiceLabels, ", ") << "}: "; + } else { + stateString << std::to_string(std::get<0>(choiceMap)) << ": "; + } + + if (choiceOriginsGiven) { + stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + std::get<1>(choiceMap)); } else { - if(!this->printUndefinedChoices) goto skipStatesWithUndefinedChoices; - stateString << "undefined."; + stateString << std::to_string(std::get<1>(choiceMap)); } + if (choiceLabelsGiven) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + std::get<1>(choiceMap)); + stateString << " {" << boost::join(choiceLabels, ", ") << "}"; + } + // Todo: print memory updates } out << stateString.str() << std::endl; // jump to label if we find one undefined choice. - skipStatesWithUndefinedChoices:; + //skipStatesWithUndefinedChoices:; } out << "___________________________________________________________________" << std::endl; } diff --git a/src/storm/storage/PostScheduler.h b/src/storm/storage/PostScheduler.h index 57c194fa6..99fc3c1b8 100644 --- a/src/storm/storage/PostScheduler.h +++ b/src/storm/storage/PostScheduler.h @@ -2,7 +2,7 @@ #include #include -#include "storm/storage/SchedulerChoice.h" +#include "storm/storage/PostSchedulerChoice.h" #include "storm/storage/Scheduler.h" #include "storm/logic/ShieldExpression.h" @@ -16,7 +16,7 @@ namespace storm { * A Choice can be undefined, deterministic */ template - class PostScheduler : public Scheduler { + class PostScheduler { public: typedef uint_fast64_t OldChoice; /*! @@ -35,7 +35,7 @@ namespace storm { * @param modelState The state of the model for which to set the choice. * @param memoryState The state of the memoryStructure for which to set the choice. */ - void setChoice(OldChoice const& oldChoice, SchedulerChoice const& newChoice, uint_fast64_t modelState, uint_fast64_t memoryState = 0); + void setChoice(PostSchedulerChoice const& newChoice, uint_fast64_t modelState, uint_fast64_t memoryState = 0); /*! * Is the scheduler defined on the states indicated by the selected-states bitvector? @@ -50,14 +50,6 @@ namespace storm { */ void clearChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0); - /*! - * Gets the choice defined by the scheduler for the given model and memory state. - * - * @param state The state for which to get the choice. - * @param memoryState the memory state which we consider. - */ - SchedulerChoice const& getChoice(uint_fast64_t modelState, OldChoice oldChoice, uint_fast64_t memoryState = 0) ; - /*! * Compute the Action Support: A bit vector that indicates all actions that are selected with positive probability in some memory state */ @@ -92,8 +84,14 @@ namespace storm { */ void printToStream(std::ostream& out, std::shared_ptr shieldingExpression, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; private: - std::vector>>> schedulerChoiceMapping; + boost::optional memoryStructure; + std::vector>> schedulerChoiceMapping; + + bool printUndefinedChoices = false; + uint_fast64_t numOfUndefinedChoices; + uint_fast64_t numOfDeterministicChoices; + uint_fast64_t numOfDontCareStates; std::vector numberOfChoicesPerState; uint_fast64_t numberOfChoices; }; diff --git a/src/storm/storage/PostSchedulerChoice.cpp b/src/storm/storage/PostSchedulerChoice.cpp new file mode 100644 index 000000000..ca714a6a4 --- /dev/null +++ b/src/storm/storage/PostSchedulerChoice.cpp @@ -0,0 +1,63 @@ +#include "storm/storage/PostSchedulerChoice.h" + +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidOperationException.h" +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" + +namespace storm { + namespace storage { + + template + PostSchedulerChoice::PostSchedulerChoice() { + // Intentionally left empty + } + + template + void PostSchedulerChoice::addChoice(uint_fast64_t oldChoiceIndex, uint_fast64_t newChoiceIndex) { + choiceMap.emplace_back(oldChoiceIndex, newChoiceIndex); + } + + template + std::vector> const& PostSchedulerChoice::getChoiceMap() const { + return choiceMap; + } + + template + std::tuple const& PostSchedulerChoice::getChoice(uint_fast64_t choiceIndex) const { + return choiceMap.at(choiceIndex); + } + + template + bool PostSchedulerChoice::isEmpty() const { + return choiceMap.size() == 0; + } + + template + std::ostream& operator<<(std::ostream& out, PostSchedulerChoice const& schedulerChoice) { + if (!schedulerChoice.isEmpty()) { + bool firstChoice = true; + for(auto const& choice : schedulerChoice.getChoiceMap()) { + if(firstChoice) firstChoice = false; + else out << ", "; + out << std::get<0>(choice) << " -> " << std::get<1>(choice); + } + } else { + out << "undefined"; + } + return out; + } + + template class PostSchedulerChoice; + template std::ostream& operator<<(std::ostream& out, PostSchedulerChoice const& schedulerChoice); + template class PostSchedulerChoice; + template std::ostream& operator<<(std::ostream& out, PostSchedulerChoice const& schedulerChoice); + template class PostSchedulerChoice; + template std::ostream& operator<<(std::ostream& out, PostSchedulerChoice const& schedulerChoice); + template class PostSchedulerChoice; + template std::ostream& operator<<(std::ostream& out, PostSchedulerChoice const& schedulerChoice); + + } +} diff --git a/src/storm/storage/PostSchedulerChoice.h b/src/storm/storage/PostSchedulerChoice.h new file mode 100644 index 000000000..29deb3ddb --- /dev/null +++ b/src/storm/storage/PostSchedulerChoice.h @@ -0,0 +1,46 @@ +#pragma once + +#include "storm/utility/constants.h" + +namespace storm { + namespace storage { + + template + class PostSchedulerChoice { + + public: + + /*! + * Creates an undefined scheduler choice + */ + PostSchedulerChoice(); + + /* + * + */ + void addChoice(uint_fast64_t oldChoiceIndex, uint_fast64_t newChoiceIndex); + + /* + * + */ + bool isEmpty() const; + + /* + * + */ + std::vector> const& getChoiceMap() const; + + /* + * + */ + std::tuple const& getChoice(uint_fast64_t choiceIndex) const; + + private: + //std::vector>> choiceMap; + std::vector> choiceMap; + }; + + template + std::ostream& operator<<(std::ostream& out, PostSchedulerChoice const& schedulerChoice); + } +} diff --git a/src/storm/storage/PreScheduler.cpp b/src/storm/storage/PreScheduler.cpp index 0f1cf775d..bb09a81f1 100644 --- a/src/storm/storage/PreScheduler.cpp +++ b/src/storm/storage/PreScheduler.cpp @@ -8,11 +8,36 @@ namespace storm { namespace storage { template - PreScheduler::PreScheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure) : Scheduler(numberOfModelStates, memoryStructure) { + PreScheduler::PreScheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure) : memoryStructure(memoryStructure) { + uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1; + schedulerChoices = std::vector>>(numOfMemoryStates, std::vector>(numberOfModelStates)); + //dontCareStates = std::vector(numOfMemoryStates, storm::storage::BitVector(numberOfModelStates, false)); + numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates; + numOfDeterministicChoices = 0; + numOfDontCareStates = 0; } template - PreScheduler::PreScheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure) : Scheduler(numberOfModelStates, std::move(memoryStructure)) { + PreScheduler::PreScheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure) : memoryStructure(std::move(memoryStructure)) { + } + + template + bool PreScheduler::isMemorylessScheduler() const { + return getNumberOfMemoryStates() == 1; + } + + template + uint_fast64_t PreScheduler::getNumberOfMemoryStates() const { + return memoryStructure ? memoryStructure->getNumberOfStates() : 1; + } + + template + void PreScheduler::setChoice(PreSchedulerChoice const& choice, uint_fast64_t modelState, uint_fast64_t memoryState) { + STORM_LOG_ASSERT(memoryState < this->getNumberOfMemoryStates(), "Illegal memory state index"); + STORM_LOG_ASSERT(modelState < this->schedulerChoices[memoryState].size(), "Illegal model state index"); + + auto& schedulerChoice = schedulerChoices[memoryState][modelState]; + schedulerChoice = choice; } template @@ -67,23 +92,23 @@ namespace storm { } // Print choice info - SchedulerChoice const& choice = this->schedulerChoices[memoryState][state]; - if (choice.isDefined()) { + PreSchedulerChoice const& choices = this->schedulerChoices[memoryState][state]; + if (!choices.isEmpty()) { bool firstChoice = true; - for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { + for (auto const& choiceProbPair : choices.getChoiceMap()) { if (firstChoice) { firstChoice = false; } else { stateString << "; "; } - stateString << choiceProbPair.second << ": ("; + stateString << std::get<0>(choiceProbPair) << ": ("; if (choiceOriginsGiven) { - stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); + stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + std::get<1>(choiceProbPair)); } else { - stateString << choiceProbPair.first; + stateString << std::get<1>(choiceProbPair); } if (choiceLabelsGiven) { - auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + std::get<1>(choiceProbPair)); stateString << " {" << boost::join(choiceLabels, ", ") << "}"; } stateString << ")"; diff --git a/src/storm/storage/PreScheduler.h b/src/storm/storage/PreScheduler.h index 8207456e1..5cfa2e8cb 100644 --- a/src/storm/storage/PreScheduler.h +++ b/src/storm/storage/PreScheduler.h @@ -3,7 +3,7 @@ #include #include #include -#include "storm/storage/SchedulerChoice.h" +#include "storm/storage/PreSchedulerChoice.h" #include "storm/storage/Scheduler.h" #include "storm/logic/ShieldExpression.h" @@ -12,14 +12,11 @@ namespace storm { /* * 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 { + class PreScheduler { public: - typedef uint_fast64_t OldChoice; + /*! * Initializes a scheduler for the given number of model states. * @@ -29,14 +26,25 @@ namespace storm { PreScheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure = boost::none); PreScheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure); + bool isMemorylessScheduler() const; + uint_fast64_t getNumberOfMemoryStates() const; + + void setChoice(PreSchedulerChoice const& choice, uint_fast64_t modelState, uint_fast64_t memoryState); + /*! * 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; + + private: + boost::optional memoryStructure; + std::vector>> schedulerChoices; + + bool printUndefinedChoices = false; + + uint_fast64_t numOfUndefinedChoices; + uint_fast64_t numOfDeterministicChoices; + uint_fast64_t numOfDontCareStates; }; } } diff --git a/src/storm/storage/PreSchedulerChoice.cpp b/src/storm/storage/PreSchedulerChoice.cpp new file mode 100644 index 000000000..e9fda23ac --- /dev/null +++ b/src/storm/storage/PreSchedulerChoice.cpp @@ -0,0 +1,56 @@ +#include "storm/storage/PreSchedulerChoice.h" + +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidOperationException.h" +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" + +namespace storm { + namespace storage { + + template + PreSchedulerChoice::PreSchedulerChoice() { + // Intentionally left empty + } + + template + void PreSchedulerChoice::addChoice(uint_fast64_t choiceIndex, ValueType probToSatisfy) { + choiceMap.emplace_back(probToSatisfy, choiceIndex); + } + + template + std::vector> const& PreSchedulerChoice::getChoiceMap() const { + return choiceMap; + } + + template + bool PreSchedulerChoice::isEmpty() const { + return choiceMap.size() == 0; + } + + template + std::ostream& operator<<(std::ostream& out, PreSchedulerChoice const& schedulerChoice) { + out << schedulerChoice.getChoiceMap().size(); + if (!schedulerChoice.isEmpty()) { + for(auto const& choice : schedulerChoice.getChoiceMap()) { + out << std::get<0>(choice) << ": " << std::get<1>(choice); + } + } else { + out << "undefined"; + } + return out; + } + + template class PreSchedulerChoice; + template std::ostream& operator<<(std::ostream& out, PreSchedulerChoice const& schedulerChoice); + template class PreSchedulerChoice; + template std::ostream& operator<<(std::ostream& out, PreSchedulerChoice const& schedulerChoice); + template class PreSchedulerChoice; + template std::ostream& operator<<(std::ostream& out, PreSchedulerChoice const& schedulerChoice); + template class PreSchedulerChoice; + template std::ostream& operator<<(std::ostream& out, PreSchedulerChoice const& schedulerChoice); + + } +} diff --git a/src/storm/storage/PreSchedulerChoice.h b/src/storm/storage/PreSchedulerChoice.h new file mode 100644 index 000000000..3e4074e84 --- /dev/null +++ b/src/storm/storage/PreSchedulerChoice.h @@ -0,0 +1,42 @@ +#pragma once + +#include "storm/utility/constants.h" + +namespace storm { + namespace storage { + + template + class PreSchedulerChoice { + + public: + + /*! + * Creates an undefined scheduler choice + */ + PreSchedulerChoice(); + + /* + * + */ + void addChoice(uint_fast64_t choiceIndex, ValueType probToSatisfy); + + /* + * + */ + bool isEmpty() const; + + /* + * + */ + std::vector> const& getChoiceMap() const; + + private: + // For now we only consider shields with deterministic choices. + //std::map> choiceMap; + std::vector> choiceMap; + }; + + template + std::ostream& operator<<(std::ostream& out, PreSchedulerChoice const& schedulerChoice); + } +}