21 changed files with 142 additions and 327 deletions
-
2src/builder/ExplicitPrismModelBuilder.h
-
2src/modelchecker/AbstractModelChecker.cpp
-
2src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
-
2src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
-
2src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
-
2src/models/AbstractModel.h
-
11src/models/Dtmc.h
-
3src/models/MarkovAutomaton.h
-
2src/models/Mdp.h
-
10src/parser/DeterministicSparseTransitionParser.cpp
-
2src/solver/GmmxxLinearEquationSolver.cpp
-
2src/solver/NativeLinearEquationSolver.cpp
-
3src/storage/DeterministicModelBisimulationDecomposition.cpp
-
2src/storage/DeterministicModelBisimulationDecomposition.h
-
2src/storage/SparseMatrix.h
-
124src/utility/ConstantsComparator.h
-
2src/utility/constants.cpp
-
226src/utility/constants.h
-
10src/utility/graph.h
-
2src/utility/vector.h
-
6test/performance/storage/SparseMatrixTest.cpp
@ -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 <limits> |
|
||||
#include <cstdint> |
|
||||
|
|
||||
#include "src/settings/SettingsManager.h" |
|
||||
#include "src/adapters/CarlAdapter.h" |
|
||||
|
|
||||
namespace storm { |
|
||||
|
|
||||
// Forward-declare MatrixEntry class. |
|
||||
namespace storage { |
|
||||
template<typename IndexType, typename ValueType> class MatrixEntry; |
|
||||
} |
|
||||
|
|
||||
namespace utility { |
|
||||
|
|
||||
template<typename ValueType> |
|
||||
ValueType one(); |
|
||||
|
|
||||
template<typename ValueType> |
|
||||
ValueType zero(); |
|
||||
|
|
||||
template<typename ValueType> |
|
||||
ValueType infinity(); |
|
||||
|
|
||||
#ifdef STORM_HAVE_CARL |
|
||||
template<> |
|
||||
storm::RationalFunction infinity(); |
|
||||
#endif |
|
||||
|
|
||||
template<typename ValueType> |
|
||||
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<typename ValueType> |
|
||||
ValueType simplify(ValueType value); |
|
||||
|
|
||||
// A class that can be used for comparing constants. |
|
||||
template<typename ValueType> |
|
||||
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<double> { |
|
||||
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<storm::RationalFunction> { |
|
||||
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<storm::Polynomial> { |
|
||||
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<typename IndexType, typename ValueType> |
|
||||
storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry); |
|
||||
|
|
||||
template<typename IndexType, typename ValueType> |
|
||||
storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry); |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
#endif /* STORM_UTILITY_CONSTANTSCOMPARATOR_H_ */ |
|
@ -1,4 +1,4 @@ |
|||||
#include "src/utility/ConstantsComparator.h"
|
|
||||
|
#include "src/utility/constants.h"
|
||||
|
|
||||
#include "src/storage/SparseMatrix.h"
|
#include "src/storage/SparseMatrix.h"
|
||||
#include "src/storage/sparse/StateType.h"
|
#include "src/storage/sparse/StateType.h"
|
Write
Preview
Loading…
Cancel
Save
Reference in new issue