Merge branch 'future' into variance_properties

Former-commit-id: 74258afddd

src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp

@@ -203,6 +203,7 @@ namespace storm {
         
         template<typename ModelType>
         void DeterministicModelBisimulationDecomposition<ModelType>::increaseProbabilityToSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block<BlockDataType> const& predecessorBlock, ValueType const& value) {
+            STORM_LOG_TRACE("Increasing probability of " << predecessor << " to splitter by " << value << ".");
             storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor);
             
             // If the position of the state is to the right of marker1, we have not seen it before.
@@ -269,6 +270,12 @@ namespace storm {
                         continue;
                     }
 
+                    // If we are computing a weak bisimulation on CTMCs and the predecessor block is the splitter, we
+                    // need to ignore it and proceed to the next predecessor.
+                    if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Ctmc && predecessorBlock == splitter) {
+                        continue;
+                    }
+                    
                     // We keep track of the probability of the predecessor moving to the splitter.
                     increaseProbabilityToSplitter(predecessor, predecessorBlock, predecessorEntry.getValue());
                     
@@ -278,7 +285,10 @@ namespace storm {
                         moveStateToMarker1(predecessor, predecessorBlock);
                     }
                     
-                    insertIntoPredecessorList(predecessorBlock, predecessorBlocks);
+                    // We must not insert the the splitter itself if we are not computing a weak bisimulation on CTMCs.
+                    if (this->options.getType() != BisimulationType::Weak || this->model.getType() != storm::models::ModelType::Ctmc || predecessorBlock != splitter) {
+                        insertIntoPredecessorList(predecessorBlock, predecessorBlocks);
+                    }
                 }
             }
             
@@ -464,6 +474,12 @@ namespace storm {
                         continue;
                     }
                     
+                    // If we are computing a weak bisimulation on CTMCs and the predecessor block is the splitter, we
+                    // need to ignore it and proceed to the next predecessor.
+                    if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Ctmc && predecessorBlock == splitter) {
+                        continue;
+                    }
+                    
                     // We keep track of the probability of the predecessor moving to the splitter.
                     increaseProbabilityToSplitter(predecessor, predecessorBlock, predecessorEntry.getValue());
                     
@@ -495,6 +511,8 @@ namespace storm {
             
             // Finally, we split the block based on the precomputed probabilities and the chosen bisimulation type.
             if (this->options.getType() == BisimulationType::Strong || this->model.getType() == storm::models::ModelType::Ctmc) {
+                // In the case of CTMCs and weak bisimulation, we still call the "splitStrong" method, but we already have
+                // taken care of not adding the splitter to the predecessor blocks, so this is safe.
                 refinePredecessorBlocksOfSplitterStrong(predecessorBlocks, splitterQueue);
             } else {
                 // If the splitter is a predecessor of we can use the computed probabilities to update the silent

src/storage/bisimulation/Partition.cpp

@@ -211,7 +211,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_TRACE("Splitting " << block.getId() << " at position " << position << " (begin was " << block.getBeginIndex() << ".");
+                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
                 // a new one.