diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 5f0d10a75..78911ef29 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -1268,7 +1268,7 @@ namespace storm { static storm::storage::VectorSet getMinimalLabelSet(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) { #ifdef STORM_HAVE_GUROBI // (0) Check whether the MDP is indeed labeled. - if (!labeledMdp.hasChoiceLabels()) { + if (!labeledMdp.hasChoiceLabeling()) { throw storm::exceptions::InvalidArgumentException() << "Minimal label set generation is impossible for unlabeled model."; } diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 6ab3e5bc0..1d7a3a90f 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1447,7 +1447,7 @@ namespace storm { storm::utility::ir::defineUndefinedConstants(program, constantDefinitionString); // (0) Check whether the MDP is indeed labeled. - if (!labeledMdp.hasChoiceLabels()) { + if (!labeledMdp.hasChoiceLabeling()) { throw storm::exceptions::InvalidArgumentException() << "Minimal command set generation is impossible for unlabeled model."; } diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 6516884a8..375d6a957 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -9,6 +9,7 @@ #include "src/models/AtomicPropositionsLabeling.h" #include "src/storage/BitVector.h" #include "src/storage/SparseMatrix.h" +#include "src/storage/Scheduler.h" #include "src/storage/VectorSet.h" #include "src/utility/Hash.h" @@ -403,7 +404,7 @@ class AbstractModel: public std::enable_shared_from_this> { * Retrieves whether this model has a labeling for the choices. * @return True if this model has a labeling. */ - bool hasChoiceLabels() const { + bool hasChoiceLabeling() const { return choiceLabeling; } @@ -459,6 +460,15 @@ class AbstractModel: public std::enable_shared_from_this> { * @return void */ virtual void setStateIdBasedChoiceLabeling() = 0; + + /* + * Applies the given scheduler to the model. + * + * @param scheduler The scheduler to apply. + * @return The model resulting from applying the scheduler to the model. + */ + virtual std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler) const = 0; + protected: /*! * Exports the model to the dot-format and prints the result to the given stream. diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index d45e2a51a..21de66e12 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -1,10 +1,11 @@ #ifndef STORM_MODELS_ABSTRACTNONDETERMINISTICMODEL_H_ #define STORM_MODELS_ABSTRACTNONDETERMINISTICMODEL_H_ -#include "AbstractModel.h" - #include +#include "AbstractModel.h" +#include "src/storage/Scheduler.h" + namespace storm { namespace models { @@ -235,7 +236,7 @@ namespace storm { this->choiceLabeling.reset(newChoiceLabeling); } - + private: /*! A vector of indices mapping states to the choices (rows) in the transition matrix. */ std::vector nondeterministicChoiceIndices; diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h index 2385ce2cf..60250d461 100644 --- a/src/models/Ctmc.h +++ b/src/models/Ctmc.h @@ -86,6 +86,17 @@ public: virtual std::size_t getHash() const override { return AbstractDeterministicModel::getHash(); } + + virtual std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler) const override { + std::vector nondeterministicChoiceIndices(this->getNumberOfStates() + 1); + for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { + nondeterministicChoiceIndices[state] = state; + } + nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates(); + storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), nondeterministicChoiceIndices, scheduler); + + return std::shared_ptr>(new Ctmc(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); +} }; } // namespace models diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h index b8d3145e2..ccf465361 100644 --- a/src/models/Ctmdp.h +++ b/src/models/Ctmdp.h @@ -115,6 +115,18 @@ public: return AbstractNondeterministicModel::getHash(); } + virtual std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler) const override { + storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), this->getNondeterministicChoiceIndices(), scheduler); + + // Construct the new nondeterministic choice indices for the resulting matrix. + std::vector nondeterministicChoiceIndices(this->getNumberOfStates() + 1); + for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { + nondeterministicChoiceIndices[state] = state; + } + nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates(); + return std::shared_ptr>(new Ctmdp(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); + } + private: /*! diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index c21d06d2f..b573f848d 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -19,6 +19,7 @@ #include "src/exceptions/InvalidArgumentException.h" #include "src/settings/Settings.h" #include "src/utility/vector.h" +#include "src/utility/matrix.h" namespace storm { @@ -276,7 +277,7 @@ public: } boost::optional>> newChoiceLabels; - if(this->hasChoiceLabels()) { + if(this->hasChoiceLabeling()) { // Get the choice label sets and move the needed values to the front. std::vector> newChoice(this->getChoiceLabeling()); @@ -299,6 +300,17 @@ public: } + virtual std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler) const override { + std::vector nondeterministicChoiceIndices(this->getNumberOfStates() + 1); + for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { + nondeterministicChoiceIndices[state] = state; + } + nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates(); + storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), nondeterministicChoiceIndices, scheduler); + + return std::shared_ptr>(new Dtmc(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); + } + private: /*! * @brief Perform some sanity checks. diff --git a/src/models/Mdp.h b/src/models/Mdp.h index 5507ddfb2..6af4b3ffd 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -18,6 +18,7 @@ #include "src/settings/Settings.h" #include "src/models/AbstractNondeterministicModel.h" #include "src/utility/set.h" +#include "src/utility/matrix.h" namespace storm { @@ -136,7 +137,7 @@ public: */ Mdp restrictChoiceLabels(storm::storage::VectorSet const& enabledChoiceLabels) const { // Only perform this operation if the given model has choice labels. - if (!this->hasChoiceLabels()) { + if (!this->hasChoiceLabeling()) { throw storm::exceptions::InvalidArgumentException() << "Restriction to label set is impossible for unlabeled model."; } @@ -192,6 +193,18 @@ public: return AbstractNondeterministicModel::getHash(); } + virtual std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler) const override { + storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), this->getNondeterministicChoiceIndices(), scheduler); + + // Construct the new nondeterministic choice indices for the resulting matrix. + std::vector nondeterministicChoiceIndices(this->getNumberOfStates() + 1); + for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { + nondeterministicChoiceIndices[state] = state; + } + nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates(); + return std::shared_ptr>(new Mdp(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); + } + private: /*! diff --git a/src/storage/PartialScheduler.cpp b/src/storage/PartialScheduler.cpp new file mode 100644 index 000000000..e6804cea3 --- /dev/null +++ b/src/storage/PartialScheduler.cpp @@ -0,0 +1,24 @@ +#include "src/storage/PartialScheduler.h" +#include "src/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace storage { + + void PartialScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) { + choices[state] = choice; + } + + bool PartialScheduler::isChoiceDefined(uint_fast64_t state) const { + return choices.find(state) != choices.end(); + } + + uint_fast64_t PartialScheduler::getChoice(uint_fast64_t state) const { + auto stateChoicePair = choices.find(state); + + if (stateChoicePair == choices.end()) { + throw storm::exceptions::InvalidArgumentException() << "Scheduler does not define a choice for state " << state; + } + } + + } // namespace storage +} // namespace storm \ No newline at end of file diff --git a/src/storage/PartialScheduler.h b/src/storage/PartialScheduler.h new file mode 100644 index 000000000..41ca228e4 --- /dev/null +++ b/src/storage/PartialScheduler.h @@ -0,0 +1,24 @@ +#ifndef STORM_STORAGE_PARTIALSCHEDULER_H_ +#define STORM_STORAGE_PARTIALSCHEDULER_H_ + +#include "src/storage/Scheduler.h" + +namespace storm { + namespace storage { + + class PartialScheduler : public Scheduler { + public: + void setChoice(uint_fast64_t state, uint_fast64_t choice) override; + + bool isChoiceDefined(uint_fast64_t state) const override; + + uint_fast64_t getChoice(uint_fast64_t state) const override; + + private: + // A mapping from all states that have defined choices to their respective choices. + std::unsorted_map choices; + }; + } +} + +#endif /* STORM_STORAGE_PARTIALSCHEDULER_H_ */ diff --git a/src/storage/Scheduler.h b/src/storage/Scheduler.h new file mode 100644 index 000000000..9f31a2a48 --- /dev/null +++ b/src/storage/Scheduler.h @@ -0,0 +1,36 @@ +#ifndef STORM_STORAGE_SCHEDULER_H_ +#define STORM_STORAGE_SCHEDULER_H_ + +namespace storm { + namespace storage { + + /* + * This class is the abstract base class of all scheduler classes. Scheduler classes define which action is chosen in a particular state of a non-deterministic model. + */ + class Scheduler { + public: + /* + * Sets the choice defined by the scheduler for the given state. + * + * @param state The state for which to set the choice. + * @param choice The choice to set for the given state. + */ + virtual void setChoice(uint_fast64_t state, uint_fast64_t choice) = 0; + + /* + * Retrieves whether this scheduler defines a choice for the given state. + * + * @param state The state for which to check whether the scheduler defines a choice. + * @return True if the scheduler defines a choice for the given state. + */ + virtual bool isChoiceDefined(uint_fast64_t state) const = 0; + + /*! + * Retrieves the choice for the given state under the assumption that the scheduler defines a proper choice for the state. + */ + virtual uint_fast64_t getChoice(uint_fast64_t state) const = 0; + }; + } +} + +#endif /* STORM_STORAGE_SCHEDULER_H_ */ diff --git a/src/storage/TotalScheduler.cpp b/src/storage/TotalScheduler.cpp new file mode 100644 index 000000000..e240fd24c --- /dev/null +++ b/src/storage/TotalScheduler.cpp @@ -0,0 +1,21 @@ +#include "src/storage/TotalScheduler.h" + +namespace storm { + namespace storage { + TotalScheduler::TotalScheduler(uint_fast64_t numberOfStates) : choices(numberOfStates) { + // Intentionally left empty. + } + + void setChoice(uint_fast64_t state, uint_fast64_t choice) override { + choices[state] = choice; + } + + bool isChoiceDefined(uint_fast64_t state) const override { + return true; + } + + uint_fast64_t getChoice(uint_fast64_t state) const override { + return choices[state]; + } + } +} \ No newline at end of file diff --git a/src/storage/TotalScheduler.h b/src/storage/TotalScheduler.h new file mode 100644 index 000000000..1679766ad --- /dev/null +++ b/src/storage/TotalScheduler.h @@ -0,0 +1,26 @@ +#ifndef STORM_STORAGE_TOTALSCHEDULER_H_ +#define STORM_STORAGE_TOTALSCHEDULER_H_ + +#include "src/storage/Scheduler.h" + +namespace storm { + namespace storage { + + class TotalScheduler : public Scheduler { + public: + TotalScheduler(uint_fast64_t numberOfStates); + + void setChoice(uint_fast64_t state, uint_fast64_t choice) override; + + bool isChoiceDefined(uint_fast64_t state) const override; + + uint_fast64_t getChoice(uint_fast64_t state) const override; + + private: + // A vector that stores the choice for each state. + std::vector choices; + }; + } // namespace storage +} // namespace storm + +#endif /* STORM_STORAGE_TOTALSCHEDULER_H_ */ diff --git a/src/utility/matrix.h b/src/utility/matrix.h new file mode 100644 index 000000000..897db4374 --- /dev/null +++ b/src/utility/matrix.h @@ -0,0 +1,52 @@ +#ifndef STORM_UTILITY_MATRIX_H_ +#define STORM_UTILITY_MATRIX_H_ + +#include "src/storage/SparseMatrix.h" +#include "src/storage/Scheduler.h" +#include "src/exceptions/InvalidStateException.h" + +namespace storm { + namespace utility { + namespace matrix { + + /*! + * Applies the given scheduler to the given transition matrix. This means that all choices that are not taken by the scheduler are + * dropped from the transition matrix. If a state has no choice enabled, it is equipped with a self-loop instead. + * + * @param transitionMatrix The transition matrix of the original system. + * @param nondeterministicChoiceIndices A vector indicating at which rows the choices for the states begin. + * @param scheduler The scheduler to apply to the system. + * @return A transition matrix that corresponds to all transitions of the given system that are selected by the given scheduler. + */ + template + storm::storage::SparseMatrix applyScheduler(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::Scheduler const& scheduler) { + storm::storage::SparseMatrix result(nondeterministicChoiceIndices.size() - 1, transitionMatrix.getColumnCount()); + + for (uint_fast64_t state = 0; state < nondeterministicChoiceIndices.size() - 1; ++state) { + if (scheduler.isChoiceDefined(state)) { + // Check whether the choice is valid for this state. + uint_fast64_t choice = nondeterministicChoiceIndices[state] + scheduler.getChoice(state); + if (choice >= nondeterministicChoiceIndices[state + 1]) { + throw storm::exceptions::InvalidStateException() << "Scheduler defines illegal choice " << choice << " for state " << state << "."; + } + + // If a valid choice for this state is defined, we copy over the corresponding entries. + typename storm::storage::SparseMatrix::Rows selectedRow = transitionMatrix.getRow(choice); + for (auto entry : selectedRow) { + result.insertNextValue(state, entry.column(), entry.value()); + } + } else { + // If no valid choice for the state is defined, we insert a self-loop. + result.insertNextValue(state, state, storm::utility::constGetOne()); + } + } + + // Finalize the matrix creation and return result. + result.finalize(); + return result; + } + } + } +} + +#endif /* STORM_UTILITY_MATRIX_H_ */