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

progress on support for gmp, with cln everything should be fine 

Former-commit-id: c91b5a7cef
tempestpy_adaptions
sjunges 9 years ago
parent
f54e511d74
commit
e0e5cd9f0e
6 changed files with 341 additions and 476 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      CMakeLists.txt
  2. 10
      src/solver/stateelimination/EliminatorBase.cpp
  3. 9
      src/solver/stateelimination/LongRunAverageEliminator.cpp
  4. 613
      src/utility/constants.cpp
  5. 173
      src/utility/constants.h
  6. 6
      src/utility/vector.h

2
CMakeLists.txt
View File

@ -374,7 +374,7 @@ find_package(CLN QUIET)
set(STORM_USE_CLN_NUMBERS OFF) set(STORM_USE_CLN_NUMBERS OFF)
if(CLN_FOUND) if(CLN_FOUND)
set(STORM_HAVE_CLN ON) set(STORM_HAVE_CLN ON)
set(STORM_USE_CLN_NUMBERS OFF)
set(STORM_USE_CLN_NUMBERS ON)
message(STATUS "StoRM - Linking with CLN ${CLN_VERSION_STRING}") message(STATUS "StoRM - Linking with CLN ${CLN_VERSION_STRING}")
include_directories("${CLN_INCLUDE_DIR}") include_directories("${CLN_INCLUDE_DIR}")
list(APPEND STORM_LINK_LIBRARIES ${CLN_LIBRARIES}) list(APPEND STORM_LINK_LIBRARIES ${CLN_LIBRARIES})

10
src/solver/stateelimination/EliminatorBase.cpp
View File

@ -49,7 +49,8 @@ namespace storm {
} else if (Mode == ScalingMode::DivideOneMinus) { } else if (Mode == ScalingMode::DivideOneMinus) {
if (hasEntryInColumn) { if (hasEntryInColumn) {
STORM_LOG_ASSERT(columnValue != storm::utility::one<ValueType>(), "The scaling mode 'divide-one-minus' requires a non-one value in the given column."); STORM_LOG_ASSERT(columnValue != storm::utility::one<ValueType>(), "The scaling mode 'divide-one-minus' requires a non-one value in the given column.");
columnValue = storm::utility::simplify(storm::utility::one<ValueType>() / (storm::utility::one<ValueType>() - columnValue));
columnValue = storm::utility::one<ValueType>() / (storm::utility::one<ValueType>() - columnValue);
columnValue = storm::utility::simplify(columnValue);
} }
} }
@ -57,7 +58,8 @@ namespace storm {
for (auto entryIt = entriesInRow.begin(), entryIte = entriesInRow.end(); entryIt != entryIte; ++entryIt) { for (auto entryIt = entriesInRow.begin(), entryIte = entriesInRow.end(); entryIt != entryIte; ++entryIt) {
// Only scale the entries in a different column. // Only scale the entries in a different column.
if (entryIt->getColumn() != column) { if (entryIt->getColumn() != column) {
entryIt->setValue(storm::utility::simplify(entryIt->getValue() * columnValue));
auto tmpVal = entryIt->getValue() * columnValue;
entryIt->setValue(storm::utility::simplify(tmpVal));
} }
} }
updateValue(column, columnValue); updateValue(column, columnValue);
@ -145,7 +147,9 @@ namespace storm {
*result = *first1; *result = *first1;
++first1; ++first1;
} else { } else {
auto probability = storm::utility::simplify(first1->getValue() + storm::utility::simplify(multiplyFactor * first2->getValue()));
ValueType sprod = multiplyFactor * first2->getValue();
ValueType sum = first1->getValue() + storm::utility::simplify(sprod);
auto probability = storm::utility::simplify(sum);
*result = storm::storage::MatrixEntry<typename storm::storage::FlexibleSparseMatrix<ValueType>::index_type, typename storm::storage::FlexibleSparseMatrix<ValueType>::value_type>(first1->getColumn(), probability); *result = storm::storage::MatrixEntry<typename storm::storage::FlexibleSparseMatrix<ValueType>::index_type, typename storm::storage::FlexibleSparseMatrix<ValueType>::value_type>(first1->getColumn(), probability);
newBackwardEntries[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, probability); newBackwardEntries[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, probability);
++first1; ++first1;

9
src/solver/stateelimination/LongRunAverageEliminator.cpp
View File

@ -12,13 +12,16 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void LongRunAverageEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { void LongRunAverageEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
this->stateValues[state] = storm::utility::simplify(loopProbability * this->stateValues[state]);
averageTimeInStates[state] = storm::utility::simplify(loopProbability * averageTimeInStates[state]);
this->stateValues[state] = loopProbability * this->stateValues[state];
this->stateValues[state] = storm::utility::simplify(this->stateValues[state]);
averageTimeInStates[state] = loopProbability * averageTimeInStates[state];
averageTimeInStates[state] = storm::utility::simplify(averageTimeInStates[state]);
} }
template<typename ValueType> template<typename ValueType>
void LongRunAverageEliminator<ValueType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { void LongRunAverageEliminator<ValueType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) {
this->stateValues[predecessor] = storm::utility::simplify(this->stateValues[predecessor] + storm::utility::simplify(probability * this->stateValues[state]));
this->stateValues[predecessor] = this->stateValues[predecessor] + storm::utility::simplify(probability * this->stateValues[state]);
this->stateValues[predecessor] = storm::utility::simplify(this->stateValues[predecessor]);
averageTimeInStates[predecessor] = storm::utility::simplify(averageTimeInStates[predecessor] + storm::utility::simplify(probability * averageTimeInStates[state])); averageTimeInStates[predecessor] = storm::utility::simplify(averageTimeInStates[predecessor] + storm::utility::simplify(probability * averageTimeInStates[state]));
} }

613
src/utility/constants.cpp
View File

@ -1,306 +1,307 @@
//#include "src/utility/constants.h"
//
//#include "src/storage/sparse/StateType.h"
#include "src/storage/SparseMatrix.h"
//#include "src/settings/SettingsManager.h"
//#include "src/settings/modules/GeneralSettings.h"
//
//#include "src/adapters/CarlAdapter.h"
//
namespace storm {
namespace utility {
// template<typename ValueType>
// ValueType one() {
// return ValueType(1);
// }
//
// template<typename ValueType>
// ValueType zero() {
// return ValueType(0);
// }
//
// template<typename ValueType>
// ValueType infinity() {
// return std::numeric_limits<ValueType>::infinity();
// }
//
// template<typename ValueType>
// bool isOne(ValueType const& a) {
// return a == one<ValueType>();
// }
//
// template<typename ValueType>
// bool isZero(ValueType const& a) {
// return a == zero<ValueType>();
// }
//
// template<typename ValueType>
// bool isConstant(ValueType const& a) {
// return true;
// }
//
// template<>
// bool isOne(storm::RationalNumber const& a) {
// return carl::isOne(a);
// }
//
// template<>
// bool isZero(storm::RationalNumber const& a) {
// return carl::isZero(a);
// }
//
// template<>
// storm::RationalNumber infinity() {
// // FIXME: this should be treated more properly.
// return storm::RationalNumber(-1);
// }
//
// template<>
// bool isOne(storm::RationalFunction const& a) {
// return a.isOne();
// }
//
// template<>
// bool isZero(storm::RationalFunction const& a) {
// return a.isZero();
// }
//
// template<>
// bool isConstant(storm::RationalFunction const& a) {
// return a.isConstant();
// }
//
// template<>
// bool isOne(storm::Polynomial const& a) {
// return a.isOne();
// }
//
// template<>
// bool isZero(storm::Polynomial const& a) {
// return a.isZero();
// }
//
// template<>
// bool isConstant(storm::Polynomial const& a) {
// return a.isConstant();
// }
//
// template<>
// storm::RationalFunction infinity() {
// // FIXME: this should be treated more properly.
// return storm::RationalFunction(-1.0);
// }
//
// template<typename ValueType>
// ValueType pow(ValueType const& value, uint_fast64_t exponent) {
// return std::pow(value, exponent);
// }
//
// template<typename ValueType>
// ValueType simplify(ValueType value) {
// // In the general case, we don't do anything here, but merely return the value. If something else is
// // supposed to happen here, the templated function can be specialized for this particular type.
// return value;
// }
//
// template<>
// double convertNumber(double const& number){
// return number;
// }
//
// template<typename ValueType>
// ValueType abs(ValueType const& number) {
// return carl::abs(number);
// }
//
// template<>
// RationalFunction& simplify(RationalFunction& value);
//
// template<>
// RationalFunction&& simplify(RationalFunction&& value);
//
// template<>
// RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) {
// return carl::pow(value, exponent);
// }
//
// template<>
// RationalFunction simplify(RationalFunction value) {
// value.simplify();
// return value;
// }
//
// template<>
// RationalFunction& simplify(RationalFunction& value) {
// value.simplify();
// return value;
// }
//
// template<>
// RationalFunction&& simplify(RationalFunction&& value) {
// value.simplify();
// return std::move(value);
// }
//
// template<>
// double convertNumber(RationalNumber const& number){
// return carl::toDouble(number);
// }
//
// template<>
// RationalNumber convertNumber(double const& number){
// return carl::rationalize<RationalNumber>(number);
// }
//
// template<>
// RationalFunction convertNumber(double const& number){
// 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());
return matrixEntry;
}
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry) {
simplify(matrixEntry.getValue());
return matrixEntry;
}
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry) {
simplify(matrixEntry.getValue());
return std::move(matrixEntry);
}
//
// // Explicit instantiations.
// template bool isOne(double const& value);
// template bool isZero(double const& value);
// template bool isConstant(double const& value);
//
// template double one();
// template double zero();
// template double infinity();
//
// template double pow(double const& value, uint_fast64_t exponent);
//
// template double simplify(double value);
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 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);
//
// template float one();
// template float zero();
// template float infinity();
//
// template float pow(float const& value, uint_fast64_t exponent);
//
// template float simplify(float value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& matrixEntry);
// template bool isOne(int const& value);
// template bool isZero(int const& value);
// template bool isConstant(int const& value);
//
// template int one();
// template int zero();
// template int infinity();
//
// template int pow(int const& value, uint_fast64_t exponent);
//
// template int simplify(int value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& matrixEntry);
// template bool isOne(storm::storage::sparse::state_type const& value);
// template bool isZero(storm::storage::sparse::state_type const& value);
// template bool isConstant(storm::storage::sparse::state_type const& value);
//
// template uint32_t one();
// template uint32_t zero();
// template uint32_t infinity();
//
// template storm::storage::sparse::state_type one();
// template storm::storage::sparse::state_type zero();
// template storm::storage::sparse::state_type infinity();
//
// template storm::storage::sparse::state_type pow(storm::storage::sparse::state_type const& value, uint_fast64_t exponent);
//
// template storm::storage::sparse::state_type simplify(storm::storage::sparse::state_type value);
//
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& matrixEntry);
//
// // Instantiations for rational number.
// template bool isOne(storm::RationalNumber const& value);
// template bool isZero(storm::RationalNumber const& value);
// template bool isConstant(storm::RationalNumber const& value);
//
// template storm::RationalNumber one();
// template storm::RationalNumber zero();
// template storm::RationalNumber infinity();
//
// 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);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& matrixEntry);
#ifdef STORM_HAVE_CARL
// template bool isOne(RationalFunction const& value);
// template bool isZero(RationalFunction const& value);
// template bool isConstant(RationalFunction const& value);
//
// template RationalFunction one();
// template RationalFunction zero();
// template storm::RationalFunction infinity();
//
// template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
// template RationalFunction simplify(RationalFunction value);
// template RationalFunction& simplify(RationalFunction& value);
// template RationalFunction&& simplify(RationalFunction&& value);
//
// template Polynomial one();
// template Polynomial zero();
//
// template bool isOne(Interval const& value);
// template bool isZero(Interval const& value);
// template bool isConstant(Interval const& value);
//
// template Interval one();
// template Interval zero();
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& matrixEntry);
#endif
//
}
}
#include "src/utility/constants.h"
#include "src/storage/sparse/StateType.h"
#include "src/storage/SparseMatrix.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/adapters/CarlAdapter.h"
namespace storm {
namespace utility {
template<typename ValueType>
ValueType one() {
return ValueType(1);
}
template<typename ValueType>
ValueType zero() {
return ValueType(0);
}
template<typename ValueType>
ValueType infinity() {
return std::numeric_limits<ValueType>::infinity();
}
template<typename ValueType>
bool isOne(ValueType const& a) {
return a == one<ValueType>();
}
template<typename ValueType>
bool isZero(ValueType const& a) {
return a == zero<ValueType>();
}
template<typename ValueType>
bool isConstant(ValueType const& a) {
return true;
}
template<>
bool isOne(storm::RationalNumber const& a) {
return carl::isOne(a);
}
template<>
bool isZero(storm::RationalNumber const& a) {
return carl::isZero(a);
}
template<>
storm::RationalNumber infinity() {
// FIXME: this should be treated more properly.
return storm::RationalNumber(-1);
}
template<>
bool isOne(storm::RationalFunction const& a) {
return a.isOne();
}
template<>
bool isZero(storm::RationalFunction const& a) {
return a.isZero();
}
template<>
bool isConstant(storm::RationalFunction const& a) {
return a.isConstant();
}
template<>
bool isOne(storm::Polynomial const& a) {
return a.isOne();
}
template<>
bool isZero(storm::Polynomial const& a) {
return a.isZero();
}
template<>
bool isConstant(storm::Polynomial const& a) {
return a.isConstant();
}
template<>
storm::RationalFunction infinity() {
//FIXME: this should be treated more properly.
return storm::RationalFunction(-1.0);
}
template<typename ValueType>
ValueType pow(ValueType const& value, uint_fast64_t exponent) {
assert(false);
//return std::pow(value, exponent);
}
template<typename ValueType>
ValueType simplify(ValueType value) {
// In the general case, we don't do anything here, but merely return the value. If something else is
// supposed to happen here, the templated function can be specialized for this particular type.
return value;
}
template<>
double convertNumber(double const& number){
return number;
}
template<typename ValueType>
ValueType abs(ValueType const& number) {
return carl::abs(number);
}
template<>
RationalFunction& simplify(RationalFunction& value);
template<>
RationalFunction&& simplify(RationalFunction&& value);
template<>
RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) {
return carl::pow(value, exponent);
}
template<>
RationalFunction simplify(RationalFunction value) {
value.simplify();
return value;
}
template<>
RationalFunction& simplify(RationalFunction& value) {
value.simplify();
return value;
}
template<>
RationalFunction&& simplify(RationalFunction&& value) {
value.simplify();
return std::move(value);
}
template<>
double convertNumber(RationalNumber const& number){
return carl::toDouble(number);
}
template<>
RationalNumber convertNumber(double const& number){
return carl::rationalize<RationalNumber>(number);
}
template<>
RationalFunction convertNumber(double const& number){
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());
return matrixEntry;
}
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry) {
simplify(matrixEntry.getValue());
return matrixEntry;
}
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry) {
simplify(matrixEntry.getValue());
return std::move(matrixEntry);
}
// Explicit instantiations.
template bool isOne(double const& value);
template bool isZero(double const& value);
template bool isConstant(double const& value);
template double one();
template double zero();
template double infinity();
template double pow(double const& value, uint_fast64_t exponent);
template double simplify(double value);
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 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);
template float one();
template float zero();
template float infinity();
template float pow(float const& value, uint_fast64_t exponent);
template float simplify(float value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& matrixEntry);
template bool isOne(int const& value);
template bool isZero(int const& value);
template bool isConstant(int const& value);
template int one();
template int zero();
template int infinity();
template int pow(int const& value, uint_fast64_t exponent);
template int simplify(int value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& matrixEntry);
template bool isOne(storm::storage::sparse::state_type const& value);
template bool isZero(storm::storage::sparse::state_type const& value);
template bool isConstant(storm::storage::sparse::state_type const& value);
template uint32_t one();
template uint32_t zero();
template uint32_t infinity();
template storm::storage::sparse::state_type one();
template storm::storage::sparse::state_type zero();
template storm::storage::sparse::state_type infinity();
template storm::storage::sparse::state_type pow(storm::storage::sparse::state_type const& value, uint_fast64_t exponent);
template storm::storage::sparse::state_type simplify(storm::storage::sparse::state_type value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& matrixEntry);
// Instantiations for rational number.
template bool isOne(storm::RationalNumber const& value);
template bool isZero(storm::RationalNumber const& value);
template bool isConstant(storm::RationalNumber const& value);
template storm::RationalNumber one();
template storm::RationalNumber zero();
template storm::RationalNumber infinity();
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);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& matrixEntry);
#ifdef STORM_HAVE_CARL
template bool isOne(RationalFunction const& value);
template bool isZero(RationalFunction const& value);
template bool isConstant(RationalFunction const& value);
template RationalFunction one();
template RationalFunction zero();
template storm::RationalFunction infinity();
template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
template RationalFunction simplify(RationalFunction value);
template RationalFunction& simplify(RationalFunction& value);
template RationalFunction&& simplify(RationalFunction&& value);
template Polynomial one();
template Polynomial zero();
template bool isOne(Interval const& value);
template bool isZero(Interval const& value);
template bool isConstant(Interval const& value);
template Interval one();
template Interval zero();
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& matrixEntry);
#endif
}
}

173
src/utility/constants.h
View File

@ -11,11 +11,6 @@
#include <limits> #include <limits>
#include <cstdint> #include <cstdint>
#include "src/storage/sparse/StateType.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/adapters/CarlAdapter.h"
namespace storm { namespace storm {
@ -27,180 +22,40 @@ namespace storm {
namespace utility { namespace utility {
template<typename ValueType> template<typename ValueType>
ValueType one() {
return ValueType(1);
}
template<typename ValueType>
ValueType zero() {
return ValueType(0);
}
ValueType one();
template<typename ValueType> template<typename ValueType>
ValueType infinity() {
return std::numeric_limits<ValueType>::infinity();
}
ValueType zero();
template<typename ValueType> template<typename ValueType>
bool isOne(ValueType const& a) {
return a == one<ValueType>();
}
ValueType infinity();
template<typename ValueType> template<typename ValueType>
bool isZero(ValueType const& a) {
return a == zero<ValueType>();
}
bool isOne(ValueType const& a);
template<typename ValueType> template<typename ValueType>
bool isConstant(ValueType const& a) {
return true;
}
template<>
bool isOne(storm::RationalNumber const& a) {
return carl::isOne(a);
}
template<>
bool isZero(storm::RationalNumber const& a) {
return carl::isZero(a);
}
template<>
storm::RationalNumber infinity() {
// FIXME: this should be treated more properly.
return storm::RationalNumber(-1);
}
template<>
bool isOne(storm::RationalFunction const& a) {
return a.isOne();
}
template<>
bool isZero(storm::RationalFunction const& a) {
return a.isZero();
}
template<>
bool isConstant(storm::RationalFunction const& a) {
return a.isConstant();
}
template<>
bool isOne(storm::Polynomial const& a) {
return a.isOne();
}
template<>
bool isZero(storm::Polynomial const& a) {
return a.isZero();
}
template<>
bool isConstant(storm::Polynomial const& a) {
return a.isConstant();
}
template<>
storm::RationalFunction infinity() {
// FIXME: this should be treated more properly.
return storm::RationalFunction(-1.0);
}
bool isZero(ValueType const& a);
template<typename ValueType> template<typename ValueType>
ValueType pow(ValueType const& value, uint_fast64_t exponent) {
return std::pow(value, exponent);
}
bool isConstant(ValueType const& a);
template<typename ValueType> template<typename ValueType>
ValueType simplify(ValueType value) {
// In the general case, we don't do anything here, but merely return the value. If something else is
// supposed to happen here, the templated function can be specialized for this particular type.
return value;
}
template<typename SourceType, typename TargetType>
TargetType convertNumber(SourceType const& number);
template<>
double convertNumber(double const& number){
return number;
}
ValueType pow(ValueType const& value, uint_fast64_t exponent);
template<typename ValueType> template<typename ValueType>
ValueType abs(ValueType const& number) {
return carl::abs(number);
}
template<>
RationalFunction& simplify(RationalFunction& value);
template<>
RationalFunction&& simplify(RationalFunction&& value);
template<>
RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) {
return carl::pow(value, exponent);
}
template<>
RationalFunction simplify(RationalFunction value) {
value.simplify();
return value;
}
template<>
RationalFunction& simplify(RationalFunction& value) {
value.simplify();
return value;
}
template<>
RationalFunction&& simplify(RationalFunction&& value) {
value.simplify();
return std::move(value);
}
template<>
double convertNumber(RationalNumber const& number){
return carl::toDouble(number);
}
template<>
RationalNumber convertNumber(double const& number){
return carl::rationalize<RationalNumber>(number);
}
template<>
RationalFunction convertNumber(double const& number){
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());
return matrixEntry;
}
ValueType simplify(ValueType value);
template<typename IndexType, typename ValueType> template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry) {
simplify(matrixEntry.getValue());
return matrixEntry;
}
storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry);
template<typename IndexType, typename ValueType> template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry) {
simplify(matrixEntry.getValue());
return std::move(matrixEntry);
}
storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry);
template<typename TargetType, typename SourceType>
TargetType convertNumber(SourceType const& number);
template<typename ValueType>
ValueType abs(ValueType const& number);
} }
} }

6
src/utility/vector.h
View File

@ -592,11 +592,13 @@ namespace storm {
if (val2 == 0) { if (val2 == 0) {
return (storm::utility::abs(val1) <= precision); return (storm::utility::abs(val1) <= precision);
} }
if (storm::utility::abs((val1 - val2)/val2) > precision) {
T relDiff = (val1 - val2)/val2;
if (storm::utility::abs(relDiff) > precision) {
return false; return false;
} }
} else { } else {
if (storm::utility::abs(val1 - val2) > precision) return false;
T diff = val1 - val2;
if (storm::utility::abs(diff) > precision) return false;
} }
return true; return true;
} }

Write Preview
Loading…
Cancel
Save