From 9f1487392ef53690c97093ec52e12832ad123053 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 19 May 2020 10:36:49 +0200 Subject: [PATCH] We now avoid the renaming of 'Eigen' to 'StormEigen' as this is (hopefully) not needed anymore. --- src/storm/adapters/EigenAdapter.cpp | 30 ++++----- src/storm/adapters/EigenAdapter.h | 12 ++-- .../solver/EigenLinearEquationSolver.cpp | 62 +++++++++---------- src/storm/solver/EigenLinearEquationSolver.h | 2 +- src/storm/storage/geometry/NativePolytope.cpp | 42 ++++++------- src/storm/storage/geometry/NativePolytope.h | 4 +- .../HyperplaneCollector.cpp | 2 +- .../HyperplaneCollector.h | 4 +- .../HyperplaneEnumeration.cpp | 14 ++--- .../HyperplaneEnumeration.h | 4 +- .../nativepolytopeconversion/QuickHull.cpp | 10 +-- .../nativepolytopeconversion/QuickHull.h | 4 +- .../SubsetEnumerator.cpp | 8 +-- src/storm/utility/eigen.h | 8 +-- .../csl/LraCtmcCslModelCheckerTest.cpp | 4 +- 15 files changed, 106 insertions(+), 104 deletions(-) diff --git a/src/storm/adapters/EigenAdapter.cpp b/src/storm/adapters/EigenAdapter.cpp index 61cf7b98f..536e01e89 100644 --- a/src/storm/adapters/EigenAdapter.cpp +++ b/src/storm/adapters/EigenAdapter.cpp @@ -4,9 +4,9 @@ namespace storm { namespace adapters { template - std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix) { + std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix) { // Build a list of triplets and let Eigen care about the insertion. - std::vector> triplets; + std::vector> triplets; triplets.reserve(matrix.getNonzeroEntryCount()); for (uint64_t row = 0; row < matrix.getRowCount(); ++row) { @@ -15,33 +15,33 @@ namespace storm { } } - std::unique_ptr> result = std::make_unique>(matrix.getRowCount(), matrix.getColumnCount()); + std::unique_ptr> result = std::make_unique>(matrix.getRowCount(), matrix.getColumnCount()); result->setFromTriplets(triplets.begin(), triplets.end()); return result; } template - std::vector EigenAdapter::toStdVector(StormEigen::Matrix const& v){ + std::vector EigenAdapter::toStdVector(Eigen::Matrix const& v){ return std::vector(v.data(), v.data() + v.rows()); } template - StormEigen::Matrix EigenAdapter::toEigenVector(std::vector const& v){ - return StormEigen::Matrix::Map(v.data(), v.size()); + Eigen::Matrix EigenAdapter::toEigenVector(std::vector const& v){ + return Eigen::Matrix::Map(v.data(), v.size()); } - template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); - template std::vector EigenAdapter::toStdVector(StormEigen::Matrix const& v); - template StormEigen::Matrix EigenAdapter::toEigenVector(std::vector const& v); + template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); + template std::vector EigenAdapter::toStdVector(Eigen::Matrix const& v); + template Eigen::Matrix EigenAdapter::toEigenVector(std::vector const& v); #ifdef STORM_HAVE_CARL - template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); - template std::vector EigenAdapter::toStdVector(StormEigen::Matrix const& v); - template StormEigen::Matrix EigenAdapter::toEigenVector(std::vector const& v); + template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); + template std::vector EigenAdapter::toStdVector(Eigen::Matrix const& v); + template Eigen::Matrix EigenAdapter::toEigenVector(std::vector const& v); - template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); - template std::vector EigenAdapter::toStdVector(StormEigen::Matrix const& v); - template StormEigen::Matrix EigenAdapter::toEigenVector(std::vector const& v); + template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); + template std::vector EigenAdapter::toStdVector(Eigen::Matrix const& v); + template Eigen::Matrix EigenAdapter::toEigenVector(std::vector const& v); #endif } } diff --git a/src/storm/adapters/EigenAdapter.h b/src/storm/adapters/EigenAdapter.h index 41d191c4f..ef32bd163 100644 --- a/src/storm/adapters/EigenAdapter.h +++ b/src/storm/adapters/EigenAdapter.h @@ -18,13 +18,13 @@ namespace storm { * @return A pointer to a row-major sparse matrix in gmm++ format. */ template - static std::unique_ptr> toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); + static std::unique_ptr> toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); template - static std::vector toStdVector(StormEigen::Matrix const& v); + static std::vector toStdVector(Eigen::Matrix const& v); template - static StormEigen::Matrix toEigenVector(std::vector const& v); + static Eigen::Matrix toEigenVector(std::vector const& v); }; } @@ -33,8 +33,8 @@ namespace storm { namespace std { template - struct hash> { - std::size_t operator()(StormEigen::Matrix const &vector) const { + struct hash> { + std::size_t operator()(Eigen::Matrix const &vector) const { size_t seed = 0; for (uint_fast64_t i = 0; i < static_cast(vector.rows()); ++i) { carl::hash_add(seed, std::hash()(vector(i))); @@ -44,7 +44,7 @@ namespace std { }; } -namespace StormEigen { +namespace Eigen { template<> struct NumTraits : GenericNumTraits { typedef storm::RationalNumber Real; diff --git a/src/storm/solver/EigenLinearEquationSolver.cpp b/src/storm/solver/EigenLinearEquationSolver.cpp index 0ca9a4554..b29aa0da8 100644 --- a/src/storm/solver/EigenLinearEquationSolver.cpp +++ b/src/storm/solver/EigenLinearEquationSolver.cpp @@ -72,14 +72,14 @@ namespace storm { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with with rational numbers using LU factorization (Eigen library)."); // Map the input vectors to Eigen's format. - auto eigenX = StormEigen::Matrix::Map(x.data(), x.size()); - auto eigenB = StormEigen::Matrix::Map(b.data(), b.size()); + auto eigenX = Eigen::Matrix::Map(x.data(), x.size()); + auto eigenB = Eigen::Matrix::Map(b.data(), b.size()); - StormEigen::SparseLU, StormEigen::COLAMDOrdering> solver; + Eigen::SparseLU, Eigen::COLAMDOrdering> solver; solver.compute(*eigenA); solver._solve_impl(eigenB, eigenX); - return solver.info() == StormEigen::ComputationInfo::Success; + return solver.info() == Eigen::ComputationInfo::Success; } // Specialization for storm::RationalFunction @@ -90,13 +90,13 @@ namespace storm { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with rational functions using LU factorization (Eigen library)."); // Map the input vectors to Eigen's format. - auto eigenX = StormEigen::Matrix::Map(x.data(), x.size()); - auto eigenB = StormEigen::Matrix::Map(b.data(), b.size()); + auto eigenX = Eigen::Matrix::Map(x.data(), x.size()); + auto eigenB = Eigen::Matrix::Map(b.data(), b.size()); - StormEigen::SparseLU, StormEigen::COLAMDOrdering> solver; + Eigen::SparseLU, Eigen::COLAMDOrdering> solver; solver.compute(*eigenA); solver._solve_impl(eigenB, eigenX); - return solver.info() == StormEigen::ComputationInfo::Success; + return solver.info() == Eigen::ComputationInfo::Success; } #endif @@ -104,19 +104,19 @@ namespace storm { template bool EigenLinearEquationSolver::internalSolveEquations(Environment const& env, std::vector& x, std::vector const& b) const { // Map the input vectors to Eigen's format. - auto eigenX = StormEigen::Matrix::Map(x.data(), x.size()); - auto eigenB = StormEigen::Matrix::Map(b.data(), b.size()); + auto eigenX = Eigen::Matrix::Map(x.data(), x.size()); + auto eigenB = Eigen::Matrix::Map(b.data(), b.size()); auto solutionMethod = getMethod(env, env.solver().isForceExact()); if (solutionMethod == EigenLinearEquationSolverMethod::SparseLU) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with sparse LU factorization (Eigen library)."); - StormEigen::SparseLU, StormEigen::COLAMDOrdering> solver; + Eigen::SparseLU, Eigen::COLAMDOrdering> solver; solver.compute(*this->eigenA); solver._solve_impl(eigenB, eigenX); } else { bool converged = false; uint64_t numberOfIterations = 0; - StormEigen::Index maxIter = std::numeric_limits::max(); + Eigen::Index maxIter = std::numeric_limits::max(); if (env.solver().eigen().getMaximalNumberOfIterations() < static_cast(maxIter)) { maxIter = env.solver().eigen().getMaximalNumberOfIterations(); } @@ -127,102 +127,102 @@ namespace storm { if (preconditioner == EigenLinearEquationSolverPreconditioner::Ilu) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BiCGSTAB with Ilu preconditioner (Eigen library)."); - StormEigen::BiCGSTAB, StormEigen::IncompleteLUT> solver; + Eigen::BiCGSTAB, Eigen::IncompleteLUT> solver; solver.compute(*this->eigenA); solver.setTolerance(precision); solver.setMaxIterations(maxIter); eigenX = solver.solveWithGuess(eigenB, eigenX); - converged = solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == Eigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else if (preconditioner == EigenLinearEquationSolverPreconditioner::Diagonal) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BiCGSTAB with Diagonal preconditioner (Eigen library)."); - StormEigen::BiCGSTAB, StormEigen::DiagonalPreconditioner> solver; + Eigen::BiCGSTAB, Eigen::DiagonalPreconditioner> solver; solver.setTolerance(precision); solver.setMaxIterations(maxIter); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); - converged = solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == Eigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BiCGSTAB with identity preconditioner (Eigen library)."); - StormEigen::BiCGSTAB, StormEigen::IdentityPreconditioner> solver; + Eigen::BiCGSTAB, Eigen::IdentityPreconditioner> solver; solver.setTolerance(precision); solver.setMaxIterations(maxIter); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); numberOfIterations = solver.iterations(); - converged = solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == Eigen::ComputationInfo::Success; } } else if (solutionMethod == EigenLinearEquationSolverMethod::DGmres) { if (preconditioner == EigenLinearEquationSolverPreconditioner::Ilu) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with DGMRES with Ilu preconditioner (Eigen library)."); - - StormEigen::DGMRES, StormEigen::IncompleteLUT> solver; + Eigen::DGMRES, Eigen::IncompleteLUT> solver; solver.setTolerance(precision); solver.setMaxIterations(maxIter); solver.set_restart(restartThreshold); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); - converged = solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == Eigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else if (preconditioner == EigenLinearEquationSolverPreconditioner::Diagonal) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with DGMRES with Diagonal preconditioner (Eigen library)."); - StormEigen::DGMRES, StormEigen::DiagonalPreconditioner> solver; + Eigen::DGMRES, Eigen::DiagonalPreconditioner> solver; solver.setTolerance(precision); solver.setMaxIterations(maxIter); solver.set_restart(restartThreshold); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); - converged = solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == Eigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with DGMRES with identity preconditioner (Eigen library)."); - StormEigen::DGMRES, StormEigen::IdentityPreconditioner> solver; + Eigen::DGMRES, Eigen::IdentityPreconditioner> solver; solver.setTolerance(precision); solver.setMaxIterations(maxIter); solver.set_restart(restartThreshold); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); - converged = solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == Eigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } + } else if (solutionMethod == EigenLinearEquationSolverMethod::Gmres) { if (preconditioner == EigenLinearEquationSolverPreconditioner::Ilu) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with GMRES with Ilu preconditioner (Eigen library)."); - StormEigen::GMRES, StormEigen::IncompleteLUT> solver; + Eigen::GMRES, Eigen::IncompleteLUT> solver; solver.setTolerance(precision); solver.setMaxIterations(maxIter); solver.set_restart(restartThreshold); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); - converged = solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == Eigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else if (preconditioner == EigenLinearEquationSolverPreconditioner::Diagonal) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with GMRES with Diagonal preconditioner (Eigen library)."); - StormEigen::GMRES, StormEigen::DiagonalPreconditioner> solver; + Eigen::GMRES, Eigen::DiagonalPreconditioner> solver; solver.setTolerance(precision); solver.setMaxIterations(maxIter); solver.set_restart(restartThreshold); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); - converged = solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == Eigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with GMRES with identity preconditioner (Eigen library)."); - StormEigen::GMRES, StormEigen::IdentityPreconditioner> solver; + Eigen::GMRES, Eigen::IdentityPreconditioner> solver; solver.setTolerance(precision); solver.setMaxIterations(maxIter); solver.set_restart(restartThreshold); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); - converged = solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == Eigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } } diff --git a/src/storm/solver/EigenLinearEquationSolver.h b/src/storm/solver/EigenLinearEquationSolver.h index 63768563a..32697b615 100644 --- a/src/storm/solver/EigenLinearEquationSolver.h +++ b/src/storm/solver/EigenLinearEquationSolver.h @@ -32,7 +32,7 @@ namespace storm { virtual uint64_t getMatrixColumnCount() const override; // The (eigen) matrix associated with this equation solver. - std::unique_ptr> eigenA; + std::unique_ptr> eigenA; }; diff --git a/src/storm/storage/geometry/NativePolytope.cpp b/src/storm/storage/geometry/NativePolytope.cpp index 5c8e0742d..9f1dc4174 100644 --- a/src/storm/storage/geometry/NativePolytope.cpp +++ b/src/storm/storage/geometry/NativePolytope.cpp @@ -22,12 +22,12 @@ namespace storm { // The polytope is universal emptyStatus = EmptyStatus::Nonempty; } else { - StormEigen::Index maxCol = halfspaces.front().normalVector().size(); - StormEigen::Index maxRow = halfspaces.size(); + Eigen::Index maxCol = halfspaces.front().normalVector().size(); + Eigen::Index maxRow = halfspaces.size(); A = EigenMatrix(maxRow, maxCol); b = EigenVector(maxRow); - for (StormEigen::Index row = 0; row < A.rows(); ++row ){ - assert((StormEigen::Index) halfspaces[row].normalVector().size() == maxCol); + for (Eigen::Index row = 0; row < A.rows(); ++row ){ + assert((Eigen::Index) halfspaces[row].normalVector().size() == maxCol); b(row) = halfspaces[row].offset(); A.row(row) = storm::adapters::EigenAdapter::toEigenVector(halfspaces[row].normalVector()); } @@ -107,7 +107,7 @@ namespace storm { std::vector> result; result.reserve(A.rows()); - for (StormEigen::Index row=0; row < A.rows(); ++row){ + for (Eigen::Index row=0; row < A.rows(); ++row){ result.emplace_back(storm::adapters::EigenAdapter::toStdVector(EigenVector(A.row(row))), b(row)); } return result; @@ -145,7 +145,7 @@ namespace storm { template bool NativePolytope::contains(Point const& point) const{ EigenVector x = storm::adapters::EigenAdapter::toEigenVector(point); - for (StormEigen::Index row=0; row < A.rows(); ++row){ + for (Eigen::Index row=0; row < A.rows(); ++row){ if ((A.row(row) * x)(0) > b(row)){ return false; } @@ -252,7 +252,7 @@ namespace storm { resultConstraints.reserve(A.rows() + nativeRhs.A.rows()); // evaluation of rhs in directions of lhs - for (StormEigen::Index i = 0; i < A.rows(); ++i) { + for (Eigen::Index i = 0; i < A.rows(); ++i) { auto optimizationRes = nativeRhs.optimize(A.row(i)); if ( optimizationRes.second ) { resultConstraints.emplace_back(A.row(i), b(i) + (A.row(i) * optimizationRes.first)(0)); @@ -261,7 +261,7 @@ namespace storm { } // evaluation of lhs in directions of rhs - for (StormEigen::Index i = 0; i < nativeRhs.A.rows(); ++i) { + for (Eigen::Index i = 0; i < nativeRhs.A.rows(); ++i) { auto optimizationRes = optimize(nativeRhs.A.row(i)); if ( optimizationRes.second ) { resultConstraints.emplace_back(nativeRhs.A.row(i), nativeRhs.b(i) + (nativeRhs.A.row(i) * optimizationRes.first)(0)); @@ -274,7 +274,7 @@ namespace storm { } else { EigenMatrix newA(resultConstraints.size(), resultConstraints.front().first.rows()); EigenVector newb(resultConstraints.size()); - for (StormEigen::Index i = 0; i < newA.rows(); ++i) { + for (Eigen::Index i = 0; i < newA.rows(); ++i) { newA.row(i) = resultConstraints[i].first; newb(i) = resultConstraints[i].second; } @@ -285,15 +285,15 @@ namespace storm { template std::shared_ptr> NativePolytope::affineTransformation(std::vector const& matrix, Point const& vector) const { STORM_LOG_THROW(!matrix.empty(), storm::exceptions::InvalidArgumentException, "Invoked affine transformation with a matrix without rows."); - StormEigen::Index rows = matrix.size(); - StormEigen::Index columns = matrix.front().size(); + Eigen::Index rows = matrix.size(); + Eigen::Index columns = matrix.front().size(); EigenMatrix eigenMatrix(rows, columns); - for (StormEigen::Index row = 0; row < rows; ++row) { + for (Eigen::Index row = 0; row < rows; ++row) { eigenMatrix.row(row) = storm::adapters::EigenAdapter::toEigenVector(matrix[row]); } EigenVector eigenVector = storm::adapters::EigenAdapter::toEigenVector(vector); - StormEigen::FullPivLU luMatrix( eigenMatrix ); + Eigen::FullPivLU luMatrix( eigenMatrix ); STORM_LOG_THROW(luMatrix.isInvertible(), storm::exceptions::NotImplementedException, "Affine Transformation of native polytope only implemented if the transformation matrix is invertable"); if (isUniversal()) { return std::make_shared>(std::vector>()); @@ -312,7 +312,7 @@ namespace storm { storm::solver::Z3LpSolver solver(storm::solver::OptimizationDirection::Maximize); std::vector variables; variables.reserve(A.cols()); - for (StormEigen::Index i = 0; i < A.cols(); ++i) { + for (Eigen::Index i = 0; i < A.cols(); ++i) { variables.push_back(solver.addUnboundedContinuousVariable("x" + std::to_string(i), direction[i])); } std::vector constraints = getConstraints(solver.getManager(), variables); @@ -343,7 +343,7 @@ namespace storm { storm::solver::Z3LpSolver solver(storm::solver::OptimizationDirection::Maximize); std::vector variables; variables.reserve(A.cols()); - for (StormEigen::Index i = 0; i < A.cols(); ++i) { + for (Eigen::Index i = 0; i < A.cols(); ++i) { variables.push_back(solver.addUnboundedContinuousVariable("x" + std::to_string(i), static_cast(direction(i)))); } std::vector constraints = getConstraints(solver.getManager(), variables); @@ -354,7 +354,7 @@ namespace storm { solver.optimize(); if (solver.isOptimal()) { auto result = std::make_pair(EigenVector(A.cols()), true); - for (StormEigen::Index i = 0; i < A.cols(); ++i) { + for (Eigen::Index i = 0; i < A.cols(); ++i) { result.first(i) = solver.getContinuousValue(variables[i]); } return result; @@ -379,7 +379,7 @@ namespace storm { std::vector NativePolytope::declareVariables(storm::expressions::ExpressionManager& manager, std::string const& namePrefix) const { std::vector result; result.reserve(A.cols()); - for (StormEigen::Index col=0; col < A.cols(); ++col){ + for (Eigen::Index col=0; col < A.cols(); ++col){ result.push_back(manager.declareVariable(namePrefix + std::to_string(col), manager.getRationalType())); } return result; @@ -388,9 +388,9 @@ namespace storm { template std::vector NativePolytope::getConstraints(storm::expressions::ExpressionManager const& manager, std::vector const& variables) const { std::vector result; - for (StormEigen::Index row = 0; row < A.rows(); ++row) { + for (Eigen::Index row = 0; row < A.rows(); ++row) { storm::expressions::Expression lhs = manager.rational(A(row,0)) * variables[0].getExpression(); - for (StormEigen::Index col=1; col < A.cols(); ++col) { + for (Eigen::Index col=1; col < A.cols(); ++col) { lhs = lhs + manager.rational(A(row,col)) * variables[col].getExpression(); } result.push_back(lhs <= manager.rational(b(row))); @@ -411,9 +411,9 @@ namespace storm { solver->add(constraint); } storm::storage::BitVector keptConstraints(A.rows(), false); - for (StormEigen::Index row = 0; row < A.rows(); ++row) { + for (Eigen::Index row = 0; row < A.rows(); ++row) { storm::expressions::Expression lhs = manager->rational(A(row,0)) * variables[0].getExpression(); - for (StormEigen::Index col=1; col < A.cols(); ++col) { + for (Eigen::Index col=1; col < A.cols(); ++col) { lhs = lhs + manager->rational(A(row,col)) * variables[col].getExpression(); } solver->push(); diff --git a/src/storm/storage/geometry/NativePolytope.h b/src/storm/storage/geometry/NativePolytope.h index 324d5b1fb..3e6886dc3 100644 --- a/src/storm/storage/geometry/NativePolytope.h +++ b/src/storm/storage/geometry/NativePolytope.h @@ -14,8 +14,8 @@ namespace storm { class NativePolytope : public Polytope { public: - typedef StormEigen::Matrix EigenMatrix; - typedef StormEigen::Matrix EigenVector; + typedef Eigen::Matrix EigenMatrix; + typedef Eigen::Matrix EigenVector; enum class EmptyStatus{ Unknown, //It is unknown whether the polytope is empty or not diff --git a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneCollector.cpp b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneCollector.cpp index 347b99488..d563f03f0 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneCollector.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneCollector.cpp @@ -15,7 +15,7 @@ namespace storm { template< typename ValueType> bool HyperplaneCollector::insert(EigenVector && normal, ValueType && offset, std::vectorconst* indexList) { //Normalize - ValueType infinityNorm = normal.template lpNorm(); + ValueType infinityNorm = normal.template lpNorm(); if(infinityNorm != (ValueType)0 ){ normal /= infinityNorm; offset /= infinityNorm; diff --git a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneCollector.h b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneCollector.h index b9c1fc21c..393c28f18 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneCollector.h +++ b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneCollector.h @@ -17,8 +17,8 @@ namespace storm { class HyperplaneCollector { public: - typedef StormEigen::Matrix EigenMatrix; - typedef StormEigen::Matrix EigenVector; + typedef Eigen::Matrix EigenMatrix; + typedef Eigen::Matrix EigenVector; HyperplaneCollector() = default; HyperplaneCollector(const HyperplaneCollector& orig) = default; diff --git a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp index 8a6277e13..4e6078797 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp @@ -11,7 +11,7 @@ namespace storm { template void HyperplaneEnumeration::generateVerticesFromConstraints(EigenMatrix const& constraintMatrix, EigenVector const& constraintVector, bool generateRelevantHyperplanesAndVertexSets) { STORM_LOG_DEBUG("Invoked Hyperplane enumeration with " << constraintMatrix.rows() << " constraints."); - StormEigen::Index dimension = constraintMatrix.cols(); + Eigen::Index dimension = constraintMatrix.cols(); if (dimension == 0) { // No halfspaces means no vertices resultVertices.clear(); @@ -28,14 +28,14 @@ namespace storm { EigenMatrix subMatrix(dimension, dimension); EigenVector subVector(dimension); - for (StormEigen::Index i = 0; i < dimension; ++i){ + for (Eigen::Index i = 0; i < dimension; ++i){ subMatrix.row(i) = constraintMatrix.row(subset[i]); subVector(i) = constraintVector(subset[i]); } EigenVector point = subMatrix.fullPivLu().solve(subVector); bool pointContained = true; - for (StormEigen::Index row=0; row < constraintMatrix.rows(); ++row){ + for (Eigen::Index row=0; row < constraintMatrix.rows(); ++row){ if ((constraintMatrix.row(row) * point)(0) > constraintVector(row)){ pointContained = false; break; @@ -53,7 +53,7 @@ namespace storm { if (generateRelevantHyperplanesAndVertexSets){ //For each hyperplane, get the number of (unique) vertices that lie on it. - std::vector verticesOnHyperplaneCounter(constraintMatrix.rows(), 0); + std::vector verticesOnHyperplaneCounter(constraintMatrix.rows(), 0); for (auto const& mapEntry : vertexCollector){ for (auto const& hyperplaneIndex : mapEntry.second){ ++verticesOnHyperplaneCounter[hyperplaneIndex]; @@ -91,7 +91,7 @@ namespace storm { for (auto const& mapEntry : vertexCollector){ for (auto const& oldHyperplaneIndex : mapEntry.second){ //ignore the hyperplanes which are redundant, i.e. for which there is no new index - if ((StormEigen::Index) oldToNewIndexMapping[oldHyperplaneIndex] < relevantVector.rows()){ + if ((Eigen::Index) oldToNewIndexMapping[oldHyperplaneIndex] < relevantVector.rows()){ vertexSets[oldToNewIndexMapping[oldHyperplaneIndex]].insert(resultVertices.size()); } } @@ -120,10 +120,10 @@ namespace storm { bool HyperplaneEnumeration::linearDependenciesFilter(std::vector const& subset, uint_fast64_t const& item, EigenMatrix const& A) { EigenMatrix subMatrix(subset.size() + 1, A.cols()); for (uint_fast64_t i = 0; i < subset.size(); ++i){ - subMatrix.row((StormEigen::Index) i) = A.row(StormEigen::Index (subset[i])); + subMatrix.row((Eigen::Index) i) = A.row(Eigen::Index (subset[i])); } subMatrix.row(subset.size()) = A.row(item); - StormEigen::FullPivLU lUMatrix( subMatrix ); + Eigen::FullPivLU lUMatrix( subMatrix ); if (lUMatrix.rank() < subMatrix.rows()){ //Linear dependent! return false; diff --git a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.h b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.h index 83c4cc575..4faf006ca 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.h +++ b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.h @@ -12,8 +12,8 @@ namespace storm{ class HyperplaneEnumeration { public: - typedef StormEigen::Matrix EigenMatrix; - typedef StormEigen::Matrix EigenVector; + typedef Eigen::Matrix EigenMatrix; + typedef Eigen::Matrix EigenVector; HyperplaneEnumeration() = default; virtual ~HyperplaneEnumeration() = default; diff --git a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp index 67a9f2942..ce0594bb9 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp @@ -117,7 +117,7 @@ namespace storm { vectorMatrix.col(i) << points[subset[i]], storm::utility::one(); } vectorMatrix.col(subset.size()) << points[item], storm::utility::one(); - return (vectorMatrix.fullPivLu().rank() > (StormEigen::Index) subset.size()); + return (vectorMatrix.fullPivLu().rank() > (Eigen::Index) subset.size()); } template @@ -172,7 +172,7 @@ namespace storm { // clear the additionally added points. Note that the order of the points might have changed storm::storage::BitVector keptPoints(points.size(), true); for (uint_fast64_t pointIndex = 0; pointIndex < points.size(); ++pointIndex) { - for (StormEigen::Index row = 0; row < resultMatrix.rows(); ++row) { + for (Eigen::Index row = 0; row < resultMatrix.rows(); ++row) { if ((resultMatrix.row(row) * points[pointIndex])(0) > resultVector(row)) { keptPoints.set(pointIndex, false); break; @@ -184,7 +184,7 @@ namespace storm { if (generateRelevantVerticesAndVertexSets) { storm::storage::BitVector keptVertices(relevantVertices.size(), true); for (uint_fast64_t vertexIndex = 0; vertexIndex < relevantVertices.size(); ++vertexIndex) { - for (StormEigen::Index row = 0; row < resultMatrix.rows(); ++row) { + for (Eigen::Index row = 0; row < resultMatrix.rows(); ++row) { if ((resultMatrix.row(row) * relevantVertices[vertexIndex])(0) > resultVector(row)) { keptVertices.set(vertexIndex, false); break; @@ -389,7 +389,7 @@ namespace storm { std::unordered_map> relevantVerticesMap; relevantVerticesMap.reserve(points.size()); for (uint_fast64_t vertexIndex = 0; vertexIndex < hyperplanesOnVertexCounter.size(); ++vertexIndex){ - if ((StormEigen::Index) hyperplanesOnVertexCounter[vertexIndex] >= points.front().rows()){ + if ((Eigen::Index) hyperplanesOnVertexCounter[vertexIndex] >= points.front().rows()){ auto mapEntry = relevantVerticesMap.insert(typename std::unordered_map>::value_type(points[vertexIndex], std::vector())).first; mapEntry->second.push_back(vertexIndex); } @@ -408,7 +408,7 @@ namespace storm { for (auto& vertexVector : vertexSets){ std::set vertexSet; for (auto const& oldIndex : vertexVector){ - if ((StormEigen::Index) hyperplanesOnVertexCounter[oldIndex] >= points.front().rows()){ + if ((Eigen::Index) hyperplanesOnVertexCounter[oldIndex] >= points.front().rows()){ vertexSet.insert(oldToNewIndexMapping[oldIndex]); } } diff --git a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.h b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.h index f0cb8d5db..65b336b86 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.h +++ b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.h @@ -14,8 +14,8 @@ namespace storm { class QuickHull { public: - typedef StormEigen::Matrix EigenMatrix; - typedef StormEigen::Matrix EigenVector; + typedef Eigen::Matrix EigenMatrix; + typedef Eigen::Matrix EigenVector; QuickHull() = default; ~QuickHull() = default; diff --git a/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp b/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp index 2de1b1c45..709fe4f6f 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp @@ -89,10 +89,10 @@ namespace storm { } template class SubsetEnumerator; - template class SubsetEnumerator>>; - template class SubsetEnumerator>>; - template class SubsetEnumerator>; - template class SubsetEnumerator>; + template class SubsetEnumerator>>; + template class SubsetEnumerator>>; + template class SubsetEnumerator>; + template class SubsetEnumerator>; } } } diff --git a/src/storm/utility/eigen.h b/src/storm/utility/eigen.h index 11b406431..959a8a658 100644 --- a/src/storm/utility/eigen.h +++ b/src/storm/utility/eigen.h @@ -1,6 +1,6 @@ #pragma once -// Include this utility header so we can access utility function from Eigen. +// Include these utility headers so we can access utility function from Eigen. #include "storm/utility/constants.h" #if defined(__clang__) @@ -14,9 +14,9 @@ #endif // Finally include the parts of Eigen we need. -#include -#include -#include +#include +#include +#include #if defined(__clang__) #pragma clang diagnostic pop diff --git a/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp index f142a764c..b20bf7f6b 100755 --- a/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp @@ -44,6 +44,7 @@ namespace { env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu); env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations); + env.solver().lra().setPrecision(storm::utility::convertNumber(1e-8)); // Need to increase precision because eq sys yields incorrect results return env; } }; @@ -61,6 +62,7 @@ namespace { env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu); env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations); + env.solver().lra().setPrecision(storm::utility::convertNumber(1e-8)); // Need to increase precision because eq sys yields incorrect results return env; } }; @@ -343,7 +345,7 @@ namespace { std::unique_ptr result; result = checker->check(this->env(), tasks[0]); - EXPECT_NEAR(this->parseNumber("0.93458866427696596"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + EXPECT_NEAR(this->parseNumber("6201111489217/6635130141055"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } TYPED_TEST(LraCtmcCslModelCheckerTest, Polling) {