From ee4c961cc94f0c40e415bc1efbcd04dc03352987 Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Thu, 29 Jan 2015 19:44:58 +0100 Subject: [PATCH] fixes for compile errors. target "storm" builds without errors tests not compiling because of property modifications. Former-commit-id: 0366cf99cdbd03c09b588a3da9aa6ba531189b4b --- src/models/PseudoModel.cpp | 2 +- src/models/PseudoModel.h | 3 +- ...onNondeterministicLinearEquationSolver.cpp | 3 +- src/storage/SparseMatrix.h | 8 ++-- src/storage/StateBlock.h | 44 ++++++++++++------- 5 files changed, 38 insertions(+), 22 deletions(-) diff --git a/src/models/PseudoModel.cpp b/src/models/PseudoModel.cpp index af446778c..1d3fecf43 100644 --- a/src/models/PseudoModel.cpp +++ b/src/models/PseudoModel.cpp @@ -58,7 +58,7 @@ namespace storm { template storm::storage::SparseMatrix - AbstractPseudoModel::extractPartitionDependencyGraph(storm::storage::Decomposition const& decomposition) const { + AbstractPseudoModel::extractPartitionDependencyGraph(storm::storage::Decomposition const& decomposition) const { uint_fast64_t numberOfStates = decomposition.size(); // First, we need to create a mapping of states to their SCC index, to ease the computation of dependency transitions later. diff --git a/src/models/PseudoModel.h b/src/models/PseudoModel.h index 4738ec388..a48bddcf5 100644 --- a/src/models/PseudoModel.h +++ b/src/models/PseudoModel.h @@ -5,6 +5,7 @@ #include "src/storage/SparseMatrix.h" #include "src/storage/Decomposition.h" #include "src/storage/StateBlock.h" +#include "src/storage/StronglyConnectedComponent.h" namespace storm { namespace models { @@ -40,7 +41,7 @@ namespace storm { * @param decomposition A decomposition containing the blocks of the partition of the system. * @return A sparse matrix with bool entries that represents the dependency graph of the blocks of the partition. */ - virtual storm::storage::SparseMatrix extractPartitionDependencyGraph(storm::storage::Decomposition const& decomposition) const; + virtual storm::storage::SparseMatrix extractPartitionDependencyGraph(storm::storage::Decomposition const& decomposition) const; }; template diff --git a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp index b073f85ca..7de319261 100644 --- a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp +++ b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp @@ -140,7 +140,8 @@ namespace storm { #endif } else { std::chrono::high_resolution_clock::time_point sccStartTime = std::chrono::high_resolution_clock::now(); - storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(A, false, false); + storm::storage::BitVector fullSystem(A.getRowGroupCount(), true); + storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(A, fullSystem, false, false); if (sccDecomposition.size() == 0) { LOG4CPLUS_ERROR(logger, "Can not solve given Equation System as the SCC Decomposition returned no SCCs."); diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 8a98c1b57..56f9856bd 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -778,13 +778,13 @@ namespace storm { */ template SparseMatrix toValueType() const { - std::vector> new_columnsAndValues; - std::vector new_rowIndications(rowIndications); - std::vector new_rowGroupIndices(rowGroupIndices); + std::vector> new_columnsAndValues; + std::vector new_rowIndications(rowIndications); + std::vector new_rowGroupIndices(rowGroupIndices); new_columnsAndValues.resize(columnsAndValues.size()); for (size_t i = 0, size = columnsAndValues.size(); i < size; ++i) { - new_columnsAndValues.at(i) = MatrixEntry(columnsAndValues.at(i).getColumn(), static_cast(columnsAndValues.at(i).getValue())); + new_columnsAndValues.at(i) = MatrixEntry(columnsAndValues.at(i).getColumn(), static_cast(columnsAndValues.at(i).getValue())); } return SparseMatrix(columnCount, std::move(new_rowIndications), std::move(new_columnsAndValues), std::move(new_rowGroupIndices)); diff --git a/src/storage/StateBlock.h b/src/storage/StateBlock.h index 528a01f6b..050652c69 100644 --- a/src/storage/StateBlock.h +++ b/src/storage/StateBlock.h @@ -74,27 +74,41 @@ namespace storm { * @return An iterator to the states in this SCC. */ iterator begin(); - - /*! - * Returns a const iterator to the states in this SCC. - * - * @return A const iterator to the states in this SCC. - */ - const_iterator begin() const; + + /*! + * Returns a const iterator to the states in this SCC. + * + * @return A const iterator to the states in this SCC. + */ + const_iterator begin() const; + + /*! + * Returns a const iterator to the states in this SCC. + * + * @return A const iterator to the states in this SCC. + */ + const_iterator cbegin() const { return this->begin(); }; /*! * Returns an iterator that points one past the end of the states in this SCC. * * @return An iterator that points one past the end of the states in this SCC. */ - iterator end(); - - /*! - * Returns a const iterator that points one past the end of the states in this SCC. - * - * @return A const iterator that points one past the end of the states in this SCC. - */ - const_iterator end() const; + iterator end(); + + /*! + * Returns a const iterator that points one past the end of the states in this SCC. + * + * @return A const iterator that points one past the end of the states in this SCC. + */ + const_iterator end() const; + + /*! + * Returns a const iterator that points one past the end of the states in this SCC. + * + * @return A const iterator that points one past the end of the states in this SCC. + */ + const_iterator cend() const { return this->end(); }; /*! * Retrieves whether the given state is in the SCC.