From 0e0027aa8e51ee9034681b4b5dacb8a66028d90b Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 13 Oct 2014 11:59:57 +0200 Subject: [PATCH] Further work on sparse bisimulation. Former-commit-id: ba256b8b0a9c5e3f1a9a5870f4ef32af7fa18396 --- ...inisticModelBisimulationDecomposition.cpp} | 273 +++++++++--------- ...rministicModelBisimulationDecomposition.h} | 25 +- ...inisticModelBisimulationDecomposition.cpp} | 43 +-- ...rministicModelBisimulationDecomposition.h} | 12 +- src/utility/cli.h | 8 +- 5 files changed, 188 insertions(+), 173 deletions(-) rename src/storage/{BisimulationDecomposition2.cpp => DeterministicModelBisimulationDecomposition.cpp} (66%) rename src/storage/{BisimulationDecomposition2.h => DeterministicModelBisimulationDecomposition.h} (92%) rename src/storage/{BisimulationDecomposition.cpp => NaiveDeterministicModelBisimulationDecomposition.cpp} (84%) rename src/storage/{BisimulationDecomposition.h => NaiveDeterministicModelBisimulationDecomposition.h} (74%) diff --git a/src/storage/BisimulationDecomposition2.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp similarity index 66% rename from src/storage/BisimulationDecomposition2.cpp rename to src/storage/DeterministicModelBisimulationDecomposition.cpp index 38d02ae90..144560557 100644 --- a/src/storage/BisimulationDecomposition2.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -1,4 +1,4 @@ -#include "src/storage/BisimulationDecomposition2.h" +#include "src/storage/DeterministicModelBisimulationDecomposition.h" #include #include @@ -11,7 +11,7 @@ namespace storm { static std::size_t globalId = 0; template - BisimulationDecomposition2::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++) { + DeterministicModelBisimulationDecomposition::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; } @@ -21,8 +21,8 @@ namespace storm { } template - void BisimulationDecomposition2::Block::print(Partition const& partition) const { - std::cout << "block " << this->getId() << " with marked position " << this->getMarkedPosition() << std::endl; + void DeterministicModelBisimulationDecomposition::Block::print(Partition const& partition) const { + std::cout << "block " << this->getId() << " with marked position " << this->getMarkedPosition() << " and original begin " << this->getOriginalBegin() << std::endl; std::cout << "begin: " << this->begin << " and end: " << this->end << " (number of states: " << this->getNumberOfStates() << ")" << std::endl; std::cout << "states:" << std::endl; for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) { @@ -40,34 +40,33 @@ namespace storm { } template - void BisimulationDecomposition2::Block::setBegin(storm::storage::sparse::state_type begin) { + void DeterministicModelBisimulationDecomposition::Block::setBegin(storm::storage::sparse::state_type begin) { this->begin = begin; this->markedPosition = begin; } template - void BisimulationDecomposition2::Block::setEnd(storm::storage::sparse::state_type end) { + void DeterministicModelBisimulationDecomposition::Block::setEnd(storm::storage::sparse::state_type end) { this->end = end; } template - void BisimulationDecomposition2::Block::incrementBegin() { + void DeterministicModelBisimulationDecomposition::Block::incrementBegin() { ++this->begin; - std::cout << "incremented begin to " << this->begin << std::endl; } template - void BisimulationDecomposition2::Block::decrementEnd() { + void DeterministicModelBisimulationDecomposition::Block::decrementEnd() { ++this->begin; } template - storm::storage::sparse::state_type BisimulationDecomposition2::Block::getBegin() const { + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getBegin() const { return this->begin; } template - storm::storage::sparse::state_type BisimulationDecomposition2::Block::getOriginalBegin() const { + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getOriginalBegin() const { if (this->hasPreviousBlock()) { return this->getPreviousBlock().getEnd(); } else { @@ -76,74 +75,73 @@ namespace storm { } template - storm::storage::sparse::state_type BisimulationDecomposition2::Block::getEnd() const { + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getEnd() const { return this->end; } template - void BisimulationDecomposition2::Block::setIterator(const_iterator it) { + void DeterministicModelBisimulationDecomposition::Block::setIterator(const_iterator it) { this->selfIt = it; } template - typename BisimulationDecomposition2::Block::const_iterator BisimulationDecomposition2::Block::getIterator() const { + typename DeterministicModelBisimulationDecomposition::Block::const_iterator DeterministicModelBisimulationDecomposition::Block::getIterator() const { return this->selfIt; } template - typename BisimulationDecomposition2::Block::const_iterator BisimulationDecomposition2::Block::getNextIterator() const { + typename DeterministicModelBisimulationDecomposition::Block::const_iterator DeterministicModelBisimulationDecomposition::Block::getNextIterator() const { return this->getNextBlock().getIterator(); } template - typename BisimulationDecomposition2::Block::const_iterator BisimulationDecomposition2::Block::getPreviousIterator() const { + typename DeterministicModelBisimulationDecomposition::Block::const_iterator DeterministicModelBisimulationDecomposition::Block::getPreviousIterator() const { return this->getPreviousBlock().getIterator(); } template - typename BisimulationDecomposition2::Block& BisimulationDecomposition2::Block::getNextBlock() { + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Block::getNextBlock() { return *this->next; } template - typename BisimulationDecomposition2::Block const& BisimulationDecomposition2::Block::getNextBlock() const { + typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Block::getNextBlock() const { return *this->next; } template - bool BisimulationDecomposition2::Block::hasNextBlock() const { + bool DeterministicModelBisimulationDecomposition::Block::hasNextBlock() const { return this->next != nullptr; } template - typename BisimulationDecomposition2::Block& BisimulationDecomposition2::Block::getPreviousBlock() { + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Block::getPreviousBlock() { return *this->prev; } template - typename BisimulationDecomposition2::Block* BisimulationDecomposition2::Block::getPreviousBlockPointer() { + typename DeterministicModelBisimulationDecomposition::Block* DeterministicModelBisimulationDecomposition::Block::getPreviousBlockPointer() { return this->prev; } template - typename BisimulationDecomposition2::Block* BisimulationDecomposition2::Block::getNextBlockPointer() { + typename DeterministicModelBisimulationDecomposition::Block* DeterministicModelBisimulationDecomposition::Block::getNextBlockPointer() { return this->next; } template - typename BisimulationDecomposition2::Block const& BisimulationDecomposition2::Block::getPreviousBlock() const { + typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Block::getPreviousBlock() const { return *this->prev; } template - bool BisimulationDecomposition2::Block::hasPreviousBlock() const { + bool DeterministicModelBisimulationDecomposition::Block::hasPreviousBlock() const { return this->prev != nullptr; } template - bool BisimulationDecomposition2::Block::check() const { + bool DeterministicModelBisimulationDecomposition::Block::check() const { if (this->begin >= this->end) { - std::cout << "beg: " << this->begin << " and end " << this->end << std::endl; assert(false); } if (this->prev != nullptr) { @@ -156,68 +154,68 @@ namespace storm { } template - std::size_t BisimulationDecomposition2::Block::getNumberOfStates() const { + std::size_t DeterministicModelBisimulationDecomposition::Block::getNumberOfStates() const { // We need to take the original begin here, because the begin is temporarily moved. return (this->end - this->getOriginalBegin()); } template - bool BisimulationDecomposition2::Block::isMarkedAsSplitter() const { + bool DeterministicModelBisimulationDecomposition::Block::isMarkedAsSplitter() const { return this->markedAsSplitter; } template - void BisimulationDecomposition2::Block::markAsSplitter() { + void DeterministicModelBisimulationDecomposition::Block::markAsSplitter() { this->markedAsSplitter = true; } template - void BisimulationDecomposition2::Block::unmarkAsSplitter() { + void DeterministicModelBisimulationDecomposition::Block::unmarkAsSplitter() { this->markedAsSplitter = false; } template - std::size_t BisimulationDecomposition2::Block::getId() const { + std::size_t DeterministicModelBisimulationDecomposition::Block::getId() const { return this->id; } template - storm::storage::sparse::state_type BisimulationDecomposition2::Block::getMarkedPosition() const { + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getMarkedPosition() const { return this->markedPosition; } template - void BisimulationDecomposition2::Block::setMarkedPosition(storm::storage::sparse::state_type position) { + void DeterministicModelBisimulationDecomposition::Block::setMarkedPosition(storm::storage::sparse::state_type position) { this->markedPosition = position; } template - void BisimulationDecomposition2::Block::resetMarkedPosition() { + void DeterministicModelBisimulationDecomposition::Block::resetMarkedPosition() { this->markedPosition = this->begin; } template - void BisimulationDecomposition2::Block::incrementMarkedPosition() { + void DeterministicModelBisimulationDecomposition::Block::incrementMarkedPosition() { ++this->markedPosition; } template - void BisimulationDecomposition2::Block::markAsPredecessorBlock() { + void DeterministicModelBisimulationDecomposition::Block::markAsPredecessorBlock() { this->markedAsPredecessorBlock = true; } template - void BisimulationDecomposition2::Block::unmarkAsPredecessorBlock() { + void DeterministicModelBisimulationDecomposition::Block::unmarkAsPredecessorBlock() { this->markedAsPredecessorBlock = false; } template - bool BisimulationDecomposition2::Block::isMarkedAsPredecessor() const { + bool DeterministicModelBisimulationDecomposition::Block::isMarkedAsPredecessor() const { return markedAsPredecessorBlock; } template - BisimulationDecomposition2::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) { + DeterministicModelBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) { // Create the block and give it an iterator to itself. typename std::list::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr); it->setIterator(it); @@ -231,117 +229,110 @@ namespace storm { } template - void BisimulationDecomposition2::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { - std::cout << "swapping states " << state1 << " and " << state2 << " at positions " << this->positions[state1] << " and " << this->positions[state2] << std::endl; + void DeterministicModelBisimulationDecomposition::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { 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]); } template - void BisimulationDecomposition2::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) { + void DeterministicModelBisimulationDecomposition::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) { storm::storage::sparse::state_type state1 = this->states[position1]; storm::storage::sparse::state_type state2 = this->states[position2]; - std::cout << "swapping states " << state1 << " and " << state2 << " at positions " << position1 << " and " << position2 << std::endl; std::swap(this->states[position1], this->states[position2]); std::swap(this->values[position1], this->values[position2]); this->positions[state1] = position2; 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; } template - storm::storage::sparse::state_type const& BisimulationDecomposition2::Partition::getPosition(storm::storage::sparse::state_type state) const { + storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition::Partition::getPosition(storm::storage::sparse::state_type state) const { return this->positions[state]; } template - void BisimulationDecomposition2::Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) { + void DeterministicModelBisimulationDecomposition::Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) { this->positions[state] = position; } template - storm::storage::sparse::state_type const& BisimulationDecomposition2::Partition::getState(storm::storage::sparse::state_type position) const { + storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition::Partition::getState(storm::storage::sparse::state_type position) const { return this->states[position]; } template - ValueType const& BisimulationDecomposition2::Partition::getValue(storm::storage::sparse::state_type state) const { + ValueType const& DeterministicModelBisimulationDecomposition::Partition::getValue(storm::storage::sparse::state_type state) const { return this->values[this->positions[state]]; } template - ValueType const& BisimulationDecomposition2::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const { + ValueType const& DeterministicModelBisimulationDecomposition::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const { return this->values[position]; } template - void BisimulationDecomposition2::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) { + void DeterministicModelBisimulationDecomposition::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) { this->values[this->positions[state]] = value; } template - std::vector& BisimulationDecomposition2::Partition::getValues() { + std::vector& DeterministicModelBisimulationDecomposition::Partition::getValues() { return this->values; } template - void BisimulationDecomposition2::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) { + void DeterministicModelBisimulationDecomposition::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) { this->values[this->positions[state]] += value; } template - void BisimulationDecomposition2::Partition::updateBlockMapping(Block& block, std::vector::iterator first, std::vector::iterator last) { + void DeterministicModelBisimulationDecomposition::Partition::updateBlockMapping(Block& block, std::vector::iterator first, std::vector::iterator last) { for (; first != last; ++first) { this->stateToBlockMapping[*first] = █ } } template - typename BisimulationDecomposition2::Block& BisimulationDecomposition2::Partition::getBlock(storm::storage::sparse::state_type state) { + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Partition::getBlock(storm::storage::sparse::state_type state) { return *this->stateToBlockMapping[state]; } template - std::vector::iterator BisimulationDecomposition2::Partition::getBeginOfStates(Block const& block) { + std::vector::iterator DeterministicModelBisimulationDecomposition::Partition::getBeginOfStates(Block const& block) { return this->states.begin() + block.getBegin(); } template - std::vector::iterator BisimulationDecomposition2::Partition::getEndOfStates(Block const& block) { + std::vector::iterator DeterministicModelBisimulationDecomposition::Partition::getEndOfStates(Block const& block) { return this->states.begin() + block.getEnd(); } template - std::vector::const_iterator BisimulationDecomposition2::Partition::getBeginOfStates(Block const& block) const { + std::vector::const_iterator DeterministicModelBisimulationDecomposition::Partition::getBeginOfStates(Block const& block) const { return this->states.begin() + block.getBegin(); } template - std::vector::const_iterator BisimulationDecomposition2::Partition::getEndOfStates(Block const& block) const { + std::vector::const_iterator DeterministicModelBisimulationDecomposition::Partition::getEndOfStates(Block const& block) const { return this->states.begin() + block.getEnd(); } template - typename std::vector::iterator BisimulationDecomposition2::Partition::getBeginOfValues(Block const& block) { + typename std::vector::iterator DeterministicModelBisimulationDecomposition::Partition::getBeginOfValues(Block const& block) { return this->values.begin() + block.getBegin(); } template - typename std::vector::iterator BisimulationDecomposition2::Partition::getEndOfValues(Block const& block) { + typename std::vector::iterator DeterministicModelBisimulationDecomposition::Partition::getEndOfValues(Block const& block) { return this->values.begin() + block.getEnd(); } template - typename BisimulationDecomposition2::Block& BisimulationDecomposition2::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) { + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) { // FIXME: this could be improved by splitting off the smaller of the two resulting blocks. - std::cout << "splitting block (" << block.getBegin() << "," << block.getEnd() << ") at position " << position << std::endl; - block.print(*this); - // In case one of the resulting blocks would be empty, we simply return the current block and do not create // a new one. if (position == block.getBegin() || position == block.getEnd()) { @@ -350,16 +341,12 @@ namespace storm { // Actually create the new block and insert it at the correct position. typename std::list::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block); - std::cout << "created new block from " << block.getBegin() << " to " << position << std::endl; selfIt->setIterator(selfIt); Block& newBlock = *selfIt; // Make the current block end at the given position. block.setBegin(position); - std::cout << "old block: " << std::endl; - block.print(*this); - // Update the mapping of the states in the newly created block. for (auto it = this->getBeginOfStates(newBlock), ite = this->getEndOfStates(newBlock); it != ite; ++it) { stateToBlockMapping[*it] = &newBlock; @@ -369,13 +356,11 @@ namespace storm { } template - typename BisimulationDecomposition2::Block& BisimulationDecomposition2::Partition::insertBlock(Block& block) { + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Partition::insertBlock(Block& block) { // Find the beginning of the new block. storm::storage::sparse::state_type begin; if (block.hasPreviousBlock()) { begin = block.getPreviousBlock().getEnd(); - std::cout << "previous block ended at " << begin << std::endl; - block.getPreviousBlock().print(*this); } else { begin = 0; } @@ -394,7 +379,7 @@ namespace storm { } template - void BisimulationDecomposition2::Partition::splitLabel(storm::storage::BitVector const& statesWithLabel) { + void DeterministicModelBisimulationDecomposition::Partition::splitLabel(storm::storage::BitVector const& statesWithLabel) { for (auto blockIterator = this->blocks.begin(), ite = this->blocks.end(); blockIterator != ite; ) { // The update of the loop was intentionally moved to the bottom of the loop. Block& block = *blockIterator; @@ -422,22 +407,22 @@ namespace storm { } template - std::list::Block> const& BisimulationDecomposition2::Partition::getBlocks() const { + std::list::Block> const& DeterministicModelBisimulationDecomposition::Partition::getBlocks() const { return this->blocks; } template - std::vector& BisimulationDecomposition2::Partition::getStates() { + std::vector& DeterministicModelBisimulationDecomposition::Partition::getStates() { return this->states; } template - std::list::Block>& BisimulationDecomposition2::Partition::getBlocks() { + std::list::Block>& DeterministicModelBisimulationDecomposition::Partition::getBlocks() { return this->blocks; } template - bool BisimulationDecomposition2::Partition::check() const { + bool DeterministicModelBisimulationDecomposition::Partition::check() const { for (uint_fast64_t state = 0; state < this->positions.size(); ++state) { if (this->states[this->positions[state]] != state) { assert(false); @@ -447,7 +432,6 @@ namespace storm { assert(block.check()); for (auto stateIt = this->getBeginOfStates(block), stateIte = this->getEndOfStates(block); stateIt != stateIte; ++stateIt) { if (this->stateToBlockMapping[*stateIt] != &block) { - std::cout << "state " << *stateIt << " has wrong block mapping " << this->stateToBlockMapping[*stateIt] << " (should have " << &block << ")" << std::endl; assert(false); } } @@ -456,7 +440,7 @@ namespace storm { } template - void BisimulationDecomposition2::Partition::print() const { + void DeterministicModelBisimulationDecomposition::Partition::print() const { for (auto const& block : this->blocks) { block.print(*this); } @@ -478,27 +462,60 @@ namespace storm { } template - std::size_t BisimulationDecomposition2::Partition::size() const { - int counter = 0; - for (auto const& element : blocks) { - ++counter; - } - std::cout << "found " << counter << " elements" << std::endl; + std::size_t DeterministicModelBisimulationDecomposition::Partition::size() const { return this->blocks.size(); } template - BisimulationDecomposition2::BisimulationDecomposition2(storm::models::Dtmc const& dtmc, bool weak) { + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& dtmc, bool weak) : model(dtmc), initialBlocks() { computeBisimulationEquivalenceClasses(dtmc, weak); } template - void BisimulationDecomposition2::computeBisimulationEquivalenceClasses(storm::models::Dtmc const& dtmc, bool weak) { + std::shared_ptr> DeterministicModelBisimulationDecomposition::getQuotient() const { + // In order to create the quotient model, we need to construct + // (a) the new transition matrix, + // (b) the new labeling, + // (c) the new reward structures. + + // Prepare a matrix builder for (a). + storm::storage::SparseMatrixBuilder builder; + + // Prepare the new state labeling for (b). + storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions()); + std::set atomicPropositionsSet = model.getStateLabeling().getAtomicPropositions(); + std::vector atomicPropositions = std::vector(atomicPropositionsSet.begin(), atomicPropositionsSet.end()); + for (auto const& ap : atomicPropositions) { + newLabeling.addAtomicProposition(ap); + } + + // Now build (a) and (b) by traversing all blocks. + for (uint_fast64_t blockIndex = 0; blockIndex < this->blocks.size(); ++blockIndex) { + auto const& block = this->blocks[blockIndex]; + + // Pick one representative state. It doesn't matter which state it is, because they all behave equally. + storm::storage::sparse::state_type representativeState = *block.begin(); + + // Add the outgoing transitions + + // Add all atomic propositions to the equivalence class that the representative state satisfies. + for (auto const& ap : atomicPropositions) { + if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) { + newLabeling.addAtomicPropositionToState(ap, blockIndex); + } + } + } + + + return nullptr; + } + + template + void DeterministicModelBisimulationDecomposition::computeBisimulationEquivalenceClasses(storm::models::Dtmc const& dtmc, bool weak) { std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); // We start by computing the initial partition. Partition partition(dtmc.getNumberOfStates()); - partition.print(); for (auto const& label : dtmc.getStateLabeling().getAtomicPropositions()) { if (label == "init") { continue; @@ -506,37 +523,47 @@ namespace storm { partition.splitLabel(dtmc.getLabeledStates(label)); } - std::cout << "initial partition:" << std::endl; - partition.print(); - assert(partition.check()); - // Initially, all blocks are potential splitter, so we insert them in the splitterQueue. std::deque splitterQueue; std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); }); + // FIXME: if weak is set, we want to eliminate the self-loops before doing bisimulation. + storm::storage::SparseMatrix backwardTransitions = dtmc.getBackwardTransitions(); // Then perform the actual splitting until there are no more splitters. while (!splitterQueue.empty()) { splitPartition(backwardTransitions, *splitterQueue.front(), partition, splitterQueue); splitterQueue.pop_front(); - - std::cout << "####### updated partition ##############" << std::endl; - partition.print(); - std::cout << "####### end of updated partition #######" << std::endl; } - std::cout << "computed a quotient of size " << partition.size() << std::endl; + // Now move the states from the internal partition into their final place in the decomposition. We do so in + // a way that maintains the block IDs as indices. + this->blocks.resize(partition.size()); + for (auto const& block : partition.getBlocks()) { + this->blocks[block.getId()] = block_type(partition.getBeginOfStates(block), partition.getEndOfStates(block)); + } + + // FIXME: as we will drop the state-to-block-mapping, we need to create the distribution of each block now. + + // Now check which of the blocks of the partition contain at least one initial state. + for (auto initialState : model.getInitialStates()) { + Block& initialBlock = partition.getBlock(initialState); + if (std::find(this->initialBlocks.begin(), this->initialBlocks.end(), initialBlock.getId()) == this->initialBlocks.end()) { + this->initialBlocks.emplace_back(initialBlock.getId()); + } + } + std::sort(this->initialBlocks.begin(), this->initialBlocks.end()); std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart; - std::cout << "Bisimulation took " << std::chrono::duration_cast(totalTime).count() << "ms." << std::endl; + + if (storm::settings::generalSettings().isShowStatisticsSet()) { + std::cout << "Computed bisimulation quotient in " << std::chrono::duration_cast(totalTime).count() << "ms." << std::endl; + } } template - std::size_t BisimulationDecomposition2::splitBlockProbabilities(Block& block, Partition& partition, std::deque& splitterQueue) { - std::cout << "part before split prob" << std::endl; - partition.print(); - + std::size_t DeterministicModelBisimulationDecomposition::splitBlockProbabilities(Block& block, Partition& partition, std::deque& splitterQueue) { // Sort the states in the block based on their probabilities. std::sort(partition.getBeginOfStates(block), partition.getEndOfStates(block), [&partition] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return partition.getValue(a) < partition.getValue(b); } ); @@ -580,37 +607,23 @@ namespace storm { beginIndex = currentIndex; } - assert(partition.check()); - return createdBlocks; } template - std::size_t BisimulationDecomposition2::splitPartition(storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, std::deque& splitterQueue) { - std::cout << "treating block " << splitter.getId() << " as splitter" << std::endl; - splitter.print(partition); - + std::size_t DeterministicModelBisimulationDecomposition::splitPartition(storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, std::deque& splitterQueue) { std::list predecessorBlocks; // Iterate over all states of the splitter and check its predecessors. storm::storage::sparse::state_type currentPosition = splitter.getBegin(); for (auto stateIterator = partition.getBeginOfStates(splitter), stateIte = partition.getEndOfStates(splitter); stateIterator != stateIte; ++stateIterator, ++currentPosition) { - std::cout << "states -----" << std::endl; - for (auto stateIterator = partition.getStates().begin() + splitter.getOriginalBegin(), stateIte = partition.getStates().begin() + splitter.getEnd(); stateIterator != stateIte; ++stateIterator) { - std::cout << *stateIterator << " "; - } - std::cout << std::endl; - storm::storage::sparse::state_type currentState = *stateIterator; - std::cout << "current state " << currentState << " at pos " << currentPosition << std::endl; uint_fast64_t elementsToSkip = 0; for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); - std::cout << "found predecessor " << predecessor << " of state " << currentState << std::endl; Block& predecessorBlock = partition.getBlock(predecessor); - std::cout << "predecessor block " << predecessorBlock.getId() << std::endl; // If the predecessor block has just one state, there is no point in splitting it. if (predecessorBlock.getNumberOfStates() <= 1) { @@ -625,11 +638,10 @@ namespace storm { // If the predecessor we just found was already processed (in terms of visiting its predecessors), // we swap it with the state that is currently at the beginning of the block and move the start // of the block one step further. - if (predecessorPosition <= currentPosition) { + if (predecessorPosition <= currentPosition + elementsToSkip) { partition.swapStates(predecessor, partition.getState(predecessorBlock.getBegin())); predecessorBlock.incrementBegin(); } else { - std::cout << "current position is " << currentPosition << std::endl; // Otherwise, we need to move the predecessor, but we need to make sure that we explore its // predecessors later. if (predecessorBlock.getMarkedPosition() == predecessorBlock.getBegin()) { @@ -656,24 +668,18 @@ 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; } } // If we had to move some elements beyond the current element, we may have to skip them. if (elementsToSkip > 0) { - std::cout << "skipping " << elementsToSkip << " elements" << std::endl; stateIterator += elementsToSkip; currentPosition += elementsToSkip; } } - 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; @@ -698,12 +704,11 @@ namespace storm { } } + // Reset the marked position of the splitter to the begin. splitter.setMarkedPosition(splitter.getBegin()); std::list blocksToSplit; - 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. for (auto blockPtr : predecessorBlocks) { @@ -714,30 +719,24 @@ namespace storm { // If we have moved the begin of the block to somewhere in the middle of the block, we need to split it. if (block.getBegin() != block.getEnd()) { - 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 " << newBlock.getId() << " from block " << block.getId() << std::endl; - newBlock.print(partition); if (!newBlock.isMarkedAsSplitter()) { splitterQueue.push_back(&newBlock); newBlock.markAsSplitter(); } - } else { - std::cout << "all states are predecessors" << std::endl; + // Schedule the block of predecessors for refinement based on probabilities. + blocksToSplit.emplace_back(&newBlock); + } else { // In this case, we can keep the block by setting its begin to the old value. block.setBegin(block.getOriginalBegin()); blocksToSplit.emplace_back(&block); } } - assert(partition.check()); - // Finally, we walk through the blocks that have a transition to the splitter and split them using // probabilistic information. for (auto blockPtr : blocksToSplit) { - std::cout << "block to split: " << blockPtr->getId() << std::endl; if (blockPtr->getNumberOfStates() <= 1) { continue; } @@ -748,6 +747,6 @@ namespace storm { return 0; } - template class BisimulationDecomposition2; + template class DeterministicModelBisimulationDecomposition; } } \ No newline at end of file diff --git a/src/storage/BisimulationDecomposition2.h b/src/storage/DeterministicModelBisimulationDecomposition.h similarity index 92% rename from src/storage/BisimulationDecomposition2.h rename to src/storage/DeterministicModelBisimulationDecomposition.h index 50153d4b5..a595d7c28 100644 --- a/src/storage/BisimulationDecomposition2.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -1,5 +1,5 @@ -#ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION2_H_ -#define STORM_STORAGE_BISIMULATIONDECOMPOSITION2_H_ +#ifndef STORM_STORAGE_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ +#define STORM_STORAGE_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ #include #include @@ -16,14 +16,19 @@ namespace storm { * This class represents the decomposition model into its bisimulation quotient. */ template - class BisimulationDecomposition2 : public Decomposition { + class DeterministicModelBisimulationDecomposition : public Decomposition { public: - BisimulationDecomposition2() = default; - /*! * Decomposes the given DTMC into equivalence classes under weak or strong bisimulation. */ - BisimulationDecomposition2(storm::models::Dtmc const& model, bool weak = false); + DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, bool weak = false); + + /*! + * Retrieves the quotient of the model under the previously computed bisimulation. + * + * @return The quotient model. + */ + std::shared_ptr> getQuotient() const; private: class Partition; @@ -277,8 +282,14 @@ namespace storm { std::size_t splitPartition(storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, std::deque& splitterQueue); std::size_t splitBlockProbabilities(Block& block, Partition& partition, std::deque& splitterQueue); + + // The model for which the bisimulation is computed. + storm::models::Dtmc const& model; + + // The indices of all blocks that hold one or more initial states. + std::vector initialBlocks; }; } } -#endif /* STORM_STORAGE_BISIMULATIONDECOMPOSITION2_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file diff --git a/src/storage/BisimulationDecomposition.cpp b/src/storage/NaiveDeterministicModelBisimulationDecomposition.cpp similarity index 84% rename from src/storage/BisimulationDecomposition.cpp rename to src/storage/NaiveDeterministicModelBisimulationDecomposition.cpp index 0d7abc44a..bf41414de 100644 --- a/src/storage/BisimulationDecomposition.cpp +++ b/src/storage/NaiveDeterministicModelBisimulationDecomposition.cpp @@ -1,4 +1,4 @@ -#include "src/storage/BisimulationDecomposition.h" +#include "src/storage/NaiveDeterministicModelBisimulationDecomposition.h" #include #include @@ -7,22 +7,26 @@ namespace storm { namespace storage { template - BisimulationDecomposition::BisimulationDecomposition(storm::models::Dtmc const& dtmc, bool weak) { + NaiveDeterministicModelBisimulationDecomposition::NaiveDeterministicModelBisimulationDecomposition(storm::models::Dtmc const& dtmc, bool weak) { computeBisimulationEquivalenceClasses(dtmc, weak); } template - void BisimulationDecomposition::computeBisimulationEquivalenceClasses(storm::models::Dtmc const& dtmc, bool weak) { + void NaiveDeterministicModelBisimulationDecomposition::computeBisimulationEquivalenceClasses(storm::models::Dtmc const& dtmc, bool weak) { 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 stateToBlockMapping(dtmc.getNumberOfStates()); - storm::storage::BitVector labeledStates = dtmc.getLabeledStates("elected"); + storm::storage::BitVector labeledStates = dtmc.getLabeledStates("observe0Greater1"); 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(); this->blocks.emplace_back(labeledStates.begin(), labeledStates.end()); std::for_each(labeledStates.begin(), labeledStates.end(), [&] (storm::storage::sparse::state_type const& state) { stateToBlockMapping[state] = 1; } ); + // Check whether any of the blocks is empty and remove it. + auto eraseIterator = std::remove_if(this->blocks.begin(), this->blocks.end(), [] (typename NaiveDeterministicModelBisimulationDecomposition::block_type const& a) { return a.empty(); }); + this->blocks.erase(eraseIterator, this->blocks.end()); + // Create empty distributions for the two initial blocks. std::vector> distributions(2); @@ -33,8 +37,9 @@ namespace storm { // is the ID of the parent block of the splitter and the second entry is the block ID of the splitter itself. std::deque refinementQueue; storm::storage::BitVector blocksInRefinementQueue(this->size()); - refinementQueue.push_back(0); - refinementQueue.push_back(1); + for (uint_fast64_t index = 0; index < this->blocks.size(); ++index) { + refinementQueue.push_back(index); + } // As long as there are blocks to refine, well, refine them. uint_fast64_t iteration = 0; @@ -50,24 +55,22 @@ namespace storm { splitBlock(dtmc, backwardTransitions, currentBlock, stateToBlockMapping, distributions, blocksInRefinementQueue, refinementQueue, weak); } - - std::cout << *this << std::endl; - + std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart; std::cout << "Bisimulation quotient has " << this->blocks.size() << " blocks and took " << iteration << " iterations and " << std::chrono::duration_cast(totalTime).count() << "ms." << std::endl; } 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, storm::storage::BitVector& splitBlocks) { - std::cout << "entering " << std::endl; + std::size_t NaiveDeterministicModelBisimulationDecomposition::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; + 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(); @@ -95,8 +98,8 @@ namespace storm { // 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; + typename NaiveDeterministicModelBisimulationDecomposition::block_type smallerBlock; + typename NaiveDeterministicModelBisimulationDecomposition::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())); @@ -143,9 +146,9 @@ namespace storm { } 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, bool weakBisimulation) { + std::size_t NaiveDeterministicModelBisimulationDecomposition::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; + std::unordered_map, typename NaiveDeterministicModelBisimulationDecomposition::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(); @@ -180,10 +183,12 @@ namespace storm { // distributions[blockId] = std::move(distributionToNewBlocks.begin()->first); } else { // In this case, we need to split the block. - typename BisimulationDecomposition::block_type tmpBlock; + typename NaiveDeterministicModelBisimulationDecomposition::block_type tmpBlock; auto distributionIterator = distributionToNewBlocks.begin(); - distributions[blockId] = std::move(distributionIterator->first); + STORM_LOG_ASSERT(distributionIterator != distributionToNewBlocks.end(), "One block has no distribution..."); + + // distributions[blockId] = std::move(distributionIterator->first); tmpBlock = std::move(distributionIterator->second); std::swap(this->blocks[blockId], tmpBlock); ++distributionIterator; @@ -252,6 +257,6 @@ namespace storm { return distributionToNewBlocks.size(); } - template class BisimulationDecomposition; + template class NaiveDeterministicModelBisimulationDecomposition; } } \ No newline at end of file diff --git a/src/storage/BisimulationDecomposition.h b/src/storage/NaiveDeterministicModelBisimulationDecomposition.h similarity index 74% rename from src/storage/BisimulationDecomposition.h rename to src/storage/NaiveDeterministicModelBisimulationDecomposition.h index 55ed556d8..300922cf5 100644 --- a/src/storage/BisimulationDecomposition.h +++ b/src/storage/NaiveDeterministicModelBisimulationDecomposition.h @@ -1,5 +1,5 @@ -#ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ -#define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ +#ifndef STORM_STORAGE_NAIVEDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ +#define STORM_STORAGE_NAIVEDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ #include #include @@ -15,14 +15,14 @@ namespace storm { * This class represents the decomposition model into its bisimulation quotient. */ template - class BisimulationDecomposition : public Decomposition { + class NaiveDeterministicModelBisimulationDecomposition : public Decomposition { public: - BisimulationDecomposition() = default; + NaiveDeterministicModelBisimulationDecomposition() = default; /*! * Decomposes the given DTMC into equivalence classes under weak or strong bisimulation. */ - BisimulationDecomposition(storm::models::Dtmc const& model, bool weak = false); + NaiveDeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, bool weak = false); private: void computeBisimulationEquivalenceClasses(storm::models::Dtmc const& model, bool weak); @@ -32,4 +32,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_NAIVEDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file diff --git a/src/utility/cli.h b/src/utility/cli.h index 6996736a4..ed63f5086 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -44,8 +44,8 @@ log4cplus::Logger logger; #include "src/adapters/ExplicitModelAdapter.h" // Headers for model processing. -#include "src/storage/BisimulationDecomposition.h" -#include "src/storage/BisimulationDecomposition2.h" +#include "src/storage/NaiveDeterministicModelBisimulationDecomposition.h" +#include "src/storage/DeterministicModelBisimulationDecomposition.h" // Headers for counterexample generation. #include "src/counterexamples/MILPMinimalLabelSetGenerator.h" @@ -261,8 +261,8 @@ 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> dtmc = result->template as>(); - storm::storage::BisimulationDecomposition bisimulationDecomposition(*dtmc); - storm::storage::BisimulationDecomposition2 bisimulationDecomposition2(*dtmc); + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc); + return bisimulationDecomposition.getQuotient(); } return result;