dehnert
10 years ago
27 changed files with 341 additions and 291 deletions
-
2CMakeLists.txt
-
1src/builder/ExplicitPrismModelBuilder.cpp
-
4src/builder/ExplicitPrismModelBuilder.h
-
9src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
-
9src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
-
9src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
-
3src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
-
2src/models/sparse/Dtmc.cpp
-
3src/models/sparse/Dtmc.h
-
1src/models/sparse/Mdp.cpp
-
47src/storage/DeterministicModelBisimulationDecomposition.cpp
-
33src/storage/DeterministicModelBisimulationDecomposition.h
-
2src/storage/StronglyConnectedComponentDecomposition.cpp
-
3src/storage/StronglyConnectedComponentDecomposition.h
-
142src/utility/ConstantsComparator.cpp
-
109src/utility/ConstantsComparator.h
-
193src/utility/constants.cpp
-
25src/utility/constants.h
-
3src/utility/numerical.h
-
1test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
-
1test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
-
1test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
-
1test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
-
2test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
-
18test/functional/storage/BitVectorTest.cpp
-
6test/functional/storage/CuddDdTest.cpp
-
2test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp
@ -0,0 +1,142 @@ |
|||
#include "src/utility/ConstantsComparator.h"
|
|||
|
|||
#include "src/utility/constants.h"
|
|||
#include "src/settings/SettingsManager.h"
|
|||
#include "src/settings/modules/GeneralSettings.h"
|
|||
|
|||
namespace storm { |
|||
namespace utility { |
|||
template<typename ValueType> |
|||
bool ConstantsComparator<ValueType>::isOne(ValueType const& value) const { |
|||
return value == one<ValueType>(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool ConstantsComparator<ValueType>::isZero(ValueType const& value) const { |
|||
return value == zero<ValueType>(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool ConstantsComparator<ValueType>::isEqual(ValueType const& value1, ValueType const& value2) const { |
|||
return value1 == value2; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool ConstantsComparator<ValueType>::isConstant(ValueType const& value) const { |
|||
return true; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool ConstantsComparator<ValueType>::isInfinity(ValueType const& value) const { |
|||
return false; |
|||
} |
|||
|
|||
ConstantsComparator<float>::ConstantsComparator() : precision(static_cast<float>(storm::settings::generalSettings().getPrecision())) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
ConstantsComparator<float>::ConstantsComparator(float precision) : precision(precision) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
bool ConstantsComparator<float>::isOne(float const& value) const { |
|||
return std::abs(value - one<float>()) <= precision; |
|||
} |
|||
|
|||
bool ConstantsComparator<float>::isZero(float const& value) const { |
|||
return std::abs(value) <= precision; |
|||
} |
|||
|
|||
bool ConstantsComparator<float>::isEqual(float const& value1, float const& value2) const { |
|||
return std::abs(value1 - value2) <= precision; |
|||
} |
|||
|
|||
bool ConstantsComparator<float>::isConstant(float const& value) const { |
|||
return true; |
|||
} |
|||
|
|||
bool ConstantsComparator<float>::isInfinity(float const& value) const { |
|||
return value == storm::utility::infinity<float>(); |
|||
} |
|||
|
|||
ConstantsComparator<double>::ConstantsComparator() : precision(storm::settings::generalSettings().getPrecision()) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
ConstantsComparator<double>::ConstantsComparator(double precision) : precision(precision) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
bool ConstantsComparator<double>::isOne(double const& value) const { |
|||
return std::abs(value - one<double>()) <= precision; |
|||
} |
|||
|
|||
bool ConstantsComparator<double>::isZero(double const& value) const { |
|||
return std::abs(value) <= precision; |
|||
} |
|||
|
|||
bool ConstantsComparator<double>::isInfinity(double const& value) const { |
|||
return value == infinity<double>(); |
|||
} |
|||
|
|||
bool ConstantsComparator<double>::isEqual(double const& value1, double const& value2) const { |
|||
return std::abs(value1 - value2) <= precision; |
|||
} |
|||
|
|||
bool ConstantsComparator<double>::isConstant(double const& value) const { |
|||
return true; |
|||
} |
|||
|
|||
#ifdef STORM_HAVE_CARL
|
|||
ConstantsComparator<storm::RationalFunction>::ConstantsComparator() { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
bool ConstantsComparator<storm::RationalFunction>::isOne(storm::RationalFunction const& value) const { |
|||
return value.isOne(); |
|||
} |
|||
|
|||
bool ConstantsComparator<storm::RationalFunction>::isZero(storm::RationalFunction const& value) const { |
|||
return value.isZero(); |
|||
} |
|||
|
|||
bool ConstantsComparator<storm::RationalFunction>::isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const { |
|||
return value1 == value2; |
|||
} |
|||
|
|||
bool ConstantsComparator<storm::RationalFunction>::isConstant(storm::RationalFunction const& value) const { |
|||
return value.isConstant(); |
|||
} |
|||
|
|||
ConstantsComparator<storm::Polynomial>::ConstantsComparator() { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
bool ConstantsComparator<storm::Polynomial>::isOne(storm::Polynomial const& value) const { |
|||
return value.isOne(); |
|||
} |
|||
|
|||
bool ConstantsComparator<storm::Polynomial>::isZero(storm::Polynomial const& value) const { |
|||
return value.isZero(); |
|||
} |
|||
|
|||
bool ConstantsComparator<storm::Polynomial>::isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const { |
|||
return value1 == value2; |
|||
} |
|||
|
|||
bool ConstantsComparator<storm::Polynomial>::isConstant(storm::Polynomial const& value) const { |
|||
return value.isConstant(); |
|||
} |
|||
#endif
|
|||
|
|||
// Explicit instantiations.
|
|||
template class ConstantsComparator<double>; |
|||
template class ConstantsComparator<float>; |
|||
template class ConstantsComparator<int>; |
|||
|
|||
#ifdef STORM_HAVE_CARL
|
|||
template class ConstantsComparator<RationalFunction>; |
|||
template class ConstantsComparator<Polynomial>; |
|||
#endif
|
|||
} |
|||
} |
|||
@ -0,0 +1,109 @@ |
|||
#ifndef STORM_UTILITY_CONSTANTSCOMPARATOR_H_ |
|||
#define STORM_UTILITY_CONSTANTSCOMPARATOR_H_ |
|||
|
|||
#include "src/adapters/CarlAdapter.h" |
|||
|
|||
namespace storm { |
|||
namespace utility { |
|||
// A class that can be used for comparing constants. |
|||
template<typename ValueType> |
|||
class ConstantsComparator { |
|||
public: |
|||
// This needs to be in here, otherwise the template specializations are not used properly. |
|||
ConstantsComparator(); |
|||
|
|||
bool isOne(ValueType const& value) const; |
|||
|
|||
bool isZero(ValueType const& value) const; |
|||
|
|||
bool isEqual(ValueType const& value1, ValueType const& value2) const; |
|||
|
|||
bool isConstant(ValueType const& value) const; |
|||
|
|||
bool isInfinity(ValueType const& value) const; |
|||
|
|||
private: |
|||
ValueType precision; |
|||
}; |
|||
|
|||
// For floats we specialize this class and consider the comparison modulo some predefined precision. |
|||
template<> |
|||
class ConstantsComparator<float> { |
|||
public: |
|||
ConstantsComparator(); |
|||
|
|||
ConstantsComparator(float precision); |
|||
|
|||
bool isOne(float const& value) const; |
|||
|
|||
bool isZero(float const& value) const; |
|||
|
|||
bool isEqual(float const& value1, float const& value2) const; |
|||
|
|||
bool isConstant(float const& value) const; |
|||
|
|||
bool isInfinity(float const& value) const; |
|||
|
|||
private: |
|||
// The precision used for comparisons. |
|||
float precision; |
|||
}; |
|||
|
|||
// 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 isInfinity(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<> |
|||
class ConstantsComparator<storm::RationalFunction> { |
|||
public: |
|||
ConstantsComparator(); |
|||
|
|||
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: |
|||
ConstantsComparator(); |
|||
|
|||
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 |
|||
|
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_UTILITY_CONSTANTSCOMPARATOR_H_ */ |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue