Fixed creation of empty blocks under certain circumstances in bisimulation.

Former-commit-id: f1240e234b

src/storage/DeterministicModelBisimulationDecomposition.cpp

@@ -262,42 +262,51 @@ namespace storm {
         
         template<typename ValueType>
         DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label, bool keepSilentProbabilities) : numberOfBlocks(0), stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
+            storm::storage::sparse::state_type position = 0;
+            Block* firstBlock = nullptr;
+            Block* secondBlock = nullptr;
+            Block* thirdBlock = nullptr;
+            if (!prob0States.empty()) {
                 typename std::list<Block>::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr, numberOfBlocks++);
-            Block& firstBlock = *firstIt;
-            firstBlock.setIterator(firstIt);
+                firstBlock = &(*firstIt);
+                firstBlock->setIterator(firstIt);
 
-            storm::storage::sparse::state_type position = 0;
                 for (auto state : prob0States) {
                     statesAndValues[position] = std::make_pair(state, storm::utility::zero<ValueType>());
                     positions[state] = position;
-                stateToBlockMapping[state] = &firstBlock;
+                    stateToBlockMapping[state] = firstBlock;
                     ++position;
                 }
-            firstBlock.setAbsorbing(true);
+                firstBlock->setAbsorbing(true);
+            }
 
-            typename std::list<Block>::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, numberOfBlocks++, std::shared_ptr<std::string>(new std::string(prob1Label)));
-            Block& secondBlock = *secondIt;
-            secondBlock.setIterator(secondIt);
+            if (!prob1States.empty()) {
+                typename std::list<Block>::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), firstBlock, nullptr, numberOfBlocks++, std::shared_ptr<std::string>(new std::string(prob1Label)));
+                secondBlock = &(*secondIt);
+                secondBlock->setIterator(secondIt);
                 
                 for (auto state : prob1States) {
                     statesAndValues[position] = std::make_pair(state, storm::utility::zero<ValueType>());
                     positions[state] = position;
-                stateToBlockMapping[state] = &secondBlock;
+                    stateToBlockMapping[state] = secondBlock;
                     ++position;
                 }
-            secondBlock.setAbsorbing(true);
-            
-            typename std::list<Block>::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, numberOfBlocks++, otherLabel == "true" ? std::shared_ptr<std::string>(nullptr) : std::shared_ptr<std::string>(new std::string(otherLabel)));
-            Block& thirdBlock = *thirdIt;
-            thirdBlock.setIterator(thirdIt);
+                secondBlock->setAbsorbing(true);
+            }
             
             storm::storage::BitVector otherStates = ~(prob0States | prob1States);
+            if (!otherStates.empty()) {
+                typename std::list<Block>::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, secondBlock, nullptr, numberOfBlocks++, otherLabel == "true" ? std::shared_ptr<std::string>(nullptr) : std::shared_ptr<std::string>(new std::string(otherLabel)));
+                thirdBlock = &(*thirdIt);
+                thirdBlock->setIterator(thirdIt);
+                
                 for (auto state : otherStates) {
                     statesAndValues[position] = std::make_pair(state, storm::utility::zero<ValueType>());
                     positions[state] = position;
-                stateToBlockMapping[state] = &thirdBlock;
+                    stateToBlockMapping[state] = thirdBlock;
                     ++position;
                 }
+            }
             
             // If we are requested to store silent probabilities, we need to prepare the vector.
             if (this->keepSilentProbabilities) {