Merge remote-tracking branch 'origin/master' into choicelabels

src/storm/parser/DeterministicSparseTransitionParser.cpp

@@ -46,7 +46,7 @@ namespace storm {
             char const* buf = file.getData();
 
             // Perform first pass, i.e. count entries that are not zero.
-            DeterministicSparseTransitionParser<ValueType>::FirstPassResult firstPass = DeterministicSparseTransitionParser<ValueType>::firstPass(file.getData());
+            DeterministicSparseTransitionParser<ValueType>::FirstPassResult firstPass = DeterministicSparseTransitionParser<ValueType>::firstPass(file.getData(), !isRewardFile);
 
             STORM_LOG_TRACE("First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " non-zeros.");
 
@@ -163,7 +163,7 @@ namespace storm {
         }
 
         template<typename ValueType>
-        typename DeterministicSparseTransitionParser<ValueType>::FirstPassResult DeterministicSparseTransitionParser<ValueType>::firstPass(char const* buf) {
+        typename DeterministicSparseTransitionParser<ValueType>::FirstPassResult DeterministicSparseTransitionParser<ValueType>::firstPass(char const* buf, bool reserveDiagonalElements) {
 
             DeterministicSparseTransitionParser<ValueType>::FirstPassResult result;
 
@@ -176,25 +176,30 @@ namespace storm {
 
             // Check all transitions for non-zero diagonal entries and deadlock states.
             uint_fast64_t row, col, lastRow = 0, lastCol = -1;
-            bool rowHadDiagonalEntry = false;
 
             // Read first row and reserve space for self-loops if necessary.
             char const* tmp;
             row = checked_strtol(buf, &tmp);
-            if (row > 0) {
+            if (row > 0 && reserveDiagonalElements) {
                 for (uint_fast64_t skippedRow = 0; skippedRow < row; ++skippedRow) {
                     ++result.numberOfNonzeroEntries;
                 }
             }
 
             while (buf[0] != '\0') {
-
                 // Read the transition.
                 row = checked_strtol(buf, &buf);
                 col = checked_strtol(buf, &buf);
                 // The actual read value is not needed here.
                 checked_strtod(buf, &buf);
 
+                if (lastRow != row && reserveDiagonalElements) {
+                    // Compensate for missing rows.
+                    for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) {
+                        ++result.numberOfNonzeroEntries;
+                    }
+                }
+                
                 // Check if a higher state id was found.
                 if (row > result.highestStateIndex) result.highestStateIndex = row;
                 if (col > result.highestStateIndex) result.highestStateIndex = col;
@@ -213,6 +218,12 @@ namespace storm {
                 buf = trimWhitespaces(buf);
             }
 
+            if (reserveDiagonalElements) {
+                for (uint_fast64_t skippedRow = (uint_fast64_t) (lastRow + 1); skippedRow <= result.highestStateIndex; ++skippedRow) {
+                    ++result.numberOfNonzeroEntries;
+                }
+            }
+        
             return result;
         }
 

src/storm/parser/DeterministicSparseTransitionParser.h

@@ -65,9 +65,11 @@ namespace storm {
              * transitions and the maximum node id.
              *
              * @param buffer The buffer that contains the input.
+             * @param reserveDiagonalElements A flag indicating whether the diagonal elements should be counted as if they
+             * were present to enable fixes later.
              * @return A structure representing the result of the first pass.
              */
-            static FirstPassResult firstPass(char const* buffer);
+            static FirstPassResult firstPass(char const* buffer, bool reserveDiagonalElements);
 
             /*
              * The main parsing routine.

src/storm/storage/bisimulation/DeterministicBlockData.cpp

@@ -13,7 +13,7 @@ namespace storm {
                 // Intentionally left empty.
             }
             
-            DeterministicBlockData::DeterministicBlockData(uint_fast64_t marker1, uint_fast64_t marker2) : valMarker1(marker1), valMarker2(marker2), splitterFlag(false), needsRefinementFlag(false), absorbingFlag(false), valRepresentativeState() {
+            DeterministicBlockData::DeterministicBlockData(uint_fast64_t marker1, uint_fast64_t marker2) : valMarker1(marker1), valMarker2(marker2), flags(0), valRepresentativeState() {
                 // Intentionally left empty.
             }
             
@@ -56,19 +56,27 @@ namespace storm {
             }
             
             bool DeterministicBlockData::splitter() const {
-                return this->splitterFlag;
+                return getFlag(SPLITTER_FLAG);
             }
             
             void DeterministicBlockData::setSplitter(bool value) {
-                this->splitterFlag = value;
+                setFlag(SPLITTER_FLAG, value);
             }
                         
             void DeterministicBlockData::setAbsorbing(bool absorbing) {
-                this->absorbingFlag = absorbing;
+                setFlag(ABSORBING_FLAG, absorbing);
             }
             
             bool DeterministicBlockData::absorbing() const {
-                return this->absorbingFlag;
+                return getFlag(ABSORBING_FLAG);
+            }
+            
+            void DeterministicBlockData::setHasRewards(bool value) {
+                setFlag(REWARD_FLAG, value);
+            }
+            
+            bool DeterministicBlockData::hasRewards() const {
+                return getFlag(REWARD_FLAG);
             }
             
             void DeterministicBlockData::setRepresentativeState(storm::storage::sparse::state_type representativeState) {
@@ -85,15 +93,27 @@ namespace storm {
             }
             
             bool DeterministicBlockData::needsRefinement() const {
-                return needsRefinementFlag;
+                return getFlag(REFINEMENT_FLAG);
             }
             
             void DeterministicBlockData::setNeedsRefinement(bool value) {
-                needsRefinementFlag = value;
+                setFlag(REFINEMENT_FLAG, value);
+            }
+            
+            bool DeterministicBlockData::getFlag(uint64_t flag) const {
+                return (this->flags & flag) != 0ull;
+            }
+            
+            void DeterministicBlockData::setFlag(uint64_t flag, bool value) {
+                if (value) {
+                    this->flags |= flag;
+                } else {
+                    this->flags &= ~flag;
+                }
             }
 
             std::ostream& operator<<(std::ostream& out, DeterministicBlockData const& data) {
-                out << "m1: " << data.marker1() << ", m2: " << data.marker2();
+                out << "m1: " << data.marker1() << ", m2: " << data.marker2() << ", r: " << data.hasRewards();
                 return out;
             }
         }

src/storm/storage/bisimulation/DeterministicBlockData.h

@@ -49,6 +49,12 @@ namespace storm {
                 // Retrieves whether the block is to be interpreted as absorbing.
                 bool absorbing() const;
                 
+                // Sets whether the states in the block have rewards.
+                void setHasRewards(bool value = true);
+                
+                // Retrieves whether the states in the block have rewards.
+                bool hasRewards() const;
+                
                 // Sets the representative state of this block
                 void setRepresentativeState(storm::storage::sparse::state_type representativeState);
                 
@@ -61,19 +67,21 @@ namespace storm {
                 friend std::ostream& operator<<(std::ostream& out, DeterministicBlockData const& data);
                 
             public:
+                // Helpers to set/retrieve flags.
+                bool getFlag(uint64_t flag) const;
+                void setFlag(uint64_t flag, bool value);
+                
                 // Two markers that can be used for various purposes. Whenever the block is split, both the markers are
                 // set to the beginning index of the block.
                 uint_fast64_t valMarker1;
                 uint_fast64_t valMarker2;
                 
-                // A flag that can be used for marking the block as being a splitter.
-                bool splitterFlag;
-                
-                // A flag that can be used for marking the block as needing refinement.
-                bool needsRefinementFlag;
-                
-                // A flag indicating whether the block is to be interpreted as absorbing or not.
-                bool absorbingFlag;
+                // Some bits to store flags: splitter flag, refinement flag, absorbing flag.
+                static const uint64_t SPLITTER_FLAG = 1ull;
+                static const uint64_t REFINEMENT_FLAG = 1ull << 1;
+                static const uint64_t ABSORBING_FLAG = 1ull << 2;
+                static const uint64_t REWARD_FLAG = 1ull << 3;
+                uint8_t flags;
                 
                 // An optional representative state for the block. If this is set, this state is used to derive the
                 // atomic propositions of the meta state in the quotient model.

src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp

@@ -118,22 +118,37 @@ namespace storm {
             this->initializeSilentProbabilities();
         }
         
+        
         template<typename ModelType>
-        void DeterministicModelBisimulationDecomposition<ModelType>::initializeMeasureDrivenPartition() {
-            BisimulationDecomposition<ModelType, BlockDataType>::initializeMeasureDrivenPartition();
-            
+        void DeterministicModelBisimulationDecomposition<ModelType>::postProcessInitialPartition() {
             if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
                 this->initializeWeakDtmcBisimulation();
             }
+            
+            if (this->options.getKeepRewards() && this->model.hasRewardModel() && this->options.getType() == BisimulationType::Weak) {
+                // For a weak bisimulation that is to preserve reward properties, we have to flag all blocks of states
+                // with non-zero reward as reward blocks to they can be refined wrt. strong bisimulation.
+                
+                // Here, we assume that the initial partition already respects state rewards. Therefore, it suffices to
+                // check the first state of each block for a non-zero reward.
+                std::vector<ValueType> const& stateRewardVector = this->model.getUniqueRewardModel().getStateRewardVector();
+                for (auto& block : this->partition.getBlocks()) {
+                    auto state = *this->partition.begin(*block);
+                    block->data().setHasRewards(!storm::utility::isZero(stateRewardVector[state]));
+                }
+            }
+        }
+        
+        template<typename ModelType>
+        void DeterministicModelBisimulationDecomposition<ModelType>::initializeMeasureDrivenPartition() {
+            BisimulationDecomposition<ModelType, BlockDataType>::initializeMeasureDrivenPartition();
+            postProcessInitialPartition();
         }
         
         template<typename ModelType>
         void DeterministicModelBisimulationDecomposition<ModelType>::initializeLabelBasedPartition() {
             BisimulationDecomposition<ModelType, BlockDataType>::initializeLabelBasedPartition();
-            
-            if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
-                this->initializeWeakDtmcBisimulation();
-            }
+            postProcessInitialPartition();
         }
         
         template<typename ModelType>
@@ -156,37 +171,49 @@ namespace storm {
             return silentProbabilities[state];
         }
         
+        template<typename ModelType>
+        void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlockOfSplitterStrong(bisimulation::Block<BlockDataType>& block, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) {
+            STORM_LOG_TRACE("Refining predecessor " << block.getId() << " of splitter");
+            
+            // Depending on the actions we need to take, the block to refine changes, so we need to keep track of it.
+            Block<BlockDataType>* blockToRefineProbabilistically = &block;
+            
+            bool split = false;
+            // If the new begin index has shifted to a non-trivial position, we need to split the block.
+            if (block.getBeginIndex() != block.data().marker1() && block.getEndIndex() != block.data().marker1()) {
+                split = true;
+                this->partition.splitBlock(block, block.data().marker1());
+                blockToRefineProbabilistically = block.getPreviousBlockPointer();
+                
+                // Keep track of whether this is a block with reward states.
+                blockToRefineProbabilistically->data().setHasRewards(block.data().hasRewards());
+            }
+            
+            split |= this->partition.splitBlock(*blockToRefineProbabilistically,
+                                                [this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
+                                                    return this->comparator.isLess(getProbabilityToSplitter(state1), getProbabilityToSplitter(state2));
+                                                },
+                                                [&splitterQueue,&block] (Block<BlockDataType>& newBlock) {
+                                                    splitterQueue.emplace_back(&newBlock);
+                                                    newBlock.data().setSplitter();
+
+                                                    // Keep track of whether this is a block with reward states.
+                                                    newBlock.data().setHasRewards(block.data().hasRewards());
+                                                });
+            
+            
+            // If the predecessor block was split, we need to insert it into the splitter vector if it is not already
+            // marked as a splitter.
+            if (split && !blockToRefineProbabilistically->data().splitter()) {
+                splitterQueue.emplace_back(blockToRefineProbabilistically);
+                blockToRefineProbabilistically->data().setSplitter();
+            }
+        }
+        
         template<typename ModelType>
         void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterStrong(std::list<Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) {
             for (auto block : predecessorBlocks) {
-                STORM_LOG_TRACE("Refining predecessor " << block->getId() << " of splitter");
-
-                // Depending on the actions we need to take, the block to refine changes, so we need to keep track of it.
-                Block<BlockDataType>* blockToRefineProbabilistically = block;
-                
-                bool split = false;
-                // If the new begin index has shifted to a non-trivial position, we need to split the block.
-                if (block->getBeginIndex() != block->data().marker1() && block->getEndIndex() != block->data().marker1()) {
-                    split = true;
-                    this->partition.splitBlock(*block, block->data().marker1());
-                    blockToRefineProbabilistically = block->getPreviousBlockPointer();
-                }
-                
-                split |= this->partition.splitBlock(*blockToRefineProbabilistically,
-                                                    [this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
-                                                        return this->comparator.isLess(getProbabilityToSplitter(state1), getProbabilityToSplitter(state2));
-                                                    },
-                                                    [&splitterQueue] (Block<BlockDataType>& block) {
-                                                        splitterQueue.emplace_back(&block); block.data().setSplitter();
-                                                    });
-                
-                
-                // If the predecessor block was split, we need to insert it into the splitter vector if it is not already
-                // marked as a splitter.
-                if (split && !blockToRefineProbabilistically->data().splitter()) {
-                    splitterQueue.emplace_back(blockToRefineProbabilistically);
-                    blockToRefineProbabilistically->data().setSplitter();
-                }
+                refinePredecessorBlockOfSplitterStrong(*block, splitterQueue);
                 
                 // If the block was *not* split, we need to reset the markers by notifying the data.
                 block->resetMarkers();
@@ -395,12 +422,15 @@ namespace storm {
                                                      [&weakStateLabels,&block,originalBlockIndex,this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
                                                          return weakStateLabels[this->partition.getPosition(state1) - originalBlockIndex] < weakStateLabels[this->partition.getPosition(state2) - originalBlockIndex];
                                                      },
-                                                     [this, &splitterQueue] (bisimulation::Block<BlockDataType>& block) {
-                                                         updateSilentProbabilitiesBasedOnTransitions(block);
+                                                     [this, &splitterQueue, &block] (bisimulation::Block<BlockDataType>& newBlock) {
+                                                         updateSilentProbabilitiesBasedOnTransitions(newBlock);
                                                          
                                                          // Insert the new block as a splitter.
-                                                         block.data().setSplitter();
-                                                         splitterQueue.emplace_back(&block);
+                                                         newBlock.data().setSplitter();
+                                                         splitterQueue.emplace_back(&newBlock);
+                                                         
+                                                         // Keep track of whether this is a block with reward states.
+                                                         newBlock.data().setHasRewards(block.data().hasRewards());
                                                      });
             
             // If the block was split, we also update the silent probabilities.
@@ -418,10 +448,14 @@ namespace storm {
         template<typename ModelType>
         void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) {
             for (auto block : predecessorBlocks) {
-                if (*block != splitter) {
-                    refinePredecessorBlockOfSplitterWeak(*block, splitterQueue);
+                if (block->data().hasRewards()) {
+                    refinePredecessorBlockOfSplitterStrong(*block, splitterQueue);
                 } else {
-                    // If the block to split is the splitter itself, we must not do any splitting here.
+                    if (*block != splitter) {
+                        refinePredecessorBlockOfSplitterWeak(*block, splitterQueue);
+                    } else {
+                        // If the block to split is the splitter itself, we must not do any splitting here.
+                    }
                 }
                 
                 block->resetMarkers();
@@ -594,7 +628,7 @@ namespace storm {
                         storm::storage::sparse::state_type targetBlock = this->partition.getBlock(entry.getColumn()).getId();
                         
                         // If we are computing a weak bisimulation quotient, there is no need to add self-loops.
-                        if ((this->options.getType() == BisimulationType::Weak) && targetBlock == blockIndex) {
+                        if ((this->options.getType() == BisimulationType::Weak) && targetBlock == blockIndex && !oldBlock.data().hasRewards()) {
                             continue;
                         }
                         
@@ -608,7 +642,7 @@ namespace storm {
                     
                     // Now add them to the actual matrix.
                     for (auto const& probabilityEntry : blockProbability) {
-                        if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
+                        if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc && !oldBlock.data().hasRewards()) {
                             builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second / (storm::utility::one<ValueType>() - getSilentProbability(representativeState)));
                         } else {
                             builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second);

src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h

@@ -42,6 +42,12 @@ namespace storm {
             virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) override;
 
         private:
+            // Post-processes the initial partition to properly initialize it.
+            void postProcessInitialPartition();
+            
+            // Refines the given block wrt to strong bisimulation.
+            void refinePredecessorBlockOfSplitterStrong(bisimulation::Block<BlockDataType>& block, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue);
+
             // Refines the predecessor blocks wrt. strong bisimulation.
             void refinePredecessorBlocksOfSplitterStrong(std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue);
 
@@ -98,11 +104,11 @@ namespace storm {
             // of the states.
             void updateSilentProbabilitiesBasedOnTransitions(bisimulation::Block<BlockDataType>& block);
             
-            // Refines the predecessor blocks of the splitter wrt. weak bisimulation in DTMCs.
-            void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue);
-            
             // Refines the given block wrt to weak bisimulation in DTMCs.
             void refinePredecessorBlockOfSplitterWeak(bisimulation::Block<BlockDataType>& block, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue);
+
+            // Refines the predecessor blocks of the splitter wrt. weak bisimulation in DTMCs.
+            void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue);
             
             // Converts the one-step probabilities of going into the splitter into the conditional probabilities needed
             // for weak bisimulation (on DTMCs).

src/storm/storage/bisimulation/Partition.cpp

@@ -89,11 +89,6 @@ namespace storm {
                 return this->positions[state];
             }
             
-            template<typename DataType>
-            void Partition<DataType>::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) {
-                this->positions[state] = position;
-            }
-            
             template<typename DataType>
             storm::storage::sparse::state_type const& Partition<DataType>::getState(storm::storage::sparse::state_type position) const {
                 return this->states[position];
@@ -214,7 +209,7 @@ namespace storm {
             
             template<typename DataType>
             std::pair<typename std::vector<std::unique_ptr<Block<DataType>>>::iterator, bool> Partition<DataType>::splitBlock(Block<DataType>& block, storm::storage::sparse::state_type position) {
-                STORM_LOG_THROW(position >= block.getBeginIndex() && position <= block.getEndIndex(), storm::exceptions::InvalidArgumentException, "Cannot split block at illegal position.");
+                STORM_LOG_ASSERT(position >= block.getBeginIndex() && position <= block.getEndIndex(), "Cannot split block at illegal position.");
                 STORM_LOG_TRACE("Splitting " << block.getId() << " at position " << position << " (begin was " << block.getBeginIndex() << ").");
 
                 // In case one of the resulting blocks would be empty, we simply return the current block and do not create
@@ -308,23 +303,6 @@ namespace storm {
                 mapStatesToPositions(block);
             }
             
-            template<typename DataType>
-            Block<DataType>& Partition<DataType>::insertBlock(Block<DataType>& block) {
-                // Find the beginning of the new block.
-                storm::storage::sparse::state_type begin = block.hasPreviousBlock() ? block.getPreviousBlock().getEndIndex() : 0;
-                
-                // Actually insert the new block.
-                blocks.emplace_back(new Block<DataType>(begin, block.getBeginIndex(), block.getPreviousBlockPointer(), &block, blocks.size()));
-                Block<DataType>& newBlock = *blocks.back();
-                
-                // Update the mapping of the states in the newly created block.
-                for (auto it = this->begin(newBlock), ite = this->end(newBlock); it != ite; ++it) {
-                    stateToBlockMapping[*it] = &newBlock;
-                }
-                
-                return newBlock;
-            }
-            
             template<typename DataType>
             std::vector<std::unique_ptr<Block<DataType>>> const& Partition<DataType>::getBlocks() const {
                 return this->blocks;

src/storm/storage/bisimulation/Partition.h

@@ -152,15 +152,6 @@ namespace storm {
                 void swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2);
                 
             private:
-                // FIXME: necessary?
-                // Inserts a block before the given block. The new block will cover all states between the beginning
-                // of the given block and the end of the previous block.
-                Block<DataType>& insertBlock(Block<DataType>& block);
-                
-                // FIXME: necessary?
-                // Sets the position of the given state.
-                void setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position);
-                
                 // The of blocks in the partition.
                 std::vector<std::unique_ptr<Block<DataType>>> blocks;
                 

src/test/parser/DeterministicSparseTransitionParserTest.cpp

@@ -33,29 +33,20 @@ TEST(DeterministicSparseTransitionParserTest, BasicTransitionsParsing) {
     storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/dtmc_general.tra");
 
     ASSERT_EQ(8ul, transitionMatrix.getColumnCount());
-    ASSERT_EQ(21ul, transitionMatrix.getEntryCount());
+    ASSERT_EQ(17ul, transitionMatrix.getEntryCount());
 
     // Test every entry of the matrix.
     storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(0);
 
-    ASSERT_EQ(0ul, cIter->getColumn());
-    ASSERT_EQ(0, cIter->getValue());
-    cIter++;
     ASSERT_EQ(1ul, cIter->getColumn());
     ASSERT_EQ(1, cIter->getValue());
     cIter++;
-    ASSERT_EQ(1ul, cIter->getColumn());
-    ASSERT_EQ(0, cIter->getValue());
-    cIter++;
     ASSERT_EQ(2ul, cIter->getColumn());
     ASSERT_EQ(0.5, cIter->getValue());
     cIter++;
     ASSERT_EQ(3ul, cIter->getColumn());
     ASSERT_EQ(0.5, cIter->getValue());
     cIter++;
-    ASSERT_EQ(2ul, cIter->getColumn());
-    ASSERT_EQ(0, cIter->getValue());
-    cIter++;
     ASSERT_EQ(3ul, cIter->getColumn());
     ASSERT_EQ(0.4, cIter->getValue());
     cIter++;
@@ -71,9 +62,6 @@ TEST(DeterministicSparseTransitionParserTest, BasicTransitionsParsing) {
     ASSERT_EQ(3ul, cIter->getColumn());
     ASSERT_EQ(1, cIter->getValue());
     cIter++;
-    ASSERT_EQ(4ul, cIter->getColumn());
-    ASSERT_EQ(0, cIter->getValue());
-    cIter++;
     ASSERT_EQ(3ul, cIter->getColumn());
     ASSERT_EQ(0.1, cIter->getValue());
     cIter++;
@@ -197,7 +185,7 @@ TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) {
     storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/dtmc_deadlock.tra");
 
     ASSERT_EQ(9ul, transitionMatrix.getColumnCount());
-    ASSERT_EQ(23ul, transitionMatrix.getEntryCount());
+    ASSERT_EQ(18ul, transitionMatrix.getEntryCount());
 
     storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(7);
     ASSERT_EQ(7ul, cIter->getColumn());
@@ -208,9 +196,6 @@ TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) {
     cIter++;
     ASSERT_EQ(7ul, cIter->getColumn());
     ASSERT_EQ(0.775347, cIter->getValue());
-    cIter++;
-    ASSERT_EQ(8ul, cIter->getColumn());
-    ASSERT_EQ(0, cIter->getValue());
 }
 
 TEST(DeterministicSparseTransitionParserTest, DontFixDeadlocks) {