From e6904dcb213daa04ed839d5b59ebb213f990186c Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 25 Oct 2014 18:09:50 +0200 Subject: [PATCH] Renamed bisimulation decomposition class to reflect that now also weak bisimulations can be computed. Former-commit-id: 1a654b7110d16c670900ee1f4abaedd6979ac55b --- ...inisticModelBisimulationDecomposition.cpp} | 355 ++++++++++-------- ...rministicModelBisimulationDecomposition.h} | 51 ++- src/utility/cli.h | 4 +- 3 files changed, 225 insertions(+), 185 deletions(-) rename src/storage/{DeterministicModelStrongBisimulationDecomposition.cpp => DeterministicModelBisimulationDecomposition.cpp} (74%) rename src/storage/{DeterministicModelStrongBisimulationDecomposition.h => DeterministicModelBisimulationDecomposition.h} (89%) diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp similarity index 74% rename from src/storage/DeterministicModelStrongBisimulationDecomposition.cpp rename to src/storage/DeterministicModelBisimulationDecomposition.cpp index 4cc536c1b..2f46baa55 100644 --- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -1,4 +1,4 @@ -#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h" +#include "src/storage/DeterministicModelBisimulationDecomposition.h" #include #include @@ -13,10 +13,10 @@ namespace storm { namespace storage { template - std::size_t DeterministicModelStrongBisimulationDecomposition::Block::blockId = 0; + std::size_t DeterministicModelBisimulationDecomposition::Block::blockId = 0; template - DeterministicModelStrongBisimulationDecomposition::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr const& label) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(blockId++), label(label) { + DeterministicModelBisimulationDecomposition::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr const& label) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(blockId++), label(label) { if (next != nullptr) { next->prev = this; } @@ -27,7 +27,7 @@ namespace storm { } template - void DeterministicModelStrongBisimulationDecomposition::Block::print(Partition const& partition) const { + 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; @@ -52,31 +52,31 @@ namespace storm { } template - void DeterministicModelStrongBisimulationDecomposition::Block::setBegin(storm::storage::sparse::state_type begin) { + void DeterministicModelBisimulationDecomposition::Block::setBegin(storm::storage::sparse::state_type begin) { this->begin = begin; this->markedPosition = begin; STORM_LOG_ASSERT(begin < end, "Unable to resize block to illegal size."); } template - void DeterministicModelStrongBisimulationDecomposition::Block::setEnd(storm::storage::sparse::state_type end) { + void DeterministicModelBisimulationDecomposition::Block::setEnd(storm::storage::sparse::state_type end) { this->end = end; STORM_LOG_ASSERT(begin < end, "Unable to resize block to illegal size."); } template - void DeterministicModelStrongBisimulationDecomposition::Block::incrementBegin() { + void DeterministicModelBisimulationDecomposition::Block::incrementBegin() { ++this->begin; STORM_LOG_ASSERT(begin <= end, "Unable to resize block to illegal size."); } template - storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition::Block::getBegin() const { + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getBegin() const { return this->begin; } template - storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition::Block::getOriginalBegin() const { + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getOriginalBegin() const { if (this->hasPreviousBlock()) { return this->getPreviousBlock().getEnd(); } else { @@ -85,72 +85,72 @@ namespace storm { } template - storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition::Block::getEnd() const { + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getEnd() const { return this->end; } template - void DeterministicModelStrongBisimulationDecomposition::Block::setIterator(iterator it) { + void DeterministicModelBisimulationDecomposition::Block::setIterator(iterator it) { this->selfIt = it; } template - typename DeterministicModelStrongBisimulationDecomposition::Block::iterator DeterministicModelStrongBisimulationDecomposition::Block::getIterator() const { + typename DeterministicModelBisimulationDecomposition::Block::iterator DeterministicModelBisimulationDecomposition::Block::getIterator() const { return this->selfIt; } template - typename DeterministicModelStrongBisimulationDecomposition::Block::iterator DeterministicModelStrongBisimulationDecomposition::Block::getNextIterator() const { + typename DeterministicModelBisimulationDecomposition::Block::iterator DeterministicModelBisimulationDecomposition::Block::getNextIterator() const { return this->getNextBlock().getIterator(); } template - typename DeterministicModelStrongBisimulationDecomposition::Block::iterator DeterministicModelStrongBisimulationDecomposition::Block::getPreviousIterator() const { + typename DeterministicModelBisimulationDecomposition::Block::iterator DeterministicModelBisimulationDecomposition::Block::getPreviousIterator() const { return this->getPreviousBlock().getIterator(); } template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Block::getNextBlock() { + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Block::getNextBlock() { return *this->next; } template - typename DeterministicModelStrongBisimulationDecomposition::Block const& DeterministicModelStrongBisimulationDecomposition::Block::getNextBlock() const { + typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Block::getNextBlock() const { return *this->next; } template - bool DeterministicModelStrongBisimulationDecomposition::Block::hasNextBlock() const { + bool DeterministicModelBisimulationDecomposition::Block::hasNextBlock() const { return this->next != nullptr; } template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Block::getPreviousBlock() { + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Block::getPreviousBlock() { return *this->prev; } template - typename DeterministicModelStrongBisimulationDecomposition::Block* DeterministicModelStrongBisimulationDecomposition::Block::getPreviousBlockPointer() { + typename DeterministicModelBisimulationDecomposition::Block* DeterministicModelBisimulationDecomposition::Block::getPreviousBlockPointer() { return this->prev; } template - typename DeterministicModelStrongBisimulationDecomposition::Block* DeterministicModelStrongBisimulationDecomposition::Block::getNextBlockPointer() { + typename DeterministicModelBisimulationDecomposition::Block* DeterministicModelBisimulationDecomposition::Block::getNextBlockPointer() { return this->next; } template - typename DeterministicModelStrongBisimulationDecomposition::Block const& DeterministicModelStrongBisimulationDecomposition::Block::getPreviousBlock() const { + typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Block::getPreviousBlock() const { return *this->prev; } template - bool DeterministicModelStrongBisimulationDecomposition::Block::hasPreviousBlock() const { + bool DeterministicModelBisimulationDecomposition::Block::hasPreviousBlock() const { return this->prev != nullptr; } template - bool DeterministicModelStrongBisimulationDecomposition::Block::check() const { + bool DeterministicModelBisimulationDecomposition::Block::check() const { assert(this->begin < this->end); assert(this->prev == nullptr || this->prev->next == this); assert(this->next == nullptr || this->next->prev == this); @@ -158,94 +158,94 @@ namespace storm { } template - std::size_t DeterministicModelStrongBisimulationDecomposition::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 DeterministicModelStrongBisimulationDecomposition::Block::isMarkedAsSplitter() const { + bool DeterministicModelBisimulationDecomposition::Block::isMarkedAsSplitter() const { return this->markedAsSplitter; } template - void DeterministicModelStrongBisimulationDecomposition::Block::markAsSplitter() { + void DeterministicModelBisimulationDecomposition::Block::markAsSplitter() { this->markedAsSplitter = true; } template - void DeterministicModelStrongBisimulationDecomposition::Block::unmarkAsSplitter() { + void DeterministicModelBisimulationDecomposition::Block::unmarkAsSplitter() { this->markedAsSplitter = false; } template - std::size_t DeterministicModelStrongBisimulationDecomposition::Block::getId() const { + std::size_t DeterministicModelBisimulationDecomposition::Block::getId() const { return this->id; } template - void DeterministicModelStrongBisimulationDecomposition::Block::setAbsorbing(bool absorbing) { + void DeterministicModelBisimulationDecomposition::Block::setAbsorbing(bool absorbing) { this->absorbing = absorbing; } template - bool DeterministicModelStrongBisimulationDecomposition::Block::isAbsorbing() const { + bool DeterministicModelBisimulationDecomposition::Block::isAbsorbing() const { return this->absorbing; } template - storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition::Block::getMarkedPosition() const { + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getMarkedPosition() const { return this->markedPosition; } template - void DeterministicModelStrongBisimulationDecomposition::Block::setMarkedPosition(storm::storage::sparse::state_type position) { + void DeterministicModelBisimulationDecomposition::Block::setMarkedPosition(storm::storage::sparse::state_type position) { this->markedPosition = position; } template - void DeterministicModelStrongBisimulationDecomposition::Block::resetMarkedPosition() { + void DeterministicModelBisimulationDecomposition::Block::resetMarkedPosition() { this->markedPosition = this->begin; } template - void DeterministicModelStrongBisimulationDecomposition::Block::incrementMarkedPosition() { + void DeterministicModelBisimulationDecomposition::Block::incrementMarkedPosition() { ++this->markedPosition; } template - void DeterministicModelStrongBisimulationDecomposition::Block::markAsPredecessorBlock() { + void DeterministicModelBisimulationDecomposition::Block::markAsPredecessorBlock() { this->markedAsPredecessorBlock = true; } template - void DeterministicModelStrongBisimulationDecomposition::Block::unmarkAsPredecessorBlock() { + void DeterministicModelBisimulationDecomposition::Block::unmarkAsPredecessorBlock() { this->markedAsPredecessorBlock = false; } template - bool DeterministicModelStrongBisimulationDecomposition::Block::isMarkedAsPredecessor() const { + bool DeterministicModelBisimulationDecomposition::Block::isMarkedAsPredecessor() const { return markedAsPredecessorBlock; } template - bool DeterministicModelStrongBisimulationDecomposition::Block::hasLabel() const { + bool DeterministicModelBisimulationDecomposition::Block::hasLabel() const { return this->label != nullptr; } template - std::string const& DeterministicModelStrongBisimulationDecomposition::Block::getLabel() const { + std::string const& DeterministicModelBisimulationDecomposition::Block::getLabel() const { STORM_LOG_THROW(this->label != nullptr, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve label of block that has none."); return *this->label; } template - std::shared_ptr const& DeterministicModelStrongBisimulationDecomposition::Block::getLabelPtr() const { + std::shared_ptr const& DeterministicModelBisimulationDecomposition::Block::getLabelPtr() const { return this->label; } template - DeterministicModelStrongBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() { + DeterministicModelBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() { // 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); @@ -264,7 +264,7 @@ namespace storm { } template - DeterministicModelStrongBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() { + DeterministicModelBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() { typename std::list::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr); Block& firstBlock = *firstIt; firstBlock.setIterator(firstIt); @@ -309,13 +309,13 @@ namespace storm { } template - void DeterministicModelStrongBisimulationDecomposition::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { + void DeterministicModelBisimulationDecomposition::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { std::swap(this->statesAndValues[this->positions[state1]], this->statesAndValues[this->positions[state2]]); std::swap(this->positions[state1], this->positions[state2]); } template - void DeterministicModelStrongBisimulationDecomposition::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->statesAndValues[position1].first; storm::storage::sparse::state_type state2 = this->statesAndValues[position2].first; @@ -326,84 +326,84 @@ namespace storm { } template - storm::storage::sparse::state_type const& DeterministicModelStrongBisimulationDecomposition::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 DeterministicModelStrongBisimulationDecomposition::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& DeterministicModelStrongBisimulationDecomposition::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->statesAndValues[position].first; } template - ValueType const& DeterministicModelStrongBisimulationDecomposition::Partition::getValue(storm::storage::sparse::state_type state) const { + ValueType const& DeterministicModelBisimulationDecomposition::Partition::getValue(storm::storage::sparse::state_type state) const { return this->statesAndValues[this->positions[state]].second; } template - ValueType const& DeterministicModelStrongBisimulationDecomposition::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const { + ValueType const& DeterministicModelBisimulationDecomposition::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const { return this->statesAndValues[position].second; } template - void DeterministicModelStrongBisimulationDecomposition::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) { + void DeterministicModelBisimulationDecomposition::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) { this->statesAndValues[this->positions[state]].second = value; } template - void DeterministicModelStrongBisimulationDecomposition::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) { + void DeterministicModelBisimulationDecomposition::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) { this->statesAndValues[this->positions[state]].second += value; } template - void DeterministicModelStrongBisimulationDecomposition::Partition::updateBlockMapping(Block& block, typename std::vector>::iterator first, typename std::vector>::iterator last) { + void DeterministicModelBisimulationDecomposition::Partition::updateBlockMapping(Block& block, typename std::vector>::iterator first, typename std::vector>::iterator last) { for (; first != last; ++first) { this->stateToBlockMapping[first->first] = █ } } template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Partition::getFirstBlock() { + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Partition::getFirstBlock() { return *this->blocks.begin(); } template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::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 - typename DeterministicModelStrongBisimulationDecomposition::Block const& DeterministicModelStrongBisimulationDecomposition::Partition::getBlock(storm::storage::sparse::state_type state) const { + typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Partition::getBlock(storm::storage::sparse::state_type state) const { return *this->stateToBlockMapping[state]; } template - typename std::vector>::iterator DeterministicModelStrongBisimulationDecomposition::Partition::getBegin(Block const& block) { + typename std::vector>::iterator DeterministicModelBisimulationDecomposition::Partition::getBegin(Block const& block) { return this->statesAndValues.begin() + block.getBegin(); } template - typename std::vector>::iterator DeterministicModelStrongBisimulationDecomposition::Partition::getEnd(Block const& block) { + typename std::vector>::iterator DeterministicModelBisimulationDecomposition::Partition::getEnd(Block const& block) { return this->statesAndValues.begin() + block.getEnd(); } template - typename std::vector>::const_iterator DeterministicModelStrongBisimulationDecomposition::Partition::getBegin(Block const& block) const { + typename std::vector>::const_iterator DeterministicModelBisimulationDecomposition::Partition::getBegin(Block const& block) const { return this->statesAndValues.begin() + block.getBegin(); } template - typename std::vector>::const_iterator DeterministicModelStrongBisimulationDecomposition::Partition::getEnd(Block const& block) const { + typename std::vector>::const_iterator DeterministicModelBisimulationDecomposition::Partition::getEnd(Block const& block) const { return this->statesAndValues.begin() + block.getEnd(); } template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) { + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) { // 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()) { @@ -425,7 +425,7 @@ namespace storm { } template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::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()) { @@ -448,7 +448,7 @@ namespace storm { } template - void DeterministicModelStrongBisimulationDecomposition::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; @@ -476,25 +476,25 @@ namespace storm { } template - bool DeterministicModelStrongBisimulationDecomposition::Partition::isSilent(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator const& comparator) const { + bool DeterministicModelBisimulationDecomposition::Partition::isSilent(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator const& comparator) const { STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to retrieve silentness of state, because silent probabilities are not tracked."); return comparator.isOne(this->silentProbabilities[state]); } template - bool DeterministicModelStrongBisimulationDecomposition::Partition::hasSilentProbability(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator const& comparator) const { + bool DeterministicModelBisimulationDecomposition::Partition::hasSilentProbability(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator const& comparator) const { STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to retrieve silentness of state, because silent probabilities are not tracked."); return !comparator.isZero(this->silentProbabilities[state]); } template - ValueType const& DeterministicModelStrongBisimulationDecomposition::Partition::getSilentProbability(storm::storage::sparse::state_type state) const { + ValueType const& DeterministicModelBisimulationDecomposition::Partition::getSilentProbability(storm::storage::sparse::state_type state) const { STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to retrieve silent probability of state, because silent probabilities are not tracked."); return this->silentProbabilities[state]; } template - void DeterministicModelStrongBisimulationDecomposition::Partition::setSilentProbabilities(typename std::vector>::iterator first, typename std::vector>::iterator last) { + void DeterministicModelBisimulationDecomposition::Partition::setSilentProbabilities(typename std::vector>::iterator first, typename std::vector>::iterator last) { STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to set silent probability of state, because silent probabilities are not tracked."); for (; first != last; ++first) { this->silentProbabilities[first->first] = first->second; @@ -502,7 +502,7 @@ namespace storm { } template - void DeterministicModelStrongBisimulationDecomposition::Partition::setSilentProbabilitiesToZero(typename std::vector>::iterator first, typename std::vector>::iterator last) { + void DeterministicModelBisimulationDecomposition::Partition::setSilentProbabilitiesToZero(typename std::vector>::iterator first, typename std::vector>::iterator last) { STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to set silent probability of state, because silent probabilities are not tracked."); for (; first != last; ++first) { this->silentProbabilities[first->first] = storm::utility::zero(); @@ -510,28 +510,28 @@ namespace storm { } template - void DeterministicModelStrongBisimulationDecomposition::Partition::setSilentProbability(storm::storage::sparse::state_type state, ValueType const& value) { + void DeterministicModelBisimulationDecomposition::Partition::setSilentProbability(storm::storage::sparse::state_type state, ValueType const& value) { STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to set silent probability of state, because silent probabilities are not tracked."); this->silentProbabilities[state] = value; } template - std::list::Block> const& DeterministicModelStrongBisimulationDecomposition::Partition::getBlocks() const { + std::list::Block> const& DeterministicModelBisimulationDecomposition::Partition::getBlocks() const { return this->blocks; } template - std::vector>& DeterministicModelStrongBisimulationDecomposition::Partition::getStatesAndValues() { + std::vector>& DeterministicModelBisimulationDecomposition::Partition::getStatesAndValues() { return this->statesAndValues; } template - std::list::Block>& DeterministicModelStrongBisimulationDecomposition::Partition::getBlocks() { + std::list::Block>& DeterministicModelBisimulationDecomposition::Partition::getBlocks() { return this->blocks; } template - bool DeterministicModelStrongBisimulationDecomposition::Partition::check() const { + bool DeterministicModelBisimulationDecomposition::Partition::check() const { for (uint_fast64_t state = 0; state < this->positions.size(); ++state) { if (this->statesAndValues[this->positions[state]].first != state) { assert(false); @@ -549,7 +549,7 @@ namespace storm { } template - void DeterministicModelStrongBisimulationDecomposition::Partition::print() const { + void DeterministicModelBisimulationDecomposition::Partition::print() const { for (auto const& block : this->blocks) { block.print(*this); } @@ -571,51 +571,53 @@ namespace storm { } template - std::size_t DeterministicModelStrongBisimulationDecomposition::Partition::size() const { + std::size_t DeterministicModelBisimulationDecomposition::Partition::size() const { return this->blocks.size(); } template - DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, bool weak, bool buildQuotient) : comparator(0) { + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, bool weak, bool buildQuotient) : comparator() { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, weak); - partitionRefinement(model, backwardTransitions, initialPartition, weak, buildQuotient); + partitionRefinement(model, backwardTransitions, initialPartition, weak ? BisimulationType::WeakDtmc : BisimulationType::Strong, buildQuotient); } template - DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc const& model, bool weak, bool buildQuotient) { + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, bool weak, bool buildQuotient) { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, weak); - partitionRefinement(model, backwardTransitions, initialPartition, weak, buildQuotient); + partitionRefinement(model, backwardTransitions, initialPartition, weak ? BisimulationType::WeakCtmc : BisimulationType::Strong, buildQuotient); } template - DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient) { + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded, bool buildQuotient) { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); + STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bounded); - partitionRefinement(model, model.getBackwardTransitions(), initialPartition, false, buildQuotient); + Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, weak, bounded); + partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak ? BisimulationType::WeakDtmc : BisimulationType::Strong, buildQuotient); } template - DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient) { + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded, bool buildQuotient) { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); + STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bounded); - partitionRefinement(model, model.getBackwardTransitions(), initialPartition, false, buildQuotient); + Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, weak, bounded); + partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak ? BisimulationType::WeakCtmc : BisimulationType::Strong, buildQuotient); } template - std::shared_ptr> DeterministicModelStrongBisimulationDecomposition::getQuotient() const { + std::shared_ptr> DeterministicModelBisimulationDecomposition::getQuotient() const { STORM_LOG_THROW(this->quotient != nullptr, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve quotient model from bisimulation decomposition, because it was not built."); return this->quotient; } template template - void DeterministicModelStrongBisimulationDecomposition::buildQuotient(ModelType const& model, Partition const& partition, bool weak) { + void DeterministicModelBisimulationDecomposition::buildQuotient(ModelType const& model, Partition const& partition, BisimulationType bisimulationType) { // In order to create the quotient model, we need to construct // (a) the new transition matrix, // (b) the new labeling, @@ -641,7 +643,7 @@ namespace storm { storm::storage::sparse::state_type representativeState = *block.begin(); // However, for weak bisimulation, we need to make sure the representative state is a non-silent one. - if (weak) { + if (bisimulationType == BisimulationType::WeakDtmc) { for (auto const& state : block) { if (!partition.isSilent(state, comparator)) { representativeState = state; @@ -674,7 +676,7 @@ namespace storm { storm::storage::sparse::state_type targetBlock = partition.getBlock(entry.getColumn()).getId(); // If we are computing a weak bisimulation quotient, there is no need to add self-loops. - if (weak && targetBlock == blockIndex) { + if ((bisimulationType == BisimulationType::WeakDtmc || bisimulationType == BisimulationType::WeakCtmc) && targetBlock == blockIndex) { continue; } @@ -688,7 +690,7 @@ namespace storm { // Now add them to the actual matrix. for (auto const& probabilityEntry : blockProbability) { - if (weak) { + if (bisimulationType == BisimulationType::WeakDtmc) { builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second / (storm::utility::one() - partition.getSilentProbability(representativeState))); } else { builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second); @@ -725,7 +727,7 @@ namespace storm { template template - void DeterministicModelStrongBisimulationDecomposition::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, bool weak, bool buildQuotient) { + void DeterministicModelBisimulationDecomposition::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient) { std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); // Initially, all blocks are potential splitter, so we insert them in the splitterQueue. @@ -744,7 +746,7 @@ namespace storm { splitter->unmarkAsSplitter(); // Now refine the partition using the current splitter. - refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitter, partition, weak, splitterQueue); + refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitter, partition, bisimulationType, splitterQueue); } std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart; @@ -763,7 +765,7 @@ namespace storm { // If we are required to build the quotient model, do so now. if (buildQuotient) { - this->buildQuotient(model, partition, weak); + this->buildQuotient(model, partition, bisimulationType); } std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart; @@ -781,7 +783,7 @@ namespace storm { } template - void DeterministicModelStrongBisimulationDecomposition::refineBlockProbabilities(Block& block, Partition& partition, std::deque& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue) { // Sort the states in the block based on their probabilities. std::sort(partition.getBegin(block), partition.getEnd(block), [&partition] (std::pair const& a, std::pair const& b) { return a.second < b.second; } ); @@ -831,7 +833,7 @@ namespace storm { } template - void DeterministicModelStrongBisimulationDecomposition::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue) { std::vector splitPoints = getSplitPointsWeak(block, partition); // Restore the original begin of the block. @@ -952,7 +954,7 @@ namespace storm { } template - std::vector DeterministicModelStrongBisimulationDecomposition::getSplitPointsWeak(Block& block, Partition& partition) { + std::vector DeterministicModelBisimulationDecomposition::getSplitPointsWeak(Block& block, Partition& partition) { std::vector result; // We first scale all probabilities with (1-p[s]) where p[s] is the silent probability of state s. std::for_each(partition.getStatesAndValues().begin() + block.getOriginalBegin(), partition.getStatesAndValues().begin() + block.getBegin(), [&] (std::pair& stateValuePair) { @@ -1003,7 +1005,7 @@ namespace storm { } template - void DeterministicModelStrongBisimulationDecomposition::refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue) { std::list predecessorBlocks; // Iterate over all states of the splitter and check its predecessors. @@ -1101,7 +1103,7 @@ namespace storm { } } - if (!weak) { + if (bisimulationType == BisimulationType::Strong || bisimulationType == BisimulationType::WeakCtmc) { std::list blocksToSplit; // Now, we can iterate over the predecessor blocks and see whether we have to create a new block for @@ -1136,9 +1138,15 @@ namespace storm { continue; } - refineBlockProbabilities(*blockPtr, partition, splitterQueue); + // In the case of weak bisimulation for CTMCs, we don't need to make sure the rate of staying inside + // the own block is the same. + if (bisimulationType == BisimulationType::WeakCtmc && blockPtr == &splitter) { + continue; + } + + refineBlockProbabilities(*blockPtr, partition, bisimulationType, splitterQueue); } - } else { + } else { // In this case, we are computing a weak bisimulation on a DTMC. // If the splitter was a predecessor of itself and we are computing a weak bisimulation, we need to update // the silent probabilities. if (splitterIsPredecessor) { @@ -1169,90 +1177,103 @@ namespace storm { template template - typename DeterministicModelStrongBisimulationDecomposition::Partition DeterministicModelStrongBisimulationDecomposition::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool bounded) { + typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded) { std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiLabel == "true" ? storm::storage::BitVector(model.getNumberOfStates(), true) : model.getLabeledStates(phiLabel), model.getLabeledStates(psiLabel)); Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded ? model.getLabeledStates(psiLabel) : statesWithProbability01.second, phiLabel, psiLabel); + + // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent + // states of each initial block and (b) initialize the vector of silent probabilities held by the partition. + if (weak) { + this->splitOffDivergentStates(model, backwardTransitions, partition); + this->initializeSilentProbabilities(model, partition); + } + return partition; } template template - typename DeterministicModelStrongBisimulationDecomposition::Partition DeterministicModelStrongBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, bool weak) { - Partition partition(model.getNumberOfStates(), weak); - for (auto const& label : model.getStateLabeling().getAtomicPropositions()) { - if (label == "init") { - continue; - } - partition.splitLabel(model.getLabeledStates(label)); - } - - // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent - // states of each initial block and (b) initialize the vector of silent probabilities held by the partition. - if (weak) { - std::vector stateStack; - stateStack.reserve(model.getNumberOfStates()); - storm::storage::BitVector nondivergentStates(model.getNumberOfStates()); - for (auto& block : partition.getBlocks()) { - nondivergentStates.clear(); + void DeterministicModelBisimulationDecomposition::splitOffDivergentStates(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition) { + std::vector stateStack; + stateStack.reserve(model.getNumberOfStates()); + storm::storage::BitVector nondivergentStates(model.getNumberOfStates()); + for (auto& block : partition.getBlocks()) { + nondivergentStates.clear(); + + for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt) { + if (nondivergentStates.get(stateIt->first)) { + continue; + } - for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt) { - if (nondivergentStates.get(stateIt->first)) { - continue; - } - - // Now traverse the forward transitions of the current state and check whether there is a - // transition to some other block. - bool isDirectlyNonDivergent = false; - for (auto const& successor : model.getRows(stateIt->first)) { - // If there is such a transition, then we can mark all states in the current block that can - // reach the state as non-divergent. - if (&partition.getBlock(successor.getColumn()) != &block) { - isDirectlyNonDivergent = true; - break; - } + // Now traverse the forward transitions of the current state and check whether there is a + // transition to some other block. + bool isDirectlyNonDivergent = false; + for (auto const& successor : model.getRows(stateIt->first)) { + // If there is such a transition, then we can mark all states in the current block that can + // reach the state as non-divergent. + if (&partition.getBlock(successor.getColumn()) != &block) { + isDirectlyNonDivergent = true; + break; } + } + + if (isDirectlyNonDivergent) { + stateStack.push_back(stateIt->first); - if (isDirectlyNonDivergent) { - stateStack.push_back(stateIt->first); + while (!stateStack.empty()) { + storm::storage::sparse::state_type currentState = stateStack.back(); + stateStack.pop_back(); + nondivergentStates.set(currentState); - while (!stateStack.empty()) { - storm::storage::sparse::state_type currentState = stateStack.back(); - stateStack.pop_back(); - nondivergentStates.set(currentState); - - for (auto const& predecessor : backwardTransitions.getRow(currentState)) { - if (&partition.getBlock(predecessor.getColumn()) == &block && !nondivergentStates.get(predecessor.getColumn())) { - stateStack.push_back(predecessor.getColumn()); - } + for (auto const& predecessor : backwardTransitions.getRow(currentState)) { + if (&partition.getBlock(predecessor.getColumn()) == &block && !nondivergentStates.get(predecessor.getColumn())) { + stateStack.push_back(predecessor.getColumn()); } } } } + } + + + if (nondivergentStates.getNumberOfSetBits() > 0 && nondivergentStates.getNumberOfSetBits() != block.getNumberOfStates()) { + // Now that we have determined all (non)divergent states in the current block, we need to split them + // off. + std::sort(partition.getBegin(block), partition.getEnd(block), [&nondivergentStates] (std::pair const& a, std::pair const& b) { return nondivergentStates.get(a.first) && !nondivergentStates.get(b.first); } ); + // Update the positions vector. + storm::storage::sparse::state_type position = block.getBegin(); + for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) { + partition.setPosition(stateIt->first, position); + } + // Finally, split the block. + Block& nondivergentBlock = partition.splitBlock(block, block.getBegin() + nondivergentStates.getNumberOfSetBits()); - if (nondivergentStates.getNumberOfSetBits() > 0 && nondivergentStates.getNumberOfSetBits() != block.getNumberOfStates()) { - // Now that we have determined all (non)divergent states in the current block, we need to split them - // off. - std::sort(partition.getBegin(block), partition.getEnd(block), [&nondivergentStates] (std::pair const& a, std::pair const& b) { return nondivergentStates.get(a.first) && !nondivergentStates.get(b.first); } ); - // Update the positions vector. - storm::storage::sparse::state_type position = block.getBegin(); - for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) { - partition.setPosition(stateIt->first, position); - } - - // Finally, split the block. - Block& nondivergentBlock = partition.splitBlock(block, block.getBegin() + nondivergentStates.getNumberOfSetBits()); - - // Since the remaining states in the block are divergent, we can mark the block as absorbing. - // This also guarantees that the self-loop will be added to the state of the quotient - // representing this block of states. - block.setAbsorbing(true); - } else if (nondivergentStates.getNumberOfSetBits() == 0) { - // If there are only diverging states in the block, we need to make it absorbing. - block.setAbsorbing(true); - } + // Since the remaining states in the block are divergent, we can mark the block as absorbing. + // This also guarantees that the self-loop will be added to the state of the quotient + // representing this block of states. + block.setAbsorbing(true); + } else if (nondivergentStates.getNumberOfSetBits() == 0) { + // If there are only diverging states in the block, we need to make it absorbing. + block.setAbsorbing(true); } - + } + } + + template + template + typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, bool weak) { + Partition partition(model.getNumberOfStates(), weak); + for (auto const& label : model.getStateLabeling().getAtomicPropositions()) { + if (label == "init") { + continue; + } + partition.splitLabel(model.getLabeledStates(label)); + } + + // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent + // states of each initial block and (b) initialize the vector of silent probabilities held by the partition. + if (weak) { + this->splitOffDivergentStates(model, backwardTransitions, partition); this->initializeSilentProbabilities(model, partition); } return partition; @@ -1260,7 +1281,7 @@ namespace storm { template template - void DeterministicModelStrongBisimulationDecomposition::initializeSilentProbabilities(ModelType const& model, Partition& partition) { + void DeterministicModelBisimulationDecomposition::initializeSilentProbabilities(ModelType const& model, Partition& partition) { for (auto const& block : partition.getBlocks()) { for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt) { ValueType silentProbability = storm::utility::zero(); @@ -1276,6 +1297,6 @@ namespace storm { } } - template class DeterministicModelStrongBisimulationDecomposition; + template class DeterministicModelBisimulationDecomposition; } } \ No newline at end of file diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h similarity index 89% rename from src/storage/DeterministicModelStrongBisimulationDecomposition.h rename to src/storage/DeterministicModelBisimulationDecomposition.h index 9719569d3..a14d5af1b 100644 --- a/src/storage/DeterministicModelStrongBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -1,5 +1,5 @@ -#ifndef STORM_STORAGE_DETERMINISTICMODELSTRONGBISIMULATIONDECOMPOSITION_H_ -#define STORM_STORAGE_DETERMINISTICMODELSTRONGBISIMULATIONDECOMPOSITION_H_ +#ifndef STORM_STORAGE_DeterministicModelBisimulationDecomposition_H_ +#define STORM_STORAGE_DeterministicModelBisimulationDecomposition_H_ #include #include @@ -19,23 +19,25 @@ namespace storm { * This class represents the decomposition model into its (strong) bisimulation quotient. */ template - class DeterministicModelStrongBisimulationDecomposition : public Decomposition { + class DeterministicModelBisimulationDecomposition : public Decomposition { public: /*! * Decomposes the given DTMC into equivalence classes under weak or strong bisimulation. * * @param model The model to decompose. + * @param weak A flag indication whether a weak bisimulation is to be computed. * @param buildQuotient Sets whether or not the quotient model is to be built. */ - DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, bool weak = false, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, bool weak = false, bool buildQuotient = false); /*! * Decomposes the given CTMC into equivalence classes under weak or strong bisimulation. * * @param model The model to decompose. + * @param weak A flag indication whether a weak bisimulation is to be computed. * @param buildQuotient Sets whether or not the quotient model is to be built. */ - DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc const& model, bool weak = false, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, bool weak = false, bool buildQuotient = false); /*! * Decomposes the given DTMC into equivalence classes under strong bisimulation in a way that onle safely @@ -44,10 +46,11 @@ namespace storm { * @param model The model to decompose. * @param phiLabel The label that all phi states carry in the model. * @param psiLabel The label that all psi states carry in the model. + * @param weak A flag indication whether a weak bisimulation is to be computed. * @param bounded If set to true, also bounded until formulas are preserved. * @param buildQuotient Sets whether or not the quotient model is to be built. */ - DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded, bool buildQuotient = false); /*! * Decomposes the given CTMC into equivalence classes under strong bisimulation in a way that onle safely @@ -56,10 +59,11 @@ namespace storm { * @param model The model to decompose. * @param phiLabel The label that all phi states carry in the model. * @param psiLabel The label that all psi states carry in the model. + * @param weak A flag indication whether a weak bisimulation is to be computed. * @param bounded If set to true, also bounded until formulas are preserved. * @param buildQuotient Sets whether or not the quotient model is to be built. */ - DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded, bool buildQuotient = false); /*! * Retrieves the quotient of the model under the previously computed bisimulation. @@ -69,6 +73,8 @@ namespace storm { std::shared_ptr> getQuotient() const; private: + enum class BisimulationType { Strong, WeakDtmc, WeakCtmc }; + class Partition; class Block { @@ -390,12 +396,12 @@ namespace storm { * @param model The model on whose state space to compute the coarses strong bisimulation relation. * @param backwardTransitions The backward transitions of the model. * @param The initial partition. - * @param weak A flag indicating whether a weak or a strong bisimulation is to be computed. + * @param bisimulationType The kind of bisimulation that is to be computed. * @param buildQuotient If set, the quotient model is built and may be retrieved using the getQuotient() * method. */ template - void partitionRefinement(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, bool weak, bool buildQuotient); + void partitionRefinement(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient); /*! * Refines the partition based on the provided splitter. After calling this method all blocks are stable @@ -406,21 +412,22 @@ namespace storm { * probabilities). * @param splitter The splitter to use. * @param partition The partition to split. - * @param weak A flag indicating whether a weak or a strong bisimulation is to be computed. + * @param bisimulationType The kind of bisimulation that is to be computed. * @param splitterQueue A queue into which all blocks that were split are inserted so they can be treated * as splitters in the future. */ - void refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque& splitterQueue); + void refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue); /*! * Refines the block based on their probability values (leading into the splitter). * * @param block The block to refine. * @param partition The partition that contains the block. + * @param bisimulationType The kind of bisimulation that is to be computed. * @param splitterQueue A queue into which all blocks that were split are inserted so they can be treated * as splitters in the future. */ - void refineBlockProbabilities(Block& block, Partition& partition, std::deque& splitterQueue); + void refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue); void refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue); @@ -440,10 +447,10 @@ namespace storm { * determining the transitions of each equivalence class. * @param partition The previously computed partition. This is used for quickly retrieving the block of a * state. - * @param weak A flag indicating whether the quotient is built for weak bisimulation. + * @param bisimulationType The kind of bisimulation that is to be computed. */ template - void buildQuotient(ModelType const& model, Partition const& partition, bool weak); + void buildQuotient(ModelType const& model, Partition const& partition, BisimulationType bisimulationType); /*! * Creates the measure-driven initial partition for reaching psi states from phi states. @@ -453,12 +460,13 @@ namespace storm { * @param backwardTransitions The backward transitions of the model. * @param phiLabel The label that all phi states carry in the model. * @param psiLabel The label that all psi states carry in the model. + * @param weak A flag indicating whether a weak bisimulation is to be computed. * @param bounded If set to true, the initial partition will be chosen in such a way that preserves bounded * reachability queries. * @return The resulting partition. */ template - Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool bounded = false); + Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded = false); /*! * Creates the initial partition based on all the labels in the given model. @@ -471,6 +479,17 @@ namespace storm { template Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, bool weak); + /*! + * Splits all blocks of the given partition into a block that contains all divergent states and another block + * containing the non-divergent states. + * + * @param model The model from which to look-up the probabilities. + * @param backwardTransitions The backward transitions of the model. + * @param partition The partition that holds the silent probabilities. + */ + template + void splitOffDivergentStates(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition); + /*! * Initializes the silent probabilities by traversing all blocks and adding the probability of going to * the very own equivalence class for each state. @@ -490,4 +509,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_DETERMINISTICMODELSTRONGBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_DeterministicModelBisimulationDecomposition_H_ */ \ No newline at end of file diff --git a/src/utility/cli.h b/src/utility/cli.h index 925f085d1..df8aa248a 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -47,7 +47,7 @@ log4cplus::Logger logger; // Headers for model processing. #include "src/storage/NaiveDeterministicModelBisimulationDecomposition.h" -#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h" +#include "src/storage/DeterministicModelBisimulationDecomposition.h" // Headers for model checking. #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" @@ -271,7 +271,7 @@ namespace storm { std::shared_ptr> dtmc = result->template as>(); STORM_PRINT(std::endl << "Performing bisimulation minimization..." << std::endl); - storm::storage::DeterministicModelStrongBisimulationDecomposition bisimulationDecomposition(*dtmc, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true); + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true); result = bisimulationDecomposition.getQuotient();