Browse Source

fixed a few issues related to having CLN numbers as storm::RationalNumber

tempestpy_adaptions
TimQu 8 years ago
parent
commit
d5d0a5f44a
  1. 4
      src/storm/adapters/NumberAdapter.h
  2. 4
      src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
  3. 2
      src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
  4. 2
      src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
  5. 19
      src/storm/utility/constants.cpp

4
src/storm/adapters/NumberAdapter.h

@ -16,7 +16,7 @@
#include <carl/numbers/numbers.h>
#if defined(STORM_HAVE_CLN) && (defined(STORM_USE_CLN_EA) || defined(STORM_USE_CLN_RF))
#if defined(STORM_HAVE_CLN)
namespace cln {
inline size_t hash_value(cl_RA const& n) {
std::hash<cln::cl_RA> h;
@ -25,7 +25,7 @@ namespace cln {
}
#endif
#if defined(STORM_HAVE_GMP) && (!defined(STORM_USE_CLN_EA) || !defined(STORM_USE_CLN_RF))
#if defined(STORM_HAVE_GMP)
inline size_t hash_value(mpq_class const& q) {
std::hash<mpq_class> h;
return h(q);

4
src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp

@ -66,7 +66,7 @@ namespace storm {
submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix;
// Create the solution vector.
std::vector<ValueType> x(maybeStates.getNonZeroCount(), ValueType(0.5));
std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::convertNumber<ValueType>(0.5));
// Translate the symbolic matrix/vector to their explicit representations and solve the equation system.
storm::storage::SparseMatrix<ValueType> explicitSubmatrix = submatrix.toMatrix(odd, odd);
@ -230,7 +230,7 @@ namespace storm {
submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix;
// Create the solution vector.
std::vector<ValueType> x(maybeStates.getNonZeroCount(), ValueType(0.5));
std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::convertNumber<ValueType>(0.5));
// Translate the symbolic matrix/vector to their explicit representations.
storm::storage::SparseMatrix<ValueType> explicitSubmatrix = submatrix.toMatrix(odd, odd);

2
src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp

@ -72,7 +72,7 @@ namespace storm {
submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs());
// Create the solution vector.
std::vector<ValueType> x(maybeStates.getNonZeroCount(), ValueType(0.5));
std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::zero<ValueType>());
// Translate the symbolic matrix/vector to their explicit representations and solve the equation system.
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);

2
src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp

@ -33,7 +33,7 @@ namespace storm {
// Check whether we need to compute exact probabilities for some states.
if (qualitative) {
// Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
return statesWithProbability01.second.template toAdd<ValueType>() + maybeStates.template toAdd<ValueType>() * model.getManager().getConstant(ValueType(0.5));
return statesWithProbability01.second.template toAdd<ValueType>() + maybeStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::convertNumber<ValueType>(0.5));
} else {
// If there are maybe states, we need to solve an equation system.
if (!maybeStates.isZero()) {

19
src/storm/utility/constants.cpp

@ -528,6 +528,11 @@ namespace storm {
RationalFunction convertNumber(ClnRationalNumber const& number) {
return RationalFunction(convertNumber<storm::RationalFunctionCoefficient>(number));
}
template<>
ClnRationalNumber convertNumber(RationalFunction const& number){
return convertNumber<ClnRationalNumber>(number.nominatorAsNumber() / number.denominatorAsNumber());
}
#endif
#if defined(STORM_HAVE_GMP)
@ -535,16 +540,21 @@ namespace storm {
RationalFunction convertNumber(GmpRationalNumber const& number) {
return RationalFunction(convertNumber<storm::RationalFunctionCoefficient>(number));
}
template<>
GmpRationalNumber convertNumber(RationalFunction const& number){
return convertNumber<GmpRationalNumber>(number.nominatorAsNumber() / number.denominatorAsNumber());
}
#endif
template<>
uint_fast64_t convertNumber(RationalFunction const& func) {
return carl::toInt<unsigned long>(func.nominatorAsNumber());
return carl::toInt<unsigned long>(convertNumber<RationalFunctionCoefficient>(func));
}
template<>
double convertNumber(RationalFunction const& func) {
return carl::toDouble(func.nominatorAsNumber()) / carl::toDouble(func.denominatorAsNumber());
return carl::toDouble(convertNumber<RationalFunctionCoefficient>(func));
}
template<>
@ -552,11 +562,6 @@ namespace storm {
return number;
}
template<>
RationalFunctionCoefficient convertNumber(RationalFunction const& number){
return number.nominatorAsNumber() / number.denominatorAsNumber();
}
template<>
RationalFunction convertNumber(storm::storage::sparse::state_type const& number) {
return RationalFunction(convertNumber<RationalFunctionCoefficient>(number));

Loading…
Cancel
Save