From 796d7652df67dfcd38ca533371f36c65c00c0268 Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 3 Mar 2016 18:49:00 +0100 Subject: [PATCH] Fixed problem with bounds in MA model checker Former-commit-id: c40c4e479513338c7739d15d99aa75343761cfa7 --- .../csl/SparseMarkovAutomatonCslModelChecker.cpp | 12 ++++++++++-- .../csl/helper/SparseMarkovAutomatonCslHelper.cpp | 6 +----- .../csl/helper/SparseMarkovAutomatonCslHelper.h | 2 +- src/utility/vector.h | 6 +++--- 4 files changed, 15 insertions(+), 11 deletions(-) diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index da8d72c47..05e2cf823 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -45,8 +45,16 @@ namespace storm { STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute time-bounded reachability probabilities in non-closed Markov automaton."); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), pathFormula.getIntervalBounds(), *minMaxLinearEquationSolverFactory); + double lowerBound = 0; + double upperBound = 0; + if (!pathFormula.hasDiscreteTimeBound()) { + std::pair const& intervalBounds = pathFormula.getIntervalBounds(); + lowerBound = intervalBounds.first; + upperBound = intervalBounds.second; + } else { + upperBound = pathFormula.getDiscreteTimeBound(); + } + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), lowerBound, upperBound, *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 95007a9e6..00a4e57c0 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -119,13 +119,9 @@ namespace storm { template - std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, double lowerBound, double upperBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); - // 'Unpack' the bounds to make them more easily accessible. - double lowerBound = boundsPair.first; - double upperBound = boundsPair.second; - // (1) Compute the accuracy we need to achieve the required error bound. ValueType maxExitRate = 0; for (auto value : exitRateVector) { diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index 5b24fe569..764eb542c 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -14,7 +14,7 @@ namespace storm { template class SparseMarkovAutomatonCslHelper { public: - static std::vector computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, double lowerBound, double upperBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); static std::vector computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); diff --git a/src/utility/vector.h b/src/utility/vector.h index b5480de9b..d9ad13e64 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -716,10 +716,10 @@ namespace storm { std::string toString(std::vector vector) { std::stringstream stream; stream << "vector (" << vector.size() << ") [ "; - for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) { - stream << vector[i] << ", "; - } if (!vector.empty()) { + for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) { + stream << vector[i] << ", "; + } stream << vector.back(); } stream << " ]";