From 360b506afe8ee186ab0f30fbddaf316bfc9d1bbc Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 17 Nov 2013 18:24:44 +0100 Subject: [PATCH] Sparse MDP model checker now correctly computes (memoryless) schedulers for Until and Reachability Reward formulas. Former-commit-id: c756093fd4f7de5fe448cfffca08e702a4bc2d50 --- examples/mdp/tiny/tiny.pctl | 2 + .../MILPMinimalLabelSetGenerator.h | 2 +- .../SMTMinimalCommandSetGenerator.h | 4 +- .../prctl/SparseMdpPrctlModelChecker.h | 38 ++++++++++--------- src/storage/PartialScheduler.cpp | 16 ++++++++ src/storage/PartialScheduler.h | 7 +++- src/storage/Scheduler.h | 2 + src/storage/TotalScheduler.cpp | 22 +++++++++-- src/storage/TotalScheduler.h | 7 ++++ 9 files changed, 75 insertions(+), 25 deletions(-) create mode 100644 examples/mdp/tiny/tiny.pctl 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 78911ef29..8e9e23503 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -1275,7 +1275,7 @@ namespace storm { // (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 1d7a3a90f..e3fa9e394 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1454,7 +1454,7 @@ namespace storm { // (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/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/storage/PartialScheduler.cpp b/src/storage/PartialScheduler.cpp index e6804cea3..850d54a92 100644 --- a/src/storage/PartialScheduler.cpp +++ b/src/storage/PartialScheduler.cpp @@ -18,6 +18,22 @@ namespace storm { 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 diff --git a/src/storage/PartialScheduler.h b/src/storage/PartialScheduler.h index 41ca228e4..ca33165d2 100644 --- a/src/storage/PartialScheduler.h +++ b/src/storage/PartialScheduler.h @@ -1,6 +1,9 @@ #ifndef STORM_STORAGE_PARTIALSCHEDULER_H_ #define STORM_STORAGE_PARTIALSCHEDULER_H_ +#include +#include + #include "src/storage/Scheduler.h" namespace storm { @@ -14,9 +17,11 @@ namespace storm { 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::unsorted_map choices; + std::unordered_map choices; }; } } diff --git a/src/storage/Scheduler.h b/src/storage/Scheduler.h index 9f31a2a48..9ea87bbdf 100644 --- a/src/storage/Scheduler.h +++ b/src/storage/Scheduler.h @@ -1,6 +1,8 @@ #ifndef STORM_STORAGE_SCHEDULER_H_ #define STORM_STORAGE_SCHEDULER_H_ +#include + namespace storm { namespace storage { diff --git a/src/storage/TotalScheduler.cpp b/src/storage/TotalScheduler.cpp index e240fd24c..41b75119c 100644 --- a/src/storage/TotalScheduler.cpp +++ b/src/storage/TotalScheduler.cpp @@ -6,16 +6,32 @@ namespace storm { // Intentionally left empty. } - void setChoice(uint_fast64_t state, uint_fast64_t choice) override { + 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 isChoiceDefined(uint_fast64_t state) const override { + bool TotalScheduler::isChoiceDefined(uint_fast64_t state) const { return true; } - uint_fast64_t getChoice(uint_fast64_t state) const override { + 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 index 1679766ad..2e29471f7 100644 --- a/src/storage/TotalScheduler.h +++ b/src/storage/TotalScheduler.h @@ -1,6 +1,9 @@ #ifndef STORM_STORAGE_TOTALSCHEDULER_H_ #define STORM_STORAGE_TOTALSCHEDULER_H_ +#include +#include + #include "src/storage/Scheduler.h" namespace storm { @@ -10,12 +13,16 @@ namespace storm { 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;