From 7e74bfbff2c489ee4c0b1fc8cca4a7d06224bfa9 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 19 Jun 2013 18:01:41 +0200 Subject: [PATCH] Fixed bug in creation of scheduler, but there is still one really obvious one. Added small MDP example. Former-commit-id: e2b5aba6d5811c922f3e5bbac82cd753b199728b --- .../prctl/SparseMdpPrctlModelChecker.h | 49 ++++++++++++++++--- src/utility/vector.h | 7 ++- 2 files changed, 44 insertions(+), 12 deletions(-) diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 229295d3a..739a6d408 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -540,6 +540,24 @@ namespace storm { storm::utility::vector::setVectorValues(*result, *targetStates, storm::utility::constGetZero()); storm::utility::vector::setVectorValues(*result, infinityStates, storm::utility::constGetInfinity()); +// std::vector myScheduler(this->getModel().getNumberOfStates()); +// this->computeTakenChoices(this->minimumOperatorStack.top(), *result, myScheduler, this->getModel().getNondeterministicChoiceIndices()); +// std::cout << "min? " << this->minimumOperatorStack.top() << " 487: " << myScheduler[487] << std::endl; +// std::cout << "513: " << (*result)[513] << " 484: " << (*result)[484] << std::endl; +// std::cout << "real scheduler: " << myScheduler << std::endl; +// storm::storage::BitVector subsys(this->getModel().getNumberOfStates(), true); +// +// std::vector stateColoring(this->getModel().getNumberOfStates()); +// for (auto target : *targetStates) { +// stateColoring[target] = 1; +// } +// +// std::vector colors(2); +// colors[0] = "white"; +// colors[1] = "blue"; +// +// this->getModel().writeDotToStream(std::cout, true, &subsys, result, nullptr, &stateColoring, &colors, &myScheduler); + // If we were required to generate a scheduler, do so now. if (scheduler != nullptr) { this->computeTakenChoices(this->minimumOperatorStack.top(), *result, *scheduler, this->getModel().getNondeterministicChoiceIndices()); @@ -559,13 +577,19 @@ 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, std::vector const& nondeterministicResult, std::vector& takenChoices, std::vector const& nondeterministicChoiceIndices) const { - std::vector temporaryResult(nondeterministicChoiceIndices.size() - 1); - if (minimize) { - storm::utility::vector::reduceVectorMin(nondeterministicResult, temporaryResult, nondeterministicChoiceIndices, &takenChoices); - } else { - storm::utility::vector::reduceVectorMax(nondeterministicResult, temporaryResult, nondeterministicChoiceIndices, &takenChoices); - } + void computeTakenChoices(bool minimize, std::vector const& result, std::vector& takenChoices, std::vector const& nondeterministicChoiceIndices) const { +// std::vector nondeterministicResult(this->getModel().getTransitionMatrix().getColumnCount()); +// std::vector temporaryResult(nondeterministicChoiceIndices.size() - 1); +// if (linearEquationSolver != nullptr) { +// this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), ); +// } else { +// throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; +// } +// if (minimize) { +// storm::utility::vector::reduceVectorMin(nondeterministicResult, temporaryResult, nondeterministicChoiceIndices, &takenChoices); +// } else { +// storm::utility::vector::reduceVectorMax(nondeterministicResult, temporaryResult, nondeterministicChoiceIndices, &takenChoices); +// } } /*! @@ -575,7 +599,6 @@ namespace storm { mutable std::stack minimumOperatorStack; private: - /*! * Computes the nondeterministic choice indices vector resulting from reducing the full system to the states given * by the parameter constraint. @@ -616,6 +639,7 @@ namespace storm { */ std::vector getInitialValueIterationValues(storm::storage::SparseMatrix const& submatrix, std::vector const& subNondeterministicChoiceIndices, std::vector const& rightHandSide) const { storm::settings::Settings* s = storm::settings::instance(); + double precision = s->get("precision"); if (s->get("use-heuristic-presolve")) { std::vector scheduler(submatrix.getColumnCount()); std::vector result(scheduler.size(), Type(0.5)); @@ -625,6 +649,15 @@ namespace storm { A.convertToEquationSystem(); std::unique_ptr> solver(new storm::solver::GmmxxLinearEquationSolver()); solver->solveEquationSystem(A, result, b); + + // As there are sometimes some very small values in the vector due to numerical solving, we set + // them to zero, because they otherwise require a certain number of value iterations. + for (auto& value : result) { + if (value < precision) { + value = 0; + } + } + return result; } else { return std::vector(submatrix.getColumnCount()); diff --git a/src/utility/vector.h b/src/utility/vector.h index 52e16c337..e11ab0583 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -191,8 +191,7 @@ void reduceVector(std::vector const& source, std::vector& target, std::vec continue; } - // We have to minimize the value, so only overwrite the current value if the - // value is actually lower. + // We have to upate the value, so only overwrite the current value if the value passes the filter. if (filter(*it, target[currentTargetRow])) { target[currentTargetRow] = *it; if (choices != nullptr) { @@ -212,7 +211,7 @@ void reduceVector(std::vector const& source, std::vector& target, std::vec */ template void reduceVectorMin(std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::vector* choices = nullptr) { - reduceVector(source, target, rowGrouping, std::less()); + reduceVector(source, target, rowGrouping, std::less(), choices); } /*! @@ -225,7 +224,7 @@ void reduceVectorMin(std::vector const& source, std::vector& target, std:: */ template void reduceVectorMax(std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::vector* choices = nullptr) { - reduceVector(source, target, rowGrouping, std::greater()); + reduceVector(source, target, rowGrouping, std::greater(), choices); } /*!