Eliminated two bugs, more to come.

Former-commit-id: 3ea21c66b9

src/storage/BisimulationDecomposition.cpp

@@ -16,7 +16,7 @@ namespace storm {
             std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
             // We start by computing the initial partition. In particular, we also keep a mapping of states to their blocks.
             std::vector<std::size_t> stateToBlockMapping(dtmc.getNumberOfStates());
-            storm::storage::BitVector labeledStates = dtmc.getLabeledStates("observe0Greater1");
+            storm::storage::BitVector labeledStates = dtmc.getLabeledStates("elected");
             this->blocks.emplace_back(labeledStates.begin(), labeledStates.end());
             std::for_each(labeledStates.begin(), labeledStates.end(), [&] (storm::storage::sparse::state_type const& state) { stateToBlockMapping[state] = 0; } );
             labeledStates.complement();

src/storage/BisimulationDecomposition2.cpp

@@ -11,7 +11,7 @@ namespace storm {
         static std::size_t globalId = 0;
         
         template<typename ValueType>
-        BisimulationDecomposition2<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedPosition(begin), id(globalId++) {
+        BisimulationDecomposition2<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), id(globalId++) {
             if (next != nullptr) {
                 next->prev = this;
             }
@@ -232,11 +232,10 @@ namespace storm {
         
         template<typename ValueType>
         void BisimulationDecomposition2<ValueType>::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
-            std::cout << "swapping states " << state1 << " and " << state2 << std::endl;
+            std::cout << "swapping states " << state1 << " and " << state2 << " at positions " << this->positions[state1] << " and " << this->positions[state2] << std::endl;
             std::swap(this->states[this->positions[state1]], this->states[this->positions[state2]]);
             std::swap(this->values[this->positions[state1]], this->values[this->positions[state2]]);
             std::swap(this->positions[state1], this->positions[state2]);
-            assert(this->check());
         }
         
         template<typename ValueType>
@@ -252,7 +251,6 @@ namespace storm {
             this->positions[state2] = position1;
             std::cout << "pos of " << state1 << " is now " << position2 << " and pos of " << state2 << " is now " << position1 << std::endl;
             std::cout << this->states[position1] << " vs " << state2 << " and " << this->states[position2] << " vs " << state1 << std::endl;
-            assert(this->check());
         }
         
         template<typename ValueType>
@@ -559,7 +557,7 @@ namespace storm {
             // Now we can check whether the block needs to be split, which is the case iff the probabilities for the
             // first and the last state are different.
             std::size_t createdBlocks = 0;
-            while (std::abs(partition.getValueAtPosition(beginIndex) - partition.getValueAtPosition(endIndex)) >= 1e-6) {
+            while (std::abs(partition.getValueAtPosition(beginIndex) - partition.getValueAtPosition(endIndex - 1)) >= 1e-6) {
                 // Now we scan for the first state in the block that disagrees on the probability value.
                 // Note that we do not have to check currentIndex for staying within bounds, because we know the matching
                 // state is within bounds.
@@ -575,9 +573,9 @@ namespace storm {
                 // Now we split the block and mark it as a potential splitter.
                 ++createdBlocks;
                 Block& newBlock = partition.splitBlock(block, currentIndex);
-                if (!newBlock.isMarkedAsPredecessor()) {
-                    newBlock.markAsSplitter();
+                if (!newBlock.isMarkedAsSplitter()) {
                     splitterQueue.push_back(&newBlock);
+                    newBlock.markAsSplitter();
                 }
                 beginIndex = currentIndex;
             }
@@ -658,8 +656,11 @@ namespace storm {
                     }
                     
                     if (!predecessorBlock.isMarkedAsPredecessor()) {
+                        std::cout << "not already in there" << std::endl;
                         predecessorBlocks.emplace_back(&predecessorBlock);
                         predecessorBlock.markAsPredecessorBlock();
+                    } else {
+                        std::cout << "already in there" << std::endl;
                     }
                 }
                 
@@ -671,6 +672,8 @@ namespace storm {
                 }
             }
             
+            std::cout << "(1)having " << predecessorBlocks.size() << " pred blocks " << std::endl;
+            
             // Now we can traverse the list of states of the splitter whose predecessors we have not yet explored.
             for (auto stateIterator = partition.getStates().begin() + splitter.getOriginalBegin(), stateIte = partition.getStates().begin() + splitter.getMarkedPosition(); stateIterator != stateIte; ++stateIterator) {
                 storm::storage::sparse::state_type currentState = *stateIterator;
@@ -699,7 +702,7 @@ namespace storm {
             
             std::list<Block*> blocksToSplit;
             
-            std::cout << "having " << predecessorBlocks.size() << " pred blocks " << std::endl;
+            std::cout << "(2)having " << predecessorBlocks.size() << " pred blocks " << std::endl;
             
             // Now, we can iterate over the predecessor blocks and see whether we have to create a new block for
             // predecessors of the splitter.
@@ -714,9 +717,12 @@ namespace storm {
                     std::cout << "moved begin of block " << block.getId() << " to " << block.getBegin() << " and end to " << block.getEnd() << std::endl;
                     
                     Block& newBlock = partition.insertBlock(block);
-                    std::cout << "created new block " << std::endl;
+                    std::cout << "created new block " << newBlock.getId() << " from block " << block.getId() << std::endl;
                     newBlock.print(partition);
-                    splitterQueue.push_back(&newBlock);
+                    if (!newBlock.isMarkedAsSplitter()) {
+                        splitterQueue.push_back(&newBlock);
+                        newBlock.markAsSplitter();
+                    }
                 } else {
                     std::cout << "all states are predecessors" << std::endl;
                     

src/utility/cli.h

@@ -261,7 +261,7 @@ namespace storm {
                 if (settings.isBisimulationSet()) {
                     STORM_LOG_THROW(result->getType() == storm::models::DTMC, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only compatible with DTMCs.");
                     std::shared_ptr<storm::models::Dtmc<double>> dtmc = result->template as<storm::models::Dtmc<double>>();
-//                    storm::storage::BisimulationDecomposition<double> bisimulationDecomposition(*dtmc);
+                    storm::storage::BisimulationDecomposition<double> bisimulationDecomposition(*dtmc);
                     storm::storage::BisimulationDecomposition2<double> bisimulationDecomposition2(*dtmc);
                 }