some more work on bisim

Former-commit-id: aaa8088b00

src/models/sparse/StandardRewardModel.cpp

@@ -147,6 +147,7 @@ namespace storm {
                 if (this->hasTransitionRewards()) {
                     if (this->hasStateActionRewards()) {
                         storm::utility::vector::addVectors<ValueType>(this->getStateActionRewardVector(), transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()), this->getStateActionRewardVector());
+                        optionalStateActionRewardVector = boost::none;
                     } else {
                         this->optionalStateActionRewardVector = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix());
                     }
@@ -157,8 +158,9 @@ namespace storm {
                         STORM_LOG_THROW(this->getStateRewardVector().size() == this->getStateActionRewardVector().size(), storm::exceptions::InvalidOperationException, "The reduction to state rewards is only possible of both the state and the state-action rewards have the same dimension.");
                         storm::utility::vector::addVectors<ValueType>(this->getStateActionRewardVector(), this->getStateRewardVector(), this->getStateRewardVector());
                     } else {
-                        this->optionalStateRewardVector = std::move(this->optionalStateRewardVector);
+                        this->optionalStateRewardVector = std::move(this->optionalStateActionRewardVector);
                     }
+                    optionalStateActionRewardVector = boost::none;
                 }
             }
             

src/storage/bisimulation/BisimulationDecomposition.cpp

@@ -28,7 +28,10 @@ namespace storm {
         
         template<typename ModelType>
         BisimulationDecomposition<ModelType>::Options::Options(ModelType const& model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : Options() {
-            if (formulas.size() == 1) {
+            if (formulas.empty()) {
+                this->respectedAtomicPropositions = model.getStateLabeling().getLabels();
+                this->keepRewards = true;
+            } if (formulas.size() == 1) {
                 this->preserveSingleFormula(model, *formulas.front());
             } else {
                 for (auto const& formula : formulas) {
@@ -202,7 +205,7 @@ namespace storm {
                 splitter->unmarkAsSplitter();
                 
                 // Now refine the partition using the current splitter.
-                std::cout << "refining based on splitter " << splitter->getId() << std::endl;
+//                std::cout << "refining based on splitter " << splitter->getId() << std::endl;
                 refinePartitionBasedOnSplitter(*splitter, splitterQueue);
             }
         }
@@ -236,8 +239,8 @@ namespace storm {
                 this->splitInitialPartitionBasedOnStateRewards();
             }
             
-            std::cout << "successfully built (label) initial partition" << std::endl;
-            partition.print();
+//            std::cout << "successfully built (label) initial partition" << std::endl;
+//            partition.print();
         }
         
         template<typename ModelType>
@@ -257,8 +260,8 @@ namespace storm {
                 this->splitInitialPartitionBasedOnStateRewards();
             }
             
-            std::cout << "successfully built (measure-driven) initial partition" << std::endl;
-            partition.print();
+//            std::cout << "successfully built (measure-driven) initial partition" << std::endl;
+//            partition.print();
         }
         
         template<typename ModelType>

src/storage/bisimulation/Block.cpp

@@ -35,7 +35,7 @@ namespace storm {
             }
             
             void Block::setBeginIndex(storm::storage::sparse::state_type beginIndex) {
-                std::cout << "setting beg index to " << beginIndex << " [" << this << "]" << std::endl;
+//                std::cout << "setting beg index to " << beginIndex << " [" << this << "]" << std::endl;
                 this->beginIndex = beginIndex;
                 STORM_LOG_ASSERT(beginIndex < endIndex, "Unable to resize block to illegal size.");
             }

src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp

@@ -29,8 +29,8 @@ namespace storm {
         
         template<typename ModelType>
         DeterministicModelBisimulationDecomposition<ModelType>::DeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition<ModelType>::Options const& options) : BisimulationDecomposition<ModelType>(model, options), probabilitiesToCurrentSplitter(model.getNumberOfStates(), storm::utility::zero<ValueType>()), predecessorsOfCurrentSplitter(model.getNumberOfStates()) {
-            STORM_LOG_THROW(!model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model.");
-            STORM_LOG_THROW(!model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls).");
+            STORM_LOG_THROW(!options.keepRewards || !model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model.");
+            STORM_LOG_THROW(!options.keepRewards || !model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls).");
             STORM_LOG_THROW(options.type != BisimulationType::Weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties.");
         }
         
@@ -160,7 +160,7 @@ namespace storm {
         template<typename ModelType>
         void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitter(std::list<Block*>& predecessorBlocks, std::deque<bisimulation::Block*>& splitterQueue) {
             for (auto block : predecessorBlocks) {
-                std::cout << "splitting predecessor block " << block->getId() << " of splitter" << std::endl;
+//                std::cout << "splitting predecessor block " << block->getId() << " of splitter" << std::endl;
                 this->partition.splitBlock(*block, [this] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) {
                     bool firstIsPredecessor = isPredecessorOfCurrentSplitter(state1);
                     bool secondIsPredecessor = isPredecessorOfCurrentSplitter(state2);
@@ -175,7 +175,7 @@ namespace storm {
                     splitterQueue.emplace_back(&block);
                 });
 //                this->partition.print();
-                std::cout << "size: " << this->partition.size() << std::endl;
+//                std::cout << "size: " << this->partition.size() << std::endl;
                 
                 // Remember that we have refined the block.
                 block->setNeedsRefinement(false);
@@ -227,10 +227,10 @@ namespace storm {
                 }
             }
             
-            std::cout << "probs of splitter predecessors: " << std::endl;
-            for (auto state : predecessorsOfCurrentSplitter) {
-                std::cout << state << " [" << this->partition.getBlock(state).getId() << "]" << " -> " << probabilitiesToCurrentSplitter[state] << std::endl;
-            }
+//            std::cout << "probs of splitter predecessors: " << std::endl;
+//            for (auto state : predecessorsOfCurrentSplitter) {
+//                std::cout << state << " [" << this->partition.getBlock(state).getId() << "]" << " -> " << probabilitiesToCurrentSplitter[state] << std::endl;
+//            }
             
             if (this->options.type == BisimulationType::Strong || this->model.getType() == storm::models::ModelType::Ctmc) {
                 refinePredecessorBlocksOfSplitter(predecessorBlocks, splitterQueue);

src/storage/bisimulation/Partition.cpp

@@ -142,7 +142,7 @@ namespace storm {
             std::pair<std::vector<std::unique_ptr<Block>>::iterator, bool> Partition::splitBlock(Block& 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.");
 
-                std::cout << "splitting " << block.getId() << " at pos " << position << " (was " << block.getBeginIndex() << " to " << block.getEndIndex() << ")" << std::endl;
+//                std::cout << "splitting " << block.getId() << " at pos " << position << " (was " << block.getBeginIndex() << " to " << block.getEndIndex() << ")" << std::endl;
                 
                 // In case one of the resulting blocks would be empty, we simply return the current block and do not create
                 // a new one.
@@ -157,7 +157,7 @@ namespace storm {
                 auto newBlockIt = std::prev(blocks.end());
                 
                 // Resize the current block appropriately.
-                std::cout << "setting begin pos of block " << block.getId() << " to " << position << std::endl;
+//                std::cout << "setting begin pos of block " << block.getId() << " to " << position << std::endl;
                 block.setBeginIndex(position);
                 
                 // Mark both blocks as splitters.
@@ -171,7 +171,7 @@ namespace storm {
             }
             
             bool Partition::splitBlock(Block& block, std::function<bool (storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const& less, std::function<void (Block&)> const& newBlockCallback) {
-                std::cout << "sorting the block [" << block.getId() << "]" << std::endl;
+//                std::cout << "sorting the block [" << block.getId() << "]" << std::endl;
                 // Sort the range of the block such that all states that have the label are moved to the front.
                 std::sort(this->begin(block), this->end(block), less);
                 

src/utility/storm.h

@@ -126,6 +126,7 @@ namespace storm {
         }
         
         storm::storage::DeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
+        bisimulationDecomposition.computeBisimulationDecomposition();
         model = bisimulationDecomposition.getQuotient();
         std::cout << "done." << std::endl << std::endl;
         return model;