From 58c8531d34af9e2a2eb7a60d795319a42c3db68f Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 17 Oct 2017 11:07:20 +0200 Subject: [PATCH 1/8] Use Carl 17.10 --- resources/3rdparty/carl/CMakeLists.txt | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/resources/3rdparty/carl/CMakeLists.txt b/resources/3rdparty/carl/CMakeLists.txt index b41ed3785..dcab4ec30 100644 --- a/resources/3rdparty/carl/CMakeLists.txt +++ b/resources/3rdparty/carl/CMakeLists.txt @@ -8,15 +8,15 @@ message(STORM_3RDPARTY_BINARY_DIR: ${STORM_3RDPARTY_BINARY_DIR}) ExternalProject_Add(carl-config GIT_REPOSITORY https://github.com/smtrat/carl - GIT_TAG 17.08 + GIT_TAG 17.10 PREFIX here SOURCE_DIR source_dir BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl CMAKE_ARGS -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DBOOST_INCLUDEDIR=${Boost_INCLUDE_DIRS} -DBOOST_LIBRARYDIR=${Boost_LIBRARY_DIRS} -DBoost_NO_SYSTEM_PATHS=ON -DEXPORT_TO_CMAKE=ON -DTHREAD_SAFE=ON -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=ON -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl - BUILD_IN_SOURCE 0 - LOG_UPDATE OFF - LOG_CONFIGURE OFF - BUILD_COMMAND "" # Disable build step. + BUILD_IN_SOURCE 0 + LOG_UPDATE OFF + LOG_CONFIGURE OFF + BUILD_COMMAND "" # Disable build step. INSTALL_COMMAND "" # Disable install step too. ) add_custom_target(build-carl) From d90c507431e0b6cd8e763634135faa68d7c2696d Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 17 Oct 2017 13:18:43 +0200 Subject: [PATCH 2/8] fixed bug in sparse bisimulation quotient extraction related to rewards --- .../IterativeMinMaxLinearEquationSolver.cpp | 18 ++++++++++++------ .../solver/NativeLinearEquationSolver.cpp | 2 +- .../dd/bisimulation/QuotientExtractor.cpp | 18 ++++++------------ 3 files changed, 19 insertions(+), 19 deletions(-) diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index d756c194b..b706ab585 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -124,23 +124,29 @@ namespace storm { template bool IterativeMinMaxLinearEquationSolver::internalSolveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b) const { + bool result = false; switch (this->getSettings().getSolutionMethod()) { case IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration: if (this->getSettings().getForceSoundness()) { - return solveEquationsSoundValueIteration(dir, x, b); + result = solveEquationsSoundValueIteration(dir, x, b); } else { - return solveEquationsValueIteration(dir, x, b); + result = solveEquationsValueIteration(dir, x, b); } + break; case IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration: - return solveEquationsPolicyIteration(dir, x, b); + result = solveEquationsPolicyIteration(dir, x, b); + break; case IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::Acyclic: - return solveEquationsAcyclic(dir, x, b); + result = solveEquationsAcyclic(dir, x, b); + break; case IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::RationalSearch: - return solveEquationsRationalSearch(dir, x, b); + result = solveEquationsRationalSearch(dir, x, b); + break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "This solver does not implement the selected solution method"); } - return false; + + return result; } template diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index e77d23d94..a0f0f03e7 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -86,7 +86,7 @@ namespace storm { void NativeLinearEquationSolverSettings::setForceSoundness(bool value) { forceSoundness = value; if (forceSoundness && method != SolutionMethod::Power && method != SolutionMethod::RationalSearch) { - STORM_LOG_WARN("To guarantee soundness, the equation solving technique has been switched to '" << storm::settings::modules::NativeEquationSolverSettings::LinearEquationMethod::Power << "'."); + STORM_LOG_INFO("To guarantee soundness, the equation solving technique has been switched to '" << storm::settings::modules::NativeEquationSolverSettings::LinearEquationMethod::Power << "'."); method = SolutionMethod::Power; } } diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 3e8682b6d..895cea154 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -269,18 +269,13 @@ namespace storm { } else { STORM_LOG_ASSERT(!this->rowPermutation.empty(), "Expected proper row permutation."); std::vector valueVector = extractVectorInternal(vector, this->allSourceVariablesCube, this->nondeterminismOdd); - + // Reorder the values according to the known row permutation. - for (uint64_t position = 0; position < valueVector.size(); ) { - if (rowPermutation[position] != position) { - std::swap(valueVector[position], valueVector[rowPermutation[position]]); - std::swap(rowPermutation[position], rowPermutation[rowPermutation[position]]); - } else { - ++position; - } + std::vector reorderedValues(valueVector.size()); + for (uint64_t pos = 0; pos < valueVector.size(); ++pos) { + reorderedValues[pos] = valueVector[rowPermutation[pos]]; } - - return valueVector; + return reorderedValues; } } @@ -857,7 +852,7 @@ namespace storm { storm::storage::SparseMatrix quotientTransitionMatrix = sparseExtractor.extractTransitionMatrix(model.getTransitionMatrix()); auto end = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); - + start = std::chrono::high_resolution_clock::now(); storm::models::sparse::StateLabeling quotientStateLabeling(partition.getNumberOfBlocks()); quotientStateLabeling.addLabel("init", sparseExtractor.extractSetExists(model.getInitialStates())); @@ -892,7 +887,6 @@ namespace storm { boost::optional> quotientStateActionRewards; if (rewardModel.hasStateActionRewards()) { - rewardModel.getStateActionRewardVector().exportToDot("vector.dot"); quotientStateActionRewards = sparseExtractor.extractStateActionVector(rewardModel.getStateActionRewardVector()); } From b8120ed73a6cfe35a8c36eb2849fb60bc57e6e5f Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 20 Oct 2017 15:46:36 +0200 Subject: [PATCH 3/8] Markov automaton model checker now clearing basic requirements --- .../csl/helper/SparseMarkovAutomatonCslHelper.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 4c49a6325..612456a0d 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -90,9 +90,11 @@ namespace storm { // Check for requirements of the solver. storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::UntilProbabilities); + requirements.clearBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(aProbabilistic); + solver->setBounds(storm::utility::zero(), storm::utility::one()); solver->setRequirementsChecked(); solver->setCachingEnabled(true); @@ -377,9 +379,11 @@ namespace storm { // Check for requirements of the solver. storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::StochasticShortestPath); + requirements.clearLowerBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(sspMatrix); + solver->setLowerBound(storm::utility::zero()); solver->setRequirementsChecked(); solver->solveEquations(dir, x, b); From 4e4526182f548eb044498f307baec4d323d5877f Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 23 Oct 2017 14:21:20 +0200 Subject: [PATCH 4/8] adding information about which technique is used to symbolic native linear equation solver --- src/storm/solver/SymbolicNativeLinearEquationSolver.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp index 21d06a678..9ad5e90af 100644 --- a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp @@ -119,7 +119,9 @@ namespace storm { template storm::dd::Add SymbolicNativeLinearEquationSolver::solveEquationsJacobi(storm::dd::Add const& x, storm::dd::Add const& b) const { storm::dd::DdManager& manager = this->getDdManager(); - + + STORM_LOG_INFO("Solving symbolic linear equation system with NativeLinearEquationSolver (jacobi)"); + // Start by computing the Jacobi decomposition of the matrix A. storm::dd::Bdd diagonal = storm::utility::dd::getRowColumnDiagonal(x.getDdManager(), this->rowColumnMetaVariablePairs); diagonal &= this->allRows; @@ -185,6 +187,7 @@ namespace storm { template storm::dd::Add SymbolicNativeLinearEquationSolver::solveEquationsPower(storm::dd::Add const& x, storm::dd::Add const& b) const { + STORM_LOG_INFO("Solving symbolic linear equation system with NativeLinearEquationSolver (power)"); PowerIterationResult result = performPowerIteration(this->getLowerBoundsVector(), b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), this->getSettings().getMaximalNumberOfIterations()); if (result.status == SolverStatus::Converged) { @@ -311,6 +314,7 @@ namespace storm { template storm::dd::Add SymbolicNativeLinearEquationSolver::solveEquationsRationalSearch(storm::dd::Add const& x, storm::dd::Add const& b) const { + STORM_LOG_INFO("Solving symbolic linear equation system with NativeLinearEquationSolver (rational search)"); return solveEquationsRationalSearchHelper(x, b); } From 33585c811fe49d29f43a525e2a8a1dfef9e183e1 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 25 Oct 2017 17:51:36 +0200 Subject: [PATCH 5/8] MinMax Solver requirements now respect whether the solution is known to be unique or not. --- ...SparseDtmcParameterLiftingModelChecker.cpp | 9 +- .../helper/SparseMarkovAutomatonCslHelper.cpp | 16 +- .../prctl/helper/HybridMdpPrctlHelper.cpp | 15 +- .../prctl/helper/SparseMdpPrctlHelper.cpp | 55 ++++--- .../prctl/helper/SymbolicMdpPrctlHelper.cpp | 30 +++- .../IterativeMinMaxLinearEquationSolver.cpp | 152 +++--------------- .../IterativeMinMaxLinearEquationSolver.h | 2 +- .../solver/LpMinMaxLinearEquationSolver.cpp | 6 +- .../solver/LpMinMaxLinearEquationSolver.h | 2 +- .../solver/MinMaxLinearEquationSolver.cpp | 19 ++- src/storm/solver/MinMaxLinearEquationSolver.h | 18 ++- .../SymbolicMinMaxLinearEquationSolver.cpp | 46 +++--- .../SymbolicMinMaxLinearEquationSolver.h | 17 +- 13 files changed, 187 insertions(+), 200 deletions(-) diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 8ac2bdea8..27960daac 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -146,9 +146,9 @@ namespace storm { lowerResultBound = storm::utility::zero(); upperResultBound = storm::utility::one(); - auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::UntilProbabilities); + // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations). + auto req = solverFactory->getRequirements(true); req.clearBounds(); - req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations). STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement."); solverFactory->setRequirementsChecked(true); } @@ -185,8 +185,8 @@ namespace storm { // We only know a lower bound for the result lowerResultBound = storm::utility::zero(); - auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::ReachabilityRewards); - req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations). + // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations). + auto req = solverFactory->getRequirements(true); req.clearLowerBounds(); if (req.requiresUpperBounds()) { solvingRequiresUpperRewardBounds = true; @@ -253,6 +253,7 @@ namespace storm { solverFactory->setMinMaxMethod(storm::solver::MinMaxMethod::PolicyIteration); } auto solver = solverFactory->create(parameterLifter->getMatrix()); + solver->setHasUniqueSolution(); if (lowerResultBound) solver->setLowerBound(lowerResultBound.get()); if (upperResultBound) { solver->setUpperBound(upperResultBound.get()); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 612456a0d..0bdc633f7 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -89,11 +89,13 @@ namespace storm { } // Check for requirements of the solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::UntilProbabilities); + // The solution is unique as we assume non-zeno MAs. + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(true, dir); requirements.clearBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(aProbabilistic); + solver->setHasUniqueSolution(); solver->setBounds(storm::utility::zero(), storm::utility::one()); solver->setRequirementsChecked(); solver->setCachingEnabled(true); @@ -378,12 +380,14 @@ namespace storm { std::vector x(numberOfSspStates); // Check for requirements of the solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::StochasticShortestPath); - requirements.clearLowerBounds(); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(true, dir); + requirements.clearBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(sspMatrix); + solver->setHasUniqueSolution(); solver->setLowerBound(storm::utility::zero()); + solver->setUpperBound(*std::max_element(lraValuesForEndComponents.begin(), lraValuesForEndComponents.end())); solver->setRequirementsChecked(); solver->solveEquations(dir, x, b); @@ -588,10 +592,14 @@ namespace storm { std::vector b = probabilisticChoiceRewards; // Check for requirements of the solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::ReachabilityRewards); + // The solution is unique as we assume non-zeno MAs. + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(true, dir); + requirements.clearLowerBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); auto solver = minMaxLinearEquationSolverFactory.create(std::move(aProbabilistic)); + solver->setLowerBound(storm::utility::zero()); + solver->setHasUniqueSolution(true); solver->setRequirementsChecked(true); solver->setCachingEnabled(true); diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 1d6864fa3..232bb91da 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -135,8 +135,10 @@ namespace storm { } else { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { + // If we minimize, we know that the solution to the equation system is unique. + bool uniqueSolution = dir == storm::solver::OptimizationDirection::Minimize; // Check for requirements of the solver early so we can adjust the maybe state computation accordingly. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::UntilProbabilities, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(uniqueSolution, dir); storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements; SolverRequirementsData solverRequirementsData; bool extendMaybeStates = false; @@ -212,6 +214,10 @@ namespace storm { std::vector x(explicitRepresentation.first.getRowGroupCount(), storm::utility::zero()); std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); + + // Set whether the equation system will have a unique solution + solver->setHasUniqueSolution(uniqueSolution); + if (solverRequirementsData.initialScheduler) { solver->setInitialScheduler(std::move(solverRequirementsData.initialScheduler.get())); } @@ -487,8 +493,10 @@ namespace storm { } else { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { + // If we maximize, we know that the solution to the equation system is unique. + bool uniqueSolution = dir == storm::solver::OptimizationDirection::Maximize; // Check for requirements of the solver this early so we can adapt the maybe states accordingly. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::ReachabilityRewards, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(uniqueSolution, dir); storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements; bool extendMaybeStates = false; if (!clearedRequirements.empty()) { @@ -568,6 +576,9 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(); + // Set whether the equation system will have a unique solution + solver->setHasUniqueSolution(uniqueSolution); + // If the solver requires upper bounds, compute them now. if (requirements.requiresUpperBounds()) { setUpperRewardBounds(*solver, dir, explicitRepresentation.first, explicitRepresentation.second, solverRequirementsData.oneStepTargetProbabilities.get()); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 4a5688f5c..73115ac64 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -22,7 +22,7 @@ #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/solver/LpSolver.h" - + #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/MinMaxEquationSolverSettings.h" @@ -38,6 +38,11 @@ namespace storm { namespace modelchecker { namespace helper { + enum class EquationSystemType { + UntilProbabilities, + ExpectedRewards + }; + template std::vector SparseMdpPrctlHelper::computeBoundedUntilProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); @@ -91,12 +96,12 @@ namespace storm { } template - std::vector computeValidSchedulerHint(storm::solver::EquationSystemType const& type, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& filterStates, storm::storage::BitVector const& targetStates) { + std::vector computeValidSchedulerHint(EquationSystemType const& type, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& filterStates, storm::storage::BitVector const& targetStates) { storm::storage::Scheduler validScheduler(maybeStates.size()); - if (type == storm::solver::EquationSystemType::UntilProbabilities) { + if (type == EquationSystemType::UntilProbabilities) { storm::utility::graph::computeSchedulerProbGreater0E(transitionMatrix, backwardTransitions, filterStates, targetStates, validScheduler, boost::none); - } else if (type == storm::solver::EquationSystemType::ReachabilityRewards) { + } else if (type == EquationSystemType::ExpectedRewards) { storm::utility::graph::computeSchedulerProb1E(maybeStates | targetStates, transitionMatrix, backwardTransitions, filterStates, targetStates, validScheduler); } else { STORM_LOG_ASSERT(false, "Unexpected equation system type."); @@ -114,7 +119,7 @@ namespace storm { template struct SparseMdpHintType { - SparseMdpHintType() : eliminateEndComponents(false), computeUpperBounds(false) { + SparseMdpHintType() : eliminateEndComponents(false), computeUpperBounds(false), uniqueSolution(false) { // Intentionally left empty. } @@ -169,6 +174,10 @@ namespace storm { bool getComputeUpperBounds() { return computeUpperBounds; } + + bool hasUniqueSolution() const { + return uniqueSolution; + } boost::optional> schedulerHint; boost::optional> valueHint; @@ -177,6 +186,7 @@ namespace storm { boost::optional> upperResultBounds; bool eliminateEndComponents; bool computeUpperBounds; + bool uniqueSolution; }; template @@ -230,19 +240,22 @@ namespace storm { } template - SparseMdpHintType computeHints(storm::solver::EquationSystemType const& type, ModelCheckerHint const& hint, storm::OptimizationDirection const& dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& targetStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional const& selectedChoices = boost::none) { + SparseMdpHintType computeHints(EquationSystemType const& type, ModelCheckerHint const& hint, storm::OptimizationDirection const& dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& targetStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional const& selectedChoices = boost::none) { SparseMdpHintType result; + // The solution to the min-max equation system is unique if we minimize until probabilities or + // maximize reachability rewards or if the hint tells us that there are no end-compontnes. + result.uniqueSolution = (dir == storm::solver::OptimizationDirection::Minimize && type == EquationSystemType::UntilProbabilities) + || (dir == storm::solver::OptimizationDirection::Maximize && type == EquationSystemType::ExpectedRewards) + || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint().getNoEndComponentsInMaybeStates()); + // Check for requirements of the solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(type, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(result.uniqueSolution, dir); if (!requirements.empty()) { - // If the hint tells us that there are no end-components, we can clear that requirement. - if (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint().getNoEndComponentsInMaybeStates()) { - requirements.clearNoEndComponents(); - } // If the solver still requires no end-components, we have to eliminate them later. if (requirements.requiresNoEndComponents()) { + STORM_LOG_ASSERT(!result.hasUniqueSolution(), "The solver requires to eliminate the end components although the solution is already assumed to be unique."); STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it."); result.eliminateEndComponents = true; requirements.clearNoEndComponents(); @@ -256,9 +269,9 @@ namespace storm { } // Finally, we have information on the bounds depending on the problem type. - if (type == storm::solver::EquationSystemType::UntilProbabilities) { + if (type == EquationSystemType::UntilProbabilities) { requirements.clearBounds(); - } else if (type == storm::solver::EquationSystemType::ReachabilityRewards) { + } else if (type == EquationSystemType::ExpectedRewards) { requirements.clearLowerBounds(); } if (requirements.requiresUpperBounds()) { @@ -273,8 +286,7 @@ namespace storm { // Only if there is no end component decomposition that we will need to do later, we use value and scheduler // hints from the provided hint. if (!result.eliminateEndComponents) { - bool skipEcWithinMaybeStatesCheck = dir == storm::OptimizationDirection::Minimize || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint().getNoEndComponentsInMaybeStates()); - extractValueAndSchedulerHint(result, transitionMatrix, backwardTransitions, maybeStates, selectedChoices, hint, skipEcWithinMaybeStatesCheck); + extractValueAndSchedulerHint(result, transitionMatrix, backwardTransitions, maybeStates, selectedChoices, hint, result.uniqueSolution); } else { STORM_LOG_WARN_COND(hint.isEmpty(), "A non-empty hint was provided, but its information will be disregarded."); } @@ -283,7 +295,7 @@ namespace storm { if (!result.hasLowerResultBound()) { result.lowerResultBound = storm::utility::zero(); } - if (!result.hasUpperResultBound() && type == storm::solver::EquationSystemType::UntilProbabilities) { + if (!result.hasUpperResultBound() && type == EquationSystemType::UntilProbabilities) { result.upperResultBound = storm::utility::one(); } @@ -326,6 +338,7 @@ namespace storm { // Set up the solver. std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix)); solver->setRequirementsChecked(); + solver->setHasUniqueSolution(hint.hasUniqueSolution()); if (hint.hasLowerResultBound()) { solver->setLowerBound(hint.getLowerResultBound()); } @@ -526,7 +539,7 @@ namespace storm { // In this case we have have to compute the remaining probabilities. // Obtain proper hint information either from the provided hint or from requirements of the solver. - SparseMdpHintType hintInformation = computeHints(storm::solver::EquationSystemType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, phiStates, qualitativeStateSets.statesWithProbability1, minMaxLinearEquationSolverFactory); + SparseMdpHintType hintInformation = computeHints(EquationSystemType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, phiStates, qualitativeStateSets.statesWithProbability1, minMaxLinearEquationSolverFactory); // Declare the components of the equation system we will solve. storm::storage::SparseMatrix submatrix; @@ -882,7 +895,7 @@ namespace storm { } // Obtain proper hint information either from the provided hint or from requirements of the solver. - SparseMdpHintType hintInformation = computeHints(storm::solver::EquationSystemType::ReachabilityRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, ~targetStates, targetStates, minMaxLinearEquationSolverFactory, selectedChoices); + SparseMdpHintType hintInformation = computeHints(EquationSystemType::ExpectedRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, ~targetStates, targetStates, minMaxLinearEquationSolverFactory, selectedChoices); // Declare the components of the equation system we will solve. storm::storage::SparseMatrix submatrix; @@ -1089,14 +1102,16 @@ namespace storm { storm::storage::SparseMatrix sspMatrix = sspMatrixBuilder.build(currentChoice, numberOfSspStates, numberOfSspStates); // Check for requirements of the solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::StochasticShortestPath); - requirements.clearLowerBounds(); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(true, goal.direction()); + requirements.clearBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::vector sspResult(numberOfSspStates); goal.restrictRelevantValues(statesNotContainedInAnyMec); std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(std::move(goal), minMaxLinearEquationSolverFactory, sspMatrix); solver->setLowerBound(storm::utility::zero()); + solver->setUpperBound(*std::max_element(lraValuesForEndComponents.begin(), lraValuesForEndComponents.end())); + solver->setHasUniqueSolution(); solver->setRequirementsChecked(); solver->solveEquations(sspResult, b); diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index 518f50acc..cc1d3bcf9 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -21,15 +21,21 @@ namespace storm { namespace modelchecker { namespace helper { + + enum class EquationSystemType { + UntilProbabilities, + ExpectedRewards + }; + template - storm::dd::Bdd computeValidSchedulerHint(storm::solver::EquationSystemType const& type, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& targetStates) { + storm::dd::Bdd computeValidSchedulerHint(EquationSystemType const& type, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& targetStates) { storm::dd::Bdd result; - if (type == storm::solver::EquationSystemType::UntilProbabilities) { + if (type == EquationSystemType::UntilProbabilities) { result = storm::utility::graph::computeSchedulerProbGreater0E(model, transitionMatrix.notZero(), maybeStates, targetStates); - } else if (type == storm::solver::EquationSystemType::ReachabilityRewards) { + } else if (type == EquationSystemType::ExpectedRewards) { result = storm::utility::graph::computeSchedulerProb1E(model, transitionMatrix.notZero(), maybeStates, targetStates, maybeStates || targetStates); } @@ -78,13 +84,18 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); + // If we minimize, we know that the solution is unique + if (dir == storm::solver::OptimizationDirection::Minimize) { + solver->setHasUniqueSolution(); + } + // Check requirements of solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(storm::solver::EquationSystemType::UntilProbabilities, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(dir); boost::optional> initialScheduler; if (!requirements.empty()) { if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) { STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it."); - initialScheduler = computeValidSchedulerHint(storm::solver::EquationSystemType::UntilProbabilities, model, transitionMatrix, maybeStates, statesWithProbability01.second); + initialScheduler = computeValidSchedulerHint(EquationSystemType::UntilProbabilities, model, transitionMatrix, maybeStates, statesWithProbability01.second); requirements.clearValidInitialScheduler(); } requirements.clearBounds(); @@ -237,13 +248,18 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); + // If we maximize, we know that the solution is unique + if (dir == storm::solver::OptimizationDirection::Maximize) { + solver->setHasUniqueSolution(); + } + // Check requirements of solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(storm::solver::EquationSystemType::ReachabilityRewards, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(dir); boost::optional> initialScheduler; if (!requirements.empty()) { if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) { STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it."); - initialScheduler = computeValidSchedulerHint(storm::solver::EquationSystemType::ReachabilityRewards, model, transitionMatrix, maybeStates, targetStates); + initialScheduler = computeValidSchedulerHint(EquationSystemType::ExpectedRewards, model, transitionMatrix, maybeStates, targetStates); requirements.clearValidInitialScheduler(); } requirements.clearLowerBounds(); diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index b706ab585..eb6a970b9 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -45,7 +45,6 @@ namespace storm { switch (solutionMethod) { case MinMaxMethod::ValueIteration: this->solutionMethod = SolutionMethod::ValueIteration; break; case MinMaxMethod::PolicyIteration: this->solutionMethod = SolutionMethod::PolicyIteration; break; - case MinMaxMethod::Acyclic: this->solutionMethod = SolutionMethod::Acyclic; break; case MinMaxMethod::RationalSearch: this->solutionMethod = SolutionMethod::RationalSearch; break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique for iterative MinMax linear equation solver."); @@ -136,9 +135,6 @@ namespace storm { case IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration: result = solveEquationsPolicyIteration(dir, x, b); break; - case IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::Acyclic: - result = solveEquationsAcyclic(dir, x, b); - break; case IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::RationalSearch: result = solveEquationsRationalSearch(dir, x, b); break; @@ -268,67 +264,44 @@ namespace storm { } template - MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver::getRequirements(EquationSystemType const& equationSystemType, boost::optional const& direction) const { + MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver::getRequirements(boost::optional const& direction) const { // Start by copying the requirements of the linear equation solver. MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements()); - // General requirements. if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration) { - requirements.requireLowerBounds(); - } else if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::RationalSearch) { - // As rational search needs to approach the solution from below, we cannot start with a valid scheduler hint as we would otherwise do. - // Instead, we need to require no end components. - if (equationSystemType == EquationSystemType::ReachabilityRewards) { - if (!direction || direction.get() == OptimizationDirection::Minimize) { + if (this->getSettings().getForceSoundness()) { + // Interval iteration requires a unique solution and lower+upper bounds + if (!this->hasUniqueSolution()) { requirements.requireNoEndComponents(); } - } - } - - // In case we perform value iteration and need to retrieve a scheduler, end components are forbidden - if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration && this->isTrackSchedulerSet()) { - requirements.requireNoEndComponents(); - } - - // Guide requirements by whether or not we force soundness. - if (this->getSettings().getForceSoundness()) { - if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration) { - // Require both bounds now. requirements.requireBounds(); - - // If we need to also converge from above, we cannot deal with end components in the notorious cases. - if (equationSystemType == EquationSystemType::UntilProbabilities) { - if (!direction || direction.get() == OptimizationDirection::Maximize) { - requirements.requireNoEndComponents(); - } - } else if (equationSystemType == EquationSystemType::ReachabilityRewards) { - if (!direction || direction.get() == OptimizationDirection::Minimize) { - requirements.requireNoEndComponents(); - } - } - } else if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration) { - if (equationSystemType == EquationSystemType::UntilProbabilities) { + } else if (!this->hasUniqueSolution()) { // Traditional value iteration has no requirements if the solution is unique. + // Computing a scheduler is only possible if the solution is unique + if (this->isTrackSchedulerSet()) { + requirements.requireNoEndComponents(); + } else { + // As we want the smallest (largest) solution for maximizing (minimizing) equation systems, we have to approach the solution from below (above). if (!direction || direction.get() == OptimizationDirection::Maximize) { - requirements.requireValidInitialScheduler(); + requirements.requireLowerBounds(); } - } else if (equationSystemType == EquationSystemType::ReachabilityRewards) { if (!direction || direction.get() == OptimizationDirection::Minimize) { - requirements.requireValidInitialScheduler(); + requirements.requireUpperBounds(); } } } - } else { - if (equationSystemType == EquationSystemType::UntilProbabilities) { - if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration) { - if (!direction || direction.get() == OptimizationDirection::Maximize) { - requirements.requireValidInitialScheduler(); - } - } - } else if (equationSystemType == EquationSystemType::ReachabilityRewards) { - if (!direction || direction.get() == OptimizationDirection::Minimize) { - requirements.requireValidInitialScheduler(); - } + } else if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::RationalSearch) { + // Rational search needs to approach the solution from below. + requirements.requireLowerBounds(); + // The solution needs to be unique in case of minimizing or in cases where we want a scheduler. + if (!this->hasUniqueSolution() && (!direction || direction.get() == OptimizationDirection::Minimize || this->isTrackSchedulerSet())) { + requirements.requireNoEndComponents(); + } + } else if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration) { + if (!this->hasUniqueSolution()) { + requirements.requireValidInitialScheduler(); } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique for iterative MinMax linear equation solver."); } return requirements; @@ -934,83 +907,6 @@ namespace storm { return solveEquationsRationalSearchHelper(dir, x, b); } - template - bool IterativeMinMaxLinearEquationSolver::solveEquationsAcyclic(OptimizationDirection dir, std::vector& x, std::vector const& b) const { - uint64_t numGroups = this->A->getRowGroupCount(); - - // Allocate memory for the scheduler (if required) - if (this->isTrackSchedulerSet()) { - if (this->schedulerChoices) { - this->schedulerChoices->resize(numGroups); - } else { - this->schedulerChoices = std::vector(numGroups); - } - } - - // We now compute a topological sort of the row groups. - // If caching is enabled, it might be possible to obtain this sort from the cache. - if (this->isCachingEnabled()) { - if (rowGroupOrdering) { - for (auto const& group : *rowGroupOrdering) { - computeOptimalValueForRowGroup(group, dir, x, b, this->isTrackSchedulerSet() ? &this->schedulerChoices.get()[group] : nullptr); - } - return true; - } else { - rowGroupOrdering = std::make_unique>(); - rowGroupOrdering->reserve(numGroups); - } - } - - auto transposedMatrix = this->A->transpose(true); - - // We store the groups that have already been processed, i.e., the groups for which x[group] was already set to the correct value. - storm::storage::BitVector processedGroups(numGroups, false); - // Furthermore, we keep track of all candidate groups for which we still need to check whether this group can be processed now. - // A group can be processed if all successors have already been processed. - // Notice that the BitVector candidates is considered in a reversed way, i.e., group i is a candidate iff candidates.get(numGroups - i - 1) is true. - // This is due to the observation that groups with higher indices usually need to be processed earlier. - storm::storage::BitVector candidates(numGroups, true); - uint64_t candidate = numGroups - 1; - for (uint64_t numCandidates = candidates.size(); numCandidates > 0; --numCandidates) { - candidates.set(numGroups - candidate - 1, false); - - // Check if the candidate row group has an unprocessed successor - bool hasUnprocessedSuccessor = false; - for (auto const& entry : this->A->getRowGroup(candidate)) { - if (!processedGroups.get(entry.getColumn())) { - hasUnprocessedSuccessor = true; - break; - } - } - - uint64_t nextCandidate = numGroups - candidates.getNextSetIndex(numGroups - candidate - 1 + 1) - 1; - - if (!hasUnprocessedSuccessor) { - // This candidate can be processed. - processedGroups.set(candidate); - computeOptimalValueForRowGroup(candidate, dir, x, b, this->isTrackSchedulerSet() ? &this->schedulerChoices.get()[candidate] : nullptr); - if (this->isCachingEnabled()) { - rowGroupOrdering->push_back(candidate); - } - - // Add new candidates - for (auto const& predecessorEntry : transposedMatrix.getRow(candidate)) { - uint64_t predecessor = predecessorEntry.getColumn(); - if (!candidates.get(numGroups - predecessor - 1)) { - candidates.set(numGroups - predecessor - 1, true); - nextCandidate = std::max(nextCandidate, predecessor); - ++numCandidates; - } - } - } - candidate = nextCandidate; - } - - assert(candidates.empty()); - STORM_LOG_THROW(processedGroups.full(), storm::exceptions::InvalidOperationException, "The MinMax equation system is not acyclic."); - return true; - } - template void IterativeMinMaxLinearEquationSolver::computeOptimalValueForRowGroup(uint_fast64_t group, OptimizationDirection dir, std::vector& x, std::vector const& b, uint_fast64_t* choice) const { uint64_t row = this->A->getRowGroupIndices()[group]; diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h index f4aa7e7a3..cfce17ddb 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h @@ -62,7 +62,7 @@ namespace storm { ValueType getPrecision() const; bool getRelative() const; - virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional const& direction = boost::none) const override; + virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional const& direction = boost::none) const override; private: bool solveEquationsPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const; diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp index 024bcf260..fce0aeae9 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -110,12 +110,12 @@ namespace storm { template - MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver::getRequirements(EquationSystemType const& equationSystemType, boost::optional const& direction) const { + MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver::getRequirements(boost::optional const& direction) const { MinMaxLinearEquationSolverRequirements requirements; - // In case we need to retrieve a scheduler, end components are forbidden - if (this->isTrackSchedulerSet()) { + // In case we need to retrieve a scheduler, the solution has to be unique + if (!this->hasUniqueSolution() && this->isTrackSchedulerSet()) { requirements.requireNoEndComponents(); } diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.h b/src/storm/solver/LpMinMaxLinearEquationSolver.h index 3e5af458f..d7bcc0c72 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.h +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.h @@ -18,7 +18,7 @@ namespace storm { virtual void clearCache() const override; - virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional const& direction = boost::none) const override; + virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional const& direction = boost::none) const override; private: std::unique_ptr> lpSolverFactory; diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index c41455e16..e4dce9084 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -19,7 +19,7 @@ namespace storm { namespace solver { template - MinMaxLinearEquationSolver::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false), cachingEnabled(false), requirementsChecked(false) { + MinMaxLinearEquationSolver::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false), uniqueSolution(false), cachingEnabled(false), requirementsChecked(false) { // Intentionally left empty. } @@ -56,6 +56,16 @@ namespace storm { direction = OptimizationDirectionSetting::Unset; } + template + void MinMaxLinearEquationSolver::setHasUniqueSolution(bool value) { + uniqueSolution = value; + } + + template + bool MinMaxLinearEquationSolver::hasUniqueSolution() const { + return uniqueSolution; + } + template void MinMaxLinearEquationSolver::setTrackScheduler(bool trackScheduler) { this->trackScheduler = trackScheduler; @@ -127,7 +137,7 @@ namespace storm { } template - MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolver::getRequirements(EquationSystemType const& equationSystemType, boost::optional const& direction) const { + MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolver::getRequirements(boost::optional const& direction) const { return MinMaxLinearEquationSolverRequirements(); } @@ -199,10 +209,11 @@ namespace storm { } template - MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory::getRequirements(EquationSystemType const& equationSystemType, boost::optional const& direction) const { + MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory::getRequirements(bool hasUniqueSolution, boost::optional const& direction) const { // Create dummy solver and ask it for requirements. std::unique_ptr> solver = this->create(); - return solver->getRequirements(equationSystemType, direction); + solver->setHasUniqueSolution(hasUniqueSolution); + return solver->getRequirements(direction); } template diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index 61742d326..5f095f5c8 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -12,7 +12,6 @@ #include "storm/storage/sparse/StateType.h" #include "storm/storage/Scheduler.h" #include "storm/solver/OptimizationDirection.h" -#include "storm/solver/EquationSystemType.h" #include "storm/solver/MinMaxLinearEquationSolverRequirements.h" #include "storm/exceptions/InvalidSettingsException.h" @@ -94,6 +93,16 @@ namespace storm { */ void unsetOptimizationDirection(); + /*! + * Sets whether the solution to the min max equation system is known to be unique. + */ + void setHasUniqueSolution(bool value = true); + + /*! + * Retrieves whether the solution to the min max equation system is assumed to be unique + */ + bool hasUniqueSolution() const; + /*! * Sets whether schedulers are generated when solving equation systems. If the argument is false, the currently * stored scheduler (if any) is deleted. @@ -155,7 +164,7 @@ namespace storm { * Retrieves the requirements of this solver for solving equations with the current settings. The requirements * are guaranteed to be ordered according to their appearance in the SolverRequirement type. */ - virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional const& direction = boost::none) const; + virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional const& direction = boost::none) const; /*! * Notifies the solver that the requirements for solving equations have been checked. If this has not been @@ -184,6 +193,9 @@ namespace storm { boost::optional> initialScheduler; private: + // Whether the solver can assume that the min-max equation system has a unique solution + bool uniqueSolution; + /// Whether some of the generated data during solver calls should be cached. bool cachingEnabled; @@ -212,7 +224,7 @@ namespace storm { * Retrieves the requirements of the solver that would be created when calling create() right now. The * requirements are guaranteed to be ordered according to their appearance in the SolverRequirement type. */ - MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional const& direction = boost::none) const; + MinMaxLinearEquationSolverRequirements getRequirements(bool hasUniqueSolution = false, boost::optional const& direction = boost::none) const; void setRequirementsChecked(bool value = true); bool isRequirementsCheckedSet() const; diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index c6c6ec261..a5845d556 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -86,12 +86,12 @@ namespace storm { } template - SymbolicMinMaxLinearEquationSolver::SymbolicMinMaxLinearEquationSolver(SymbolicMinMaxLinearEquationSolverSettings const& settings) : SymbolicEquationSolver(), settings(settings), requirementsChecked(false) { + SymbolicMinMaxLinearEquationSolver::SymbolicMinMaxLinearEquationSolver(SymbolicMinMaxLinearEquationSolverSettings const& settings) : SymbolicEquationSolver(), settings(settings), uniqueSolution(false), requirementsChecked(false) { // Intentionally left empty. } template - SymbolicMinMaxLinearEquationSolver::SymbolicMinMaxLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs, std::unique_ptr>&& linearEquationSolverFactory, SymbolicMinMaxLinearEquationSolverSettings const& settings) : SymbolicEquationSolver(allRows), A(A), illegalMask(illegalMask), illegalMaskAdd(illegalMask.ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), settings(settings), requirementsChecked(false) { + SymbolicMinMaxLinearEquationSolver::SymbolicMinMaxLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs, std::unique_ptr>&& linearEquationSolverFactory, SymbolicMinMaxLinearEquationSolverSettings const& settings) : SymbolicEquationSolver(allRows), A(A), illegalMask(illegalMask), illegalMaskAdd(illegalMask.ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), settings(settings), uniqueSolution(false), requirementsChecked(false) { // Intentionally left empty. } @@ -419,39 +419,42 @@ namespace storm { } template - MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolver::getRequirements(EquationSystemType const& equationSystemType, boost::optional const& direction) const { + MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolver::getRequirements(boost::optional const& direction) const { MinMaxLinearEquationSolverRequirements requirements; if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration) { - if (equationSystemType == EquationSystemType::UntilProbabilities) { - if (!direction || direction.get() == OptimizationDirection::Maximize) { - requirements.requireValidInitialScheduler(); - } - } - if (equationSystemType == EquationSystemType::ReachabilityRewards) { - if (!direction || direction.get() == OptimizationDirection::Minimize) { - requirements.requireValidInitialScheduler(); - } + if (!this->hasUniqueSolution()) { + requirements.requireValidInitialScheduler(); } } else if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration) { - requirements.requireLowerBounds(); - if (equationSystemType == EquationSystemType::ReachabilityRewards) { - if (!direction || direction.get() == OptimizationDirection::Minimize) { + if (!this->hasUniqueSolution()) { + if (!direction || direction.get() == storm::solver::OptimizationDirection::Maximize) { + requirements.requireLowerBounds(); + } + if (!direction || direction.get() == storm::solver::OptimizationDirection::Minimize) { requirements.requireValidInitialScheduler(); } } } else if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings::SolutionMethod::RationalSearch) { requirements.requireLowerBounds(); - if (equationSystemType == EquationSystemType::ReachabilityRewards) { - if (!direction || direction.get() == OptimizationDirection::Minimize) { - requirements.requireNoEndComponents(); - } + if (!this->hasUniqueSolution() && (!direction || direction.get() == storm::solver::OptimizationDirection::Minimize)) { + requirements.requireNoEndComponents(); } } return requirements; } + template + void SymbolicMinMaxLinearEquationSolver::setHasUniqueSolution(bool value) { + this->uniqueSolution = value; + } + + template + bool SymbolicMinMaxLinearEquationSolver::hasUniqueSolution() const { + return this->uniqueSolution; + } + template void SymbolicMinMaxLinearEquationSolver::setRequirementsChecked(bool value) { this->requirementsChecked = value; @@ -484,9 +487,10 @@ namespace storm { } template - MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolverFactory::getRequirements(EquationSystemType const& equationSystemType, boost::optional const& direction) const { + MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolverFactory::getRequirements(bool hasUniqueSolution, boost::optional const& direction) const { std::unique_ptr> solver = this->create(); - return solver->getRequirements(equationSystemType, direction); + solver->setHasUniqueSolution(hasUniqueSolution); + return solver->getRequirements(direction); } template diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h index 6853582f1..a58552b01 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h @@ -127,7 +127,17 @@ namespace storm { /*! * Retrieves the requirements of the solver. */ - virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional const& direction = boost::none) const; + virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional const& direction = boost::none) const; + + /*! + * Sets whether the solution to the min max equation system is known to be unique. + */ + void setHasUniqueSolution(bool value = true); + + /*! + * Retrieves whether the solution to the min max equation system is assumed to be unique + */ + bool hasUniqueSolution() const; /*! * Notifies the solver that the requirements for solving equations have been checked. If this has not been @@ -208,6 +218,9 @@ namespace storm { // The settings to use. SymbolicMinMaxLinearEquationSolverSettings settings; + // Whether the solver can assume that the min-max equation system has a unique solution + bool uniqueSolution; + // A flag indicating whether the requirements were checked. bool requirementsChecked; @@ -230,7 +243,7 @@ namespace storm { * Retrieves the requirements of the solver that would be created when calling create() right now. The * requirements are guaranteed to be ordered according to their appearance in the SolverRequirement type. */ - MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional const& direction = boost::none) const; + MinMaxLinearEquationSolverRequirements getRequirements(bool hasUniqueSolution = false, boost::optional const& direction = boost::none) const; private: virtual std::unique_ptr> create() const = 0; From 3571f0ddcada672ef3bab7ed264f4ec9775059b4 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 25 Oct 2017 19:48:17 +0200 Subject: [PATCH 6/8] Respected that the solution is unique when doing value iteration --- src/storm/solver/AbstractEquationSolver.cpp | 22 ++++++++--------- src/storm/solver/AbstractEquationSolver.h | 1 + .../IterativeMinMaxLinearEquationSolver.cpp | 24 ++++++++++++------- .../SymbolicMinMaxLinearEquationSolver.cpp | 12 ++++++---- 4 files changed, 35 insertions(+), 24 deletions(-) diff --git a/src/storm/solver/AbstractEquationSolver.cpp b/src/storm/solver/AbstractEquationSolver.cpp index afbec8ac7..c7fe0bd01 100644 --- a/src/storm/solver/AbstractEquationSolver.cpp +++ b/src/storm/solver/AbstractEquationSolver.cpp @@ -168,6 +168,16 @@ namespace storm { } } + template + void AbstractEquationSolver::createUpperBoundsVector(std::vector& upperBoundsVector) const { + STORM_LOG_ASSERT(this->hasUpperBound(), "Expecting upper bound(s)."); + if (this->hasUpperBound(BoundType::Global)) { + upperBoundsVector.assign(upperBoundsVector.size(), this->getUpperBound()); + } else { + upperBoundsVector.assign(this->getUpperBounds().begin(), this->getUpperBounds().end()); + } + } + template void AbstractEquationSolver::createUpperBoundsVector(std::unique_ptr>& upperBoundsVector, uint64_t length) const { STORM_LOG_ASSERT(this->hasUpperBound(), "Expecting upper bound(s)."); @@ -179,17 +189,7 @@ namespace storm { upperBoundsVector = std::make_unique>(length, this->getUpperBound()); } } else { - if (this->hasUpperBound(BoundType::Global)) { - for (auto& e : *upperBoundsVector) { - e = this->getUpperBound(); - } - } else { - auto upperBoundsIt = this->getUpperBounds().begin(); - for (auto& e : *upperBoundsVector) { - e = *upperBoundsIt; - ++upperBoundsIt; - } - } + createUpperBoundsVector(*upperBoundsVector); } } diff --git a/src/storm/solver/AbstractEquationSolver.h b/src/storm/solver/AbstractEquationSolver.h index 22e9d0f56..98f6895f4 100644 --- a/src/storm/solver/AbstractEquationSolver.h +++ b/src/storm/solver/AbstractEquationSolver.h @@ -160,6 +160,7 @@ namespace storm { TerminationCondition const& getTerminationCondition() const; std::unique_ptr> const& getTerminationConditionPointer() const; + void createUpperBoundsVector(std::vector& upperBoundsVector) const; void createUpperBoundsVector(std::unique_ptr>& upperBoundsVector, uint64_t length) const; void createLowerBoundsVector(std::vector& lowerBoundsVector) const; diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index eb6a970b9..1aa038ebd 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -367,9 +367,8 @@ namespace storm { auxiliaryRowGroupVector = std::make_unique>(this->A->getRowGroupCount()); } - // By default, the guarantee that we can provide is that our solution is always less-or-equal than the - // actual solution. - SolverGuarantee guarantee = SolverGuarantee::LessOrEqual; + // By default, we can not provide any guarantee + SolverGuarantee guarantee = SolverGuarantee::None; if (this->hasInitialScheduler()) { // Resolve the nondeterminism according to the initial scheduler. @@ -391,14 +390,21 @@ namespace storm { } submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector); - // If we were given an initial scheduler and are in fact minimizing, our current solution becomes - // always greater-or-equal than the actual solution. - if (dir == storm::OptimizationDirection::Minimize) { + // If we were given an initial scheduler and are maximizing (minimizing), our current solution becomes + // always less-or-equal (greater-or-equal) than the actual solution. + if (dir == storm::OptimizationDirection::Maximize) { + guarantee = SolverGuarantee::LessOrEqual; + } else { + guarantee = SolverGuarantee::GreaterOrEqual; + } + } else if (!this->hasUniqueSolution()) { + if (dir == storm::OptimizationDirection::Maximize) { + this->createLowerBoundsVector(x); + guarantee = SolverGuarantee::LessOrEqual; + } else { + this->createUpperBoundsVector(x); guarantee = SolverGuarantee::GreaterOrEqual; } - } else { - // If no initial scheduler is given, we start from the lower bound. - this->createLowerBoundsVector(x); } std::vector* newX = auxiliaryRowGroupVector.get(); diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index a5845d556..5036ce5ea 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -280,11 +280,15 @@ namespace storm { // Set up the environment. storm::dd::Add localX; - // If we were given an initial scheduler, we take its solution as the starting point. - if (this->hasInitialScheduler()) { - localX = solveEquationsWithScheduler(this->getInitialScheduler(), x, b); + if (this->hasUniqueSolution()) { + localX = x; } else { - localX = this->getLowerBoundsVector(); + // If we were given an initial scheduler, we take its solution as the starting point. + if (this->hasInitialScheduler()) { + localX = solveEquationsWithScheduler(this->getInitialScheduler(), x, b); + } else { + localX = this->getLowerBoundsVector(); + } } ValueIterationResult viResult = performValueIteration(dir, localX, b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), this->settings.getMaximalNumberOfIterations()); From f44ce8801c2aa359d7d24ec9356257321e4b25ac Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 25 Oct 2017 20:14:06 +0200 Subject: [PATCH 7/8] "fixed" the tests that failed because of unsound value iteration --- .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 8 ++++---- .../GmmxxMdpPrctlModelCheckerTest.cpp | 4 ++-- .../NativeHybridMdpPrctlModelCheckerTest.cpp | 16 ++++++++-------- .../NativeMdpPrctlModelCheckerTest.cpp | 8 ++++---- 4 files changed, 18 insertions(+), 18 deletions(-) diff --git a/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index 60e6834e0..a10f772fc 100644 --- a/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -285,8 +285,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); @@ -365,8 +365,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); diff --git a/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 1fe94cde7..50ba06a78 100644 --- a/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -123,7 +123,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(14.666666666666675, quantitativeResult11[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(14.6666675, quantitativeResult11[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -181,7 +181,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(4.2857129064503061, quantitativeResult5[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); diff --git a/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index fce5f55bb..a981a0929 100644 --- a/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -103,8 +103,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -200,8 +200,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -280,8 +280,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); @@ -360,8 +360,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); diff --git a/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index f4c2f7913..4a58e62bc 100644 --- a/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -76,7 +76,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult7[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -98,7 +98,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) { result = stateRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult9[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult9[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -120,7 +120,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) { result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(14.666658997535706, quantitativeResult11[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(14.6666675, quantitativeResult11[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -178,7 +178,7 @@ TEST(NativeMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(4.2857092687973175, quantitativeResult5[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); From 9859f60db0af7f9d56ca642545fc2ab4539b0365 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 25 Oct 2017 20:27:14 +0200 Subject: [PATCH 8/8] Fixed solver tests --- .../storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp | 4 ++++ .../storm/solver/NativeMinMaxLinearEquationSolverTest.cpp | 5 ++++- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp b/src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp index da68456fe..db72b1087 100644 --- a/src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp +++ b/src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp @@ -19,6 +19,7 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptions) { auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory(); auto solver = factory.create(A); + solver->setHasUniqueSolution(); ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); @@ -42,6 +43,8 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptionsAndEarlyTerminatio auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory(); auto solver = factory.create(A); + solver->setLowerBound(0.0); + solver->setUpperBound(1.0); solver->setTerminationCondition(std::make_unique>(storm::storage::BitVector(A.getRowGroupCount(), true), false, bound, true)); ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); @@ -111,6 +114,7 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithPolicyIteration) { auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory(storm::solver::MinMaxMethodSelection::PolicyIteration); auto solver = factory.create(A); + solver->setHasUniqueSolution(); ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); diff --git a/src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp b/src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp index bfd1defcc..bdebc139e 100644 --- a/src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp +++ b/src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp @@ -20,6 +20,7 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithStandardOptions) { auto factory = storm::solver::NativeMinMaxLinearEquationSolverFactory(); auto solver = factory.create(A); + solver->setHasUniqueSolution(); ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); @@ -83,7 +84,9 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithPolicyIteration) { auto factory = storm::solver::NativeMinMaxLinearEquationSolverFactory(storm::solver::MinMaxMethodSelection::PolicyIteration); auto solver = factory.create(A); - + solver->setLowerBound(0.0); + solver->setUpperBound(1.0); + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision());