From 9b9468fbfda4b9a2c02284c1692f57168402c885 Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 25 Jan 2016 15:18:34 +0100 Subject: [PATCH 1/5] Fixed issues in graph.cpp when CARL is not available. Former-commit-id: 513070f1940c78208abf920cfd228c1f2525c00b --- src/utility/graph.cpp | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index 193b0ff28..bac64948f 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -986,9 +986,10 @@ namespace storm { template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +#ifdef STORM_HAVE_CARL + template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +#endif template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); @@ -1004,19 +1005,24 @@ namespace storm { template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +#ifdef STORM_HAVE_CARL template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +#endif template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; template storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +#ifdef STORM_HAVE_CARL template storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +#endif template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; template std::pair performProb01Min(storm::models::sparse::NondeterministicModel> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template std::pair performProb01Min(storm::models::sparse::NondeterministicModel> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - +#ifdef STORM_HAVE_CARL + template std::pair performProb01Min(storm::models::sparse::NondeterministicModel> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +#endif template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; From 8eec3f230608f6e0e58c57da82c303e1be16e706 Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 25 Jan 2016 15:31:07 +0100 Subject: [PATCH 2/5] Fixed issue in ExplicitPrismModelBuilder.cpp when CARL is not available. Former-commit-id: 08c6ec6dbeb033e1cf410cc036e5ca30ccc0f2fc --- src/builder/ExplicitPrismModelBuilder.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 96b6298d0..a3d80d067 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -244,7 +244,7 @@ namespace storm { // not only appear in the probabilities, we re if (!std::is_same::value && preparedProgram->hasUndefinedConstants()) { #else - if (preparedProgram.hasUndefinedConstants()) { + if (preparedProgram->hasUndefinedConstants()) { #endif std::vector> undefinedConstants = preparedProgram->getUndefinedConstants(); std::stringstream stream; From f0f3e8cbb3ee97af02ac12eea6aac4362ef86afb Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 25 Jan 2016 16:01:55 +0100 Subject: [PATCH 3/5] Fixed test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp when MathSAT support is unavailable. Former-commit-id: c4b91a2ac5aa70a08c1327cdd23fd010011485db --- .../permissiveschedulers/SmtPermissiveSchedulerTest.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp index 04f706221..4d87796b8 100644 --- a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp +++ b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp @@ -10,6 +10,9 @@ #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" + +#ifdef STORM_HAVE_MSAT + TEST(SmtPermissiveSchedulerTest, DieSelection) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die_c1.nm"); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); @@ -58,3 +61,5 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) { // } + +#endif // STORM_HAVE_MSAT From 3cda2d153aec8249d71d00bb01c7d1181071db20 Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 25 Jan 2016 16:42:44 +0100 Subject: [PATCH 4/5] Fixed MathsatExpressionAdapter.h, where the adaption of std::hash was already wrapped in "namespace std" but the definition used std:: again. Former-commit-id: 1d8aaaeca9b5a8ce8c2e5d07ebf7709d2ba67a4c --- src/adapters/MathsatExpressionAdapter.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/adapters/MathsatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h index 854b20542..9fec0cf15 100644 --- a/src/adapters/MathsatExpressionAdapter.h +++ b/src/adapters/MathsatExpressionAdapter.h @@ -22,9 +22,9 @@ namespace std { // Define hashing operator for MathSAT's declarations. template <> - struct std::hash { - std::size_t operator()(msat_decl const& declaration) const { - return std::hash()(declaration.repr); + struct hash { + size_t operator()(msat_decl const& declaration) const { + return hash()(declaration.repr); } }; } From 93be84a4a82aeb23a4dd7fcec02fc6b7182ec22f Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 25 Jan 2016 16:51:14 +0100 Subject: [PATCH 5/5] fix in get parameters from model Former-commit-id: c4c11b2b294d7fbc07548ba5b5a10a74051b829b --- src/models/sparse/Model.cpp | 2 +- src/storage/SparseMatrix.cpp | 13 +++++++++++++ src/storage/SparseMatrix.h | 14 +++++--------- 3 files changed, 19 insertions(+), 10 deletions(-) diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index a1e71c0b7..e30965998 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -320,7 +320,7 @@ namespace storm { return this->rewardModels; } - std::set getProbabilityParameters(Model const& model) { + std::set getProbabilityParameters(Model const& model) { return storm::storage::getVariables(model.getTransitionMatrix()); } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 1bc2f9af0..253609210 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -1208,6 +1208,19 @@ namespace storm { return result; } + +#ifdef STORM_HAVE_CARL + std::set getVariables(SparseMatrix const& matrix) + { + std::set result; + for(auto const& entry : matrix) { + entry.getValue().gatherVariables(result); + } + return result; + } + +#endif + // Explicitly instantiate the entry, builder and the matrix. // double template class MatrixEntry::index_type, double>; diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 21d675cab..f9d9916c4 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -8,7 +8,7 @@ #include #include "src/utility/OsDetection.h" - +#include "src/adapters/CarlAdapter.h" #include // Forward declaration for adapter classes. @@ -970,14 +970,10 @@ namespace storm { }; - std::set getVariables(SparseMatrix const& matrix) { - std::set result; - for(auto const& entry : matrix) { - entry.probability.gatherVariables(result); - } - return result; - } - +#ifdef STORM_HAVE_CARL + std::set getVariables(SparseMatrix const& matrix); +#endif + } // namespace storage } // namespace storm