From b67ac0619f2cd9825744d70536dfbb5001dccb6f Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 8 Oct 2014 23:18:10 +0200 Subject: [PATCH] Weak bisimulation now supported. Still need to improve the performance of the quotienting, however. Former-commit-id: d0f76808bb9269df3a39e3fde9b05cd11af1916e --- src/storage/BisimulationDecomposition.cpp | 114 +++++++++++++++++----- src/storage/BisimulationDecomposition.h | 4 +- src/storage/Distribution.cpp | 13 +++ src/storage/Distribution.h | 9 ++ 4 files changed, 113 insertions(+), 27 deletions(-) diff --git a/src/storage/BisimulationDecomposition.cpp b/src/storage/BisimulationDecomposition.cpp index 53459fb38..1c107d1a8 100644 --- a/src/storage/BisimulationDecomposition.cpp +++ b/src/storage/BisimulationDecomposition.cpp @@ -48,7 +48,7 @@ namespace storm { refinementQueue.pop_front(); blocksInRefinementQueue.set(currentBlock, false); - splitBlock(dtmc, backwardTransitions, currentBlock, stateToBlockMapping, distributions, blocksInRefinementQueue, refinementQueue); + splitBlock(dtmc, backwardTransitions, currentBlock, stateToBlockMapping, distributions, blocksInRefinementQueue, refinementQueue, weak); } std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart; @@ -57,52 +57,96 @@ namespace storm { } template - std::size_t BisimulationDecomposition::splitPredecessorsGraphBased(storm::models::Dtmc const& dtmc, storm::storage::SparseMatrix const& backwardTransitions, std::size_t const& blockId, std::vector& stateToBlockMapping, std::vector>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque& graphRefinementQueue) { + std::size_t BisimulationDecomposition::splitPredecessorsGraphBased(storm::models::Dtmc const& dtmc, storm::storage::SparseMatrix const& backwardTransitions, std::size_t const& blockId, std::vector& stateToBlockMapping, std::vector>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque& graphRefinementQueue, storm::storage::BitVector& splitBlocks) { + std::cout << "entering " << std::endl; + std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); + +// std::cout << "refining predecessors of " << blockId << std::endl; // This method tries to split the blocks of predecessors of the provided block by checking whether there is // a transition into the current block or not. std::unordered_map::block_type> predecessorBlockToNewBlock; // Now for each predecessor block which state could actually reach the current block. + std::chrono::high_resolution_clock::time_point predIterStart = std::chrono::high_resolution_clock::now(); + int predCounter = 0; + storm::storage::BitVector preds(dtmc.getNumberOfStates()); for (auto const& state : this->blocks[blockId]) { for (auto const& predecessorEntry : backwardTransitions.getRow(state)) { + ++predCounter; storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); - predecessorBlockToNewBlock[stateToBlockMapping[predecessor]].insert(predecessor); + if (!preds.get(predecessor)) { +// std::cout << "having pred " << predecessor << " with block " << stateToBlockMapping[predecessor] << std::endl; + predecessorBlockToNewBlock[stateToBlockMapping[predecessor]].insert(predecessor); + preds.set(predecessor); + } } } - + std::chrono::high_resolution_clock::duration predIterTime = std::chrono::high_resolution_clock::now() - predIterStart; + std::cout << "took " << std::chrono::duration_cast(predIterTime).count() << "ms. for " << predCounter << " predecessors" << std::endl; + // Now, we can check for each predecessor block whether it needs to be split. for (auto const& blockNewBlockPair : predecessorBlockToNewBlock) { if (this->blocks[blockNewBlockPair.first].size() > blockNewBlockPair.second.size()) { - // Add the states which have a successor in the current block to a totally new block. - this->blocks.emplace_back(std::move(blockNewBlockPair.second)); + std::cout << "splitting!" << std::endl; +// std::cout << "found that not all " << this->blocks[blockNewBlockPair.first].size() << " states of block " << blockNewBlockPair.first << " have a successor in " << blockId << " but only " << blockNewBlockPair.second.size() << std::endl; +// std::cout << "original: " << this->blocks[blockNewBlockPair.first] << std::endl; +// std::cout << "states with pred: " << blockNewBlockPair.second << std::endl; + // Now update the block mapping for the smaller of the two blocks. + typename BisimulationDecomposition::block_type smallerBlock; + typename BisimulationDecomposition::block_type largerBlock; + if (blockNewBlockPair.second.size() < this->blocks[blockNewBlockPair.first].size()/2) { + smallerBlock = std::move(blockNewBlockPair.second); + std::set_difference(this->blocks[blockNewBlockPair.first].begin(), this->blocks[blockNewBlockPair.first].end(), smallerBlock.begin(), smallerBlock.end(), std::inserter(largerBlock, largerBlock.begin())); + } else { + largerBlock = std::move(blockNewBlockPair.second); + std::set_difference(this->blocks[blockNewBlockPair.first].begin(), this->blocks[blockNewBlockPair.first].end(), largerBlock.begin(), largerBlock.end(), std::inserter(smallerBlock, smallerBlock.begin())); + } - // Compute the set of states that remains in the old block; - typename BisimulationDecomposition::block_type newBlock; - std::set_difference(this->blocks[blockId].begin(), this->blocks[blockId].end(), this->blocks.back().begin(), this->blocks.back().end(), std::inserter(newBlock, newBlock.begin())); - this->blocks[blockNewBlockPair.first] = std::move(newBlock); +// std::cout << "created a smaller block with " << smallerBlock.size() << " states and a larger one with " << largerBlock.size() << "states" << std::endl; +// std::cout << "smaller: " << smallerBlock << std::endl; +// std::cout << "larger: " << largerBlock << std::endl; + + this->blocks.emplace_back(std::move(smallerBlock)); + this->blocks[blockNewBlockPair.first] = std::move(largerBlock); + + // Update the block mapping of all moved states. + std::size_t newBlockId = this->blocks.size() - 1; + for (auto const& state : this->blocks.back()) { + stateToBlockMapping[state] = newBlockId; +// std::cout << "updating " << state << " to block " << newBlockId << std::endl; + } blocksInRefinementQueue.resize(this->blocks.size()); - // Add the smaller part of the old block to the queue. - std::size_t blockToAddToQueue = this->blocks.back().size() < this->blocks[blockNewBlockPair.first].size() ? this->blocks.size() - 1 : blockNewBlockPair.first; - if (!blocksInRefinementQueue.get(blockToAddToQueue)) { - graphRefinementQueue.push_back(blockToAddToQueue); - blocksInRefinementQueue.set(blockToAddToQueue, true); + // Add both parts of the old block to the queue. + if (!blocksInRefinementQueue.get(blockNewBlockPair.first)) { + graphRefinementQueue.push_back(blockNewBlockPair.first); + blocksInRefinementQueue.set(blockNewBlockPair.first, true); +// std::cout << "adding " << blockNewBlockPair.first << " to refine further using graph-based analysis " << std::endl; } + + graphRefinementQueue.push_back(this->blocks.size() - 1); + blocksInRefinementQueue.set(this->blocks.size() - 1); +// std::cout << "adding " << this->blocks.size() - 1 << " to refine further using graph-based analysis " << std::endl; } } + std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart; + std::cout << "refinement of predecessors of block " << blockId << " took " << std::chrono::duration_cast(totalTime).count() << "ms." << std::endl; + +// std::cout << "done. "<< std::endl; // FIXME return 0; } template - std::size_t BisimulationDecomposition::splitBlock(storm::models::Dtmc const& dtmc, storm::storage::SparseMatrix const& backwardTransitions, std::size_t const& blockId, std::vector& stateToBlockMapping, std::vector>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque& refinementQueue) { + std::size_t BisimulationDecomposition::splitBlock(storm::models::Dtmc const& dtmc, storm::storage::SparseMatrix const& backwardTransitions, std::size_t const& blockId, std::vector& stateToBlockMapping, std::vector>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque& refinementQueue, bool weakBisimulation) { std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); std::unordered_map, typename BisimulationDecomposition::block_type> distributionToNewBlocks; // Traverse all states of the block and check whether they have different distributions. + std::chrono::high_resolution_clock::time_point gatherStart = std::chrono::high_resolution_clock::now(); for (auto const& state : this->blocks[blockId]) { // Now construct the distribution of this state wrt. to the current partitioning. storm::storage::Distribution distribution; @@ -110,6 +154,12 @@ namespace storm { distribution.addProbability(static_cast(stateToBlockMapping[successorEntry.getColumn()]), successorEntry.getValue()); } + // If we are requested to compute a weak bisimulation, we need to scale the distribution with the + // self-loop probability. + if (weakBisimulation) { + distribution.scale(blockId); + } + // If the distribution already exists, we simply add the state. Otherwise, we open a new block. auto distributionIterator = distributionToNewBlocks.find(distribution); if (distributionIterator != distributionToNewBlocks.end()) { @@ -119,10 +169,13 @@ namespace storm { } } + std::chrono::high_resolution_clock::duration gatherTime = std::chrono::high_resolution_clock::now() - gatherStart; + std::cout << "time to iterate over all states was " << std::chrono::duration_cast(gatherTime).count() << "ms." << std::endl; + // Now we are ready to split the block. if (distributionToNewBlocks.size() == 1) { // If there is just one behavior, we just set the distribution as the new one for this block. - distributions[blockId] = std::move(distributionToNewBlocks.begin()->first); + // distributions[blockId] = std::move(distributionToNewBlocks.begin()->first); } else { // In this case, we need to split the block. typename BisimulationDecomposition::block_type tmpBlock; @@ -154,21 +207,32 @@ namespace storm { std::deque localRefinementQueue; storm::storage::BitVector blocksInLocalRefinementQueue(this->size()); localRefinementQueue.push_back(blockId); +// std::cout << "adding " << blockId << " to local ref queue " << std::endl; + blocksInLocalRefinementQueue.set(blockId); for (std::size_t i = beforeNumberOfBlocks; i < this->blocks.size(); ++i) { localRefinementQueue.push_back(i); + blocksInLocalRefinementQueue.set(i); +// std::cout << "adding " << i << " to local refinement queue " << std::endl; } + + // We need to keep track of which blocks were split so we can later add all their predecessors as + // candidates for furter splitting. + storm::storage::BitVector splitBlocks(this->size()); - while (!localRefinementQueue.empty()) { - std::size_t currentBlock = localRefinementQueue.front(); - localRefinementQueue.pop_front(); - blocksInLocalRefinementQueue.set(currentBlock, false); - - splitPredecessorsGraphBased(dtmc, backwardTransitions, blockId, stateToBlockMapping, distributions, blocksInLocalRefinementQueue, localRefinementQueue); - } +// while (!localRefinementQueue.empty()) { +// std::size_t currentBlock = localRefinementQueue.front(); +// localRefinementQueue.pop_front(); +// blocksInLocalRefinementQueue.set(currentBlock, false); +// +// splitPredecessorsGraphBased(dtmc, backwardTransitions, currentBlock, stateToBlockMapping, distributions, blocksInLocalRefinementQueue, localRefinementQueue, splitBlocks); +// } + +// std::cout << "split blocks: " << std::endl; +// std::cout << splitBlocks << std::endl; // Since we created some new blocks, we need to extend the bit vector storing the blocks in the // refinement queue. - blocksInRefinementQueue.resize(blocksInRefinementQueue.size() + (distributionToNewBlocks.size() - 1)); + blocksInRefinementQueue.resize(this->blocks.size()); // Insert blocks that possibly need a refinement into the queue. for (auto const& state : tmpBlock) { diff --git a/src/storage/BisimulationDecomposition.h b/src/storage/BisimulationDecomposition.h index d02d02bc1..55ed556d8 100644 --- a/src/storage/BisimulationDecomposition.h +++ b/src/storage/BisimulationDecomposition.h @@ -26,8 +26,8 @@ namespace storm { private: void computeBisimulationEquivalenceClasses(storm::models::Dtmc const& model, bool weak); - std::size_t splitPredecessorsGraphBased(storm::models::Dtmc const& dtmc, storm::storage::SparseMatrix const& backwardTransitions, std::size_t const& block, std::vector& stateToBlockMapping, std::vector>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque& refinementQueue); - std::size_t splitBlock(storm::models::Dtmc const& dtmc, storm::storage::SparseMatrix const& backwardTransitions, std::size_t const& block, std::vector& stateToBlockMapping, std::vector>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque& refinementQueue); + std::size_t splitPredecessorsGraphBased(storm::models::Dtmc const& dtmc, storm::storage::SparseMatrix const& backwardTransitions, std::size_t const& block, std::vector& stateToBlockMapping, std::vector>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque& refinementQueue, storm::storage::BitVector& splitBlocks); + std::size_t splitBlock(storm::models::Dtmc const& dtmc, storm::storage::SparseMatrix const& backwardTransitions, std::size_t const& block, std::vector& stateToBlockMapping, std::vector>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque& refinementQueue, bool weakBisimulation); }; } } diff --git a/src/storage/Distribution.cpp b/src/storage/Distribution.cpp index 55de31d51..50e93f567 100644 --- a/src/storage/Distribution.cpp +++ b/src/storage/Distribution.cpp @@ -65,6 +65,19 @@ namespace storm { return this->distribution.end(); } + template + void Distribution::scale(storm::storage::sparse::state_type const& state) { + auto probabilityIterator = this->distribution.find(state); + if (probabilityIterator != this->distribution.end()) { + ValueType scaleValue = 1 / probabilityIterator->second; + this->distribution.erase(probabilityIterator); + + for (auto& entry : this->distribution) { + entry.second *= scaleValue; + } + } + } + template std::size_t Distribution::getHash() const { return this->hash ^ (this->distribution.size() << 8); diff --git a/src/storage/Distribution.h b/src/storage/Distribution.h index a888a88ed..010cf43bc 100644 --- a/src/storage/Distribution.h +++ b/src/storage/Distribution.h @@ -66,6 +66,15 @@ namespace storm { */ const_iterator end() const; + /*! + * Scales the distribution by multiplying all the probabilities with 1/p where p is the probability of moving + * to the given state and sets the probability of moving to the given state to zero. If the probability is + * already zero, this operation has no effect. + * + * @param state The state whose associated probability is used to scale the distribution. + */ + void scale(storm::storage::sparse::state_type const& state); + /*! * Retrieves the hash value of the distribution. *