fixed a bug in sparse matrix builder, fixed some tests

resources/examples/testfiles/dtmc/die.pm

@@ -24,3 +24,6 @@ rewards "coin_flips"
 endrewards
 
 label "one" = s=7&d=1;
+label "two" = s=7&d=2;
+label "three" = s=7&d=3;
+label "done" = s=7;

src/storm/builder/ExplicitModelBuilder.cpp

@@ -306,7 +306,7 @@ namespace storm {
             
             // initialize the model components with the obtained information.
             storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel(), std::move(markovianStates));
-
+            
             // Now finalize all reward models.
             for (auto& rewardModelBuilder : rewardModelBuilders) {
                 modelComponents.rewardModels.emplace(rewardModelBuilder.getName(), rewardModelBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount()));

src/storm/generator/PrismNextStateGenerator.cpp

@@ -216,7 +216,6 @@ namespace storm {
             for (auto& choice : allLabeledChoices) {
                 allChoices.push_back(std::move(choice));
             }
-            
             std::size_t totalNumberOfChoices = allChoices.size();
             
             // If there is not a single choice, we return immediately, because the state has no behavior (other than
@@ -283,9 +282,9 @@ namespace storm {
             for (auto& choice : allChoices) {
                 result.addChoice(std::move(choice));
             }
-            
+
             this->postprocess(result);
-                        
+            
             return result;
         }
         
@@ -394,7 +393,7 @@ namespace storm {
                     if (!this->evaluator->asBool(command.getGuardExpression())) {
                         continue;
                     }
-                                        
+                    
                     result.push_back(Choice<ValueType>(command.getActionIndex(), command.isMarkovian()));
                     Choice<ValueType>& choice = result.back();
                     

src/storm/modelchecker/exploration/Bounds.cpp

@@ -98,11 +98,13 @@ 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

@@ -476,12 +476,25 @@ namespace storm {
             }
             
             // Set the bounds of the identified states.
+            std::cout << "prob0: " << statesWithProbability0 << std::endl;
             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);
             }
             for (auto state : statesWithProbability1) {
+                // Skip the sink state as it is not contained in the original system.
+                if (state == sink) {
+                    continue;
+                }
+
                 StateType originalState = relevantStates[state];
                 bounds.setLowerBoundForState(originalState, explorationInformation, storm::utility::one<ValueType>());
                 explorationInformation.addTerminalState(originalState);

src/storm/storage/SparseMatrix.cpp

@@ -193,13 +193,15 @@ namespace storm {
             ++currentRowGroup;
             
             // Close all rows from the most recent one to the starting row.
-            for (index_type i = lastRow + 1; i <= startingRow; ++i) {
+            for (index_type i = lastRow + 1; i < startingRow; ++i) {
                 rowIndications.push_back(currentEntryCount);
             }
             
-            // Reset the most recently seen row/column to allow for proper insertion of the following elements.
-            lastRow = startingRow;
-            lastColumn = 0;
+            if (lastRow + 1 < startingRow) {
+                // Reset the most recently seen row/column to allow for proper insertion of the following elements.
+                lastRow = startingRow - 1;
+                lastColumn = 0;
+            }
         }
         
         template<typename ValueType>
@@ -228,7 +230,7 @@ namespace storm {
             // as now the indices of row i are always between rowIndications[i] and rowIndications[i + 1], also for
             // the first and last row.
             rowIndications.push_back(currentEntryCount);
-            assert(rowCount == rowIndications.size() - 1);
+            STORM_LOG_ASSERT(rowCount == rowIndications.size() - 1, "Wrong sizes of vectors.");
             uint_fast64_t columnCount = hasEntries ? highestColumn + 1 : 0;
             if (initialColumnCountSet && forceInitialDimensions) {
                 STORM_LOG_THROW(columnCount <= initialColumnCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialColumnCount << " columns, but got " << columnCount << ".");
@@ -1589,8 +1591,9 @@ namespace storm {
         template<typename ValueType>
         bool SparseMatrix<ValueType>::isProbabilistic() const {
             storm::utility::ConstantsComparator<ValueType> comparator;
-            for(index_type row = 0; row < this->rowCount; ++row) {
-                if(!comparator.isOne(getRowSum(row))) {
+            for (index_type row = 0; row < this->rowCount; ++row) {
+                ValueType sum = getRowSum(row);
+                if (!comparator.isOne(sum)) {
                     return false;
                 }
             }