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<typename ValueType>
- SparseMarkovAutomatonCslModelChecker<ValueType>::SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton<ValueType> const& model, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<ValueType>>&& nondeterministicLinearEquationSolverFactory) : model(model), nondeterministicLinearEquationSolverFactory(std::move(nondeterministicLinearEquationSolverFactory)) {
+ SparseMarkovAutomatonCslModelChecker<ValueType>::SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton<ValueType> const& model, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType>>&& MinMaxLinearEquationSolverFactory) : model(model), MinMaxLinearEquationSolverFactory(std::move(MinMaxLinearEquationSolverFactory)) {
// Intentionally left empty.
}
template<typename ValueType>
- SparseMarkovAutomatonCslModelChecker<ValueType>::SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton<ValueType> const& model) : model(model), nondeterministicLinearEquationSolverFactory(new storm::utility::solver::NondeterministicLinearEquationSolverFactory<ValueType>()) {
+ SparseMarkovAutomatonCslModelChecker<ValueType>::SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton<ValueType> const& model) : model(model), MinMaxLinearEquationSolverFactory(new storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType>()) {
// Intentionally left empty.
}
@@ -36,7 +36,7 @@ namespace storm {
}
template<typename ValueType>
- void SparseMarkovAutomatonCslModelChecker<ValueType>::computeBoundedReachabilityProbabilities(bool min, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector<ValueType>& markovianNonGoalValues, std::vector<ValueType>& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::NondeterministicLinearEquationSolverFactory<ValueType> const& nondeterministicLinearEquationSolverFactory) {
+ void SparseMarkovAutomatonCslModelChecker<ValueType>::computeBoundedReachabilityProbabilities(bool min, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector<ValueType>& markovianNonGoalValues, std::vector<ValueType>& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> 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<storm::solver::NondeterministicLinearEquationSolver<ValueType>> solver = nondeterministicLinearEquationSolverFactory.create(aProbabilistic);
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<ValueType> vProbabilistic(probabilisticNonGoalStates.getNumberOfSetBits());
std::vector<ValueType> 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<ValueType>()) {
@@ -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<ValueType> result(model.getNumberOfStates());
@@ -198,7 +198,7 @@ namespace storm {
template<typename ValueType>
std::vector<ValueType> SparseMarkovAutomatonCslModelChecker<ValueType>::computeUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const {
- return storm::modelchecker::SparseMdpPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(minimize, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, *nondeterministicLinearEquationSolverFactory, qualitative);
+ return storm::modelchecker::SparseMdpPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(minimize, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, *MinMaxLinearEquationSolverFactory, qualitative);
}
template<typename ValueType>
@@ -379,7 +379,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> sspMatrix = sspMatrixBuilder.build(currentChoice);
std::vector<ValueType> x(numberOfStatesNotInMecs + mecDecomposition.size());
- std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> solver = nondeterministicLinearEquationSolverFactory->create(sspMatrix);
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<storm::solver::NondeterministicLinearEquationSolver<ValueType>> solver = nondeterministicLinearEquationSolverFactory->create(submatrix);
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<typename ValueType>
class SparseMarkovAutomatonCslModelChecker : public AbstractModelChecker {
public:
- explicit SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton<ValueType> const& model, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<ValueType>>&& nondeterministicLinearEquationSolver);
+ explicit SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton<ValueType> const& model, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType>>&& MinMaxLinearEquationSolver);
explicit SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton<ValueType> 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<ValueType> computeBoundedUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& psiStates, std::pair<double, double> const& boundsPair) const;
- static void computeBoundedReachabilityProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector<ValueType>& markovianNonGoalValues, std::vector<ValueType>& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::NondeterministicLinearEquationSolverFactory<ValueType> const& nondeterministicLinearEquationSolverFactory);
+ static void computeBoundedReachabilityProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector<ValueType>& markovianNonGoalValues, std::vector<ValueType>& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& MinMaxLinearEquationSolverFactory);
std::vector<ValueType> computeUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const;
std::vector<ValueType> computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const;
std::vector<ValueType> computeLongRunAverageHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const;
@@ -67,7 +67,7 @@ namespace storm {
storm::models::sparse::MarkovAutomaton<ValueType> 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<storm::utility::solver::NondeterministicLinearEquationSolverFactory<ValueType>> nondeterministicLinearEquationSolverFactory;
+ std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType>> 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<typename ValueType>
- SparseMdpPrctlModelChecker<ValueType>::SparseMdpPrctlModelChecker(storm::models::sparse::Mdp<ValueType> const& model) : SparsePropositionalModelChecker<ValueType>(model), nondeterministicLinearEquationSolverFactory(new storm::utility::solver::NondeterministicLinearEquationSolverFactory<ValueType>()) {
+ SparseMdpPrctlModelChecker<ValueType>::SparseMdpPrctlModelChecker(storm::models::sparse::Mdp<ValueType> const& model) : SparsePropositionalModelChecker<ValueType>(model), MinMaxLinearEquationSolverFactory(new storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType>()) {
// Intentionally left empty.
}
template<typename ValueType>
- SparseMdpPrctlModelChecker<ValueType>::SparseMdpPrctlModelChecker(storm::models::sparse::Mdp<ValueType> const& model, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<ValueType>>&& nondeterministicLinearEquationSolverFactory) : SparsePropositionalModelChecker<ValueType>(model), nondeterministicLinearEquationSolverFactory(std::move(nondeterministicLinearEquationSolverFactory)) {
+ SparseMdpPrctlModelChecker<ValueType>::SparseMdpPrctlModelChecker(storm::models::sparse::Mdp<ValueType> const& model, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType>>&& MinMaxLinearEquationSolverFactory) : SparsePropositionalModelChecker<ValueType>(model), MinMaxLinearEquationSolverFactory(std::move(MinMaxLinearEquationSolverFactory)) {
// Intentionally left empty.
}
@@ -57,8 +57,8 @@ namespace storm {
std::vector<ValueType> subresult(statesWithProbabilityGreater0.getNumberOfSetBits());
storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::one<ValueType>());
- STORM_LOG_THROW(nondeterministicLinearEquationSolverFactory != nullptr, storm::exceptions::InvalidStateException, "No valid equation solver available.");
- std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> solver = nondeterministicLinearEquationSolverFactory->create(submatrix);
+ STORM_LOG_THROW(MinMaxLinearEquationSolverFactory != nullptr, storm::exceptions::InvalidStateException, "No valid equation solver available.");
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<ValueType> result(this->getModel().getNumberOfStates());
storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one<ValueType>());
- STORM_LOG_THROW(nondeterministicLinearEquationSolverFactory != nullptr, storm::exceptions::InvalidStateException, "No valid equation solver available.");
- std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> solver = nondeterministicLinearEquationSolverFactory->create(this->getModel().getTransitionMatrix());
+ STORM_LOG_THROW(MinMaxLinearEquationSolverFactory != nullptr, storm::exceptions::InvalidStateException, "No valid equation solver available.");
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = MinMaxLinearEquationSolverFactory->create(this->getModel().getTransitionMatrix());
solver->performMatrixVectorMultiplication(minimize, result);
return result;
@@ -103,11 +103,11 @@ namespace storm {
template<typename ValueType>
std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::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<typename ValueType>
- std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::utility::solver::NondeterministicLinearEquationSolverFactory<ValueType> const& nondeterministicLinearEquationSolverFactory, bool qualitative) {
+ std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> 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<ValueType> x(maybeStates.getNumberOfSetBits());
// Solve the corresponding system of equations.
- std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> solver = nondeterministicLinearEquationSolverFactory.create(submatrix);
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
- return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(SparseMdpPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), *nondeterministicLinearEquationSolverFactory, qualitative)));
+ return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(SparseMdpPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), *MinMaxLinearEquationSolverFactory, qualitative)));
}
template<typename ValueType>
@@ -197,7 +197,7 @@ namespace storm {
result.resize(this->getModel().getNumberOfStates());
}
- std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> solver = nondeterministicLinearEquationSolverFactory->create(this->getModel().getTransitionMatrix());
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<ValueType> result(this->getModel().getStateRewardVector());
- STORM_LOG_THROW(nondeterministicLinearEquationSolverFactory != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
- std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> solver = nondeterministicLinearEquationSolverFactory->create(this->getModel().getTransitionMatrix());
+ STORM_LOG_THROW(MinMaxLinearEquationSolverFactory != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = MinMaxLinearEquationSolverFactory->create(this->getModel().getTransitionMatrix());
solver->performMatrixVectorMultiplication(minimize, result, nullptr, stepCount);
return result;
@@ -233,7 +233,7 @@ namespace storm {
}
template<typename ValueType>
- std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeReachabilityRewardsHelper(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, boost::optional<std::vector<ValueType>> const& stateRewardVector, boost::optional<storm::storage::SparseMatrix<ValueType>> const& transitionRewardMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::utility::solver::NondeterministicLinearEquationSolverFactory<ValueType> const& nondeterministicLinearEquationSolverFactory, bool qualitative) const {
+ std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeReachabilityRewardsHelper(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, boost::optional<std::vector<ValueType>> const& stateRewardVector, boost::optional<storm::storage::SparseMatrix<ValueType>> const& transitionRewardMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> 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<ValueType> x(maybeStates.getNumberOfSetBits());
// Solve the corresponding system of equations.
- std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> solver = nondeterministicLinearEquationSolverFactory.create(submatrix);
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
- return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(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<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(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<typename ValueType>
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<ValueType>;
explicit SparseMdpPrctlModelChecker(storm::models::sparse::Mdp<ValueType> const& model);
- explicit SparseMdpPrctlModelChecker(storm::models::sparse::Mdp<ValueType> const& model, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<ValueType>>&& nondeterministicLinearEquationSolverFactory);
+ explicit SparseMdpPrctlModelChecker(storm::models::sparse::Mdp<ValueType> const& model, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType>>&& 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<ValueType> computeBoundedUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound) const;
std::vector<ValueType> computeNextProbabilitiesHelper(bool minimize, storm::storage::BitVector const& nextStates);
std::vector<ValueType> computeUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const;
- static std::vector<ValueType> computeUntilProbabilitiesHelper(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::utility::solver::NondeterministicLinearEquationSolverFactory<ValueType> const& nondeterministicLinearEquationSolverFactory, bool qualitative);
+ static std::vector<ValueType> computeUntilProbabilitiesHelper(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& MinMaxLinearEquationSolverFactory, bool qualitative);
std::vector<ValueType> computeInstantaneousRewardsHelper(bool minimize, uint_fast64_t stepCount) const;
std::vector<ValueType> computeCumulativeRewardsHelper(bool minimize, uint_fast64_t stepBound) const;
- std::vector<ValueType> computeReachabilityRewardsHelper(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, boost::optional<std::vector<ValueType>> const& stateRewardVector, boost::optional<storm::storage::SparseMatrix<ValueType>> const& transitionRewardMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::utility::solver::NondeterministicLinearEquationSolverFactory<ValueType> const& nondeterministicLinearEquationSolverFactory, bool qualitative) const;
+ std::vector<ValueType> computeReachabilityRewardsHelper(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, boost::optional<std::vector<ValueType>> const& stateRewardVector, boost::optional<storm::storage::SparseMatrix<ValueType>> const& transitionRewardMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> 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<storm::utility::solver::NondeterministicLinearEquationSolverFactory<ValueType>> nondeterministicLinearEquationSolverFactory;
+ std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType>> 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 <utility>
@@ -10,7 +10,7 @@ namespace storm {
namespace solver {
template<typename ValueType>
- GmmxxNondeterministicLinearEquationSolver<ValueType>::GmmxxNondeterministicLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A) : gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(A)), rowGroupIndices(A.getRowGroupIndices()) {
+ GmmxxMinMaxLinearEquationSolver<ValueType>::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A) : gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(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<typename ValueType>
- GmmxxNondeterministicLinearEquationSolver<ValueType>::GmmxxNondeterministicLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(A)), rowGroupIndices(A.getRowGroupIndices()), precision(precision), relative(relative), maximalNumberOfIterations(maximalNumberOfIterations) {
+ GmmxxMinMaxLinearEquationSolver<ValueType>::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(A)), rowGroupIndices(A.getRowGroupIndices()), precision(precision), relative(relative), maximalNumberOfIterations(maximalNumberOfIterations) {
// Intentionally left empty.
}
template<typename ValueType>
- void GmmxxNondeterministicLinearEquationSolver<ValueType>::solveEquationSystem(bool minimize, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
+ void GmmxxMinMaxLinearEquationSolver<ValueType>::solveEquationSystem(bool minimize, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* 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<typename ValueType>
- void GmmxxNondeterministicLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(bool minimize, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
+ void GmmxxMinMaxLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(bool minimize, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
bool multiplyResultMemoryProvided = true;
if (multiplyResult == nullptr) {
multiplyResult = new std::vector<ValueType>(gmmxxMatrix->nr);
@@ -120,6 +120,6 @@ namespace storm {
}
// Explicitly instantiate the solver.
- template class GmmxxNondeterministicLinearEquationSolver<double>;
+ template class GmmxxMinMaxLinearEquationSolver<double>;
} // 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 ValueType>
- class GmmxxNondeterministicLinearEquationSolver : public NondeterministicLinearEquationSolver<ValueType> {
+ class GmmxxMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver<ValueType> {
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<ValueType> const& A);
+ GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> 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<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true);
+ GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true);
virtual void performMatrixVectorMultiplication(bool minimize, std::vector<ValueType>& x, std::vector<ValueType>* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* 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 <vector>
@@ -14,7 +14,7 @@ namespace storm {
* provided.
*/
template<class ValueType>
- 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 <utility>
@@ -9,7 +9,7 @@ namespace storm {
namespace solver {
template<typename ValueType>
- NativeNondeterministicLinearEquationSolver<ValueType>::NativeNondeterministicLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A) : A(A) {
+ NativeMinMaxLinearEquationSolver<ValueType>::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> 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<typename ValueType>
- NativeNondeterministicLinearEquationSolver<ValueType>::NativeNondeterministicLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), precision(precision), relative(relative), maximalNumberOfIterations(maximalNumberOfIterations) {
+ NativeMinMaxLinearEquationSolver<ValueType>::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), precision(precision), relative(relative), maximalNumberOfIterations(maximalNumberOfIterations) {
// Intentionally left empty.
}
template<typename ValueType>
- void NativeNondeterministicLinearEquationSolver<ValueType>::solveEquationSystem(bool minimize, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
+ void NativeMinMaxLinearEquationSolver<ValueType>::solveEquationSystem(bool minimize, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* 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<typename ValueType>
- void NativeNondeterministicLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(bool minimize, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
+ void NativeMinMaxLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(bool minimize, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* 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<double>;
- template class NativeNondeterministicLinearEquationSolver<float>;
+ template class NativeMinMaxLinearEquationSolver<double>;
+ template class NativeMinMaxLinearEquationSolver<float>;
} // 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 ValueType>
- class NativeNondeterministicLinearEquationSolver : public NondeterministicLinearEquationSolver<ValueType> {
+ class NativeMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver<ValueType> {
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<ValueType> const& A);
+ NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> 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<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true);
+ NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true);
virtual void performMatrixVectorMultiplication(bool minimize, std::vector<ValueType>& x, std::vector<ValueType>* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* 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 <utility>
#include <chrono>
@@ -23,7 +23,7 @@ namespace storm {
namespace solver {
template<typename ValueType>
- TopologicalNondeterministicLinearEquationSolver<ValueType>::TopologicalNondeterministicLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A) : NativeNondeterministicLinearEquationSolver<ValueType>(A) {
+ TopologicalMinMaxLinearEquationSolver<ValueType>::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A) : NativeMinMaxLinearEquationSolver<ValueType>(A) {
// Get the settings object to customize solving.
//storm::settings::Settings* settings = storm::settings::Settings::getInstance();
@@ -44,12 +44,12 @@ namespace storm {
}
template<typename ValueType>
- TopologicalNondeterministicLinearEquationSolver<ValueType>::TopologicalNondeterministicLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : NativeNondeterministicLinearEquationSolver<ValueType>(A, precision, maximalNumberOfIterations, relative) {
+ TopologicalMinMaxLinearEquationSolver<ValueType>::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : NativeMinMaxLinearEquationSolver<ValueType>(A, precision, maximalNumberOfIterations, relative) {
// Intentionally left empty.
}
template<typename ValueType>
- void TopologicalNondeterministicLinearEquationSolver<ValueType>::solveEquationSystem(bool minimize, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
+ void TopologicalMinMaxLinearEquationSolver<ValueType>::solveEquationSystem(bool minimize, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* 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<float> newA = this->A.template toValueType<float>();
- TopologicalNondeterministicLinearEquationSolver<float> newSolver(newA, this->precision, this->maximalNumberOfIterations, this->relative);
+ TopologicalMinMaxLinearEquationSolver<float> newSolver(newA, this->precision, this->maximalNumberOfIterations, this->relative);
std::vector<float> new_x = storm::utility::vector::toValueType<float>(x);
std::vector<float> const new_b = storm::utility::vector::toValueType<float>(b);
@@ -322,7 +322,7 @@ namespace storm {
template<typename ValueType>
std::vector<std::pair<bool, storm::storage::StateBlock>>
- TopologicalNondeterministicLinearEquationSolver<ValueType>::getOptimalGroupingFromTopologicalSccDecomposition(storm::storage::StronglyConnectedComponentDecomposition<ValueType> const& sccDecomposition, std::vector<uint_fast64_t> const& topologicalSort, storm::storage::SparseMatrix<ValueType> const& matrix) const {
+ TopologicalMinMaxLinearEquationSolver<ValueType>::getOptimalGroupingFromTopologicalSccDecomposition(storm::storage::StronglyConnectedComponentDecomposition<ValueType> const& sccDecomposition, std::vector<uint_fast64_t> const& topologicalSort, storm::storage::SparseMatrix<ValueType> const& matrix) const {
std::vector<std::pair<bool, storm::storage::StateBlock>> 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<double>;
- template class TopologicalNondeterministicLinearEquationSolver<float>;
+ template class TopologicalMinMaxLinearEquationSolver<double>;
+ template class TopologicalMinMaxLinearEquationSolver<float>;
} // 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 ValueType>
- class TopologicalNondeterministicLinearEquationSolver : public NativeNondeterministicLinearEquationSolver<ValueType> {
+ class TopologicalMinMaxLinearEquationSolver : public NativeMinMaxLinearEquationSolver<ValueType> {
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<ValueType> const& A);
+ TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> 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<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true);
+ TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true);
virtual void solveEquationSystem(bool minimize, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* 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<typename T>
- 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<ValueType>;
+ friend class storm::solver::TopologicalValueIterationMinMaxLinearEquationSolver<ValueType>;
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<typename ValueType>
- std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> NondeterministicLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> MinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> 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<storm::solver::NondeterministicLinearEquationSolver<ValueType>>(new storm::solver::GmmxxNondeterministicLinearEquationSolver<ValueType>(matrix));
- case storm::settings::modules::GeneralSettings::EquationSolver::Native: return std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>>(new storm::solver::NativeNondeterministicLinearEquationSolver<ValueType>(matrix));
+ case storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx: return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::GmmxxMinMaxLinearEquationSolver<ValueType>(matrix));
+ case storm::settings::modules::GeneralSettings::EquationSolver::Native: return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::NativeMinMaxLinearEquationSolver<ValueType>(matrix));
}
}
template<typename ValueType>
- std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> GmmxxNondeterministicLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
- return std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>>(new storm::solver::GmmxxNondeterministicLinearEquationSolver<ValueType>(matrix));
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> GmmxxMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
+ return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::GmmxxMinMaxLinearEquationSolver<ValueType>(matrix));
}
template<typename ValueType>
- std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> NativeNondeterministicLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
- return std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>>(new storm::solver::NativeNondeterministicLinearEquationSolver<ValueType>(matrix));
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> NativeMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
+ return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::NativeMinMaxLinearEquationSolver<ValueType>(matrix));
}
template<typename ValueType>
- std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> TopologicalNondeterministicLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
- return std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>>(new storm::solver::TopologicalNondeterministicLinearEquationSolver<ValueType>(matrix));
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> TopologicalMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
+ return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::TopologicalMinMaxLinearEquationSolver<ValueType>(matrix));
}
std::unique_ptr<storm::solver::LpSolver> LpSolverFactory::create(std::string const& name) const {
@@ -82,10 +82,10 @@ namespace storm {
template class LinearEquationSolverFactory<double>;
template class GmmxxLinearEquationSolverFactory<double>;
template class NativeLinearEquationSolverFactory<double>;
- template class NondeterministicLinearEquationSolverFactory<double>;
- template class GmmxxNondeterministicLinearEquationSolverFactory<double>;
- template class NativeNondeterministicLinearEquationSolverFactory<double>;
- template class TopologicalNondeterministicLinearEquationSolverFactory<double>;
+ template class MinMaxLinearEquationSolverFactory<double>;
+ template class GmmxxMinMaxLinearEquationSolverFactory<double>;
+ template class NativeMinMaxLinearEquationSolverFactory<double>;
+ template class TopologicalMinMaxLinearEquationSolverFactory<double>;
}
}
}
\ 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<typename ValueType>
- class NondeterministicLinearEquationSolverFactory {
+ class MinMaxLinearEquationSolverFactory {
public:
/*!
* Creates a new nondeterministic linear equation solver instance with the given matrix.
*/
- virtual std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const;
+ virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const;
};
template<typename ValueType>
- class NativeNondeterministicLinearEquationSolverFactory : public NondeterministicLinearEquationSolverFactory<ValueType> {
+ class NativeMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory<ValueType> {
public:
- virtual std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
+ virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
};
template<typename ValueType>
- class GmmxxNondeterministicLinearEquationSolverFactory : public NondeterministicLinearEquationSolverFactory<ValueType> {
+ class GmmxxMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory<ValueType> {
public:
- virtual std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
+ virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
};
template<typename ValueType>
- class TopologicalNondeterministicLinearEquationSolverFactory : public NondeterministicLinearEquationSolverFactory<ValueType> {
+ class TopologicalMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory<ValueType> {
public:
- virtual std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
+ virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> 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<double> checker(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@@ -90,7 +90,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
- storm::modelchecker::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
@@ -114,7 +114,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
- storm::modelchecker::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
@@ -143,7 +143,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(3172ull, mdp->getNumberOfStates());
ASSERT_EQ(7144ull, mdp->getNumberOfTransitions());
- storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(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<double> checker(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@@ -90,7 +90,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
- storm::modelchecker::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
@@ -114,7 +114,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
- storm::modelchecker::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
@@ -143,7 +143,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(3172ull, mdp->getNumberOfStates());
ASSERT_EQ(7144ull, mdp->getNumberOfTransitions());
- storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(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<double> mc(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
//storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("two");
auto apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
@@ -137,7 +137,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
// ------------- state rewards --------------
std::shared_ptr<storm::models::sparse::Mdp<double>> 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::models::sparse::Mdp<double>>();
- storm::modelchecker::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
@@ -172,7 +172,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
// -------------------------------- state and transition reward ------------------------
std::shared_ptr<storm::models::sparse::Mdp<double>> 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::models::sparse::Mdp<double>>();
- storm::modelchecker::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
@@ -212,7 +212,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(mdp->getNumberOfStates(), 3172ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull);
- storm::modelchecker::SparseMdpPrctlModelChecker<double> mc(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
auto apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(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<double> 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<double> x(1);
std::vector<double> b = {0.099, 0.5};
- storm::solver::GmmxxNondeterministicLinearEquationSolver<double> solver(A);
+ storm::solver::GmmxxMinMaxLinearEquationSolver<double> 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<double> 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<double> x = {0, 1, 0};
- ASSERT_NO_THROW(storm::solver::GmmxxNondeterministicLinearEquationSolver<double> solver(A));
+ ASSERT_NO_THROW(storm::solver::GmmxxMinMaxLinearEquationSolver<double> solver(A));
- storm::solver::GmmxxNondeterministicLinearEquationSolver<double> solver(A);
+ storm::solver::GmmxxMinMaxLinearEquationSolver<double> 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<double> 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<double> x(1);
std::vector<double> b = {0.099, 0.5};
- storm::solver::NativeNondeterministicLinearEquationSolver<double> solver(A);
+ storm::solver::NativeMinMaxLinearEquationSolver<double> 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<double> 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<double> x = {0, 1, 0};
- ASSERT_NO_THROW(storm::solver::NativeNondeterministicLinearEquationSolver<double> solver(A));
+ ASSERT_NO_THROW(storm::solver::NativeMinMaxLinearEquationSolver<double> solver(A));
- storm::solver::NativeNondeterministicLinearEquationSolver<double> solver(A);
+ storm::solver::NativeMinMaxLinearEquationSolver<double> 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<double> checker(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@@ -79,7 +79,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(63616ull, mdp->getNumberOfStates());
ASSERT_EQ(213472ull, mdp->getNumberOfTransitions());
- storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(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<double> checker(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@@ -79,7 +79,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(63616ull, mdp->getNumberOfStates());
ASSERT_EQ(213472ull, mdp->getNumberOfTransitions());
- storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(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<double> mc(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
auto apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
@@ -86,7 +86,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(mdp->getNumberOfStates(), 63616ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull);
- storm::modelchecker::SparseMdpPrctlModelChecker<double> mc(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalNondeterministicLinearEquationSolverFactory<double>()));
+ storm::modelchecker::SparseMdpPrctlModelChecker<double> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
auto apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);