diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index b1c14e6d5..c0b1b0544 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -32,7 +32,8 @@ file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOUR
file(GLOB_RECURSE STORM_PARSER_PRISMPARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.h ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.cpp)
file(GLOB STORM_SETTINGS_FILES ${PROJECT_SOURCE_DIR}/src/settings/*.h ${PROJECT_SOURCE_DIR}/src/settings/*.cpp)
file(GLOB STORM_SETTINGS_MODULES_FILES ${PROJECT_SOURCE_DIR}/src/settings/modules/*.h ${PROJECT_SOURCE_DIR}/src/settings/modules/*.cpp)
-file(GLOB_RECURSE STORM_SOLVER_FILES ${PROJECT_SOURCE_DIR}/src/solver/*.h ${PROJECT_SOURCE_DIR}/src/solver/*.cpp)
+file(GLOB STORM_SOLVER_FILES ${PROJECT_SOURCE_DIR}/src/solver/*.h ${PROJECT_SOURCE_DIR}/src/solver/*.cpp)
+file(GLOB STORM_SOLVER_STATEELIMINATION_FILES ${PROJECT_SOURCE_DIR}/src/solver/stateelimination/*.h ${PROJECT_SOURCE_DIR}/src/solver/stateelimination/*.cpp)
file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp)
file(GLOB STORM_STORAGE_BISIMULATION_FILES ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.h ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.cpp)
file(GLOB STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp)
@@ -83,6 +84,7 @@ source_group(parser\\prismparser FILES ${STORM_PARSER_PRISMPARSER_FILES})
source_group(settings FILES ${STORM_SETTINGS_FILES})
source_group(settings\\modules FILES ${STORM_SETTINGS_MODULES_FILES})
source_group(solver FILES ${STORM_SOLVER_FILES})
+source_group(solver\\stateelimination FILES ${STORM_SOLVER_STATEELIMINATION_FILES})
source_group(storage FILES ${STORM_STORAGE_FILES})
source_group(storage\\bisimulation FILES ${STORM_STORAGE_BISIMULATION_FILES})
source_group(storage\\dd FILES ${STORM_STORAGE_DD_FILES})
diff --git a/src/adapters/CarlAdapter.h b/src/adapters/CarlAdapter.h
index 4fd2a98a0..61bd3998b 100644
--- a/src/adapters/CarlAdapter.h
+++ b/src/adapters/CarlAdapter.h
@@ -41,6 +41,14 @@ namespace carl {
std::hash<Interval<Number>> h;
return h(i);
}
+
+}
+
+namespace cln {
+ inline size_t hash_value(cl_RA const& n) {
+ std::hash<cln::cl_RA> h;
+ return h(n);
+ }
}
namespace storm {
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index 85a432b12..2ea8fa459 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
@@ -739,15 +739,12 @@ namespace storm {
eliminationOrderNeedsReversedDistances(order));
}
- std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now();
storm::storage::FlexibleSparseMatrix<ValueType> flexibleMatrix(submatrix);
storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(submatrixTransposed, true);
- std::chrono::high_resolution_clock::time_point conversionEnd = std::chrono::high_resolution_clock::now();
std::shared_ptr<StatePriorityQueue<ValueType>> statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate);
STORM_LOG_INFO("Computing conditional probilities." << std::endl);
- std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now();
uint_fast64_t numberOfStatesToEliminate = statePriorities->size();
STORM_LOG_INFO("Eliminating " << numberOfStatesToEliminate << " states using the state elimination technique." << std::endl);
performPrioritizedStateElimination(statePriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, this->getModel().getInitialStates(), true);
@@ -969,10 +966,7 @@ namespace storm {
// Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
storm::storage::FlexibleSparseMatrix<ValueType> flexibleMatrix(transitionMatrix);
storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(backwardTransitions);
- auto conversionEnd = std::chrono::high_resolution_clock::now();
-
- std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now();
-
+
storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder();
boost::optional<std::vector<uint_fast64_t>> distanceBasedPriorities;
if (eliminationOrderNeedsDistances(order)) {
diff --git a/src/solver/EliminationLinearEquationSolver.cpp b/src/solver/EliminationLinearEquationSolver.cpp
index 67a281b70..98c791c0a 100644
--- a/src/solver/EliminationLinearEquationSolver.cpp
+++ b/src/solver/EliminationLinearEquationSolver.cpp
@@ -54,7 +54,7 @@ namespace storm {
template class EliminationLinearEquationSolver<double>;
// TODO: make this work with the proper implementation of solveEquationSystem.
- template class EliminationLinearEquationSolver<storm::RationalNumber>;
+ template class EliminationLinearEquationSolver<storm::CarlRationalNumber>;
template class EliminationLinearEquationSolver<storm::RationalFunction>;
}
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index 65f74d874..d41e2ef2c 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -1257,6 +1257,15 @@ namespace storm {
template bool SparseMatrix<int>::isSubmatrixOf(SparseMatrix<storm::storage::sparse::state_type> const& matrix) const;
#ifdef STORM_HAVE_CARL
+ // Rat Function
+ template class MatrixEntry<typename SparseMatrix<CarlRationalNumber>::index_type, CarlRationalNumber>;
+ template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, CarlRationalNumber> const& entry);
+ template class SparseMatrixBuilder<CarlRationalNumber>;
+ template class SparseMatrix<CarlRationalNumber>;
+ template std::ostream& operator<<(std::ostream& out, SparseMatrix<CarlRationalNumber> const& matrix);
+ template std::vector<storm::CarlRationalNumber> SparseMatrix<CarlRationalNumber>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::CarlRationalNumber> const& otherMatrix) const;
+ template bool SparseMatrix<storm::CarlRationalNumber>::isSubmatrixOf(SparseMatrix<storm::CarlRationalNumber> const& matrix) const;
+
// Rat Function
template class MatrixEntry<typename SparseMatrix<RationalFunction>::index_type, RationalFunction>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, RationalFunction> const& entry);
diff --git a/src/utility/ConstantsComparator.cpp b/src/utility/ConstantsComparator.cpp
index 4ad0a2612..e22efbc5e 100644
--- a/src/utility/ConstantsComparator.cpp
+++ b/src/utility/ConstantsComparator.cpp
@@ -114,6 +114,7 @@ namespace storm {
template class ConstantsComparator<RationalFunction>;
template class ConstantsComparator<Polynomial>;
template class ConstantsComparator<Interval>;
+ template class ConstantsComparator<CarlRationalNumber>;
#endif
}
}
\ No newline at end of file
diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp
index 900482a72..be0fcb079 100644
--- a/src/utility/constants.cpp
+++ b/src/utility/constants.cpp
@@ -76,6 +76,17 @@ namespace storm {
// FIXME: this should be treated more properly.
return storm::RationalFunction(-1.0);
}
+
+ template<>
+ bool isOne(storm::CarlRationalNumber const& a) {
+ return carl::isOne(a);
+ }
+
+ template<>
+ bool isZero(storm::CarlRationalNumber const& a) {
+ return carl::isZero(a);
+ }
+
#endif
template<typename ValueType>
@@ -214,13 +225,21 @@ namespace storm {
template storm::RationalFunction infinity();
template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
-
- template Polynomial one();
- template Polynomial zero();
template RationalFunction simplify(RationalFunction value);
template RationalFunction& simplify(RationalFunction& value);
template RationalFunction&& simplify(RationalFunction&& value);
+
+ template Polynomial one();
+ template Polynomial zero();
+
+ template bool isOne(CarlRationalNumber const& value);
+ template bool isZero(CarlRationalNumber const& value);
+ template bool isConstant(CarlRationalNumber const& value);
+
+ template CarlRationalNumber one();
+ template CarlRationalNumber zero();
+
template bool isOne(Interval const& value);
template bool isZero(Interval const& value);
template bool isConstant(Interval const& value);