sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

made all instantiations to call MDP model checking with rational numbers 

Former-commit-id: d3f8df7804
tempestpy_adaptions
dehnert 9 years ago
parent
d27c75c3d8
commit
b1f2c26df0
23 changed files with 198 additions and 306 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 1
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
  2. 24
      src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  3. 160
      src/solver/EigenLinearEquationSolver.cpp
  4. 2
      src/solver/EigenLinearEquationSolver.h
  5. 37
      src/solver/EliminationLinearEquationSolver.cpp
  6. 1
      src/solver/EliminationLinearEquationSolver.h
  7. 44
      src/solver/GmmxxLinearEquationSolver.cpp
  8. 1
      src/solver/GmmxxLinearEquationSolver.h
  9. 2
      src/solver/LinearEquationSolver.h
  10. 14
      src/solver/MinMaxLinearEquationSolver.cpp
  11. 37
      src/solver/NativeLinearEquationSolver.cpp
  12. 1
      src/solver/NativeLinearEquationSolver.h
  13. 7
      src/solver/SolveGoal.cpp
  14. 81
      src/solver/StandardMinMaxLinearEquationSolver.cpp
  15. 23
      src/solver/StandardMinMaxLinearEquationSolver.h
  16. 8
      src/solver/TerminationCondition.cpp
  17. 2
      src/solver/TerminationCondition.h
  18. 3
      src/storage/MaximalEndComponentDecomposition.cpp
  19. 14
      src/utility/constants.cpp
  20. 3
      src/utility/constants.h
  21. 4
      src/utility/graph.cpp
  22. 28
      src/utility/storm.h
  23. 7
      src/utility/vector.h

1
src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
View File

@ -147,5 +147,6 @@ namespace storm {
}
template class SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>>;
template class SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
}
}

24
src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -20,6 +20,7 @@
#include "src/exceptions/InvalidStateException.h"
#include "src/exceptions/InvalidPropertyException.h"
#include "src/exceptions/InvalidSettingsException.h"
#include "src/exceptions/IllegalFunctionCallException.h"
namespace storm {
namespace modelchecker {
@ -70,7 +71,6 @@ namespace storm {
return result;
}
template<typename ValueType>
MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
@ -107,7 +107,7 @@ namespace storm {
// Check whether we need to compute exact probabilities for some states.
if (qualitative) {
// Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, ValueType(0.5));
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, storm::utility::convertNumber<ValueType>(0.5));
} else {
if (!maybeStates.empty()) {
// In this case we have have to compute the probabilities.
@ -270,6 +270,11 @@ namespace storm {
}, \
targetStates, qualitative, minMaxLinearEquationSolverFactory);
}
template<>
std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::models::sparse::StandardRewardModel<storm::Interval> const& intervalRewardModel, bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory) {
STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Computing reachability rewards is unsupported for this data type.");
}
#endif
template<typename ValueType>
@ -357,7 +362,7 @@ namespace storm {
}
// Start by decomposing the MDP into its MECs.
storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition(transitionMatrix, backwardTransitions);
storm::storage::MaximalEndComponentDecomposition<ValueType> mecDecomposition(transitionMatrix, backwardTransitions);
// Get some data members for convenience.
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
@ -517,12 +522,12 @@ namespace storm {
ValueType r = 0;
for (auto element : transitionMatrix.getRow(choice)) {
constraint = constraint + stateToVariableMap.at(element.getColumn()) * solver->getConstant(element.getValue());
constraint = constraint + stateToVariableMap.at(element.getColumn()) * solver->getConstant(storm::utility::convertNumber<double>(element.getValue()));
if (psiStates.get(element.getColumn())) {
r += element.getValue();
}
}
constraint = solver->getConstant(r) + constraint;
constraint = solver->getConstant(storm::utility::convertNumber<double>(r)) + constraint;
if (dir == OptimizationDirection::Minimize) {
constraint = stateToVariableMap.at(state) <= constraint;
@ -534,7 +539,7 @@ namespace storm {
}
solver->optimize();
return solver->getContinuousValue(lambda);
return storm::utility::convertNumber<ValueType>(solver->getContinuousValue(lambda));
}
template<typename ValueType>
@ -644,7 +649,12 @@ namespace storm {
template std::vector<double> SparseMdpPrctlHelper<double>::computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::models::sparse::StandardRewardModel<double> const& rewardModel, uint_fast64_t stepCount, storm::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
template std::vector<double> SparseMdpPrctlHelper<double>::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::models::sparse::StandardRewardModel<double> const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
template std::vector<double> SparseMdpPrctlHelper<double>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
template class SparseMdpPrctlHelper<storm::RationalNumber>;
template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, uint_fast64_t stepCount, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory);
}
}
}

160
src/solver/EigenLinearEquationSolver.cpp
View File

@ -224,45 +224,45 @@ namespace storm {
}
}
template<typename ValueType>
void EigenLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
// Typedef the map-type so we don't have to spell it out.
typedef decltype(Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::Map(b->data(), b->size())) MapType;
bool multiplyResultProvided = multiplyResult != nullptr;
if (!multiplyResult) {
multiplyResult = new std::vector<ValueType>(eigenA->cols());
}
auto eigenMultiplyResult = Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::Map(multiplyResult->data(), multiplyResult->size());
// Map the input vectors x and b to Eigen's format.
std::unique_ptr<MapType> eigenB;
if (b != nullptr) {
eigenB = std::make_unique<MapType>(Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::Map(b->data(), b->size()));
}
auto eigenX = Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::Map(x.data(), x.size());
// Perform n matrix-vector multiplications.
auto currentX = &eigenX;
auto nextX = &eigenMultiplyResult;
for (uint64_t iteration = 0; iteration < n; ++iteration) {
if (eigenB) {
nextX->noalias() = *eigenA * *currentX + *eigenB;
} else {
nextX->noalias() = *eigenA * *currentX;
}
std::swap(nextX, currentX);
}
// If the last result we obtained is not the one in the input vector x, we swap the result there.
if (currentX != &eigenX) {
std::swap(*nextX, *currentX);
}
if (!multiplyResultProvided) {
delete multiplyResult;
}
}
// template<typename ValueType>
// void EigenLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
// // Typedef the map-type so we don't have to spell it out.
// typedef decltype(Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::Map(b->data(), b->size())) MapType;
//
// bool multiplyResultProvided = multiplyResult != nullptr;
// if (!multiplyResult) {
// multiplyResult = new std::vector<ValueType>(eigenA->cols());
// }
// auto eigenMultiplyResult = Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::Map(multiplyResult->data(), multiplyResult->size());
//
// // Map the input vectors x and b to Eigen's format.
// std::unique_ptr<MapType> eigenB;
// if (b != nullptr) {
// eigenB = std::make_unique<MapType>(Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::Map(b->data(), b->size()));
// }
// auto eigenX = Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::Map(x.data(), x.size());
//
// // Perform n matrix-vector multiplications.
// auto currentX = &eigenX;
// auto nextX = &eigenMultiplyResult;
// for (uint64_t iteration = 0; iteration < n; ++iteration) {
// if (eigenB) {
// nextX->noalias() = *eigenA * *currentX + *eigenB;
// } else {
// nextX->noalias() = *eigenA * *currentX;
// }
// std::swap(nextX, currentX);
// }
//
// // If the last result we obtained is not the one in the input vector x, we swap the result there.
// if (currentX != &eigenX) {
// std::swap(*nextX, *currentX);
// }
//
// if (!multiplyResultProvided) {
// delete multiplyResult;
// }
// }
template<typename ValueType>
EigenLinearEquationSolverSettings<ValueType>& EigenLinearEquationSolver<ValueType>::getSettings() {
@ -287,46 +287,6 @@ namespace storm {
solver._solve_impl(eigenB, eigenX);
}
template<>
void EigenLinearEquationSolver<storm::RationalNumber>::performMatrixVectorMultiplication(std::vector<storm::RationalNumber>& x, std::vector<storm::RationalNumber> const* b, uint_fast64_t n, std::vector<storm::RationalNumber>* multiplyResult) const {
// Typedef the map-type so we don't have to spell it out.
typedef decltype(Eigen::Matrix<storm::RationalNumber, Eigen::Dynamic, 1>::Map(b->data(), b->size())) MapType;
bool multiplyResultProvided = multiplyResult != nullptr;
if (!multiplyResult) {
multiplyResult = new std::vector<storm::RationalNumber>(eigenA->cols());
}
auto eigenMultiplyResult = Eigen::Matrix<storm::RationalNumber, Eigen::Dynamic, 1>::Map(multiplyResult->data(), multiplyResult->size());
// Map the input vectors x and b to Eigen's format.
std::unique_ptr<MapType> eigenB;
if (b != nullptr) {
eigenB = std::make_unique<MapType>(Eigen::Matrix<storm::RationalNumber, Eigen::Dynamic, 1>::Map(b->data(), b->size()));
}
auto eigenX = Eigen::Matrix<storm::RationalNumber, Eigen::Dynamic, 1>::Map(x.data(), x.size());
// Perform n matrix-vector multiplications.
auto currentX = &eigenX;
auto nextX = &eigenMultiplyResult;
for (uint64_t iteration = 0; iteration < n; ++iteration) {
if (eigenB) {
nextX->noalias() = *eigenA * *currentX + *eigenB;
} else {
nextX->noalias() = *eigenA * *currentX;
}
std::swap(nextX, currentX);
}
// If the last result we obtained is not the one in the input vector x, we swap the result there.
if (currentX != &eigenX) {
std::swap(*nextX, *currentX);
}
if (!multiplyResultProvided) {
delete multiplyResult;
}
}
// Specialization form storm::RationalFunction
template<>
@ -339,47 +299,7 @@ namespace storm {
solver.compute(*eigenA);
solver._solve_impl(eigenB, eigenX);
}
template<>
void EigenLinearEquationSolver<storm::RationalFunction>::performMatrixVectorMultiplication(std::vector<storm::RationalFunction>& x, std::vector<storm::RationalFunction> const* b, uint_fast64_t n, std::vector<storm::RationalFunction>* multiplyResult) const {
// Typedef the map-type so we don't have to spell it out.
typedef decltype(Eigen::Matrix<storm::RationalFunction, Eigen::Dynamic, 1>::Map(b->data(), b->size())) MapType;
bool multiplyResultProvided = multiplyResult != nullptr;
if (!multiplyResult) {
multiplyResult = new std::vector<storm::RationalFunction>(eigenA->cols());
}
auto eigenMultiplyResult = Eigen::Matrix<storm::RationalFunction, Eigen::Dynamic, 1>::Map(multiplyResult->data(), multiplyResult->size());
// Map the input vectors x and b to Eigen's format.
std::unique_ptr<MapType> eigenB;
if (b != nullptr) {
eigenB = std::make_unique<MapType>(Eigen::Matrix<storm::RationalFunction, Eigen::Dynamic, 1>::Map(b->data(), b->size()));
}
auto eigenX = Eigen::Matrix<storm::RationalFunction, Eigen::Dynamic, 1>::Map(x.data(), x.size());
// Perform n matrix-vector multiplications.
auto currentX = &eigenX;
auto nextX = &eigenMultiplyResult;
for (uint64_t iteration = 0; iteration < n; ++iteration) {
if (eigenB) {
nextX->noalias() = *eigenA * *currentX + *eigenB;
} else {
nextX->noalias() = *eigenA * *currentX;
}
std::swap(nextX, currentX);
}
// If the last result we obtained is not the one in the input vector x, we swap the result there.
if (currentX != &eigenX) {
std::swap(*nextX, *currentX);
}
if (!multiplyResultProvided) {
delete multiplyResult;
}
}
template<typename ValueType>
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> EigenLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
return std::make_unique<storm::solver::EigenLinearEquationSolver<ValueType>>(matrix, settings);

2
src/solver/EigenLinearEquationSolver.h
View File

@ -62,7 +62,7 @@ namespace storm {
EigenLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, EigenLinearEquationSolverSettings<ValueType> const& settings = EigenLinearEquationSolverSettings<ValueType>());
virtual void solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const override;
// virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b = nullptr) const override;
EigenLinearEquationSolverSettings<ValueType>& getSettings();

37
src/solver/EliminationLinearEquationSolver.cpp
View File

@ -100,43 +100,6 @@ namespace storm {
};
}
template<typename ValueType>
void EliminationLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
// Set up some temporary variables so that we can just swap pointers instead of copying the result after
// each iteration.
std::vector<ValueType>* currentX = &x;
bool multiplyResultProvided = true;
std::vector<ValueType>* nextX = multiplyResult;
if (nextX == nullptr) {
nextX = new std::vector<ValueType>(x.size());
multiplyResultProvided = false;
}
std::vector<ValueType> const* copyX = nextX;
// Now perform matrix-vector multiplication as long as we meet the bound.
for (uint_fast64_t i = 0; i < n; ++i) {
A.multiplyWithVector(*currentX, *nextX);
std::swap(nextX, currentX);
// If requested, add an offset to the current result vector.
if (b != nullptr) {
storm::utility::vector::addVectors(*currentX, *b, *currentX);
}
}
// If we performed an odd number of repetitions, we need to swap the contents of currentVector and x,
// because the output is supposed to be stored in the input vector x.
if (currentX == copyX) {
std::swap(x, *currentX);
}
// If the vector for the temporary multiplication result was not provided, we need to delete it.
if (!multiplyResultProvided) {
delete copyX;
}
}
template<typename ValueType>
void EliminationLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b) const {
if (&x != &result) {

1
src/solver/EliminationLinearEquationSolver.h
View File

@ -30,7 +30,6 @@ namespace storm {
EliminationLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, EliminationLinearEquationSolverSettings<ValueType> const& settings = EliminationLinearEquationSolverSettings<ValueType>());
virtual void solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b = nullptr) const override;
EliminationLinearEquationSolverSettings<ValueType>& getSettings();

44
src/solver/GmmxxLinearEquationSolver.cpp
View File

@ -177,48 +177,12 @@ namespace storm {
}
}
template<typename ValueType>
void GmmxxLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
// Set up some temporary variables so that we can just swap pointers instead of copying the result after
// each iteration.
std::vector<ValueType>* currentX = &x;
bool multiplyResultProvided = true;
std::vector<ValueType>* nextX = multiplyResult;
if (nextX == nullptr) {
nextX = new std::vector<ValueType>(x.size());
multiplyResultProvided = false;
}
std::vector<ValueType> const* copyX = nextX;
// Now perform matrix-vector multiplication as long as we meet the bound.
for (uint_fast64_t i = 0; i < n; ++i) {
gmm::mult(*gmmxxMatrix, *currentX, *nextX);
std::swap(nextX, currentX);
// If requested, add an offset to the current result vector.
if (b != nullptr) {
gmm::add(*b, *currentX);
}
}
// If we performed an odd number of repetitions, we need to swap the contents of currentVector and x,
// because the output is supposed to be stored in the input vector x.
if (currentX == copyX) {
std::swap(x, *currentX);
}
// If the vector for the temporary multiplication result was not provided, we need to delete it.
if (!multiplyResultProvided) {
delete copyX;
}
}
template<typename ValueType>
void GmmxxLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b) const {
gmm::mult(*gmmxxMatrix, x, result);
if (b != nullptr) {
gmm::add(*b, result);
if (b) {
gmm::mult_add(*gmmxxMatrix, x, *b, result);
} else {
gmm::mult(*gmmxxMatrix, x, result);
}
}

1
src/solver/GmmxxLinearEquationSolver.h
View File

@ -90,7 +90,6 @@ namespace storm {
GmmxxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, GmmxxLinearEquationSolverSettings<ValueType> const& settings = GmmxxLinearEquationSolverSettings<ValueType>());
virtual void solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b = nullptr) const override;
GmmxxLinearEquationSolverSettings<ValueType>& getSettings();

2
src/solver/LinearEquationSolver.h
View File

@ -58,7 +58,7 @@ namespace storm {
* @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this
* vector must be equal to the number of rows of A.
*/
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const;
void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const;
};
template<typename ValueType>

14
src/solver/MinMaxLinearEquationSolver.cpp
View File

@ -128,12 +128,24 @@ namespace storm {
}
return result;
}
template<>
template<typename MatrixType>
std::unique_ptr<MinMaxLinearEquationSolver<storm::RationalNumber>> GeneralMinMaxLinearEquationSolverFactory<storm::RationalNumber>::selectSolver(MatrixType&& matrix) const {
std::unique_ptr<MinMaxLinearEquationSolver<storm::RationalNumber>> result;
auto method = storm::settings::getModule<storm::settings::modules::MinMaxEquationSolverSettings>().getMinMaxEquationSolvingMethod();
STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration, storm::exceptions::InvalidSettingsException, "For this data type only value iteration and policy iteration are available.");
return std::make_unique<StandardMinMaxLinearEquationSolver<storm::RationalNumber>>(std::forward<MatrixType>(matrix), std::make_unique<GeneralLinearEquationSolverFactory<storm::RationalNumber>>());
}
template class MinMaxLinearEquationSolver<float>;
template class MinMaxLinearEquationSolver<double>;
template class MinMaxLinearEquationSolver<storm::RationalNumber>;
template class MinMaxLinearEquationSolverFactory<double>;
template class GeneralMinMaxLinearEquationSolverFactory<double>;
template class MinMaxLinearEquationSolverFactory<storm::RationalNumber>;
template class GeneralMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
}
}

37
src/solver/NativeLinearEquationSolver.cpp
View File

@ -182,43 +182,6 @@ namespace storm {
}
}
template<typename ValueType>
void NativeLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
// Set up some temporary variables so that we can just swap pointers instead of copying the result after
// each iteration.
std::vector<ValueType>* currentX = &x;
bool multiplyResultProvided = true;
std::vector<ValueType>* nextX = multiplyResult;
if (nextX == nullptr) {
nextX = new std::vector<ValueType>(x.size());
multiplyResultProvided = false;
}
std::vector<ValueType> const* copyX = nextX;
// Now perform matrix-vector multiplication as long as we meet the bound.
for (uint_fast64_t i = 0; i < n; ++i) {
A.multiplyWithVector(*currentX, *nextX);
std::swap(nextX, currentX);
// If requested, add an offset to the current result vector.
if (b != nullptr) {
storm::utility::vector::addVectors(*currentX, *b, *currentX);
}
}
// If we performed an odd number of repetitions, we need to swap the contents of currentVector and x,
// because the output is supposed to be stored in the input vector x.
if (currentX == copyX) {
std::swap(x, *currentX);
}
// If the vector for the temporary multiplication result was not provided, we need to delete it.
if (!multiplyResultProvided) {
delete copyX;
}
}
template<typename ValueType>
void NativeLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b) const {
if (&x != &result) {

1
src/solver/NativeLinearEquationSolver.h
View File

@ -47,7 +47,6 @@ namespace storm {
NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, NativeLinearEquationSolverSettings<ValueType> const& settings = NativeLinearEquationSolverSettings<ValueType>());
virtual void solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b = nullptr) const override;
NativeLinearEquationSolverSettings<ValueType>& getSettings();

7
src/solver/SolveGoal.cpp
View File

@ -17,7 +17,7 @@ namespace storm {
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> configureMinMaxLinearEquationSolver(BoundedGoal<ValueType> const& goal, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& factory, storm::storage::SparseMatrix<ValueType> const& matrix) {
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> p = factory.create(matrix);
p->setOptimizationDirection(goal.direction());
p->setTerminationCondition(std::make_unique<TerminateIfFilteredExtremumExceedsThreshold<double>>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), goal.minimize()));
p->setTerminationCondition(std::make_unique<TerminateIfFilteredExtremumExceedsThreshold<ValueType>>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), goal.minimize()));
return p;
}
@ -50,6 +50,9 @@ namespace storm {
template std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<double>> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::solver::MinMaxLinearEquationSolverFactory<double> const& factory, storm::storage::SparseMatrix<double> const& matrix);
template std::unique_ptr<storm::solver::LinearEquationSolver<double>> configureLinearEquationSolver(BoundedGoal<double> const& goal, storm::solver::LinearEquationSolverFactory<double> const& factory, storm::storage::SparseMatrix<double> const& matrix);
template std::unique_ptr<storm::solver::LinearEquationSolver<double>> configureLinearEquationSolver(SolveGoal const& goal, storm::solver::LinearEquationSolverFactory<double> const& factory, storm::storage::SparseMatrix<double> const& matrix);
template std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<storm::RationalNumber>> configureMinMaxLinearEquationSolver(BoundedGoal<storm::RationalNumber> const& goal, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& factory, storm::storage::SparseMatrix<storm::RationalNumber> const& matrix);
template std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<storm::RationalNumber>> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& factory, storm::storage::SparseMatrix<storm::RationalNumber> const& matrix);
}
}

81
src/solver/StandardMinMaxLinearEquationSolver.cpp
View File

@ -15,12 +15,13 @@
namespace storm {
namespace solver {
StandardMinMaxLinearEquationSolverSettings::StandardMinMaxLinearEquationSolverSettings() {
template<typename ValueType>
StandardMinMaxLinearEquationSolverSettings<ValueType>::StandardMinMaxLinearEquationSolverSettings() {
// Get the settings object to customize linear solving.
storm::settings::modules::MinMaxEquationSolverSettings const& settings = storm::settings::getModule<storm::settings::modules::MinMaxEquationSolverSettings>();
maximalNumberOfIterations = settings.getMaximalIterationCount();
precision = settings.getPrecision();
precision = storm::utility::convertNumber<ValueType>(settings.getPrecision());
relative = settings.getConvergenceCriterion() == storm::settings::modules::MinMaxEquationSolverSettings::ConvergenceCriterion::Relative;
auto method = settings.getMinMaxEquationSolvingMethod();
@ -32,53 +33,61 @@ namespace storm {
}
}
void StandardMinMaxLinearEquationSolverSettings::setSolutionMethod(SolutionMethod const& solutionMethod) {
template<typename ValueType>
void StandardMinMaxLinearEquationSolverSettings<ValueType>::setSolutionMethod(SolutionMethod const& solutionMethod) {
this->solutionMethod = solutionMethod;
}
void StandardMinMaxLinearEquationSolverSettings::setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations) {
template<typename ValueType>
void StandardMinMaxLinearEquationSolverSettings<ValueType>::setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations) {
this->maximalNumberOfIterations = maximalNumberOfIterations;
}
void StandardMinMaxLinearEquationSolverSettings::setRelativeTerminationCriterion(bool value) {
template<typename ValueType>
void StandardMinMaxLinearEquationSolverSettings<ValueType>::setRelativeTerminationCriterion(bool value) {
this->relative = value;
}
void StandardMinMaxLinearEquationSolverSettings::setPrecision(double precision) {
template<typename ValueType>
void StandardMinMaxLinearEquationSolverSettings<ValueType>::setPrecision(ValueType precision) {
this->precision = precision;
}
StandardMinMaxLinearEquationSolverSettings::SolutionMethod const& StandardMinMaxLinearEquationSolverSettings::getSolutionMethod() const {
template<typename ValueType>
typename StandardMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod const& StandardMinMaxLinearEquationSolverSettings<ValueType>::getSolutionMethod() const {
return solutionMethod;
}
uint64_t StandardMinMaxLinearEquationSolverSettings::getMaximalNumberOfIterations() const {
template<typename ValueType>
uint64_t StandardMinMaxLinearEquationSolverSettings<ValueType>::getMaximalNumberOfIterations() const {
return maximalNumberOfIterations;
}
double StandardMinMaxLinearEquationSolverSettings::getPrecision() const {
template<typename ValueType>
ValueType StandardMinMaxLinearEquationSolverSettings<ValueType>::getPrecision() const {
return precision;
}
bool StandardMinMaxLinearEquationSolverSettings::getRelativeTerminationCriterion() const {
template<typename ValueType>
bool StandardMinMaxLinearEquationSolverSettings<ValueType>::getRelativeTerminationCriterion() const {
return relative;
}
template<typename ValueType>
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings const& settings) : settings(settings), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(nullptr), A(A) {
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings<ValueType> const& settings) : settings(settings), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(nullptr), A(A) {
// Intentionally left empty.
}
template<typename ValueType>
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings const& settings) : settings(settings), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(A))), A(*localA) {
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings<ValueType> const& settings) : settings(settings), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(A))), A(*localA) {
// Intentionally left empty.
}
template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::solveEquationSystem(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
switch (this->getSettings().getSolutionMethod()) {
case StandardMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration: solveEquationSystemValueIteration(dir, x, b, multiplyResult, newX); break;
case StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration: solveEquationSystemPolicyIteration(dir, x, b, multiplyResult, newX); break;
case StandardMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration: solveEquationSystemValueIteration(dir, x, b, multiplyResult, newX); break;
case StandardMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration: solveEquationSystemPolicyIteration(dir, x, b, multiplyResult, newX); break;
}
}
@ -90,7 +99,7 @@ namespace storm {
if (multiplyResult == nullptr) {
multiplyResult = new std::vector<ValueType>(this->A.getRowCount());
}
// Create the initial scheduler.
std::vector<storm::storage::sparse::state_type> scheduler(this->A.getRowGroupCount());
@ -107,12 +116,14 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(scheduler, true);
submatrix.convertToEquationSystem();
storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, this->A.getRowGroupIndices(), b);
// Solve the equation system for the 'DTMC'.
// FIXME: we need to remove the 0- and 1- states to make the solution unique.
// HOWEVER: if we start with a valid scheduler, then we will never get an illegal one, because staying
// within illegal MECs will never strictly improve the value. Is this true?
auto solver = linearEquationSolverFactory->create(submatrix);
solver->solveEquationSystem(x, subB, &deterministicMultiplyResult);
// Go through the multiplication result and see whether we can improve any of the choices.
bool schedulerImproved = false;
for (uint_fast64_t group = 0; group < this->A.getRowGroupCount(); ++group) {
@ -121,7 +132,7 @@ namespace storm {
if (choice - this->A.getRowGroupIndices()[group] == scheduler[group]) {
continue;
}
// Create the value of the choice.
ValueType choiceValue = storm::utility::zero<ValueType>();
for (auto const& entry : this->A.getRow(choice)) {
@ -204,7 +215,7 @@ namespace storm {
storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, this->A.getRowGroupIndices());
// Determine whether the method converged.
if (storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, static_cast<ValueType>(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion())) {
if (storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion())) {
status = Status::Converged;
}
@ -278,12 +289,12 @@ namespace storm {
}
template<typename ValueType>
StandardMinMaxLinearEquationSolverSettings const& StandardMinMaxLinearEquationSolver<ValueType>::getSettings() const {
StandardMinMaxLinearEquationSolverSettings<ValueType> const& StandardMinMaxLinearEquationSolver<ValueType>::getSettings() const {
return settings;
}
template<typename ValueType>
StandardMinMaxLinearEquationSolverSettings& StandardMinMaxLinearEquationSolver<ValueType>::getSettings() {
StandardMinMaxLinearEquationSolverSettings<ValueType>& StandardMinMaxLinearEquationSolver<ValueType>::getSettings() {
return settings;
}
@ -300,10 +311,20 @@ namespace storm {
template<typename ValueType>
StandardMinMaxLinearEquationSolverFactory<ValueType>::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, bool trackScheduler) : MinMaxLinearEquationSolverFactory<ValueType>(trackScheduler) {
switch (solverType) {
case EquationSolverType::Gmmxx: linearEquationSolverFactory = std::make_unique<GmmxxLinearEquationSolverFactory<ValueType>>(); break;
case EquationSolverType::Eigen: linearEquationSolverFactory = std::make_unique<EigenLinearEquationSolverFactory<ValueType>>(); break;
case EquationSolverType::Native: linearEquationSolverFactory = std::make_unique<NativeLinearEquationSolverFactory<ValueType>>(); break;
case EquationSolverType::Elimination: linearEquationSolverFactory = std::make_unique<EliminationLinearEquationSolverFactory<ValueType>>(); break;
case EquationSolverType::Gmmxx: linearEquationSolverFactory = std::make_unique<GmmxxLinearEquationSolverFactory<ValueType>>(); break;
case EquationSolverType::Eigen: linearEquationSolverFactory = std::make_unique<EigenLinearEquationSolverFactory<ValueType>>(); break;
case EquationSolverType::Native: linearEquationSolverFactory = std::make_unique<NativeLinearEquationSolverFactory<ValueType>>(); break;
case EquationSolverType::Elimination: linearEquationSolverFactory = std::make_unique<EliminationLinearEquationSolverFactory<ValueType>>(); break;
}
}
template<>
StandardMinMaxLinearEquationSolverFactory<storm::RationalNumber>::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, bool trackScheduler) : MinMaxLinearEquationSolverFactory<storm::RationalNumber>(trackScheduler) {
switch (solverType) {
case EquationSolverType::Eigen: linearEquationSolverFactory = std::make_unique<EigenLinearEquationSolverFactory<storm::RationalNumber>>(); break;
case EquationSolverType::Elimination: linearEquationSolverFactory = std::make_unique<EliminationLinearEquationSolverFactory<storm::RationalNumber>>(); break;
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot create the requested solver for this data type.");
}
}
@ -331,12 +352,12 @@ namespace storm {
}
template<typename ValueType>
StandardMinMaxLinearEquationSolverSettings& StandardMinMaxLinearEquationSolverFactory<ValueType>::getSettings() {
StandardMinMaxLinearEquationSolverSettings<ValueType>& StandardMinMaxLinearEquationSolverFactory<ValueType>::getSettings() {
return settings;
}
template<typename ValueType>
StandardMinMaxLinearEquationSolverSettings const& StandardMinMaxLinearEquationSolverFactory<ValueType>::getSettings() const {
StandardMinMaxLinearEquationSolverSettings<ValueType> const& StandardMinMaxLinearEquationSolverFactory<ValueType>::getSettings() const {
return settings;
}
@ -361,12 +382,16 @@ namespace storm {
}
template class StandardMinMaxLinearEquationSolver<double>;
template class StandardMinMaxLinearEquationSolverFactory<double>;
template class GmmxxMinMaxLinearEquationSolverFactory<double>;
template class EigenMinMaxLinearEquationSolverFactory<double>;
template class NativeMinMaxLinearEquationSolverFactory<double>;
template class EliminationMinMaxLinearEquationSolverFactory<double>;
template class StandardMinMaxLinearEquationSolver<storm::RationalNumber>;
template class StandardMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
template class EigenMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
template class EliminationMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
}
}

23
src/solver/StandardMinMaxLinearEquationSolver.h
View File

@ -6,6 +6,7 @@
namespace storm {
namespace solver {
template<typename ValueType>
class StandardMinMaxLinearEquationSolverSettings {
public:
StandardMinMaxLinearEquationSolverSettings();
@ -17,31 +18,31 @@ namespace storm {
void setSolutionMethod(SolutionMethod const& solutionMethod);
void setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations);
void setRelativeTerminationCriterion(bool value);
void setPrecision(double precision);
void setPrecision(ValueType precision);
SolutionMethod const& getSolutionMethod() const;
uint64_t getMaximalNumberOfIterations() const;
double getPrecision() const;
ValueType getPrecision() const;
bool getRelativeTerminationCriterion() const;
private:
SolutionMethod solutionMethod;
uint64_t maximalNumberOfIterations;
double precision;
ValueType precision;
bool relative;
};
template<typename ValueType>
class StandardMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver<ValueType> {
public:
StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings const& settings = StandardMinMaxLinearEquationSolverSettings());
StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings const& settings = StandardMinMaxLinearEquationSolverSettings());
StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings<ValueType> const& settings = StandardMinMaxLinearEquationSolverSettings<ValueType>());
StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings<ValueType> const& settings = StandardMinMaxLinearEquationSolverSettings<ValueType>());
virtual void solveEquationSystem(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* newX = nullptr) const override;
virtual void performMatrixVectorMultiplication(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const override;
StandardMinMaxLinearEquationSolverSettings const& getSettings() const;
StandardMinMaxLinearEquationSolverSettings& getSettings();
StandardMinMaxLinearEquationSolverSettings<ValueType> const& getSettings() const;
StandardMinMaxLinearEquationSolverSettings<ValueType>& getSettings();
private:
void solveEquationSystemPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const;
@ -57,7 +58,7 @@ namespace storm {
void reportStatus(Status status, uint64_t iterations) const;
/// The settings of this solver.
StandardMinMaxLinearEquationSolverSettings settings;
StandardMinMaxLinearEquationSolverSettings<ValueType> settings;
/// The factory used to obtain linear equation solvers.
std::unique_ptr<LinearEquationSolverFactory<ValueType>> linearEquationSolverFactory;
@ -81,11 +82,11 @@ namespace storm {
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const override;
StandardMinMaxLinearEquationSolverSettings& getSettings();
StandardMinMaxLinearEquationSolverSettings const& getSettings() const;
StandardMinMaxLinearEquationSolverSettings<ValueType>& getSettings();
StandardMinMaxLinearEquationSolverSettings<ValueType> const& getSettings() const;
private:
StandardMinMaxLinearEquationSolverSettings settings;
StandardMinMaxLinearEquationSolverSettings<ValueType> settings;
std::unique_ptr<LinearEquationSolverFactory<ValueType>> linearEquationSolverFactory;
};

8
src/solver/TerminationCondition.cpp
View File

@ -1,6 +1,8 @@
#include "src/solver/TerminationCondition.h"
#include "src/utility/vector.h"
#include "src/adapters/CarlAdapter.h"
#include "src/utility/macros.h"
namespace storm {
@ -24,7 +26,7 @@ namespace storm {
}
template<typename ValueType>
TerminateIfFilteredExtremumExceedsThreshold<ValueType>::TerminateIfFilteredExtremumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict, bool useMinimum) : TerminateIfFilteredSumExceedsThreshold<ValueType>(filter, threshold, strict), useMinimum(useMinimum) {
TerminateIfFilteredExtremumExceedsThreshold<ValueType>::TerminateIfFilteredExtremumExceedsThreshold(storm::storage::BitVector const& filter, bool strict, ValueType const& threshold, bool useMinimum) : TerminateIfFilteredSumExceedsThreshold<ValueType>(filter, threshold, strict), useMinimum(useMinimum) {
// Intentionally left empty.
}
@ -37,5 +39,9 @@ namespace storm {
template class TerminateIfFilteredSumExceedsThreshold<double>;
template class TerminateIfFilteredExtremumExceedsThreshold<double>;
template class TerminateIfFilteredSumExceedsThreshold<storm::RationalNumber>;
template class TerminateIfFilteredExtremumExceedsThreshold<storm::RationalNumber>;
}
}

2
src/solver/TerminationCondition.h
View File

@ -34,7 +34,7 @@ namespace storm {
template<typename ValueType>
class TerminateIfFilteredExtremumExceedsThreshold : public TerminateIfFilteredSumExceedsThreshold<ValueType>{
public:
TerminateIfFilteredExtremumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict, bool useMinimum);
TerminateIfFilteredExtremumExceedsThreshold(storm::storage::BitVector const& filter, bool strict, ValueType const& threshold, bool useMinimum);
bool terminateNow(std::vector<ValueType> const& currentValue) const;
protected:

3
src/storage/MaximalEndComponentDecomposition.cpp
View File

@ -193,5 +193,8 @@ namespace storm {
template class MaximalEndComponentDecomposition<double>;
template MaximalEndComponentDecomposition<double>::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<double> const& model);
template class MaximalEndComponentDecomposition<storm::RationalNumber>;
template MaximalEndComponentDecomposition<storm::RationalNumber>::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<storm::RationalNumber> const& model);
}
}

14
src/utility/constants.cpp
View File

@ -109,6 +109,11 @@ namespace storm {
return number;
}
template<typename ValueType>
ValueType abs(ValueType const& number) {
return std::fabs(number);
}
template<>
RationalFunction& simplify(RationalFunction& value);
@ -153,6 +158,11 @@ namespace storm {
return RationalFunction(carl::rationalize<RationalNumber>(number));
}
template<>
storm::RationalNumber abs(storm::RationalNumber const& number) {
return carl::abs(number);
}
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType> simplify(storm::storage::MatrixEntry<IndexType, ValueType> matrixEntry) {
simplify(matrixEntry.getValue());
@ -188,6 +198,8 @@ namespace storm {
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& matrixEntry);
template double abs(double const& number);
template bool isOne(float const& value);
template bool isZero(float const& value);
template bool isConstant(float const& value);
@ -252,6 +264,8 @@ namespace storm {
template double convertNumber(storm::RationalNumber const& number);
template storm::RationalNumber convertNumber(double const& number);
template storm::RationalNumber abs(storm::RationalNumber const& number);
// template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent);
template storm::RationalNumber simplify(storm::RationalNumber value);

3
src/utility/constants.h
View File

@ -53,6 +53,9 @@ namespace storm {
template<typename TargetType, typename SourceType>
TargetType convertNumber(SourceType const& number);
template<typename ValueType>
ValueType abs(ValueType const& number);
}
}

4
src/utility/graph.cpp
View File

@ -1200,7 +1200,11 @@ namespace storm {
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<storm::storage::BitVector> const& rowFilter);
template storm::storage::PartialScheduler computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix);
template storm::storage::PartialScheduler computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ;

28
src/utility/storm.h
View File

@ -294,6 +294,18 @@ namespace storm {
return result;
}
template<typename ValueType>
std::unique_ptr<storm::modelchecker::CheckResult> verifySparseMdp(std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp, storm::modelchecker::CheckTask<storm::logic::Formula> const& task) {
std::unique_ptr<storm::modelchecker::CheckResult> result;
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported.");
}
return result;
}
template<typename ValueType>
std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant = false) {
storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
@ -302,19 +314,7 @@ namespace storm {
if (model->getType() == storm::models::ModelType::Dtmc) {
result = verifySparseDtmc(model->template as<storm::models::sparse::Dtmc<ValueType>>(), task);
} else if (model->getType() == storm::models::ModelType::Mdp) {
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
#ifdef STORM_HAVE_CUDA
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isCudaSet()) {
storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<ValueType> modelchecker(*mdp);
result = modelchecker.check(task);
} else {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
result = modelchecker.check(task);
}
#else
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
result = modelchecker.check(task);
#endif
result = verifySparseMdp(model->template as<storm::models::sparse::Mdp<ValueType>>(), task);
} else if (model->getType() == storm::models::ModelType::Ctmc) {
result = verifySparseCtmc(model->template as<storm::models::sparse::Ctmc<ValueType>>(), task);
} else if (model->getType() == storm::models::ModelType::MarkovAutomaton) {
@ -341,6 +341,8 @@ namespace storm {
result = verifySparseDtmc(model->template as<storm::models::sparse::Dtmc<storm::RationalNumber>>(), task);
} else if (model->getType() == storm::models::ModelType::Ctmc) {
result = verifySparseCtmc(model->template as<storm::models::sparse::Ctmc<storm::RationalNumber>>(), task);
} else if (model->getType() == storm::models::ModelType::Mdp) {
result = verifySparseMdp(model->template as<storm::models::sparse::Mdp<storm::RationalNumber>>(), task);
} else {
STORM_LOG_ASSERT(false, "Illegal model type.");
}

7
src/utility/vector.h
View File

@ -12,6 +12,7 @@
#include <functional>
#include "src/storage/BitVector.h"
#include "src/utility/constants.h"
#include "src/utility/macros.h"
#include "src/solver/OptimizationDirection.h"
@ -590,13 +591,13 @@ namespace storm {
bool equalModuloPrecision(T const& val1, T const& val2, T precision, bool relativeError = true) {
if (relativeError) {
if (val2 == 0) {
return (std::abs(val1) <= precision);
return (storm::utility::abs(val1) <= precision);
}
if (std::abs((val1 - val2)/val2) > precision) {
if (storm::utility::abs((val1 - val2)/val2) > precision) {
return false;
}
} else {
if (std::abs(val1 - val2) > precision) return false;
if (storm::utility::abs(val1 - val2) > precision) return false;
}
return true;
}

Write Preview
Loading…
Cancel
Save