Browse Source

Minor fixes.

Former-commit-id: c0d75f260e
tempestpy_adaptions
dehnert 10 years ago
parent
commit
5aafbae9a0
  1. 2
      src/modelchecker/reachability/SparseSccModelChecker.cpp
  2. 10
      src/storage/SparseMatrix.cpp
  3. 2
      src/utility/graph.h

2
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<ValueType>() && !newSccAsBitVector.get(predecessor.getColumn())) {
if (predecessor.getValue() != storm::utility::constantZero<ValueType>() && !newSccAsBitVector.get(predecessor.getColumn())) {
entryStates.set(state);
}
}

10
src/storage/SparseMatrix.cpp

@ -978,13 +978,17 @@ namespace storm {
template class SparseMatrix<int>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix);
#ifdef PARAMETRIC_SYSTEMS
template class SparseMatrixBuilder<Polynomial>;
template class SparseMatrix<Polynomial>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<Polynomial> const& matrix);
template class MatrixEntry<typename SparseMatrix<RationalFunction>::index_type, RationalFunction>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, RationalFunction> const& entry);
template class SparseMatrixBuilder<RationalFunction>;
template class SparseMatrix<RationalFunction>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<RationalFunction> const& matrix);
template class MatrixEntry<typename SparseMatrix<Polynomial>::index_type, Polynomial>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, Polynomial> const& entry);
template class SparseMatrixBuilder<Polynomial>;
template class SparseMatrix<Polynomial>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<Polynomial> const& matrix);
#endif

2
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<T>() && !reachableStates.get(successor.getColumn())) {
if (successor.getValue() != storm::utility::constantZero<T>() && !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())) {

Loading…
Cancel
Save