small fixes in matrix builder and removal of debug output

src/storm/modelchecker/exploration/Bounds.cpp

@@ -98,13 +98,11 @@ namespace storm {
             
             template<typename StateType, typename ValueType>
             void Bounds<StateType, ValueType>::setUpperBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& value) {
-                std::cout << "setting value " << value << " for state " << state << " with row group " << explorationInformation.getRowGroup(state) << std::endl;
                 setUpperBoundForRowGroup(explorationInformation.getRowGroup(state), value);
             }
             
             template<typename StateType, typename ValueType>
             void Bounds<StateType, ValueType>::setUpperBoundForRowGroup(StateType const& group, ValueType const& value) {
-                std::cout << "setting value " << value << " for state (row group) " << group << " where size is " << boundsPerState.size() << std::endl;
                 boundsPerState[group].second = value;
             }
             

src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp

@@ -440,8 +440,9 @@ namespace storm {
                 // duplicate work is the following. Optimally, we would only do the MEC decomposition, because we need
                 // it anyway. However, when only detecting (accepting) MECs, we do not infer which of the other states
                 // (not contained in MECs) also have probability 0/1.
-                statesWithProbability0 = storm::utility::graph::performProb0A(transposedMatrix, allStates, targetStates);
                 targetStates.set(sink, true);
+                statesWithProbability0 = storm::utility::graph::performProb0A(transposedMatrix, allStates, targetStates);
+                targetStates.set(sink, false);
                 statesWithProbability1 = storm::utility::graph::performProb1E(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates);
                 
                 storm::storage::MaximalEndComponentDecomposition<ValueType> mecDecomposition(relevantStatesMatrix, relevantStatesMatrix.transpose(true));
@@ -449,7 +450,8 @@ namespace storm {
                 STORM_LOG_TRACE("Successfully computed MEC decomposition. Found " << (mecDecomposition.size() > 1 ? (mecDecomposition.size() - 1) : 0) << " MEC(s).");
                 
                 // If the decomposition contains only the MEC consisting of the sink state, we count it as 'failed'.
-                if (mecDecomposition.size() > 1) {
+                STORM_LOG_ASSERT(mecDecomposition.size() > 0, "Expected at least one MEC (the trivial sink MEC).");
+                if (mecDecomposition.size() == 1) {
                     ++stats.failedEcDetections;
                 } else {
                     stats.totalNumberOfEcDetected += mecDecomposition.size() - 1;
@@ -476,16 +478,14 @@ namespace storm {
             }
             
             // Set the bounds of the identified states.
-            std::cout << "prob0: " << statesWithProbability0 << std::endl;
+            STORM_LOG_ASSERT((statesWithProbability0 & statesWithProbability1).empty(), "States with probability 0 and 1 overlap.");
             for (auto state : statesWithProbability0) {
                 // Skip the sink state as it is not contained in the original system.
                 if (state == sink) {
                     continue;
                 }
                 
-                std::cout << "setting 0 for state " << state << std::endl;
                 StateType originalState = relevantStates[state];
-                std::cout << "original state is " << originalState << ", size: " << relevantStates.size() << std::endl;
                 bounds.setUpperBoundForState(originalState, explorationInformation, storm::utility::zero<ValueType>());
                 explorationInformation.addTerminalState(originalState);
             }

src/storm/solver/GmmxxLinearEquationSolver.cpp

@@ -224,10 +224,11 @@ namespace storm {
         
         template<typename ValueType>
         void GmmxxLinearEquationSolver<ValueType>::multiply(std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const {
-            if(!gmmxxA) {
+            if (!gmmxxA) {
                 gmmxxA = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(*A);
             }
             if (b) {
+                std::cout << "A: " << A->getRowCount() << "x" << A->getColumnCount() << ", x: " << x.size() << ", b: " << b->size() << ", r: " << result.size() << std::endl;
                 gmm::mult_add(*gmmxxA, x, *b, result);
             } else {
                 gmm::mult(*gmmxxA, x, result);

src/storm/storage/SparseMatrix.cpp

@@ -210,10 +210,19 @@ namespace storm {
             bool hasEntries = currentEntryCount != 0;
             
             uint_fast64_t rowCount = hasEntries ? lastRow + 1 : 0;
+
+            // If the last row group was empty, we need to add one more to the row count, because otherwise this empty row is not counted.
+            if (hasCustomRowGrouping) {
+                if (lastRow < rowGroupIndices->back()) {
+                    ++rowCount;
+                }
+            }
+            
             if (initialRowCountSet && forceInitialDimensions) {
                 STORM_LOG_THROW(rowCount <= initialRowCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowCount << " rows, but got " << rowCount << ".");
                 rowCount = std::max(rowCount, initialRowCount);
             }
+            
             rowCount = std::max(rowCount, overriddenRowCount);
             
             // If the current row count was overridden, we may need to add empty rows.

src/storm/storage/SparseMatrix.h

@@ -293,6 +293,9 @@ namespace storm {
             // Stores the currently active row group. This is used for correctly constructing the row grouping of the
             // matrix.
             index_type currentRowGroup;
+            
+            // A flag that stores whether the current row group does not yet contain an element.
+            bool currentRowGroupEmpty;
         };
         
         /*!