From d5d0a5f44a864f5eb9cbf8f97f2a8c27e0477f00 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 4 Apr 2017 20:45:53 +0200 Subject: [PATCH] fixed a few issues related to having CLN numbers as storm::RationalNumber --- src/storm/adapters/NumberAdapter.h | 4 ++-- .../prctl/helper/HybridDtmcPrctlHelper.cpp | 4 ++-- .../prctl/helper/HybridMdpPrctlHelper.cpp | 2 +- .../prctl/helper/SymbolicDtmcPrctlHelper.cpp | 2 +- src/storm/utility/constants.cpp | 19 ++++++++++++------- 5 files changed, 18 insertions(+), 13 deletions(-) diff --git a/src/storm/adapters/NumberAdapter.h b/src/storm/adapters/NumberAdapter.h index 6d792e258..6ef941c78 100644 --- a/src/storm/adapters/NumberAdapter.h +++ b/src/storm/adapters/NumberAdapter.h @@ -16,7 +16,7 @@ #include -#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 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 h; return h(q); diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index 81cdce1f8..3daaee646 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -66,7 +66,7 @@ namespace storm { submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; // Create the solution vector. - std::vector x(maybeStates.getNonZeroCount(), ValueType(0.5)); + std::vector x(maybeStates.getNonZeroCount(), storm::utility::convertNumber(0.5)); // Translate the symbolic matrix/vector to their explicit representations and solve the equation system. storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(odd, odd); @@ -230,7 +230,7 @@ namespace storm { submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; // Create the solution vector. - std::vector x(maybeStates.getNonZeroCount(), ValueType(0.5)); + std::vector x(maybeStates.getNonZeroCount(), storm::utility::convertNumber(0.5)); // Translate the symbolic matrix/vector to their explicit representations. storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(odd, odd); diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 81db71dfd..b0363cd4e 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -72,7 +72,7 @@ namespace storm { submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); // Create the solution vector. - std::vector x(maybeStates.getNonZeroCount(), ValueType(0.5)); + std::vector x(maybeStates.getNonZeroCount(), storm::utility::zero()); // Translate the symbolic matrix/vector to their explicit representations and solve the equation system. std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); diff --git a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index b57f6aa3b..c54d15b92 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/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() + maybeStates.template toAdd() * model.getManager().getConstant(ValueType(0.5)); + return statesWithProbability01.second.template toAdd() + maybeStates.template toAdd() * model.getManager().getConstant(storm::utility::convertNumber(0.5)); } else { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index e1ff17ce0..6664c13d7 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -528,6 +528,11 @@ namespace storm { RationalFunction convertNumber(ClnRationalNumber const& number) { return RationalFunction(convertNumber(number)); } + + template<> + ClnRationalNumber convertNumber(RationalFunction const& number){ + return convertNumber(number.nominatorAsNumber() / number.denominatorAsNumber()); + } #endif #if defined(STORM_HAVE_GMP) @@ -535,16 +540,21 @@ namespace storm { RationalFunction convertNumber(GmpRationalNumber const& number) { return RationalFunction(convertNumber(number)); } + + template<> + GmpRationalNumber convertNumber(RationalFunction const& number){ + return convertNumber(number.nominatorAsNumber() / number.denominatorAsNumber()); + } #endif template<> uint_fast64_t convertNumber(RationalFunction const& func) { - return carl::toInt(func.nominatorAsNumber()); + return carl::toInt(convertNumber(func)); } template<> double convertNumber(RationalFunction const& func) { - return carl::toDouble(func.nominatorAsNumber()) / carl::toDouble(func.denominatorAsNumber()); + return carl::toDouble(convertNumber(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(number));