From 67626ff9bb4f30f7f13fd9d6a5a3517a5814e8d3 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Tue, 16 Feb 2016 11:18:47 +0100
Subject: [PATCH 1/7] Xcode support for new directory
Former-commit-id: 7d3776d555dd6406de30e9d5e13a1bab71ff45d9
---
src/CMakeLists.txt | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index be3b825a0..b8fbd6953 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -31,7 +31,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)
@@ -79,6 +80,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})
From 6b31b23c624e5c10e54a5421d0bc145c92aed49e Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Tue, 16 Feb 2016 11:21:37 +0100
Subject: [PATCH 2/7] Removed unused time keeping variables
Former-commit-id: 67449791d505d85b39295f700ae502adab7d55d4
---
.../reachability/SparseDtmcEliminationModelChecker.cpp | 8 +-------
1 file changed, 1 insertion(+), 7 deletions(-)
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index c969a639f..5d0bd164c 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
@@ -720,15 +720,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);
@@ -950,10 +947,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)) {
From 16a21527944659dbf797b119ebee019b3fc450fb Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 17 Feb 2016 20:44:07 +0100
Subject: [PATCH 3/7] hash_value for cln::cl_ra
Former-commit-id: 934795bd78c7f530ff4e47eda1b7df0a5821d273
---
src/adapters/CarlAdapter.h | 8 ++++++++
1 file changed, 8 insertions(+)
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 {
From 266d41716812392911418fec17f6d497dea30361 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 17 Feb 2016 20:44:35 +0100
Subject: [PATCH 4/7] constants.h/cpp extended to treat carl rational numbers
Former-commit-id: 12f0dfbc2ce5e76a4afd404dfb697755e6c20210
---
src/utility/constants.cpp | 25 ++++++++++++++++++++++---
1 file changed, 22 insertions(+), 3 deletions(-)
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);
From e24343516c4c49014d272a0841f619a0443533cb Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 17 Feb 2016 20:45:19 +0100
Subject: [PATCH 5/7] constants comparator extended to carlrationalnumber
(cln/cl_ra)
Former-commit-id: a14c5c4092e2ee17e3f2900cffee79a3c57f2310
---
src/utility/ConstantsComparator.cpp | 1 +
1 file changed, 1 insertion(+)
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
From aa72d8a158883d2362173f99e036308a151ec3fb Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 17 Feb 2016 20:46:19 +0100
Subject: [PATCH 6/7] added missing instantiation of sparse matrix with carl
ratnumber
Former-commit-id: c080e9b4a513d376b4bc1a5559b5ef93eee78179
---
src/storage/SparseMatrix.cpp | 9 +++++++++
1 file changed, 9 insertions(+)
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);
From 3209c52a7cc7ca21d1b066b24920b276f5d6802f Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 17 Feb 2016 20:48:00 +0100
Subject: [PATCH 7/7] elim linear equation solver used the wrong rational
number
Former-commit-id: ca468397cec8d3039a23eee100cf6106d3467cc9
---
src/solver/EliminationLinearEquationSolver.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
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>;
}