From 5aafbae9a00a1ad65064d1419651a2576a71f76e Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 19 Sep 2014 14:01:19 +0200 Subject: [PATCH] Minor fixes. Former-commit-id: c0d75f260ea63169e8010447e834116d52429349 --- .../reachability/SparseSccModelChecker.cpp | 2 +- src/storage/SparseMatrix.cpp | 10 +++++++--- src/utility/graph.h | 2 +- 3 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index 12707dbd9..45246c5d2 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -78,7 +78,7 @@ namespace storm { storm::storage::BitVector entryStates(dtmc.getNumberOfStates()); for (auto const& state : newScc) { for (auto const& predecessor : backwardTransitions.getRow(state)) { - if (predecessor.getValue() > storm::utility::constantZero() && !newSccAsBitVector.get(predecessor.getColumn())) { + if (predecessor.getValue() != storm::utility::constantZero() && !newSccAsBitVector.get(predecessor.getColumn())) { entryStates.set(state); } } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index ec70b874f..03b72c8cf 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -978,13 +978,17 @@ namespace storm { template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); #ifdef PARAMETRIC_SYSTEMS - template class SparseMatrixBuilder; - template class SparseMatrix; - template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); + template class MatrixEntry::index_type, RationalFunction>; + template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); + template class MatrixEntry::index_type, Polynomial>; + template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); + template class SparseMatrixBuilder; + template class SparseMatrix; + template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); #endif diff --git a/src/utility/graph.h b/src/utility/graph.h index 21972adbc..33f637877 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -58,7 +58,7 @@ namespace storm { for (auto const& successor : transitionMatrix.getRow(currentState)) { // Only explore the state if the transition was actually there and the successor has not yet // been visited. - if (successor.getValue() > storm::utility::constantZero() && !reachableStates.get(successor.getColumn())) { + if (successor.getValue() != storm::utility::constantZero() && !reachableStates.get(successor.getColumn())) { // If the successor is one of the target states, we need to include it, but must not explore // it further. if (targetStates.get(successor.getColumn())) {