From eb5d4100a62854842e065dda9b91459be4bbca87 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 27 Mar 2015 09:45:48 +0100 Subject: [PATCH] Renamed Nondeterminstic equation solver as this name is more than misleading. Former-commit-id: 7f08ed130c67981039e3077b4b72f34d8897b4f3 --- CMakeLists.txt | 4 +-- .../SMTMinimalCommandSetGenerator.h | 2 +- .../SparseMarkovAutomatonCslModelChecker.cpp | 18 +++++------ .../SparseMarkovAutomatonCslModelChecker.h | 8 ++--- .../prctl/SparseMdpPrctlModelChecker.cpp | 32 +++++++++---------- .../prctl/SparseMdpPrctlModelChecker.h | 10 +++--- ...pp => GmmxxMinMaxLinearEquationSolver.cpp} | 12 +++---- ...er.h => GmmxxMinMaxLinearEquationSolver.h} | 20 ++++++------ ...nSolver.h => MinMaxLinearEquationSolver.h} | 8 ++--- ...p => NativeMinMaxLinearEquationSolver.cpp} | 14 ++++---- ...r.h => NativeMinMaxLinearEquationSolver.h} | 20 ++++++------ ...TopologicalMinMaxLinearEquationSolver.cpp} | 16 +++++----- ...> TopologicalMinMaxLinearEquationSolver.h} | 20 ++++++------ src/storage/SparseMatrix.h | 4 +-- src/utility/solver.cpp | 32 +++++++++---------- src/utility/solver.h | 18 +++++------ .../GmmxxMdpPrctlModelCheckerTest.cpp | 8 ++--- .../SparseMdpPrctlModelCheckerTest.cpp | 8 ++--- ...ValueIterationMdpPrctlModelCheckerTest.cpp | 8 ++--- ...> GmmxxMinMaxLinearEquationSolverTest.cpp} | 12 +++---- ... NativeMinMaxLinearEquationSolverTest.cpp} | 12 +++---- .../GmmxxMdpPrctlModelCheckerTest.cpp | 4 +-- .../NativeMdpPrctlModelCheckerTest.cpp | 4 +-- ...ValueIterationMdpPrctlModelCheckerTest.cpp | 4 +-- 24 files changed, 149 insertions(+), 149 deletions(-) rename src/solver/{GmmxxNondeterministicLinearEquationSolver.cpp => GmmxxMinMaxLinearEquationSolver.cpp} (78%) rename src/solver/{GmmxxNondeterministicLinearEquationSolver.h => GmmxxMinMaxLinearEquationSolver.h} (69%) rename src/solver/{NondeterministicLinearEquationSolver.h => MinMaxLinearEquationSolver.h} (93%) rename src/solver/{NativeNondeterministicLinearEquationSolver.cpp => NativeMinMaxLinearEquationSolver.cpp} (81%) rename src/solver/{NativeNondeterministicLinearEquationSolver.h => NativeMinMaxLinearEquationSolver.h} (67%) rename src/solver/{TopologicalNondeterministicLinearEquationSolver.cpp => TopologicalMinMaxLinearEquationSolver.cpp} (93%) rename src/solver/{TopologicalNondeterministicLinearEquationSolver.h => TopologicalMinMaxLinearEquationSolver.h} (86%) rename test/functional/solver/{GmmxxNondeterministicLinearEquationSolverTest.cpp => GmmxxMinMaxLinearEquationSolverTest.cpp} (84%) rename test/functional/solver/{NativeNondeterministicLinearEquationSolverTest.cpp => NativeMinMaxLinearEquationSolverTest.cpp} (84%) diff --git a/CMakeLists.txt b/CMakeLists.txt index 9e7b240a5..6b37526c9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -417,7 +417,7 @@ file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PR file(GLOB STORM_FUNCTIONAL_TEST_MAIN_FILE ${STORM_CPP_TESTS_BASE_PATH}/functional/storm-functional-tests.cpp) file(GLOB_RECURSE STORM_FUNCTIONAL_TEST_FILES ${STORM_CPP_TESTS_BASE_PATH}/functional/*.h ${STORM_CPP_TESTS_BASE_PATH}/functional/*.cpp) file(GLOB STORM_PERFORMANCE_TEST_MAIN_FILE ${STORM_CPP_TESTS_BASE_PATH}/performance/storm-performance-tests.cpp) -file(GLOB_RECURSE STORM_PERFORMANCE_TEST_FILES ${STORM_CPP_TESTS_BASE_PATH}/performance/*/*.h ${STORM_CPP_TESTS_BASE_PATH}/performance/*/*.cpp) +file(GLOB_RECURSE STORM_PERFORMANCE_TEST_FILES ${STORM_CPP_TESTS_BASE_PATH}/performance/*.h ${STORM_CPP_TESTS_BASE_PATH}/performance/*.cpp) # Additional include files like the storm-config.h file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h) @@ -451,7 +451,7 @@ source_group(storage\\prism FILES ${STORM_STORAGE_PRISM_FILES}) source_group(storage\\sparse FILES ${STORM_STORAGE_SPARSE_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES}) source_group(functional-test FILES ${STORM_FUNCTIONAL_TEST_FILES}) -source_group(performance-test FILES ${STORM_PERFORMANCE_TEST_FILES}) +source_group(performance-test FILES ${STORM_PERFORMANCE_TEST_FILES} ${}) # Add custom additional include or link directories if (ADDITIONAL_INCLUDE_DIRS) diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index cdd04e8fd..a096810ed 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -10,7 +10,7 @@ #include "src/storage/expressions/Expression.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" +#include "src/solver/GmmxxMinMaxLinearEquationSolver.h" #include "src/utility/counterexamples.h" #include "src/utility/prism.h" diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 87fb93b00..04b36d823 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -21,12 +21,12 @@ namespace storm { namespace modelchecker { template - SparseMarkovAutomatonCslModelChecker::SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton const& model, std::unique_ptr>&& nondeterministicLinearEquationSolverFactory) : model(model), nondeterministicLinearEquationSolverFactory(std::move(nondeterministicLinearEquationSolverFactory)) { + SparseMarkovAutomatonCslModelChecker::SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton const& model, std::unique_ptr>&& MinMaxLinearEquationSolverFactory) : model(model), MinMaxLinearEquationSolverFactory(std::move(MinMaxLinearEquationSolverFactory)) { // Intentionally left empty. } template - SparseMarkovAutomatonCslModelChecker::SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton const& model) : model(model), nondeterministicLinearEquationSolverFactory(new storm::utility::solver::NondeterministicLinearEquationSolverFactory()) { + SparseMarkovAutomatonCslModelChecker::SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton const& model) : model(model), MinMaxLinearEquationSolverFactory(new storm::utility::solver::MinMaxLinearEquationSolverFactory()) { // Intentionally left empty. } @@ -36,7 +36,7 @@ namespace storm { } template - void SparseMarkovAutomatonCslModelChecker::computeBoundedReachabilityProbabilities(bool min, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::NondeterministicLinearEquationSolverFactory const& nondeterministicLinearEquationSolverFactory) { + void SparseMarkovAutomatonCslModelChecker::computeBoundedReachabilityProbabilities(bool min, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::MinMaxLinearEquationSolverFactory const& MinMaxLinearEquationSolverFactory) { // Start by computing four sparse matrices: // * a matrix aMarkovian with all (discretized) transitions from Markovian non-goal states to all Markovian non-goal states. // * a matrix aMarkovianToProbabilistic with all (discretized) transitions from Markovian non-goal states to all probabilistic non-goal states. @@ -89,7 +89,7 @@ namespace storm { } } - std::unique_ptr> solver = nondeterministicLinearEquationSolverFactory.create(aProbabilistic); + std::unique_ptr> solver = MinMaxLinearEquationSolverFactory.create(aProbabilistic); // Perform the actual value iteration // * loop until the step bound has been reached @@ -149,7 +149,7 @@ namespace storm { std::vector vProbabilistic(probabilisticNonGoalStates.getNumberOfSetBits()); std::vector vMarkovian(markovianNonGoalStates.getNumberOfSetBits()); - computeBoundedReachabilityProbabilities(minimize, transitionMatrix, exitRates, markovianStates, psiStates, markovianNonGoalStates, probabilisticNonGoalStates, vMarkovian, vProbabilistic, delta, numberOfSteps, *nondeterministicLinearEquationSolverFactory); + computeBoundedReachabilityProbabilities(minimize, transitionMatrix, exitRates, markovianStates, psiStates, markovianNonGoalStates, probabilisticNonGoalStates, vMarkovian, vProbabilistic, delta, numberOfSteps, *MinMaxLinearEquationSolverFactory); // (4) If the lower bound of interval was non-zero, we need to take the current values as the starting values for a subsequent value iteration. if (lowerBound != storm::utility::zero()) { @@ -167,7 +167,7 @@ namespace storm { STORM_LOG_INFO("Performing " << numberOfSteps << " iterations (delta=" << delta << ") for interval [0, " << lowerBound << "]." << std::endl); // Compute the bounded reachability for interval [0, b-a]. - computeBoundedReachabilityProbabilities(minimize, transitionMatrix, exitRates, markovianStates, storm::storage::BitVector(model.getNumberOfStates()), markovianStates, ~markovianStates, vAllMarkovian, vAllProbabilistic, delta, numberOfSteps, *nondeterministicLinearEquationSolverFactory); + computeBoundedReachabilityProbabilities(minimize, transitionMatrix, exitRates, markovianStates, storm::storage::BitVector(model.getNumberOfStates()), markovianStates, ~markovianStates, vAllMarkovian, vAllProbabilistic, delta, numberOfSteps, *MinMaxLinearEquationSolverFactory); // Create the result vector out of vAllProbabilistic and vAllMarkovian and return it. std::vector result(model.getNumberOfStates()); @@ -198,7 +198,7 @@ namespace storm { template std::vector SparseMarkovAutomatonCslModelChecker::computeUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const { - return storm::modelchecker::SparseMdpPrctlModelChecker::computeUntilProbabilitiesHelper(minimize, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, *nondeterministicLinearEquationSolverFactory, qualitative); + return storm::modelchecker::SparseMdpPrctlModelChecker::computeUntilProbabilitiesHelper(minimize, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, *MinMaxLinearEquationSolverFactory, qualitative); } template @@ -379,7 +379,7 @@ namespace storm { storm::storage::SparseMatrix sspMatrix = sspMatrixBuilder.build(currentChoice); std::vector x(numberOfStatesNotInMecs + mecDecomposition.size()); - std::unique_ptr> solver = nondeterministicLinearEquationSolverFactory->create(sspMatrix); + std::unique_ptr> solver = MinMaxLinearEquationSolverFactory->create(sspMatrix); solver->solveEquationSystem(minimize, x, b); // Prepare result vector. @@ -563,7 +563,7 @@ namespace storm { storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, model.getNondeterministicChoiceIndices(), rewardValues); // Solve the corresponding system of equations. - std::unique_ptr> solver = nondeterministicLinearEquationSolverFactory->create(submatrix); + std::unique_ptr> solver = MinMaxLinearEquationSolverFactory->create(submatrix); solver->solveEquationSystem(minimize, x, b); // Create resulting vector. diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 4c29dc743..cd51608eb 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -5,7 +5,7 @@ #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/models/sparse/MarkovAutomaton.h" #include "src/storage/MaximalEndComponentDecomposition.h" -#include "src/solver/NondeterministicLinearEquationSolver.h" +#include "src/solver/MinMaxLinearEquationSolver.h" #include "src/utility/solver.h" namespace storm { @@ -14,7 +14,7 @@ namespace storm { template class SparseMarkovAutomatonCslModelChecker : public AbstractModelChecker { public: - explicit SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton const& model, std::unique_ptr>&& nondeterministicLinearEquationSolver); + explicit SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton const& model, std::unique_ptr>&& MinMaxLinearEquationSolver); explicit SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton const& model); // The implemented methods of the AbstractModelChecker interface. @@ -30,7 +30,7 @@ namespace storm { private: // The methods that perform the actual checking. std::vector computeBoundedUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& psiStates, std::pair const& boundsPair) const; - static void computeBoundedReachabilityProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::NondeterministicLinearEquationSolverFactory const& nondeterministicLinearEquationSolverFactory); + static void computeBoundedReachabilityProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::MinMaxLinearEquationSolverFactory const& MinMaxLinearEquationSolverFactory); std::vector computeUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const; std::vector computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const; std::vector computeLongRunAverageHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const; @@ -67,7 +67,7 @@ namespace storm { storm::models::sparse::MarkovAutomaton const& model; // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices. - std::unique_ptr> nondeterministicLinearEquationSolverFactory; + std::unique_ptr> MinMaxLinearEquationSolverFactory; }; } } diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 8b5975aca..516090698 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -16,12 +16,12 @@ namespace storm { namespace modelchecker { template - SparseMdpPrctlModelChecker::SparseMdpPrctlModelChecker(storm::models::sparse::Mdp const& model) : SparsePropositionalModelChecker(model), nondeterministicLinearEquationSolverFactory(new storm::utility::solver::NondeterministicLinearEquationSolverFactory()) { + SparseMdpPrctlModelChecker::SparseMdpPrctlModelChecker(storm::models::sparse::Mdp const& model) : SparsePropositionalModelChecker(model), MinMaxLinearEquationSolverFactory(new storm::utility::solver::MinMaxLinearEquationSolverFactory()) { // Intentionally left empty. } template - SparseMdpPrctlModelChecker::SparseMdpPrctlModelChecker(storm::models::sparse::Mdp const& model, std::unique_ptr>&& nondeterministicLinearEquationSolverFactory) : SparsePropositionalModelChecker(model), nondeterministicLinearEquationSolverFactory(std::move(nondeterministicLinearEquationSolverFactory)) { + SparseMdpPrctlModelChecker::SparseMdpPrctlModelChecker(storm::models::sparse::Mdp const& model, std::unique_ptr>&& MinMaxLinearEquationSolverFactory) : SparsePropositionalModelChecker(model), MinMaxLinearEquationSolverFactory(std::move(MinMaxLinearEquationSolverFactory)) { // Intentionally left empty. } @@ -57,8 +57,8 @@ namespace storm { std::vector subresult(statesWithProbabilityGreater0.getNumberOfSetBits()); storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::one()); - STORM_LOG_THROW(nondeterministicLinearEquationSolverFactory != nullptr, storm::exceptions::InvalidStateException, "No valid equation solver available."); - std::unique_ptr> solver = nondeterministicLinearEquationSolverFactory->create(submatrix); + STORM_LOG_THROW(MinMaxLinearEquationSolverFactory != nullptr, storm::exceptions::InvalidStateException, "No valid equation solver available."); + std::unique_ptr> solver = MinMaxLinearEquationSolverFactory->create(submatrix); solver->performMatrixVectorMultiplication(minimize, subresult, nullptr, stepBound); // Set the values of the resulting vector accordingly. @@ -86,8 +86,8 @@ namespace storm { std::vector result(this->getModel().getNumberOfStates()); storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one()); - STORM_LOG_THROW(nondeterministicLinearEquationSolverFactory != nullptr, storm::exceptions::InvalidStateException, "No valid equation solver available."); - std::unique_ptr> solver = nondeterministicLinearEquationSolverFactory->create(this->getModel().getTransitionMatrix()); + STORM_LOG_THROW(MinMaxLinearEquationSolverFactory != nullptr, storm::exceptions::InvalidStateException, "No valid equation solver available."); + std::unique_ptr> solver = MinMaxLinearEquationSolverFactory->create(this->getModel().getTransitionMatrix()); solver->performMatrixVectorMultiplication(minimize, result); return result; @@ -103,11 +103,11 @@ namespace storm { template std::vector SparseMdpPrctlModelChecker::computeUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const { - return computeUntilProbabilitiesHelper(minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), phiStates, psiStates, *nondeterministicLinearEquationSolverFactory, qualitative); + return computeUntilProbabilitiesHelper(minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), phiStates, psiStates, *MinMaxLinearEquationSolverFactory, qualitative); } template - std::vector SparseMdpPrctlModelChecker::computeUntilProbabilitiesHelper(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::utility::solver::NondeterministicLinearEquationSolverFactory const& nondeterministicLinearEquationSolverFactory, bool qualitative) { + std::vector SparseMdpPrctlModelChecker::computeUntilProbabilitiesHelper(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& MinMaxLinearEquationSolverFactory, bool qualitative) { size_t numberOfStates = phiStates.size(); // We need to identify the states which have to be taken out of the matrix, i.e. @@ -148,7 +148,7 @@ namespace storm { std::vector x(maybeStates.getNumberOfSetBits()); // Solve the corresponding system of equations. - std::unique_ptr> solver = nondeterministicLinearEquationSolverFactory.create(submatrix); + std::unique_ptr> solver = MinMaxLinearEquationSolverFactory.create(submatrix); solver->solveEquationSystem(minimize, x, b); // Set values of resulting vector according to result. @@ -170,7 +170,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(SparseMdpPrctlModelChecker::computeUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), *nondeterministicLinearEquationSolverFactory, qualitative))); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(SparseMdpPrctlModelChecker::computeUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), *MinMaxLinearEquationSolverFactory, qualitative))); } template @@ -197,7 +197,7 @@ namespace storm { result.resize(this->getModel().getNumberOfStates()); } - std::unique_ptr> solver = nondeterministicLinearEquationSolverFactory->create(this->getModel().getTransitionMatrix()); + std::unique_ptr> solver = MinMaxLinearEquationSolverFactory->create(this->getModel().getTransitionMatrix()); solver->performMatrixVectorMultiplication(minimize, result, &totalRewardVector, stepBound); return result; @@ -218,8 +218,8 @@ namespace storm { // Initialize result to state rewards of the this->getModel(). std::vector result(this->getModel().getStateRewardVector()); - STORM_LOG_THROW(nondeterministicLinearEquationSolverFactory != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available."); - std::unique_ptr> solver = nondeterministicLinearEquationSolverFactory->create(this->getModel().getTransitionMatrix()); + STORM_LOG_THROW(MinMaxLinearEquationSolverFactory != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available."); + std::unique_ptr> solver = MinMaxLinearEquationSolverFactory->create(this->getModel().getTransitionMatrix()); solver->performMatrixVectorMultiplication(minimize, result, nullptr, stepCount); return result; @@ -233,7 +233,7 @@ namespace storm { } template - std::vector SparseMdpPrctlModelChecker::computeReachabilityRewardsHelper(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, boost::optional> const& stateRewardVector, boost::optional> const& transitionRewardMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::utility::solver::NondeterministicLinearEquationSolverFactory const& nondeterministicLinearEquationSolverFactory, bool qualitative) const { + std::vector SparseMdpPrctlModelChecker::computeReachabilityRewardsHelper(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, boost::optional> const& stateRewardVector, boost::optional> const& transitionRewardMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& MinMaxLinearEquationSolverFactory, bool qualitative) const { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(stateRewardVector || transitionRewardMatrix, storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -299,7 +299,7 @@ namespace storm { std::vector x(maybeStates.getNumberOfSetBits()); // Solve the corresponding system of equations. - std::unique_ptr> solver = nondeterministicLinearEquationSolverFactory.create(submatrix); + std::unique_ptr> solver = MinMaxLinearEquationSolverFactory.create(submatrix); solver->solveEquationSystem(minimize, x, b); // Set values of resulting vector according to result. @@ -318,7 +318,7 @@ namespace storm { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic."); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeReachabilityRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getOptionalStateRewardVector(), this->getModel().getOptionalTransitionRewardMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), *this->nondeterministicLinearEquationSolverFactory, qualitative))); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeReachabilityRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getOptionalStateRewardVector(), this->getModel().getOptionalTransitionRewardMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), *this->MinMaxLinearEquationSolverFactory, qualitative))); } template diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index b712f1f2f..6246b846c 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -4,7 +4,7 @@ #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "src/models/sparse/Mdp.h" #include "src/utility/solver.h" -#include "src/solver/NondeterministicLinearEquationSolver.h" +#include "src/solver/MinMaxLinearEquationSolver.h" namespace storm { namespace counterexamples { @@ -29,7 +29,7 @@ namespace storm { friend class storm::counterexamples::MILPMinimalLabelSetGenerator; explicit SparseMdpPrctlModelChecker(storm::models::sparse::Mdp const& model); - explicit SparseMdpPrctlModelChecker(storm::models::sparse::Mdp const& model, std::unique_ptr>&& nondeterministicLinearEquationSolverFactory); + explicit SparseMdpPrctlModelChecker(storm::models::sparse::Mdp const& model, std::unique_ptr>&& MinMaxLinearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; @@ -48,13 +48,13 @@ namespace storm { std::vector computeBoundedUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound) const; std::vector computeNextProbabilitiesHelper(bool minimize, storm::storage::BitVector const& nextStates); std::vector computeUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const; - static std::vector computeUntilProbabilitiesHelper(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::utility::solver::NondeterministicLinearEquationSolverFactory const& nondeterministicLinearEquationSolverFactory, bool qualitative); + static std::vector computeUntilProbabilitiesHelper(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& MinMaxLinearEquationSolverFactory, bool qualitative); std::vector computeInstantaneousRewardsHelper(bool minimize, uint_fast64_t stepCount) const; std::vector computeCumulativeRewardsHelper(bool minimize, uint_fast64_t stepBound) const; - std::vector computeReachabilityRewardsHelper(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, boost::optional> const& stateRewardVector, boost::optional> const& transitionRewardMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::utility::solver::NondeterministicLinearEquationSolverFactory const& nondeterministicLinearEquationSolverFactory, bool qualitative) const; + std::vector computeReachabilityRewardsHelper(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, boost::optional> const& stateRewardVector, boost::optional> const& transitionRewardMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& MinMaxLinearEquationSolverFactory, bool qualitative) const; // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices. - std::unique_ptr> nondeterministicLinearEquationSolverFactory; + std::unique_ptr> MinMaxLinearEquationSolverFactory; }; } // namespace modelchecker } // namespace storm diff --git a/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp similarity index 78% rename from src/solver/GmmxxNondeterministicLinearEquationSolver.cpp rename to src/solver/GmmxxMinMaxLinearEquationSolver.cpp index 6f78f3caa..3b349d2ff 100644 --- a/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp @@ -1,4 +1,4 @@ -#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" +#include "src/solver/GmmxxMinMaxLinearEquationSolver.h" #include @@ -10,7 +10,7 @@ namespace storm { namespace solver { template - GmmxxNondeterministicLinearEquationSolver::GmmxxNondeterministicLinearEquationSolver(storm::storage::SparseMatrix const& A) : gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()) { + GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A) : gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()) { // Get the settings object to customize solving. storm::settings::modules::GmmxxEquationSolverSettings const& settings = storm::settings::gmmxxEquationSolverSettings(); @@ -21,13 +21,13 @@ namespace storm { } template - GmmxxNondeterministicLinearEquationSolver::GmmxxNondeterministicLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()), precision(precision), relative(relative), maximalNumberOfIterations(maximalNumberOfIterations) { + GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()), precision(precision), relative(relative), maximalNumberOfIterations(maximalNumberOfIterations) { // Intentionally left empty. } template - void GmmxxNondeterministicLinearEquationSolver::solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { + void GmmxxMinMaxLinearEquationSolver::solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { // Set up the environment for the power method. If scratch memory was not provided, we need to create it. bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { @@ -92,7 +92,7 @@ namespace storm { } template - void GmmxxNondeterministicLinearEquationSolver::performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { + void GmmxxMinMaxLinearEquationSolver::performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { multiplyResult = new std::vector(gmmxxMatrix->nr); @@ -120,6 +120,6 @@ namespace storm { } // Explicitly instantiate the solver. - template class GmmxxNondeterministicLinearEquationSolver; + template class GmmxxMinMaxLinearEquationSolver; } // namespace solver } // namespace storm diff --git a/src/solver/GmmxxNondeterministicLinearEquationSolver.h b/src/solver/GmmxxMinMaxLinearEquationSolver.h similarity index 69% rename from src/solver/GmmxxNondeterministicLinearEquationSolver.h rename to src/solver/GmmxxMinMaxLinearEquationSolver.h index 2d87c60ca..951ae2578 100644 --- a/src/solver/GmmxxNondeterministicLinearEquationSolver.h +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.h @@ -1,29 +1,29 @@ -#ifndef STORM_SOLVER_GMMXXNONDETERMINISTICLINEAREQUATIONSOLVER_H_ -#define STORM_SOLVER_GMMXXNONDETERMINISTICLINEAREQUATIONSOLVER_H_ +#ifndef STORM_SOLVER_GMMXXMINMAXLINEAREQUATIONSOLVER_H_ +#define STORM_SOLVER_GMMXXMINMAXLINEAREQUATIONSOLVER_H_ #include "gmm/gmm_matrix.h" -#include "src/solver/NondeterministicLinearEquationSolver.h" +#include "src/solver/MinMaxLinearEquationSolver.h" namespace storm { namespace solver { /*! - * A class that uses the gmm++ library to implement the NondeterministicLinearEquationSolver interface. + * A class that uses the gmm++ library to implement the MinMaxLinearEquationSolver interface. */ template - class GmmxxNondeterministicLinearEquationSolver : public NondeterministicLinearEquationSolver { + class GmmxxMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver { public: /*! - * Constructs a nondeterministic linear equation solver with parameters being set according to the settings + * Constructs a min/max linear equation solver with parameters being set according to the settings * object. * * @param A The matrix defining the coefficients of the linear equation system. */ - GmmxxNondeterministicLinearEquationSolver(storm::storage::SparseMatrix const& A); + GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A); /*! - * Constructs a nondeterminstic linear equation solver with the given parameters. + * Constructs a min/max linear equation solver with the given parameters. * * @param A The matrix defining the coefficients of the linear equation system. * @param precision The precision to use for convergence detection. @@ -31,7 +31,7 @@ namespace storm { * @param relative If set, the relative error rather than the absolute error is considered for convergence * detection. */ - GmmxxNondeterministicLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true); + GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true); virtual void performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; @@ -56,4 +56,4 @@ namespace storm { } // namespace solver } // namespace storm -#endif /* STORM_SOLVER_GMMXXNONDETERMINISTICLINEAREQUATIONSOLVER_H_ */ \ No newline at end of file +#endif /* STORM_SOLVER_GMMXXMINMAXLINEAREQUATIONSOLVER_H_ */ \ No newline at end of file diff --git a/src/solver/NondeterministicLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h similarity index 93% rename from src/solver/NondeterministicLinearEquationSolver.h rename to src/solver/MinMaxLinearEquationSolver.h index 28751d87a..8b69058cf 100644 --- a/src/solver/NondeterministicLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -1,5 +1,5 @@ -#ifndef STORM_SOLVER_NONDETERMINISTICLINEAREQUATIONSOLVER_H_ -#define STORM_SOLVER_NONDETERMINISTICLINEAREQUATIONSOLVER_H_ +#ifndef STORM_SOLVER_MINMAXLINEAREQUATIONSOLVER_H_ +#define STORM_SOLVER_MINMAXLINEAREQUATIONSOLVER_H_ #include @@ -14,7 +14,7 @@ namespace storm { * provided. */ template - class NondeterministicLinearEquationSolver { + class MinMaxLinearEquationSolver { public: /*! * Solves the equation system x = min/max(A*x + b) given by the parameters. Note that the matrix A has @@ -56,4 +56,4 @@ namespace storm { } // namespace solver } // namespace storm -#endif /* STORM_SOLVER_NONDETERMINISTICLINEAREQUATIONSOLVER_H_ */ +#endif /* STORM_SOLVER_MINMAXLINEAREQUATIONSOLVER_H_ */ diff --git a/src/solver/NativeNondeterministicLinearEquationSolver.cpp b/src/solver/NativeMinMaxLinearEquationSolver.cpp similarity index 81% rename from src/solver/NativeNondeterministicLinearEquationSolver.cpp rename to src/solver/NativeMinMaxLinearEquationSolver.cpp index 7965c9dda..48ef291c7 100644 --- a/src/solver/NativeNondeterministicLinearEquationSolver.cpp +++ b/src/solver/NativeMinMaxLinearEquationSolver.cpp @@ -1,4 +1,4 @@ -#include "src/solver/NativeNondeterministicLinearEquationSolver.h" +#include "src/solver/NativeMinMaxLinearEquationSolver.h" #include @@ -9,7 +9,7 @@ namespace storm { namespace solver { template - NativeNondeterministicLinearEquationSolver::NativeNondeterministicLinearEquationSolver(storm::storage::SparseMatrix const& A) : A(A) { + NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A) : A(A) { // Get the settings object to customize solving. storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); @@ -20,12 +20,12 @@ namespace storm { } template - NativeNondeterministicLinearEquationSolver::NativeNondeterministicLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), precision(precision), relative(relative), maximalNumberOfIterations(maximalNumberOfIterations) { + NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), precision(precision), relative(relative), maximalNumberOfIterations(maximalNumberOfIterations) { // Intentionally left empty. } template - void NativeNondeterministicLinearEquationSolver::solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { + void NativeMinMaxLinearEquationSolver::solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { // Set up the environment for the power method. If scratch memory was not provided, we need to create it. bool multiplyResultMemoryProvided = true; @@ -91,7 +91,7 @@ namespace storm { } template - void NativeNondeterministicLinearEquationSolver::performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { + void NativeMinMaxLinearEquationSolver::performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { // If scratch memory was not provided, we need to create it. bool multiplyResultMemoryProvided = true; @@ -124,7 +124,7 @@ namespace storm { } // Explicitly instantiate the solver. - template class NativeNondeterministicLinearEquationSolver; - template class NativeNondeterministicLinearEquationSolver; + template class NativeMinMaxLinearEquationSolver; + template class NativeMinMaxLinearEquationSolver; } // namespace solver } // namespace storm diff --git a/src/solver/NativeNondeterministicLinearEquationSolver.h b/src/solver/NativeMinMaxLinearEquationSolver.h similarity index 67% rename from src/solver/NativeNondeterministicLinearEquationSolver.h rename to src/solver/NativeMinMaxLinearEquationSolver.h index b70a3b03d..9044f5ca8 100644 --- a/src/solver/NativeNondeterministicLinearEquationSolver.h +++ b/src/solver/NativeMinMaxLinearEquationSolver.h @@ -1,27 +1,27 @@ -#ifndef STORM_SOLVER_NATIVENONDETERMINISTICLINEAREQUATIONSOLVER_H_ -#define STORM_SOLVER_NATIVENONDETERMINISTICLINEAREQUATIONSOLVER_H_ +#ifndef STORM_SOLVER_NATIVEMINMAXLINEAREQUATIONSOLVER_H_ +#define STORM_SOLVER_NATIVEMINMAXLINEAREQUATIONSOLVER_H_ -#include "src/solver/NondeterministicLinearEquationSolver.h" +#include "src/solver/MinMaxLinearEquationSolver.h" namespace storm { namespace solver { /*! - * A class that uses the gmm++ library to implement the NondeterminsticLinearEquationSolver interface. + * A class that uses the gmm++ library to implement the MinMaxLinearEquationSolver interface. */ template - class NativeNondeterministicLinearEquationSolver : public NondeterministicLinearEquationSolver { + class NativeMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver { public: /*! - * Constructs a nondeterministic linear equation solver with parameters being set according to the settings + * Constructs a min/max linear equation solver with parameters being set according to the settings * object. * * @param A The matrix defining the coefficients of the linear equation system. */ - NativeNondeterministicLinearEquationSolver(storm::storage::SparseMatrix const& A); + NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A); /*! - * Constructs a nondeterminstic linear equation solver with the given parameters. + * Constructs a min/max linear equation solver with the given parameters. * * @param A The matrix defining the coefficients of the linear equation system. * @param precision The precision to use for convergence detection. @@ -29,7 +29,7 @@ namespace storm { * @param relative If set, the relative error rather than the absolute error is considered for convergence * detection. */ - NativeNondeterministicLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true); + NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true); virtual void performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* newX = nullptr) const override; @@ -51,4 +51,4 @@ namespace storm { } // namespace solver } // namespace storm -#endif /* STORM_SOLVER_NATIVENONDETERMINISTICLINEAREQUATIONSOLVER_H_ */ +#endif /* STORM_SOLVER_NATIVEMINMAXLINEAREQUATIONSOLVER_H_ */ diff --git a/src/solver/TopologicalNondeterministicLinearEquationSolver.cpp b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp similarity index 93% rename from src/solver/TopologicalNondeterministicLinearEquationSolver.cpp rename to src/solver/TopologicalMinMaxLinearEquationSolver.cpp index fda2998f2..66de10ed9 100644 --- a/src/solver/TopologicalNondeterministicLinearEquationSolver.cpp +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -1,4 +1,4 @@ -#include "src/solver/TopologicalNondeterministicLinearEquationSolver.h" +#include "src/solver/TopologicalMinMaxLinearEquationSolver.h" #include #include @@ -23,7 +23,7 @@ namespace storm { namespace solver { template - TopologicalNondeterministicLinearEquationSolver::TopologicalNondeterministicLinearEquationSolver(storm::storage::SparseMatrix const& A) : NativeNondeterministicLinearEquationSolver(A) { + TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A) : NativeMinMaxLinearEquationSolver(A) { // Get the settings object to customize solving. //storm::settings::Settings* settings = storm::settings::Settings::getInstance(); @@ -44,12 +44,12 @@ namespace storm { } template - TopologicalNondeterministicLinearEquationSolver::TopologicalNondeterministicLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : NativeNondeterministicLinearEquationSolver(A, precision, maximalNumberOfIterations, relative) { + TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : NativeMinMaxLinearEquationSolver(A, precision, maximalNumberOfIterations, relative) { // Intentionally left empty. } template - void TopologicalNondeterministicLinearEquationSolver::solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { + void TopologicalMinMaxLinearEquationSolver::solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { #ifdef GPU_USE_FLOAT #define __FORCE_FLOAT_CALCULATION true @@ -60,7 +60,7 @@ namespace storm { // FIXME: This actually allocates quite some storage, because of this conversion, is it really necessary? storm::storage::SparseMatrix newA = this->A.template toValueType(); - TopologicalNondeterministicLinearEquationSolver newSolver(newA, this->precision, this->maximalNumberOfIterations, this->relative); + TopologicalMinMaxLinearEquationSolver newSolver(newA, this->precision, this->maximalNumberOfIterations, this->relative); std::vector new_x = storm::utility::vector::toValueType(x); std::vector const new_b = storm::utility::vector::toValueType(b); @@ -322,7 +322,7 @@ namespace storm { template std::vector> - TopologicalNondeterministicLinearEquationSolver::getOptimalGroupingFromTopologicalSccDecomposition(storm::storage::StronglyConnectedComponentDecomposition const& sccDecomposition, std::vector const& topologicalSort, storm::storage::SparseMatrix const& matrix) const { + TopologicalMinMaxLinearEquationSolver::getOptimalGroupingFromTopologicalSccDecomposition(storm::storage::StronglyConnectedComponentDecomposition const& sccDecomposition, std::vector const& topologicalSort, storm::storage::SparseMatrix const& matrix) const { std::vector> result; #ifdef STORM_HAVE_CUDA // 95% to have a bit of padding @@ -459,7 +459,7 @@ namespace storm { } // Explicitly instantiate the solver. - template class TopologicalNondeterministicLinearEquationSolver; - template class TopologicalNondeterministicLinearEquationSolver; + template class TopologicalMinMaxLinearEquationSolver; + template class TopologicalMinMaxLinearEquationSolver; } // namespace solver } // namespace storm diff --git a/src/solver/TopologicalNondeterministicLinearEquationSolver.h b/src/solver/TopologicalMinMaxLinearEquationSolver.h similarity index 86% rename from src/solver/TopologicalNondeterministicLinearEquationSolver.h rename to src/solver/TopologicalMinMaxLinearEquationSolver.h index c8eed7a99..4f748672c 100644 --- a/src/solver/TopologicalNondeterministicLinearEquationSolver.h +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.h @@ -1,7 +1,7 @@ -#ifndef STORM_SOLVER_TOPOLOGICALVALUEITERATIONNONDETERMINISTICLINEAREQUATIONSOLVER_H_ -#define STORM_SOLVER_TOPOLOGICALVALUEITERATIONNONDETERMINISTICLINEAREQUATIONSOLVER_H_ +#ifndef STORM_SOLVER_TOPOLOGICALVALUEITERATIONMINMAXLINEAREQUATIONSOLVER_H_ +#define STORM_SOLVER_TOPOLOGICALVALUEITERATIONMINMAXLINEAREQUATIONSOLVER_H_ -#include "src/solver/NativeNondeterministicLinearEquationSolver.h" +#include "src/solver/NativeMinMaxLinearEquationSolver.h" #include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/storage/SparseMatrix.h" #include "src/exceptions/NotImplementedException.h" @@ -19,21 +19,21 @@ namespace storm { namespace solver { /*! - * A class that uses SCC Decompositions to solve a linear equation system. + * A class that uses SCC Decompositions to solve a min/max linear equation system. */ template - class TopologicalNondeterministicLinearEquationSolver : public NativeNondeterministicLinearEquationSolver { + class TopologicalMinMaxLinearEquationSolver : public NativeMinMaxLinearEquationSolver { public: /*! - * Constructs a nondeterministic linear equation solver with parameters being set according to the settings + * Constructs a min-max linear equation solver with parameters being set according to the settings * object. * * @param A The matrix defining the coefficients of the linear equation system. */ - TopologicalNondeterministicLinearEquationSolver(storm::storage::SparseMatrix const& A); + TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A); /*! - * Constructs a nondeterminstic linear equation solver with the given parameters. + * Constructs a min/max linear equation solver with the given parameters. * * @param A The matrix defining the coefficients of the linear equation system. * @param precision The precision to use for convergence detection. @@ -41,7 +41,7 @@ namespace storm { * @param relative If set, the relative error rather than the absolute error is considered for convergence * detection. */ - TopologicalNondeterministicLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true); + TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true); virtual void solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; private: @@ -99,4 +99,4 @@ namespace storm { } // namespace solver } // namespace storm -#endif /* STORM_SOLVER_NATIVENONDETERMINISTICLINEAREQUATIONSOLVER_H_ */ +#endif /* STORM_SOLVER_TOPOLOGICALVALUEITERATIONMINMAXLINEAREQUATIONSOLVER_H_ */ diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 954a9837d..1bac30a6c 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -24,7 +24,7 @@ namespace storm { } namespace solver { template - class TopologicalValueIterationNondeterministicLinearEquationSolver; + class TopologicalValueIterationMinMaxLinearEquationSolver; } } @@ -276,7 +276,7 @@ namespace storm { friend class storm::adapters::GmmxxAdapter; friend class storm::adapters::EigenAdapter; friend class storm::adapters::StormAdapter; - friend class storm::solver::TopologicalValueIterationNondeterministicLinearEquationSolver; + friend class storm::solver::TopologicalValueIterationMinMaxLinearEquationSolver; typedef uint_fast64_t index_type; typedef ValueType value_type; diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 76429ebdf..2d2c0cdcb 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -5,9 +5,9 @@ #include "src/solver/NativeLinearEquationSolver.h" #include "src/solver/GmmxxLinearEquationSolver.h" -#include "src/solver/NativeNondeterministicLinearEquationSolver.h" -#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" -#include "src/solver/TopologicalNondeterministicLinearEquationSolver.h" +#include "src/solver/NativeMinMaxLinearEquationSolver.h" +#include "src/solver/GmmxxMinMaxLinearEquationSolver.h" +#include "src/solver/TopologicalMinMaxLinearEquationSolver.h" #include "src/solver/GurobiLpSolver.h" #include "src/solver/GlpkLpSolver.h" @@ -35,27 +35,27 @@ namespace storm { } template - std::unique_ptr> NondeterministicLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { + std::unique_ptr> MinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { storm::settings::modules::GeneralSettings::EquationSolver equationSolver = storm::settings::generalSettings().getEquationSolver(); switch (equationSolver) { - case storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx: return std::unique_ptr>(new storm::solver::GmmxxNondeterministicLinearEquationSolver(matrix)); - case storm::settings::modules::GeneralSettings::EquationSolver::Native: return std::unique_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver(matrix)); + case storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx: return std::unique_ptr>(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix)); + case storm::settings::modules::GeneralSettings::EquationSolver::Native: return std::unique_ptr>(new storm::solver::NativeMinMaxLinearEquationSolver(matrix)); } } template - std::unique_ptr> GmmxxNondeterministicLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::unique_ptr>(new storm::solver::GmmxxNondeterministicLinearEquationSolver(matrix)); + std::unique_ptr> GmmxxMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { + return std::unique_ptr>(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix)); } template - std::unique_ptr> NativeNondeterministicLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::unique_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver(matrix)); + std::unique_ptr> NativeMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { + return std::unique_ptr>(new storm::solver::NativeMinMaxLinearEquationSolver(matrix)); } template - std::unique_ptr> TopologicalNondeterministicLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::unique_ptr>(new storm::solver::TopologicalNondeterministicLinearEquationSolver(matrix)); + std::unique_ptr> TopologicalMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { + return std::unique_ptr>(new storm::solver::TopologicalMinMaxLinearEquationSolver(matrix)); } std::unique_ptr LpSolverFactory::create(std::string const& name) const { @@ -82,10 +82,10 @@ namespace storm { template class LinearEquationSolverFactory; template class GmmxxLinearEquationSolverFactory; template class NativeLinearEquationSolverFactory; - template class NondeterministicLinearEquationSolverFactory; - template class GmmxxNondeterministicLinearEquationSolverFactory; - template class NativeNondeterministicLinearEquationSolverFactory; - template class TopologicalNondeterministicLinearEquationSolverFactory; + template class MinMaxLinearEquationSolverFactory; + template class GmmxxMinMaxLinearEquationSolverFactory; + template class NativeMinMaxLinearEquationSolverFactory; + template class TopologicalMinMaxLinearEquationSolverFactory; } } } \ No newline at end of file diff --git a/src/utility/solver.h b/src/utility/solver.h index d9f934c98..a72bbdbb1 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -2,7 +2,7 @@ #define STORM_UTILITY_SOLVER_H_ #include "src/solver/LinearEquationSolver.h" -#include "src/solver/NondeterministicLinearEquationSolver.h" +#include "src/solver/MinMaxLinearEquationSolver.h" #include "src/solver/LpSolver.h" #include "src/exceptions/InvalidSettingsException.h" @@ -35,30 +35,30 @@ namespace storm { }; template - class NondeterministicLinearEquationSolverFactory { + class MinMaxLinearEquationSolverFactory { public: /*! * Creates a new nondeterministic linear equation solver instance with the given matrix. */ - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const; + virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const; }; template - class NativeNondeterministicLinearEquationSolverFactory : public NondeterministicLinearEquationSolverFactory { + class NativeMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; + virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; }; template - class GmmxxNondeterministicLinearEquationSolverFactory : public NondeterministicLinearEquationSolverFactory { + class GmmxxMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; + virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; }; template - class TopologicalNondeterministicLinearEquationSolverFactory : public NondeterministicLinearEquationSolverFactory { + class TopologicalMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; + virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; }; class LpSolverFactory { diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 0c45cb83d..41eade466 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -18,7 +18,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("two"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -90,7 +90,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateRewardMdp = abstractModel->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker stateRewardModelChecker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker stateRewardModelChecker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); labelFormula = std::make_shared("done"); reachabilityRewardFormula = std::make_shared(labelFormula); @@ -114,7 +114,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::GmmxxNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); labelFormula = std::make_shared("done"); reachabilityRewardFormula = std::make_shared(labelFormula); @@ -143,7 +143,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(3172ull, mdp->getNumberOfStates()); ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("elected"); auto eventuallyFormula = std::make_shared(labelFormula); diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index 2587ceafd..c12baf505 100644 --- a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -18,7 +18,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("two"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -90,7 +90,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateRewardMdp = abstractModel->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::NativeNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); labelFormula = std::make_shared("done"); reachabilityRewardFormula = std::make_shared(labelFormula); @@ -114,7 +114,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::NativeNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); labelFormula = std::make_shared("done"); reachabilityRewardFormula = std::make_shared(labelFormula); @@ -143,7 +143,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(3172ull, mdp->getNumberOfStates()); ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("elected"); auto eventuallyFormula = std::make_shared(labelFormula); diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index 932516c34..4920fe746 100644 --- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -19,7 +19,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - storm::modelchecker::SparseMdpPrctlModelChecker mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); //storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("two"); auto apFormula = std::make_shared("two"); @@ -137,7 +137,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { // ------------- state rewards -------------- std::shared_ptr> stateRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "")->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::TopologicalNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); apFormula = std::make_shared("done"); reachabilityRewardFormula = std::make_shared(apFormula); @@ -172,7 +172,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { // -------------------------------- state and transition reward ------------------------ std::shared_ptr> stateAndTransitionRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew")->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::TopologicalNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); apFormula = std::make_shared("done"); @@ -212,7 +212,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(mdp->getNumberOfStates(), 3172ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull); - storm::modelchecker::SparseMdpPrctlModelChecker mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); auto apFormula = std::make_shared("elected"); auto eventuallyFormula = std::make_shared(apFormula); diff --git a/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp similarity index 84% rename from test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp rename to test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp index 0441ebbbf..56357f546 100644 --- a/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp +++ b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp @@ -1,10 +1,10 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" +#include "src/solver/GmmxxMinMaxLinearEquationSolver.h" #include "src/settings/SettingsManager.h" -TEST(GmmxxNondeterministicLinearEquationSolver, SolveWithStandardOptions) { +TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptions) { storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true); ASSERT_NO_THROW(builder.newRowGroup(0)); ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); @@ -15,7 +15,7 @@ TEST(GmmxxNondeterministicLinearEquationSolver, SolveWithStandardOptions) { std::vector x(1); std::vector b = {0.099, 0.5}; - storm::solver::GmmxxNondeterministicLinearEquationSolver solver(A); + storm::solver::GmmxxMinMaxLinearEquationSolver solver(A); ASSERT_NO_THROW(solver.solveEquationSystem(true, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -23,7 +23,7 @@ TEST(GmmxxNondeterministicLinearEquationSolver, SolveWithStandardOptions) { ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::gmmxxEquationSolverSettings().getPrecision()); } -TEST(GmmxxNondeterministicLinearEquationSolver, MatrixVectorMultiplication) { +TEST(GmmxxMinMaxLinearEquationSolver, MatrixVectorMultiplication) { storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true); ASSERT_NO_THROW(builder.newRowGroup(0)); ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); @@ -41,9 +41,9 @@ TEST(GmmxxNondeterministicLinearEquationSolver, MatrixVectorMultiplication) { std::vector x = {0, 1, 0}; - ASSERT_NO_THROW(storm::solver::GmmxxNondeterministicLinearEquationSolver solver(A)); + ASSERT_NO_THROW(storm::solver::GmmxxMinMaxLinearEquationSolver solver(A)); - storm::solver::GmmxxNondeterministicLinearEquationSolver solver(A); + storm::solver::GmmxxMinMaxLinearEquationSolver solver(A); ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, x, nullptr, 1)); ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::gmmxxEquationSolverSettings().getPrecision()); diff --git a/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp b/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp similarity index 84% rename from test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp rename to test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp index 55cf5fb2f..d2e014dd5 100644 --- a/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp +++ b/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp @@ -1,10 +1,10 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/solver/NativeNondeterministicLinearEquationSolver.h" +#include "src/solver/NativeMinMaxLinearEquationSolver.h" #include "src/settings/SettingsManager.h" -TEST(NativeNondeterministicLinearEquationSolver, SolveWithStandardOptions) { +TEST(NativeMinMaxLinearEquationSolver, SolveWithStandardOptions) { storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true); ASSERT_NO_THROW(builder.newRowGroup(0)); ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); @@ -15,7 +15,7 @@ TEST(NativeNondeterministicLinearEquationSolver, SolveWithStandardOptions) { std::vector x(1); std::vector b = {0.099, 0.5}; - storm::solver::NativeNondeterministicLinearEquationSolver solver(A); + storm::solver::NativeMinMaxLinearEquationSolver solver(A); ASSERT_NO_THROW(solver.solveEquationSystem(true, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -23,7 +23,7 @@ TEST(NativeNondeterministicLinearEquationSolver, SolveWithStandardOptions) { ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::nativeEquationSolverSettings().getPrecision()); } -TEST(NativeNondeterministicLinearEquationSolver, MatrixVectorMultiplication) { +TEST(NativeMinMaxLinearEquationSolver, MatrixVectorMultiplication) { storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true); ASSERT_NO_THROW(builder.newRowGroup(0)); ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); @@ -41,9 +41,9 @@ TEST(NativeNondeterministicLinearEquationSolver, MatrixVectorMultiplication) { std::vector x = {0, 1, 0}; - ASSERT_NO_THROW(storm::solver::NativeNondeterministicLinearEquationSolver solver(A)); + ASSERT_NO_THROW(storm::solver::NativeMinMaxLinearEquationSolver solver(A)); - storm::solver::NativeNondeterministicLinearEquationSolver solver(A); + storm::solver::NativeMinMaxLinearEquationSolver solver(A); ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, x, nullptr, 1)); ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::nativeEquationSolverSettings().getPrecision()); diff --git a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index c834ece2e..1db6f796d 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -17,7 +17,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("elected"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -79,7 +79,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("finished"); auto eventuallyFormula = std::make_shared(labelFormula); diff --git a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index b2bbba7fa..788f1fee6 100644 --- a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -17,7 +17,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("elected"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -79,7 +79,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("finished"); auto eventuallyFormula = std::make_shared(labelFormula); diff --git a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index f73102617..d42408232 100644 --- a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -14,7 +14,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); - storm::modelchecker::SparseMdpPrctlModelChecker mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); auto apFormula = std::make_shared("elected"); auto eventuallyFormula = std::make_shared(apFormula); @@ -86,7 +86,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); - storm::modelchecker::SparseMdpPrctlModelChecker mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalNondeterministicLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); auto apFormula = std::make_shared("finished"); auto eventuallyFormula = std::make_shared(apFormula);