diff --git a/src/storm/storage/PostScheduler.cpp b/src/storm/storage/PostScheduler.cpp new file mode 100644 index 000000000..30c306abc --- /dev/null +++ b/src/storm/storage/PostScheduler.cpp @@ -0,0 +1,167 @@ +#include "storm/utility/vector.h" +#include "storm/storage/PostScheduler.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotImplementedException.h" +#include + +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"); + 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]); + } + numberOfChoices = 0; + for(std::vector::iterator it = numberOfChoicesPerState.begin(); it != numberOfChoicesPerState.end(); ++it) + numberOfChoices += *it; + this->numOfUndefinedChoices = numOfMemoryStates * numberOfChoices; + this->numOfDeterministicChoices = 0; + } + + template + PostScheduler::PostScheduler(uint_fast64_t numberOfModelStates, std::vector numberOfChoicesPerState, boost::optional&& memoryStructure) : Scheduler(numberOfModelStates, 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]); + } + numberOfChoices = 0; + for(std::vector::iterator it = numberOfChoicesPerState.begin(); it != numberOfChoicesPerState.end(); ++it) + numberOfChoices += *it; + this->numOfUndefinedChoices = numOfMemoryStates * numberOfChoices; + this->numOfDeterministicChoices = 0; + } + + template + void PostScheduler::setChoice(OldChoice const& oldChoice, SchedulerChoice const& newChoice, 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"); + + //auto& schedulerChoice = schedulerChoiceMapping[memoryState][modelState]; + //if (schedulerChoice.isDefined()) { + // if (!choice.isDefined()) { + // ++numOfUndefinedChoices; + // } + //} else { + // if (choice.isDefined()) { + // assert(numOfUndefinedChoices > 0); + // --numOfUndefinedChoices; + // } + //} + //if (schedulerChoice.isDeterministic()) { + // if (!choice.isDeterministic()) { + // assert(numOfDeterministicChoices > 0); + // --numOfDeterministicChoices; + // } + //} else { + // if (choice.isDeterministic()) { + // ++numOfDeterministicChoices; + // } + //} + 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]; + } + + + template + bool PostScheduler::isDeterministicScheduler() const { + return true; + } + + template + bool PostScheduler::isMemorylessScheduler() const { + return true; + } + + template + void PostScheduler::printToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { + + 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(schedulerChoiceMapping.front().size()).length(); + if (stateValuationsGiven) { + widthOfStates += model->getStateValuations().getStateInfo(schedulerChoiceMapping.front().size() - 1).length() + 5; + } + widthOfStates = std::max(widthOfStates, (uint_fast64_t)12); + 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) { + // Print the state info + if (stateValuationsGiven) { + out << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state)); + } else { + out << std::setw(widthOfStates) << state; + } + out << " "; + + bool firstChoiceIndex = true; + for(uint choiceIndex = 0; choiceIndex < schedulerChoiceMapping[0][state].size(); choiceIndex++) { + SchedulerChoice const& choice = schedulerChoiceMapping[0][state][choiceIndex]; + if(firstChoiceIndex) { + firstChoiceIndex = false; + out << std::to_string(choiceIndex) << ": "; + } else { + out << std::setw(widthOfStates + 5) << std::to_string(choiceIndex) << ": "; + } + if (choice.isDefined()) { + if (choice.isDeterministic()) { + if (choiceOriginsGiven) { + out << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); + } else { + out << choice.getDeterministicChoice(); + } + if (choiceLabelsGiven) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); + out << " {" << boost::join(choiceLabels, ", ") << "}"; + } + } else { + bool firstChoice = true; + for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { + if (firstChoice) { + firstChoice = false; + } else { + out << " + "; + } + out << choiceProbPair.second << ": ("; + if (choiceOriginsGiven) { + out << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); + } else { + out << choiceProbPair.first; + } + if (choiceLabelsGiven) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); + out << " {" << boost::join(choiceLabels, ", ") << "}"; + } + out << ")"; + } + } + } else { + out << "undefined."; + } + + // Todo: print memory updates + out << std::endl; + } + } + } + + template class PostScheduler; +#ifdef STORM_HAVE_CARL + template class PostScheduler; +#endif + } +} diff --git a/src/storm/storage/PostScheduler.h b/src/storm/storage/PostScheduler.h new file mode 100644 index 000000000..4a64ba756 --- /dev/null +++ b/src/storm/storage/PostScheduler.h @@ -0,0 +1,100 @@ +#pragma once + +#include +#include +#include "storm/storage/SchedulerChoice.h" +#include "storm/storage/Scheduler.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 PostScheduler : 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. + */ + PostScheduler(uint_fast64_t numberOfModelStates, std::vector numberOfChoicesPerState, boost::optional const& memoryStructure = boost::none); + PostScheduler(uint_fast64_t numberOfModelStates, std::vector numberOfChoicesPerState, boost::optional&& memoryStructure); + + /*! + * Sets the choice defined by the scheduler for the given state. + * + * @param choice The choice to set for the given state. + * @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); + + /*! + * Is the scheduler defined on the states indicated by the selected-states bitvector? + */ + bool isChoiceSelected(BitVector const& selectedStates, uint64_t memoryState = 0) const; + + /*! + * Clears the choice defined by the scheduler for the given state. + * + * @param modelState The state of the model for which to clear the choice. + * @param memoryState The state of the memoryStructure for which to clear the choice. + */ + 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 + */ + //storm::storage::BitVector computeActionSupport(std::vector const& nondeterministicChoiceIndicies) const; + + /*! + * Retrieves whether all defined choices are deterministic + */ + bool isDeterministicScheduler() const; + + /*! + * Retrieves whether the scheduler considers a trivial memory structure (i.e., a memory structure with just a single state) + */ + bool isMemorylessScheduler() const; + + /*! + * Retrieves the number of memory states this scheduler considers. + */ + //uint_fast64_t getNumberOfMemoryStates() const; + + /*! + * Retrieves the memory structure associated with this scheduler + */ + //boost::optional const& getMemoryStructure() const; + + /*! + * 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> model = nullptr, bool skipUniqueChoices = false) const; + private: + std::vector>>> schedulerChoiceMapping; + + std::vector numberOfChoicesPerState; + uint_fast64_t numberOfChoices; + }; + } +} diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index 492a7a2f3..43340133d 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -5,10 +5,9 @@ #include "storm/storage/SchedulerChoice.h" namespace storm { - - namespace storage { - + template + class PostScheduler; /* * 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). @@ -17,7 +16,8 @@ namespace storm { template class Scheduler { public: - + friend class PostScheduler; + /*! * Initializes a scheduler for the given number of model states. * @@ -26,7 +26,7 @@ namespace storm { */ Scheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure = boost::none); Scheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure); - + /*! * Sets the choice defined by the scheduler for the given state. * @@ -40,7 +40,7 @@ namespace storm { * Is the scheduler defined on the states indicated by the selected-states bitvector? */ bool isChoiceSelected(BitVector const& selectedStates, uint64_t memoryState = 0) const; - + /*! * Clears the choice defined by the scheduler for the given state. * @@ -48,7 +48,7 @@ namespace storm { * @param memoryState The state of the memoryStructure for which to clear the choice. */ 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. * @@ -66,22 +66,22 @@ namespace storm { * Retrieves whether there is a pair of model and memory state for which the choice is undefined. */ bool isPartialScheduler() const; - + /*! * Retrieves whether all defined choices are deterministic */ bool isDeterministicScheduler() const; - + /*! * Retrieves whether the scheduler considers a trivial memory structure (i.e., a memory structure with just a single state) */ bool isMemorylessScheduler() const; - + /*! * Retrieves the number of memory states this scheduler considers. */ uint_fast64_t getNumberOfMemoryStates() const; - + /*! * Retrieves the memory structure associated with this scheduler */ @@ -101,7 +101,7 @@ namespace storm { } return newScheduler; } - + /*! * Prints the scheduler to the given output stream. * @param out The output stream @@ -111,19 +111,19 @@ namespace storm { */ void printToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = 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; - + private: - + boost::optional memoryStructure; std::vector>> schedulerChoices; + protected: uint_fast64_t numOfUndefinedChoices; uint_fast64_t numOfDeterministicChoices; }; } } -