From 9b9468fbfda4b9a2c02284c1692f57168402c885 Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 25 Jan 2016 15:18:34 +0100 Subject: [PATCH 1/4] 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/4] 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/4] 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/4] 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); } }; }