diff --git a/CMakeLists.txt b/CMakeLists.txt index 51a4b9004..1f6c9b578 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -90,6 +90,7 @@ if ("${Z3_ROOT}" STREQUAL "") set(ENABLE_Z3 OFF) else() set(ENABLE_Z3 ON) + set(Z3_LIB_NAME "z3") endif() message(STATUS "StoRM - CMAKE_BUILD_TYPE: ${CMAKE_BUILD_TYPE}") @@ -132,6 +133,10 @@ elseif(MSVC) # Windows.h breaks GMM in gmm_except.h because of its macro definition for min and max add_definitions(/DNOMINMAX) + if(ENABLE_Z3) + set(Z3_LIB_NAME "libz3") + endif() + # MSVC does not do strict-aliasing, so no option needed else(CLANG) message(STATUS "StoRM - Using Compiler Configuration: Clang (LLVM)") @@ -362,9 +367,9 @@ endif(ENABLE_GUROBI) if (ENABLE_Z3) message (STATUS "StoRM - Linking with Z3") include_directories("${Z3_ROOT}/include") - target_link_libraries(storm "z3") - target_link_libraries(storm-functional-tests "z3") - target_link_libraries(storm-performance-tests "z3") + target_link_libraries(storm ${Z3_LIB_NAME}) + target_link_libraries(storm-functional-tests ${Z3_LIB_NAME}) + target_link_libraries(storm-performance-tests ${Z3_LIB_NAME}) endif(ENABLE_Z3) ############################################################# diff --git a/examples/mdp/tiny/tiny.pctl b/examples/mdp/tiny/tiny.pctl new file mode 100644 index 000000000..393670a26 --- /dev/null +++ b/examples/mdp/tiny/tiny.pctl @@ -0,0 +1,2 @@ +Pmin=? [ F a ] +Pmax=? [ F a ] \ No newline at end of file diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 5f0d10a75..8e9e23503 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -1268,14 +1268,14 @@ 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."; } // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); - std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false, nullptr); + std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; for (auto state : labeledMdp.getInitialStates()) { maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); } diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 6ab3e5bc0..e3fa9e394 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1447,14 +1447,14 @@ 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."; } // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); - std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false, nullptr); + std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; for (auto state : labeledMdp.getInitialStates()) { maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); } @@ -1517,7 +1517,7 @@ namespace storm { storm::models::Mdp subMdp = labeledMdp.restrictChoiceLabels(commandSet); storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(subMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); LOG4CPLUS_DEBUG(logger, "Invoking model checker."); - std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false, nullptr); + std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; LOG4CPLUS_DEBUG(logger, "Computed model checking results."); totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock; diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.cpp b/src/ir/expressions/BinaryNumericalFunctionExpression.cpp index 452fb278a..a80e04ae4 100644 --- a/src/ir/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/ir/expressions/BinaryNumericalFunctionExpression.cpp @@ -6,6 +6,7 @@ */ #include +#include #include "BinaryNumericalFunctionExpression.h" diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 9f9683a06..69c2644b4 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -19,6 +19,7 @@ #include "src/utility/vector.h" #include "src/utility/graph.h" #include "src/settings/Settings.h" +#include "src/storage/TotalScheduler.h" namespace storm { namespace modelchecker { @@ -265,7 +266,7 @@ namespace storm { * checker. If the qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector checkUntil(const storm::property::prctl::Until& formula, bool qualitative) const { - return this->checkUntil(this->minimumOperatorStack.top(), formula.getLeft().check(*this), formula.getRight().check(*this), qualitative, nullptr); + return this->checkUntil(this->minimumOperatorStack.top(), formula.getLeft().check(*this), formula.getRight().check(*this), qualitative).first; } /*! @@ -284,7 +285,7 @@ namespace storm { * @return The probabilities for the satisfying phi until psi for each state of the model. If the * qualitative flag is set, exact probabilities might not be computed. */ - std::vector checkUntil(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, std::vector* scheduler) const { + std::pair, storm::storage::TotalScheduler> checkUntil(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const { // We need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. std::pair statesWithProbability01; @@ -347,12 +348,10 @@ namespace storm { storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::constGetZero()); storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::constGetOne()); - // If we were required to generate a scheduler, do so now. - if (scheduler != nullptr) { - this->computeTakenChoices(this->minimumOperatorStack.top(), false, result, *scheduler, this->getModel().getNondeterministicChoiceIndices()); - } + // Finally, compute a scheduler that achieves the extramal value. + storm::storage::TotalScheduler scheduler = this->computeExtremalScheduler(this->minimumOperatorStack.top(), false, result); - return result; + return std::make_pair(result, scheduler); } /*! @@ -443,7 +442,7 @@ namespace storm { * checker. If the qualitative flag is set, exact values might not be computed. */ virtual std::vector checkReachabilityReward(const storm::property::prctl::ReachabilityReward& formula, bool qualitative) const { - return this->checkReachabilityReward(this->minimumOperatorStack.top(), formula.getChild().check(*this), qualitative, nullptr); + return this->checkReachabilityReward(this->minimumOperatorStack.top(), formula.getChild().check(*this), qualitative).first; } /*! @@ -461,7 +460,7 @@ namespace storm { * @return The expected reward values gained before a target state is reached for each state. If the * qualitative flag is set, exact values might not be computed. */ - virtual std::vector checkReachabilityReward(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative, std::vector* scheduler) const { + virtual std::pair, storm::storage::TotalScheduler> checkReachabilityReward(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative) const { // Only compute the result if the model has at least one reward model. if (!(this->getModel().hasStateRewards() || this->getModel().hasTransitionRewards())) { LOG4CPLUS_ERROR(logger, "Missing reward model for formula."); @@ -548,12 +547,10 @@ namespace storm { storm::utility::vector::setVectorValues(result, targetStates, storm::utility::constGetZero()); storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constGetInfinity()); - // If we were required to generate a scheduler, do so now. - if (scheduler != nullptr) { - this->computeTakenChoices(this->minimumOperatorStack.top(), true, result, *scheduler, this->getModel().getNondeterministicChoiceIndices()); - } + // Finally, compute a scheduler that achieves the extramal value. + storm::storage::TotalScheduler scheduler = this->computeExtremalScheduler(this->minimumOperatorStack.top(), false, result); - return result; + return std::make_pair(result, scheduler); } protected: @@ -565,8 +562,8 @@ namespace storm { * @param takenChoices The output vector that is to store the taken choices. * @param nondeterministicChoiceIndices The assignment of states to their nondeterministic choices in the matrix. */ - void computeTakenChoices(bool minimize, bool addRewards, std::vector const& result, std::vector& takenChoices, std::vector const& nondeterministicChoiceIndices) const { - std::vector temporaryResult(nondeterministicChoiceIndices.size() - 1); + storm::storage::TotalScheduler computeExtremalScheduler(bool minimize, bool addRewards, std::vector const& result) const { + std::vector temporaryResult(this->getModel().getNondeterministicChoiceIndices().size() - 1); std::vector nondeterministicResult(result); storm::solver::GmmxxLinearEquationSolver solver; solver.performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), nondeterministicResult, nullptr, 1); @@ -585,11 +582,16 @@ namespace storm { } storm::utility::vector::addVectorsInPlace(nondeterministicResult, totalRewardVector); } + + std::vector choices(this->getModel().getNumberOfStates()); + if (minimize) { - storm::utility::vector::reduceVectorMin(nondeterministicResult, temporaryResult, nondeterministicChoiceIndices, &takenChoices); + storm::utility::vector::reduceVectorMin(nondeterministicResult, temporaryResult, this->getModel().getNondeterministicChoiceIndices(), &choices); } else { - storm::utility::vector::reduceVectorMax(nondeterministicResult, temporaryResult, nondeterministicChoiceIndices, &takenChoices); + storm::utility::vector::reduceVectorMax(nondeterministicResult, temporaryResult, this->getModel().getNondeterministicChoiceIndices(), &choices); } + + return storm::storage::TotalScheduler(choices); } /*! diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 8689802e3..84663dbc0 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/storage/StronglyConnectedComponentDecomposition.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,7 +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; + /*! * 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..850d54a92 --- /dev/null +++ b/src/storage/PartialScheduler.cpp @@ -0,0 +1,40 @@ +#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; + } + + return stateChoicePair->second; + } + + std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler) { + out << "partial scheduler (defined on " << scheduler.choices.size() << " states) [ "; + uint_fast64_t remainingEntries = scheduler.choices.size(); + for (auto stateChoicePair : scheduler.choices) { + out << stateChoicePair.first << " -> " << stateChoicePair.second; + --remainingEntries; + if (remainingEntries > 0) { + out << ", "; + } + } + out << "]"; + return out; + } + + } // 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..ca33165d2 --- /dev/null +++ b/src/storage/PartialScheduler.h @@ -0,0 +1,29 @@ +#ifndef STORM_STORAGE_PARTIALSCHEDULER_H_ +#define STORM_STORAGE_PARTIALSCHEDULER_H_ + +#include +#include + +#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; + + friend std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler); + + private: + // A mapping from all states that have defined choices to their respective choices. + std::unordered_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..d9363c8fb --- /dev/null +++ b/src/storage/Scheduler.h @@ -0,0 +1,39 @@ +#ifndef STORM_STORAGE_SCHEDULER_H_ +#define STORM_STORAGE_SCHEDULER_H_ + +#include + +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. + * 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). + */ + 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..41b75119c --- /dev/null +++ b/src/storage/TotalScheduler.cpp @@ -0,0 +1,37 @@ +#include "src/storage/TotalScheduler.h" + +namespace storm { + namespace storage { + TotalScheduler::TotalScheduler(uint_fast64_t numberOfStates) : choices(numberOfStates) { + // Intentionally left empty. + } + + TotalScheduler::TotalScheduler(std::vector const& choices) : choices(choices) { + // Intentionally left empty. + } + + void TotalScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) { + choices[state] = choice; + } + + bool TotalScheduler::isChoiceDefined(uint_fast64_t state) const { + return true; + } + + uint_fast64_t TotalScheduler::getChoice(uint_fast64_t state) const { + return choices[state]; + } + + std::ostream& operator<<(std::ostream& out, TotalScheduler const& scheduler) { + out << "total scheduler (defined on " << scheduler.choices.size() << " states) [ "; + for (uint_fast64_t state = 0; state < scheduler.choices.size() - 1; ++state) { + out << state << " -> " << scheduler.choices[state] << ", "; + } + if (scheduler.choices.size() > 0) { + out << (scheduler.choices.size() - 1) << " -> " << scheduler.choices[scheduler.choices.size() - 1] << " ]"; + } + return out; + } + + } +} \ No newline at end of file diff --git a/src/storage/TotalScheduler.h b/src/storage/TotalScheduler.h new file mode 100644 index 000000000..2e29471f7 --- /dev/null +++ b/src/storage/TotalScheduler.h @@ -0,0 +1,33 @@ +#ifndef STORM_STORAGE_TOTALSCHEDULER_H_ +#define STORM_STORAGE_TOTALSCHEDULER_H_ + +#include +#include + +#include "src/storage/Scheduler.h" + +namespace storm { + namespace storage { + + class TotalScheduler : public Scheduler { + public: + TotalScheduler(uint_fast64_t numberOfStates); + + TotalScheduler(std::vector const& choices); + + 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; + + friend std::ostream& operator<<(std::ostream& out, TotalScheduler const& scheduler); + + 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/storage/VectorSet.h b/src/storage/VectorSet.h index 1257bbec3..7ceaa466f 100644 --- a/src/storage/VectorSet.h +++ b/src/storage/VectorSet.h @@ -8,6 +8,7 @@ #ifndef STORM_STORAGE_VECTORSET_H #define STORM_STORAGE_VECTORSET_H +#include #include #include #include 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_ */