...

Former-commit-id: 47c139f3bf

src/modelchecker/region/SparseDtmcRegionModelChecker.cpp

@@ -141,7 +141,7 @@ namespace storm {
                         }
                     }
                     if(eliminateThisState){
-                        storm::storage::FlexibleSparseMatrix<ParametricType>::eliminateState(flexibleTransitions, oneStepProbabilities, state, state, flexibleBackwardTransitions, stateRewards);
+                        storm::storage::FlexibleSparseMatrix<ParametricType>::eliminateState(flexibleTransitions, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards);
                         subsystem.set(state,false);
                     }
                 }

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.");

src/storage/FlexibleSparseMatrix.cpp

@@ -89,6 +89,11 @@ namespace storm {
         }
 
 
+        template<typename ValueType>
+        void FlexibleSparseMatrix<ValueType>::eliminateState(FlexibleSparseMatrix& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional<std::vector<ValueType>>& stateRewards, bool removeForwardTransitions, bool constrained, storm::storage::BitVector const& predecessorConstraint) {
+            eliminateState(matrix, oneStepProbabilities, state, state, backwardTransitions, stateRewards, removeForwardTransitions, constrained, predecessorConstraint);
+        }
+        
         template<typename ValueType>
         void FlexibleSparseMatrix<ValueType>::eliminateState(FlexibleSparseMatrix& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, uint_fast64_t row, FlexibleSparseMatrix& backwardTransitions, boost::optional<std::vector<ValueType>>& stateRewards, bool removeForwardTransitions, bool constrained, storm::storage::BitVector const& predecessorConstraint) {
 

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<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional<std::vector<ValueType>>& stateRewards, bool removeForwardTransitions = true, bool constrained = false, storm::storage::BitVector const& predecessorConstraint = storm::storage::BitVector());
             static void eliminateState(FlexibleSparseMatrix& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, uint_fast64_t row, FlexibleSparseMatrix& backwardTransitions, boost::optional<std::vector<ValueType>>& stateRewards, bool removeForwardTransitions = true, bool constrained = false, storm::storage::BitVector const& predecessorConstraint = storm::storage::BitVector());
 
         private: