From c3c83fbe4f4d3ebb46bd8805fbb9189e1c47d268 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 13 Feb 2015 11:34:05 +0100 Subject: [PATCH] Fixed some compilation errors. Former-commit-id: dc626450b8e9974896dbb2ba793a6f1e4b0af184 --- src/builder/ExplicitPrismModelBuilder.h | 2 +- src/modelchecker/AbstractModelChecker.cpp | 2 +- .../SparseMarkovAutomatonCslModelChecker.cpp | 2 +- .../prctl/SparseMdpPrctlModelChecker.cpp | 2 +- .../SparseDtmcEliminationModelChecker.h | 2 +- src/models/AbstractModel.h | 2 +- src/models/Dtmc.h | 11 +- src/models/MarkovAutomaton.h | 3 +- src/models/Mdp.h | 2 +- .../DeterministicSparseTransitionParser.cpp | 10 +- src/solver/GmmxxLinearEquationSolver.cpp | 2 +- src/solver/NativeLinearEquationSolver.cpp | 2 +- ...ministicModelBisimulationDecomposition.cpp | 3 +- ...erministicModelBisimulationDecomposition.h | 2 +- src/storage/SparseMatrix.h | 2 +- src/utility/ConstantsComparator.h | 124 -------- ...{ConstantsComparator.cpp => constants.cpp} | 2 +- src/utility/constants.h | 276 +++++++----------- src/utility/graph.h | 10 +- src/utility/vector.h | 2 +- test/performance/storage/SparseMatrixTest.cpp | 6 +- 21 files changed, 142 insertions(+), 327 deletions(-) delete mode 100644 src/utility/ConstantsComparator.h rename src/utility/{ConstantsComparator.cpp => constants.cpp} (99%) diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index 43ef3625a..a9a3075d2 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -20,7 +20,7 @@ #include "src/storage/SparseMatrix.h" #include "src/settings/SettingsManager.h" -#include "src/utility/ConstantsComparator.h" +#include "src/utility/constants.h" #include "src/utility/PrismUtility.h" namespace storm { diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 621712f10..eb9d539a9 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -1,6 +1,6 @@ #include "src/modelchecker/AbstractModelChecker.h" -#include "src/utility/ConstantsComparator.h" +#include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/InvalidOperationException.h" diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index f641854d4..42a718cfd 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -3,7 +3,7 @@ #include #include -#include "src/utility/ConstantsComparator.h" +#include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/utility/vector.h" #include "src/utility/graph.h" diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index a12489838..3aec3ef8d 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -2,7 +2,7 @@ #include -#include "src/utility/ConstantsComparator.h" +#include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/utility/vector.h" #include "src/utility/graph.h" diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 4fb381aad..4ae3d7a9e 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -4,7 +4,7 @@ #include "src/storage/sparse/StateType.h" #include "src/models/Dtmc.h" #include "src/modelchecker/AbstractModelChecker.h" -#include "src/utility/ConstantsComparator.h" +#include "src/utility/constants.h" namespace storm { namespace modelchecker { diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 99e37b3a7..12a2d3e32 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -11,7 +11,7 @@ #include "src/storage/SparseMatrix.h" #include "src/storage/Scheduler.h" #include "src/storage/StronglyConnectedComponentDecomposition.h" -#include "src/utility/ConstantsComparator.h" +#include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/utility/Hash.h" #include "src/utility/vector.h" diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index b42e0c9e3..dc1001948 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -18,9 +18,10 @@ #include "src/storage/SparseMatrix.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/settings/SettingsManager.h" +#include "src/utility/constants.h" #include "src/utility/vector.h" #include "src/utility/matrix.h" -#include "src/utility/ConstantsComparator.h" +#include "src/utility/constants.h" namespace storm { @@ -202,7 +203,7 @@ public: // Now fill the matrix. newRow = 0; - T rest = utility::constantZero(); + T rest = storm::utility::zero(); for(uint_fast64_t row = 0; row < origMat.getRowCount(); ++row) { if(subSysStates.get(row)){ // Transfer transitions @@ -216,14 +217,14 @@ public: // Insert the transition taking care of the remaining outgoing probability. newMatBuilder.addNextValue(newRow, newStateCount - 1, rest); - rest = storm::utility::constantZero(); + rest = storm::utility::zero(); newRow++; } } // Insert last transition: self loop on s_b - newMatBuilder.addNextValue(newStateCount - 1, newStateCount - 1, storm::utility::constantOne()); + newMatBuilder.addNextValue(newStateCount - 1, newStateCount - 1, storm::utility::one()); // 3. Take care of the labeling. storm::models::AtomicPropositionsLabeling newLabeling = storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates); @@ -266,7 +267,7 @@ public: } // Insert the reward (e.g. 0) for the transition taking care of the remaining outgoing probability. - newTransRewardsBuilder.addNextValue(newRow, newStateCount - 1, storm::utility::constantZero()); + newTransRewardsBuilder.addNextValue(newRow, newStateCount - 1, storm::utility::zero()); newRow++; } diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index 106cc0e7d..19e1fa278 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -13,6 +13,7 @@ #include "src/storage/SparseMatrix.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/settings/SettingsManager.h" +#include "src/utility/constants.h" #include "src/utility/vector.h" #include "src/utility/matrix.h" @@ -100,7 +101,7 @@ namespace storm { } T getMaximalExitRate() const { - T result = storm::utility::constantZero(); + T result = storm::utility::zero(); for (auto markovianState : this->markovianStates) { result = std::max(result, this->exitRates[markovianState]); } diff --git a/src/models/Mdp.h b/src/models/Mdp.h index c8a97003f..9a090fee4 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -18,7 +18,7 @@ #include "src/storage/SparseMatrix.h" #include "src/settings/SettingsManager.h" #include "src/models/AbstractNondeterministicModel.h" -#include "src/utility/ConstantsComparator.h" +#include "src/utility/constants.h" #include "src/utility/matrix.h" namespace storm { diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 5a8057f13..1f248430a 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -123,7 +123,7 @@ namespace storm { for (uint_fast64_t skippedRow = 0; skippedRow < row; ++skippedRow) { hadDeadlocks = true; if (!dontFixDeadlocks) { - resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne()); + resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::one()); LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted."); } else { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions."); @@ -144,7 +144,7 @@ namespace storm { if (lastRow != row) { if (!rowHadDiagonalEntry) { if (insertDiagonalEntriesIfMissing) { - resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero()); + resultMatrix.addNextValue(lastRow, lastRow, storm::utility::zero()); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)"); } else { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); @@ -155,7 +155,7 @@ namespace storm { for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { hadDeadlocks = true; if (!dontFixDeadlocks) { - resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne()); + resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::one()); LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted."); } else { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions."); @@ -172,7 +172,7 @@ namespace storm { if (col > row && !rowHadDiagonalEntry) { if (insertDiagonalEntriesIfMissing) { - resultMatrix.addNextValue(row, row, storm::utility::constantZero()); + resultMatrix.addNextValue(row, row, storm::utility::zero()); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)"); } else { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself."); @@ -186,7 +186,7 @@ namespace storm { if (!rowHadDiagonalEntry) { if (insertDiagonalEntriesIfMissing) { - resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero()); + resultMatrix.addNextValue(lastRow, lastRow, storm::utility::zero()); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)"); } else { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp index 695beb683..63bb8f224 100644 --- a/src/solver/GmmxxLinearEquationSolver.cpp +++ b/src/solver/GmmxxLinearEquationSolver.cpp @@ -186,7 +186,7 @@ namespace storm { while (!converged && iterationCount < maximalNumberOfIterations) { // Compute D^-1 * (b - LU * x) and store result in nextX. gmm::mult(*gmmLU, *currentX, tmpX); - gmm::add(b, gmm::scaled(tmpX, -storm::utility::constantOne()), tmpX); + gmm::add(b, gmm::scaled(tmpX, -storm::utility::one()), tmpX); gmm::mult(*gmmDinv, tmpX, *nextX); // Now check if the process already converged within our precision. diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index 14c520068..a872643b4 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/src/solver/NativeLinearEquationSolver.cpp @@ -61,7 +61,7 @@ namespace storm { while (!converged && iterationCount < maximalNumberOfIterations) { // Compute D^-1 * (b - LU * x) and store result in nextX. jacobiDecomposition.first.multiplyWithVector(*currentX, tmpX); - storm::utility::vector::scaleVectorInPlace(tmpX, -storm::utility::constantOne()); + storm::utility::vector::scaleVectorInPlace(tmpX, -storm::utility::one()); storm::utility::vector::addVectorsInPlace(tmpX, b); jacobiDecomposition.second.multiplyWithVector(tmpX, *nextX); diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index ba1e52efa..6e974f58c 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -11,6 +11,7 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/utility/graph.h" +#include "src/utility/constants.h" #include "src/exceptions/IllegalFunctionCallException.h" #include "src/exceptions/InvalidOptionException.h" @@ -770,7 +771,7 @@ namespace storm { // If the block is absorbing, we simply add a self-loop. if (oldBlock.isAbsorbing()) { - builder.addNextValue(blockIndex, blockIndex, storm::utility::constantOne()); + builder.addNextValue(blockIndex, blockIndex, storm::utility::one()); // If the block has a special representative state, we retrieve it now. if (oldBlock.hasRepresentativeState()) { diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h index 4199d39e5..969c1d7b2 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -10,7 +10,7 @@ #include "src/models/Dtmc.h" #include "src/models/Ctmc.h" #include "src/storage/Distribution.h" -#include "src/utility/ConstantsComparator.h" +#include "src/utility/constants.h" #include "src/utility/OsDetection.h" namespace storm { diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 4c819c6c8..7d35aed96 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -7,7 +7,7 @@ #include #include "src/storage/BitVector.h" -#include "src/utility/ConstantsComparator.h" +#include "src/utility/constants.h" #include "src/utility/OsDetection.h" #include "src/exceptions/InvalidArgumentException.h" diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h deleted file mode 100644 index f31774468..000000000 --- a/src/utility/ConstantsComparator.h +++ /dev/null @@ -1,124 +0,0 @@ -#ifndef STORM_UTILITY_CONSTANTSCOMPARATOR_H_ -#define STORM_UTILITY_CONSTANTSCOMPARATOR_H_ - -#ifdef max -# undef max -#endif - -#ifdef min -# undef min -#endif - -#include -#include - -#include "src/settings/SettingsManager.h" -#include "src/adapters/CarlAdapter.h" - -namespace storm { - - // Forward-declare MatrixEntry class. - namespace storage { - template class MatrixEntry; - } - - namespace utility { - - template - ValueType one(); - - template - ValueType zero(); - - template - ValueType infinity(); - -#ifdef STORM_HAVE_CARL - template<> - storm::RationalFunction infinity(); -#endif - - template - ValueType pow(ValueType const& value, uint_fast64_t exponent); - -#ifdef STORM_HAVE_CARL - template<> - RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent); -#endif - - template - ValueType simplify(ValueType value); - - // A class that can be used for comparing constants. - template - class ConstantsComparator { - public: - bool isOne(ValueType const& value) const; - - bool isZero(ValueType const& value) const; - - bool isEqual(ValueType const& value1, ValueType const& value2) const; - }; - - // For doubles we specialize this class and consider the comparison modulo some predefined precision. - template<> - class ConstantsComparator { - public: - ConstantsComparator(); - - ConstantsComparator(double precision); - - bool isOne(double const& value) const; - - bool isZero(double const& value) const; - - bool isEqual(double const& value1, double const& value2) const; - - bool isConstant(double const& value) const; - - private: - // The precision used for comparisons. - double precision; - }; - -#ifdef STORM_HAVE_CARL - template<> - RationalFunction& simplify(RationalFunction& value); - - template<> - RationalFunction&& simplify(RationalFunction&& value); - - template<> - class ConstantsComparator { - public: - bool isOne(storm::RationalFunction const& value) const; - - bool isZero(storm::RationalFunction const& value) const; - - bool isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const; - - bool isConstant(storm::RationalFunction const& value) const; - }; - - template<> - class ConstantsComparator { - public: - bool isOne(storm::Polynomial const& value) const; - - bool isZero(storm::Polynomial const& value) const; - - bool isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const; - - bool isConstant(storm::Polynomial const& value) const; - }; -#endif - - template - storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); - - template - storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - } -} - -#endif /* STORM_UTILITY_CONSTANTSCOMPARATOR_H_ */ \ No newline at end of file diff --git a/src/utility/ConstantsComparator.cpp b/src/utility/constants.cpp similarity index 99% rename from src/utility/ConstantsComparator.cpp rename to src/utility/constants.cpp index 6fbc296da..231205ae7 100644 --- a/src/utility/ConstantsComparator.cpp +++ b/src/utility/constants.cpp @@ -1,4 +1,4 @@ -#include "src/utility/ConstantsComparator.h" +#include "src/utility/constants.h" #include "src/storage/SparseMatrix.h" #include "src/storage/sparse/StateType.h" diff --git a/src/utility/constants.h b/src/utility/constants.h index 5e913e98d..f31774468 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -1,12 +1,5 @@ -/* - * constants.h - * - * Created on: 11.10.2012 - * Author: Thomas Heinemann - */ - -#ifndef STORM_UTILITY_CONSTTEMPLATES_H_ -#define STORM_UTILITY_CONSTTEMPLATES_H_ +#ifndef STORM_UTILITY_CONSTANTSCOMPARATOR_H_ +#define STORM_UTILITY_CONSTANTSCOMPARATOR_H_ #ifdef max # undef max @@ -17,172 +10,115 @@ #endif #include - -#include "src/exceptions/InvalidArgumentException.h" +#include #include "src/settings/SettingsManager.h" +#include "src/adapters/CarlAdapter.h" namespace storm { - -namespace utility { - -/*! - * Returns a constant value of 0 that is fit to the type it is being written to. - * As (at least) gcc has problems to use the correct template by the return value - * only, the function gets a pointer as a parameter to infer the return type. - * - * @note - * The template parameter is just inferred by the return type; GCC is not able to infer this - * automatically, hence the type should always be stated explicitly (e.g. @c constantZero();) - * - * @return Value 0, fit to the return type - */ -template -static inline _Scalar constantZero() { - return _Scalar(0); -} - -/*! @cond TEMPLATE_SPECIALIZATION - * (By default, the template specifications are not included in the documentation) - */ - -/*! - * Template specialization for int_fast32_t - * @return Value 0, fit to the type int_fast32_t - */ -template <> -inline int_fast32_t constantZero() { - return 0; -} - -/*! - * Template specialization for uint_fast64_t - * @return Value 0, fit to the type uint_fast64_t - */ -template <> -inline uint_fast64_t constantZero() { - return 0; -} - -/*! - * Template specialization for double - * @return Value 0.0, fit to the type double - */ -template <> -inline double constantZero() { - return 0.0; -} -/*! @endcond */ - -/*! - * Returns a constant value of 1 that is fit to the type it is being written to. - * As (at least) gcc has problems to use the correct template by the return value - * only, the function gets a pointer as a parameter to infer the return type. - * - * @note - * The template parameter is just inferred by the return type; GCC is not able to infer this - * automatically, hence the type should always be stated explicitly (e.g. @c constantOne();) - * - * @return Value 1, fit to the return type - */ -template -static inline _Scalar constantOne() { - return _Scalar(1); -} - -/*! @cond TEMPLATE_SPECIALIZATION - * (By default, the template specializations are not included in the documentation) - */ - -/*! - * Template specialization for int_fast32_t - * @return Value 1, fit to the type int_fast32_t - */ -template<> -inline int_fast32_t constantOne() { - return 1; -} - -/*! - * Template specialization for uint_fast64_t - * @return Value 1, fit to the type uint_fast61_t - */ -template<> -inline uint_fast64_t constantOne() { - return 1; -} - -/*! - * Template specialization for double - * @return Value 1.0, fit to the type double - */ -template<> -inline double constantOne() { - return 1.0; -} - -/*! @endcond */ - -/*! - * Returns a constant value of infinity that is fit to the type it is being written to. - * As (at least) gcc has problems to use the correct template by the return value - * only, the function gets a pointer as a parameter to infer the return type. - * - * @note - * The template parameter is just inferred by the return type; GCC is not able to infer this - * automatically, hence the type should always be stated explicitly (e.g. @c constantOne();) - * - * @return Value Infinity, fit to the return type - */ -template -static inline _Scalar constantInfinity() { - return std::numeric_limits<_Scalar>::infinity(); -} - -/*! @cond TEMPLATE_SPECIALIZATION - * (By default, the template specializations are not included in the documentation) - */ - -/*! - * Template specialization for int_fast32_t - * @return Value Infinity, fit to the type uint_fast32_t - */ -template<> -inline int_fast32_t constantInfinity() { - throw storm::exceptions::InvalidArgumentException() << "Integer has no infinity."; - return std::numeric_limits::max(); -} - -/*! - * Template specialization for uint_fast64_t - * @return Value Infinity, fit to the type uint_fast64_t - */ -template<> -inline uint_fast64_t constantInfinity() { - throw storm::exceptions::InvalidArgumentException() << "Integer has no infinity."; - return std::numeric_limits::max(); -} - -/*! - * Template specialization for double - * @return Value Infinity, fit to the type double - */ -template<> -inline double constantInfinity() { - return std::numeric_limits::infinity(); -} - -/*! @endcond */ + // Forward-declare MatrixEntry class. + namespace storage { + template class MatrixEntry; + } + + namespace utility { + + template + ValueType one(); + + template + ValueType zero(); + + template + ValueType infinity(); + +#ifdef STORM_HAVE_CARL + template<> + storm::RationalFunction infinity(); +#endif + + template + ValueType pow(ValueType const& value, uint_fast64_t exponent); + +#ifdef STORM_HAVE_CARL + template<> + RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent); +#endif + + template + ValueType simplify(ValueType value); + + // A class that can be used for comparing constants. + template + class ConstantsComparator { + public: + bool isOne(ValueType const& value) const; + + bool isZero(ValueType const& value) const; + + bool isEqual(ValueType const& value1, ValueType const& value2) const; + }; + + // For doubles we specialize this class and consider the comparison modulo some predefined precision. + template<> + class ConstantsComparator { + public: + ConstantsComparator(); + + ConstantsComparator(double precision); + + bool isOne(double const& value) const; + + bool isZero(double const& value) const; + + bool isEqual(double const& value1, double const& value2) const; + + bool isConstant(double const& value) const; + + private: + // The precision used for comparisons. + double precision; + }; + +#ifdef STORM_HAVE_CARL + template<> + RationalFunction& simplify(RationalFunction& value); + + template<> + RationalFunction&& simplify(RationalFunction&& value); + + template<> + class ConstantsComparator { + public: + bool isOne(storm::RationalFunction const& value) const; + + bool isZero(storm::RationalFunction const& value) const; + + bool isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const; + + bool isConstant(storm::RationalFunction const& value) const; + }; + + template<> + class ConstantsComparator { + public: + bool isOne(storm::Polynomial const& value) const; + + bool isZero(storm::Polynomial const& value) const; + + bool isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const; + + bool isConstant(storm::Polynomial const& value) const; + }; +#endif + + template + storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); -template -inline bool isConstant(T const& v) -{ - return true; + template + storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + } } -} //namespace utility - -} //namespace storm - -#endif /* STORM_UTILITY_CONSTTEMPLATES_H_ */ +#endif /* STORM_UTILITY_CONSTANTSCOMPARATOR_H_ */ \ No newline at end of file diff --git a/src/utility/graph.h b/src/utility/graph.h index 42cb82160..4f8ba36e7 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -54,7 +54,7 @@ namespace storm { for (auto const& successor : transitionMatrix.getRow(currentState)) { // Only explore the state if the transition was actually there and the successor has not yet // been visited. - if (successor.getValue() != storm::utility::constantZero() && !reachableStates.get(successor.getColumn())) { + if (successor.getValue() != storm::utility::zero() && !reachableStates.get(successor.getColumn())) { // If the successor is one of the target states, we need to include it, but must not explore // it further. if (targetStates.get(successor.getColumn())) { @@ -757,16 +757,16 @@ namespace storm { LOG4CPLUS_INFO(logger, "Performing Dijkstra search."); - const uint_fast64_t noPredecessorValue = storm::utility::constantZero(); - std::vector probabilities(model.getNumberOfStates(), storm::utility::constantZero()); + const uint_fast64_t noPredecessorValue = storm::utility::zero(); + std::vector probabilities(model.getNumberOfStates(), storm::utility::zero()); std::vector predecessors(model.getNumberOfStates(), noPredecessorValue); // Set the probability to 1 for all starting states. std::set, DistanceCompare> probabilityStateSet; for (auto state : startingStates) { - probabilityStateSet.emplace(storm::utility::constantOne(), state); - probabilities[state] = storm::utility::constantOne(); + probabilityStateSet.emplace(storm::utility::one(), state); + probabilities[state] = storm::utility::one(); } // As long as there is one reachable state, we need to consider it. diff --git a/src/utility/vector.h b/src/utility/vector.h index 91e9ba0c7..ebfcc4298 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -125,7 +125,7 @@ namespace storm { template void subtractFromConstantOneVector(std::vector& vector) { for (auto& element : vector) { - element = storm::utility::constantOne() - element; + element = storm::utility::one() - element; } } diff --git a/test/performance/storage/SparseMatrixTest.cpp b/test/performance/storage/SparseMatrixTest.cpp index b59d283af..3b2849c05 100644 --- a/test/performance/storage/SparseMatrixTest.cpp +++ b/test/performance/storage/SparseMatrixTest.cpp @@ -25,8 +25,8 @@ TEST(SparseMatrix, Iteration) { TEST(SparseMatrix, SparseMultiplication) { storm::storage::SparseMatrixBuilder matrixBuilder; for (uint_fast64_t row = 0; row < 100000; ++row) { - ASSERT_NO_THROW(matrixBuilder.addNextValue(row, 0, storm::utility::constantOne())); - ASSERT_NO_THROW(matrixBuilder.addNextValue(row, 1, storm::utility::constantOne())); + ASSERT_NO_THROW(matrixBuilder.addNextValue(row, 0, storm::utility::one())); + ASSERT_NO_THROW(matrixBuilder.addNextValue(row, 1, storm::utility::one())); } storm::storage::SparseMatrix matrix; @@ -74,7 +74,7 @@ TEST(SparseMatrix, DenseMultiplication) { uint_fast64_t const size = 2000; for (uint_fast64_t row = 0; row < size; ++row) { for (uint_fast64_t column = 0; column < size; ++column) { - ASSERT_NO_THROW(matrixBuilder.addNextValue(row, column, storm::utility::constantOne())); + ASSERT_NO_THROW(matrixBuilder.addNextValue(row, column, storm::utility::one())); } }