From 135c38777f88c452b9856a7a31615885a374bfd3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 7 Jun 2018 22:53:41 +0200 Subject: [PATCH] game-based abstraction working with rational numbers --- .../abstraction/AbstractionInformation.cpp | 6 ++-- src/storm/api/verification.h | 4 +-- .../abstraction/GameBasedMdpModelChecker.cpp | 29 ++++++++++++++----- src/storm/utility/ConstantsComparator.cpp | 8 ++--- src/storm/utility/constants.h | 4 +-- src/storm/utility/graph.cpp | 10 ++++++- 6 files changed, 42 insertions(+), 19 deletions(-) diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp index 7fd9a9d16..4b61ed4d8 100644 --- a/src/storm/abstraction/AbstractionInformation.cpp +++ b/src/storm/abstraction/AbstractionInformation.cpp @@ -491,7 +491,7 @@ namespace storm { template template std::map> AbstractionInformation::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const { - std::map> result; + std::map> result; storm::dd::Add lowerChoiceAsAdd = choice.template toAdd(); for (auto const& successorValuePair : lowerChoiceAsAdd) { @@ -614,8 +614,10 @@ namespace storm { template std::map> AbstractionInformation::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const; template std::map> AbstractionInformation::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const; - + template std::map> AbstractionInformation::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const; + template std::vector>> AbstractionInformation::decodeChoicesToUpdateSuccessorMapping(std::set const& player2Variables, storm::dd::Bdd const& choices) const; template std::vector>> AbstractionInformation::decodeChoicesToUpdateSuccessorMapping(std::set const& player2Variables, storm::dd::Bdd const& choices) const; + template std::vector>> AbstractionInformation::decodeChoicesToUpdateSuccessorMapping(std::set const& player2Variables, storm::dd::Bdd const& choices) const; } } diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h index 5d07f9f51..2bec11dcf 100644 --- a/src/storm/api/verification.h +++ b/src/storm/api/verification.h @@ -38,7 +38,7 @@ namespace storm { } template - typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task) { + typename std::enable_if::value || std::is_same::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task) { STORM_LOG_THROW(model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC || model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MDP, storm::exceptions::NotSupportedException, "Can only treat DTMCs/MDPs using the abstraction refinement engine."); std::unique_ptr result; @@ -60,7 +60,7 @@ namespace storm { } template - typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask const&) { + typename std::enable_if::value && !std::is_same::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Abstraction-refinement engine does not support data type."); } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index d1078b8c8..c8b758516 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -713,13 +713,19 @@ namespace storm { quantitativeResult.max = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min)); quantitativeWatch.stop(); result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.getInitialStatesRange()); + totalSolutionWatch.add(quantitativeWatch); if (result) { - totalSolutionWatch.add(quantitativeWatch); return result; } - - totalSolutionWatch.add(quantitativeWatch); - STORM_LOG_INFO("Obtained quantitative bounds [" << quantitativeResult.min.getInitialStatesRange().first << ", " << quantitativeResult.max.getInitialStatesRange().second << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms."); + + ValueType minVal = quantitativeResult.min.getInitialStatesRange().first; + ValueType maxVal = quantitativeResult.max.getInitialStatesRange().second; + if (std::is_same::value) { + STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms."); + } else { + STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] (approx. [" << storm::utility::convertNumber(minVal) << ", " << storm::utility::convertNumber(maxVal) << "]) on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms."); + } + // (9) Check whether the lower and upper bounds are close enough to terminate with an answer. result = checkForResultAfterQuantitativeCheck(quantitativeResult.min.getInitialStatesRange().first, quantitativeResult.max.getInitialStatesRange().second, comparator); @@ -1142,7 +1148,7 @@ namespace storm { ValueType maxDiff = storm::utility::zero(); uint64_t maxState = 0; for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { - ValueType const& diff = storm::utility::abs(sanityValues[state] - quantitativeResult.getMin().getValues()[state]); + ValueType diff = storm::utility::abs(ValueType(sanityValues[state] - quantitativeResult.getMin().getValues()[state])); if (diff > maxDiff) { maxState = state; maxDiff = diff; @@ -1180,7 +1186,7 @@ namespace storm { maxDiff = storm::utility::zero(); maxState = 0; for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { - ValueType const& diff = storm::utility::abs(sanityValues[state] - quantitativeResult.getMax().getValues()[state]); + ValueType diff = storm::utility::abs(ValueType(sanityValues[state] - quantitativeResult.getMax().getValues()[state])); if (diff > maxDiff) { maxState = state; maxDiff = diff; @@ -1373,11 +1379,18 @@ namespace storm { quantitativeResult.setMax(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, transitionMatrix, player1Groups, qualitativeResult, maybeMax, maxStrategyPair, odd, &quantitativeResult.getMin(), &minStrategyPair)); quantitativeWatch.stop(); result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.getMax().getRange(initialStates)); + totalSolutionWatch.add(quantitativeWatch); if (result) { - totalSolutionWatch.add(quantitativeWatch); return result; } - STORM_LOG_INFO("Obtained quantitative bounds [" << quantitativeResult.getMin().getRange(initialStates).first << ", " << quantitativeResult.getMax().getRange(initialStates).second << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms."); + + ValueType minVal = quantitativeResult.getMin().getRange(initialStates).first; + ValueType maxVal = quantitativeResult.getMax().getRange(initialStates).second; + if (std::is_same::value) { + STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms."); + } else { + STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] (approx. [" << storm::utility::convertNumber(minVal) << ", " << storm::utility::convertNumber(maxVal) << "]) on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms."); + } // (9) Check whether the lower and upper bounds are close enough to terminate with an answer. result = checkForResultAfterQuantitativeCheck(quantitativeResult.getMin().getRange(initialStates).first, quantitativeResult.getMax().getRange(initialStates).second, comparator); diff --git a/src/storm/utility/ConstantsComparator.cpp b/src/storm/utility/ConstantsComparator.cpp index 6d8318047..2b7aad2d9 100644 --- a/src/storm/utility/ConstantsComparator.cpp +++ b/src/storm/utility/ConstantsComparator.cpp @@ -112,7 +112,7 @@ namespace storm { // Intentionally left empty. } - ConstantsComparator::ConstantsComparator(storm::RationalNumber precision, bool relative) : precision(precision), relative(false) { + ConstantsComparator::ConstantsComparator(storm::RationalNumber precision, bool relative) : precision(precision), relative(relative) { // Intentionally left empty. } @@ -120,7 +120,7 @@ namespace storm { if (storm::utility::isZero(precision)) { return storm::utility::isOne(value); } - return storm::utility::abs(value - one()) <= precision; + return storm::utility::abs(storm::RationalNumber(value - one())) <= precision; } bool ConstantsComparator::isZero(storm::RationalNumber const& value) const { @@ -136,9 +136,9 @@ namespace storm { } if (relative) { - return value1 == value2 || storm::utility::abs(value1 - value2)/storm::utility::abs(value1 + value2) <= precision; + return value1 == value2 || storm::utility::abs(storm::RationalNumber(value1 - value2))/storm::utility::abs(storm::RationalNumber(value1 + value2)) <= precision; } else { - return storm::utility::abs(value1 - value2) <= precision; + return storm::utility::abs(storm::RationalNumber(value1 - value2)) <= precision; } } diff --git a/src/storm/utility/constants.h b/src/storm/utility/constants.h index 069303c04..9d83a0a49 100644 --- a/src/storm/utility/constants.h +++ b/src/storm/utility/constants.h @@ -38,7 +38,7 @@ namespace storm { struct DoubleLess { bool operator()(double a, double b) const { - return b - a > 1e-17; + return b - a > 1e-18; } }; @@ -54,7 +54,7 @@ namespace storm { struct DoubleGreater { bool operator()(double a, double b) const { - return a - b > 1e-17; + return a - b > 1e-18; } }; diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 4844abb83..36b377051 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1736,6 +1736,10 @@ namespace storm { template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair); + + template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair, boost::optional const& player1Candidates); + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix); // End of instantiations for storm::RationalNumber. @@ -1869,7 +1873,7 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); template SymbolicGameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); - + template SymbolicGameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates); // Instantiations for Sylvan (rational number). @@ -1908,6 +1912,10 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template SymbolicGameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); + + template SymbolicGameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates); + // Instantiations for Sylvan (rational function). template storm::dd::Bdd performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, boost::optional const& stepBound = boost::optional());