Browse Source

fixes for compile errors. target "storm" builds without errors

tests not compiling because of property modifications.


Former-commit-id: 0366cf99cd
tempestpy_adaptions
David_Korzeniewski 10 years ago
parent
commit
ee4c961cc9
  1. 2
      src/models/PseudoModel.cpp
  2. 3
      src/models/PseudoModel.h
  3. 3
      src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp
  4. 8
      src/storage/SparseMatrix.h
  5. 14
      src/storage/StateBlock.h

2
src/models/PseudoModel.cpp

@ -58,7 +58,7 @@ namespace storm {
template<typename ValueType>
storm::storage::SparseMatrix<ValueType>
AbstractPseudoModel<ValueType>::extractPartitionDependencyGraph(storm::storage::Decomposition<storm::storage::StateBlock> const& decomposition) const {
AbstractPseudoModel<ValueType>::extractPartitionDependencyGraph(storm::storage::Decomposition<storm::storage::StronglyConnectedComponent> 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.

3
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<ValueType> extractPartitionDependencyGraph(storm::storage::Decomposition<storm::storage::StateBlock> const& decomposition) const;
virtual storm::storage::SparseMatrix<ValueType> extractPartitionDependencyGraph(storm::storage::Decomposition<storm::storage::StronglyConnectedComponent> const& decomposition) const;
};
template <typename ValueType>

3
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<ValueType> sccDecomposition(A, false, false);
storm::storage::BitVector fullSystem(A.getRowGroupCount(), true);
storm::storage::StronglyConnectedComponentDecomposition<ValueType> 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.");

8
src/storage/SparseMatrix.h

@ -778,13 +778,13 @@ namespace storm {
*/
template<typename NewValueType>
SparseMatrix<NewValueType> toValueType() const {
std::vector<MatrixEntry<NewValueType>> new_columnsAndValues;
std::vector<uint_fast64_t> new_rowIndications(rowIndications);
std::vector<uint_fast64_t> new_rowGroupIndices(rowGroupIndices);
std::vector<MatrixEntry<SparseMatrix::index_type, NewValueType>> new_columnsAndValues;
std::vector<SparseMatrix::index_type> new_rowIndications(rowIndications);
std::vector<SparseMatrix::index_type> new_rowGroupIndices(rowGroupIndices);
new_columnsAndValues.resize(columnsAndValues.size());
for (size_t i = 0, size = columnsAndValues.size(); i < size; ++i) {
new_columnsAndValues.at(i) = MatrixEntry<NewValueType>(columnsAndValues.at(i).getColumn(), static_cast<NewValueType>(columnsAndValues.at(i).getValue()));
new_columnsAndValues.at(i) = MatrixEntry<SparseMatrix::index_type, NewValueType>(columnsAndValues.at(i).getColumn(), static_cast<NewValueType>(columnsAndValues.at(i).getValue()));
}
return SparseMatrix<NewValueType>(columnCount, std::move(new_rowIndications), std::move(new_columnsAndValues), std::move(new_rowGroupIndices));

14
src/storage/StateBlock.h

@ -82,6 +82,13 @@ namespace storm {
*/
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.
*
@ -96,6 +103,13 @@ namespace storm {
*/
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.
*

Loading…
Cancel
Save