From b09d123779a5eae659f22b1e31c8b2f5017232ad Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 19 Oct 2015 20:04:14 +0200 Subject: [PATCH] ... Former-commit-id: 47c139f3bfb1cfad8285245caee295ed886c52a1 --- src/modelchecker/region/SparseDtmcRegionModelChecker.cpp | 2 +- src/modelchecker/region/SparseMdpRegionModelChecker.cpp | 1 - src/storage/FlexibleSparseMatrix.cpp | 5 +++++ src/storage/FlexibleSparseMatrix.h | 1 + 4 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index a1abe1e15..f89d4aec4 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -141,7 +141,7 @@ namespace storm { } } if(eliminateThisState){ - storm::storage::FlexibleSparseMatrix::eliminateState(flexibleTransitions, oneStepProbabilities, state, state, flexibleBackwardTransitions, stateRewards); + storm::storage::FlexibleSparseMatrix::eliminateState(flexibleTransitions, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards); subsystem.set(state,false); } } diff --git a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp index f7e284773..a22615f16 100644 --- a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp @@ -121,7 +121,6 @@ namespace storm { } } STORM_LOG_DEBUG("Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions."); - std::cout << "Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions." << std::endl; //Build the simple model STORM_LOG_DEBUG("Building the resulting simplified model."); diff --git a/src/storage/FlexibleSparseMatrix.cpp b/src/storage/FlexibleSparseMatrix.cpp index 1b1f6eb1b..d012008e2 100644 --- a/src/storage/FlexibleSparseMatrix.cpp +++ b/src/storage/FlexibleSparseMatrix.cpp @@ -89,6 +89,11 @@ namespace storm { } + template + void FlexibleSparseMatrix::eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional>& stateRewards, bool removeForwardTransitions, bool constrained, storm::storage::BitVector const& predecessorConstraint) { + eliminateState(matrix, oneStepProbabilities, state, state, backwardTransitions, stateRewards, removeForwardTransitions, constrained, predecessorConstraint); + } + template void FlexibleSparseMatrix::eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, uint_fast64_t row, FlexibleSparseMatrix& backwardTransitions, boost::optional>& stateRewards, bool removeForwardTransitions, bool constrained, storm::storage::BitVector const& predecessorConstraint) { diff --git a/src/storage/FlexibleSparseMatrix.h b/src/storage/FlexibleSparseMatrix.h index d29b46995..4a26b2a30 100644 --- a/src/storage/FlexibleSparseMatrix.h +++ b/src/storage/FlexibleSparseMatrix.h @@ -40,6 +40,7 @@ namespace storm { */ bool hasSelfLoop(storm::storage::sparse::state_type state); + static void eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional>& stateRewards, bool removeForwardTransitions = true, bool constrained = false, storm::storage::BitVector const& predecessorConstraint = storm::storage::BitVector()); static void eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, uint_fast64_t row, FlexibleSparseMatrix& backwardTransitions, boost::optional>& stateRewards, bool removeForwardTransitions = true, bool constrained = false, storm::storage::BitVector const& predecessorConstraint = storm::storage::BitVector()); private: