From 1c091d764095f1951ec13829bdef851fc6ea2576 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 14 Oct 2014 17:46:40 +0200 Subject: [PATCH] Renamed some classes to indicate that only strong bisimulation can be computed. Added option to start with an initial partition that preserves only certain formulas. Added ConstantsComparator concept that is to be used when constants have to be compared with other constants. Former-commit-id: feacadfa381d58e69a9f9d8f2f74358f90627b2f --- src/models/Ctmc.h | 10 +- ...cModelStrongBisimulationDecomposition.cpp} | 368 ++++++++++++------ ...ticModelStrongBisimulationDecomposition.h} | 179 ++++++++- src/utility/ConstantsComparator.h | 84 ++++ src/utility/cli.h | 6 +- src/utility/graph.h | 19 + 6 files changed, 523 insertions(+), 143 deletions(-) rename src/storage/{DeterministicModelBisimulationDecomposition.cpp => DeterministicModelStrongBisimulationDecomposition.cpp} (57%) rename src/storage/{DeterministicModelBisimulationDecomposition.h => DeterministicModelStrongBisimulationDecomposition.h} (56%) create mode 100644 src/utility/ConstantsComparator.h diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h index 229ccfe9e..b3c1f1ef1 100644 --- a/src/models/Ctmc.h +++ b/src/models/Ctmc.h @@ -36,8 +36,9 @@ public: * propositions to each state. */ Ctmc(storm::storage::SparseMatrix const& rateMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, - boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional> const& optionalStateRewardVector = boost::optional>(), + boost::optional> const& optionalTransitionRewardMatrix = boost::optional>(), + boost::optional>> const& optionalChoiceLabeling = boost::optional>>()) : AbstractDeterministicModel(rateMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { // Intentionally left empty. } @@ -51,8 +52,9 @@ public: * propositions to each state. */ Ctmc(storm::storage::SparseMatrix&& rateMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, - boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>>&& optionalChoiceLabeling) + boost::optional>&& optionalStateRewardVector = boost::optional>(), + boost::optional>&& optionalTransitionRewardMatrix = boost::optional>(), + boost::optional>>&& optionalChoiceLabeling = boost::optional>>()) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class : AbstractDeterministicModel(std::move(rateMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) { diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp similarity index 57% rename from src/storage/DeterministicModelBisimulationDecomposition.cpp rename to src/storage/DeterministicModelStrongBisimulationDecomposition.cpp index d9023d153..93433d19f 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp @@ -1,19 +1,21 @@ -#include "src/storage/DeterministicModelBisimulationDecomposition.h" +#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h" #include #include #include #include +#include "src/utility/graph.h" #include "src/exceptions/IllegalFunctionCallException.h" namespace storm { namespace storage { - static std::size_t globalId = 0; + template + std::size_t DeterministicModelStrongBisimulationDecomposition::Block::blockId = 0; template - 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++) { + 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) { if (next != nullptr) { next->prev = this; } @@ -23,7 +25,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::Block::print(Partition const& partition) const { + void DeterministicModelStrongBisimulationDecomposition::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; @@ -42,33 +44,33 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::Block::setBegin(storm::storage::sparse::state_type begin) { + void DeterministicModelStrongBisimulationDecomposition::Block::setBegin(storm::storage::sparse::state_type begin) { this->begin = begin; this->markedPosition = begin; } template - void DeterministicModelBisimulationDecomposition::Block::setEnd(storm::storage::sparse::state_type end) { + void DeterministicModelStrongBisimulationDecomposition::Block::setEnd(storm::storage::sparse::state_type end) { this->end = end; } template - void DeterministicModelBisimulationDecomposition::Block::incrementBegin() { + void DeterministicModelStrongBisimulationDecomposition::Block::incrementBegin() { ++this->begin; } template - void DeterministicModelBisimulationDecomposition::Block::decrementEnd() { + void DeterministicModelStrongBisimulationDecomposition::Block::decrementEnd() { ++this->begin; } template - storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getBegin() const { + storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition::Block::getBegin() const { return this->begin; } template - storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getOriginalBegin() const { + storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition::Block::getOriginalBegin() const { if (this->hasPreviousBlock()) { return this->getPreviousBlock().getEnd(); } else { @@ -77,72 +79,72 @@ namespace storm { } template - storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getEnd() const { + storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition::Block::getEnd() const { return this->end; } template - void DeterministicModelBisimulationDecomposition::Block::setIterator(const_iterator it) { + void DeterministicModelStrongBisimulationDecomposition::Block::setIterator(const_iterator it) { this->selfIt = it; } template - typename DeterministicModelBisimulationDecomposition::Block::const_iterator DeterministicModelBisimulationDecomposition::Block::getIterator() const { + typename DeterministicModelStrongBisimulationDecomposition::Block::const_iterator DeterministicModelStrongBisimulationDecomposition::Block::getIterator() const { return this->selfIt; } template - typename DeterministicModelBisimulationDecomposition::Block::const_iterator DeterministicModelBisimulationDecomposition::Block::getNextIterator() const { + typename DeterministicModelStrongBisimulationDecomposition::Block::const_iterator DeterministicModelStrongBisimulationDecomposition::Block::getNextIterator() const { return this->getNextBlock().getIterator(); } template - typename DeterministicModelBisimulationDecomposition::Block::const_iterator DeterministicModelBisimulationDecomposition::Block::getPreviousIterator() const { + typename DeterministicModelStrongBisimulationDecomposition::Block::const_iterator DeterministicModelStrongBisimulationDecomposition::Block::getPreviousIterator() const { return this->getPreviousBlock().getIterator(); } template - typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Block::getNextBlock() { + typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Block::getNextBlock() { return *this->next; } template - typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Block::getNextBlock() const { + typename DeterministicModelStrongBisimulationDecomposition::Block const& DeterministicModelStrongBisimulationDecomposition::Block::getNextBlock() const { return *this->next; } template - bool DeterministicModelBisimulationDecomposition::Block::hasNextBlock() const { + bool DeterministicModelStrongBisimulationDecomposition::Block::hasNextBlock() const { return this->next != nullptr; } template - typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Block::getPreviousBlock() { + typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Block::getPreviousBlock() { return *this->prev; } template - typename DeterministicModelBisimulationDecomposition::Block* DeterministicModelBisimulationDecomposition::Block::getPreviousBlockPointer() { + typename DeterministicModelStrongBisimulationDecomposition::Block* DeterministicModelStrongBisimulationDecomposition::Block::getPreviousBlockPointer() { return this->prev; } template - typename DeterministicModelBisimulationDecomposition::Block* DeterministicModelBisimulationDecomposition::Block::getNextBlockPointer() { + typename DeterministicModelStrongBisimulationDecomposition::Block* DeterministicModelStrongBisimulationDecomposition::Block::getNextBlockPointer() { return this->next; } template - typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Block::getPreviousBlock() const { + typename DeterministicModelStrongBisimulationDecomposition::Block const& DeterministicModelStrongBisimulationDecomposition::Block::getPreviousBlock() const { return *this->prev; } template - bool DeterministicModelBisimulationDecomposition::Block::hasPreviousBlock() const { + bool DeterministicModelStrongBisimulationDecomposition::Block::hasPreviousBlock() const { return this->prev != nullptr; } template - bool DeterministicModelBisimulationDecomposition::Block::check() const { + bool DeterministicModelStrongBisimulationDecomposition::Block::check() const { if (this->begin >= this->end) { assert(false); } @@ -156,68 +158,94 @@ namespace storm { } template - std::size_t DeterministicModelBisimulationDecomposition::Block::getNumberOfStates() const { + std::size_t DeterministicModelStrongBisimulationDecomposition::Block::getNumberOfStates() const { // We need to take the original begin here, because the begin is temporarily moved. return (this->end - this->getOriginalBegin()); } template - bool DeterministicModelBisimulationDecomposition::Block::isMarkedAsSplitter() const { + bool DeterministicModelStrongBisimulationDecomposition::Block::isMarkedAsSplitter() const { return this->markedAsSplitter; } template - void DeterministicModelBisimulationDecomposition::Block::markAsSplitter() { + void DeterministicModelStrongBisimulationDecomposition::Block::markAsSplitter() { this->markedAsSplitter = true; } template - void DeterministicModelBisimulationDecomposition::Block::unmarkAsSplitter() { + void DeterministicModelStrongBisimulationDecomposition::Block::unmarkAsSplitter() { this->markedAsSplitter = false; } template - std::size_t DeterministicModelBisimulationDecomposition::Block::getId() const { + std::size_t DeterministicModelStrongBisimulationDecomposition::Block::getId() const { return this->id; } template - storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getMarkedPosition() const { + void DeterministicModelStrongBisimulationDecomposition::Block::setAbsorbing(bool absorbing) { + this->absorbing = absorbing; + } + + template + bool DeterministicModelStrongBisimulationDecomposition::Block::isAbsorbing() const { + return this->absorbing; + } + + template + storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition::Block::getMarkedPosition() const { return this->markedPosition; } template - void DeterministicModelBisimulationDecomposition::Block::setMarkedPosition(storm::storage::sparse::state_type position) { + void DeterministicModelStrongBisimulationDecomposition::Block::setMarkedPosition(storm::storage::sparse::state_type position) { this->markedPosition = position; } template - void DeterministicModelBisimulationDecomposition::Block::resetMarkedPosition() { + void DeterministicModelStrongBisimulationDecomposition::Block::resetMarkedPosition() { this->markedPosition = this->begin; } template - void DeterministicModelBisimulationDecomposition::Block::incrementMarkedPosition() { + void DeterministicModelStrongBisimulationDecomposition::Block::incrementMarkedPosition() { ++this->markedPosition; } template - void DeterministicModelBisimulationDecomposition::Block::markAsPredecessorBlock() { + void DeterministicModelStrongBisimulationDecomposition::Block::markAsPredecessorBlock() { this->markedAsPredecessorBlock = true; } template - void DeterministicModelBisimulationDecomposition::Block::unmarkAsPredecessorBlock() { + void DeterministicModelStrongBisimulationDecomposition::Block::unmarkAsPredecessorBlock() { this->markedAsPredecessorBlock = false; } template - bool DeterministicModelBisimulationDecomposition::Block::isMarkedAsPredecessor() const { + bool DeterministicModelStrongBisimulationDecomposition::Block::isMarkedAsPredecessor() const { return markedAsPredecessorBlock; } template - DeterministicModelBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) { + bool DeterministicModelStrongBisimulationDecomposition::Block::hasLabel() const { + return this->label != nullptr; + } + + template + std::string const& DeterministicModelStrongBisimulationDecomposition::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 { + return this->label; + } + + template + DeterministicModelStrongBisimulationDecomposition::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,14 +259,54 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { + 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) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) { + typename std::list::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr); + Block& firstBlock = *firstIt; + firstBlock.setIterator(firstIt); + + storm::storage::sparse::state_type position = 0; + for (auto state : prob0States) { + states[position] = state; + positions[state] = position; + stateToBlockMapping[state] = &firstBlock; + ++position; + } + firstBlock.setAbsorbing(true); + + typename std::list::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, std::shared_ptr(new std::string(prob1Label))); + Block& secondBlock = *secondIt; + secondBlock.setIterator(secondIt); + + for (auto state : prob1States) { + states[position] = state; + positions[state] = position; + stateToBlockMapping[state] = &secondBlock; + ++position; + } + secondBlock.setAbsorbing(true); + + typename std::list::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, otherLabel == "true" ? std::shared_ptr(nullptr) : std::shared_ptr(new std::string(otherLabel))); + Block& thirdBlock = *thirdIt; + thirdBlock.setIterator(thirdIt); + + storm::storage::BitVector otherStates = ~(prob0States | prob1States); + for (auto state : otherStates) { + states[position] = state; + positions[state] = position; + stateToBlockMapping[state] = &thirdBlock; + ++position; + } + } + + template + void DeterministicModelStrongBisimulationDecomposition::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 DeterministicModelBisimulationDecomposition::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) { + void DeterministicModelStrongBisimulationDecomposition::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]; @@ -250,94 +318,99 @@ namespace storm { } template - storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition::Partition::getPosition(storm::storage::sparse::state_type state) const { + storm::storage::sparse::state_type const& DeterministicModelStrongBisimulationDecomposition::Partition::getPosition(storm::storage::sparse::state_type state) const { return this->positions[state]; } template - void DeterministicModelBisimulationDecomposition::Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) { + void DeterministicModelStrongBisimulationDecomposition::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& DeterministicModelBisimulationDecomposition::Partition::getState(storm::storage::sparse::state_type position) const { + storm::storage::sparse::state_type const& DeterministicModelStrongBisimulationDecomposition::Partition::getState(storm::storage::sparse::state_type position) const { return this->states[position]; } template - ValueType const& DeterministicModelBisimulationDecomposition::Partition::getValue(storm::storage::sparse::state_type state) const { + ValueType const& DeterministicModelStrongBisimulationDecomposition::Partition::getValue(storm::storage::sparse::state_type state) const { return this->values[this->positions[state]]; } template - ValueType const& DeterministicModelBisimulationDecomposition::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const { + ValueType const& DeterministicModelStrongBisimulationDecomposition::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const { return this->values[position]; } template - void DeterministicModelBisimulationDecomposition::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) { + void DeterministicModelStrongBisimulationDecomposition::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) { this->values[this->positions[state]] = value; } template - std::vector& DeterministicModelBisimulationDecomposition::Partition::getValues() { + std::vector& DeterministicModelStrongBisimulationDecomposition::Partition::getValues() { return this->values; } template - void DeterministicModelBisimulationDecomposition::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) { + void DeterministicModelStrongBisimulationDecomposition::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) { this->values[this->positions[state]] += value; } template - void DeterministicModelBisimulationDecomposition::Partition::updateBlockMapping(Block& block, std::vector::iterator first, std::vector::iterator last) { + void DeterministicModelStrongBisimulationDecomposition::Partition::updateBlockMapping(Block& block, std::vector::iterator first, std::vector::iterator last) { for (; first != last; ++first) { this->stateToBlockMapping[*first] = █ } } template - typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Partition::getBlock(storm::storage::sparse::state_type state) { + typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Partition::getFirstBlock() { + return *this->blocks.begin(); + } + + template + typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Partition::getBlock(storm::storage::sparse::state_type state) { return *this->stateToBlockMapping[state]; } template - typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Partition::getBlock(storm::storage::sparse::state_type state) const { + typename DeterministicModelStrongBisimulationDecomposition::Block const& DeterministicModelStrongBisimulationDecomposition::Partition::getBlock(storm::storage::sparse::state_type state) const { return *this->stateToBlockMapping[state]; } template - std::vector::iterator DeterministicModelBisimulationDecomposition::Partition::getBeginOfStates(Block const& block) { + std::vector::iterator DeterministicModelStrongBisimulationDecomposition::Partition::getBeginOfStates(Block const& block) { return this->states.begin() + block.getBegin(); } template - std::vector::iterator DeterministicModelBisimulationDecomposition::Partition::getEndOfStates(Block const& block) { + std::vector::iterator DeterministicModelStrongBisimulationDecomposition::Partition::getEndOfStates(Block const& block) { return this->states.begin() + block.getEnd(); } template - std::vector::const_iterator DeterministicModelBisimulationDecomposition::Partition::getBeginOfStates(Block const& block) const { + std::vector::const_iterator DeterministicModelStrongBisimulationDecomposition::Partition::getBeginOfStates(Block const& block) const { return this->states.begin() + block.getBegin(); } template - std::vector::const_iterator DeterministicModelBisimulationDecomposition::Partition::getEndOfStates(Block const& block) const { + std::vector::const_iterator DeterministicModelStrongBisimulationDecomposition::Partition::getEndOfStates(Block const& block) const { return this->states.begin() + block.getEnd(); } template - typename std::vector::iterator DeterministicModelBisimulationDecomposition::Partition::getBeginOfValues(Block const& block) { + typename std::vector::iterator DeterministicModelStrongBisimulationDecomposition::Partition::getBeginOfValues(Block const& block) { return this->values.begin() + block.getBegin(); } template - typename std::vector::iterator DeterministicModelBisimulationDecomposition::Partition::getEndOfValues(Block const& block) { + typename std::vector::iterator DeterministicModelStrongBisimulationDecomposition::Partition::getEndOfValues(Block const& block) { return this->values.begin() + block.getEnd(); } template - typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) { + typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::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. // In case one of the resulting blocks would be empty, we simply return the current block and do not create @@ -347,7 +420,7 @@ 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); + typename std::list::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr()); selfIt->setIterator(selfIt); Block& newBlock = *selfIt; @@ -363,7 +436,7 @@ namespace storm { } template - typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Partition::insertBlock(Block& block) { + typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Partition::insertBlock(Block& block) { // Find the beginning of the new block. storm::storage::sparse::state_type begin; if (block.hasPreviousBlock()) { @@ -386,7 +459,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::Partition::splitLabel(storm::storage::BitVector const& statesWithLabel) { + void DeterministicModelStrongBisimulationDecomposition::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; @@ -414,22 +487,22 @@ namespace storm { } template - std::list::Block> const& DeterministicModelBisimulationDecomposition::Partition::getBlocks() const { + std::list::Block> const& DeterministicModelStrongBisimulationDecomposition::Partition::getBlocks() const { return this->blocks; } template - std::vector& DeterministicModelBisimulationDecomposition::Partition::getStates() { + std::vector& DeterministicModelStrongBisimulationDecomposition::Partition::getStates() { return this->states; } template - std::list::Block>& DeterministicModelBisimulationDecomposition::Partition::getBlocks() { + std::list::Block>& DeterministicModelStrongBisimulationDecomposition::Partition::getBlocks() { return this->blocks; } template - bool DeterministicModelBisimulationDecomposition::Partition::check() const { + bool DeterministicModelStrongBisimulationDecomposition::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 +520,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::Partition::print() const { + void DeterministicModelStrongBisimulationDecomposition::Partition::print() const { for (auto const& block : this->blocks) { block.print(*this); } @@ -469,24 +542,49 @@ namespace storm { } template - std::size_t DeterministicModelBisimulationDecomposition::Partition::size() const { + std::size_t DeterministicModelStrongBisimulationDecomposition::Partition::size() const { return this->blocks.size(); } template - DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& dtmc, bool weak, bool buildQuotient) { - STORM_LOG_THROW(!dtmc.hasStateRewards() && !dtmc.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); - computeBisimulationEquivalenceClasses(dtmc, weak, buildQuotient); + DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, bool buildQuotient) { + STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); + Partition initialPartition = getLabelBasedInitialPartition(model); + partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient); + } + + template + DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc const& model, bool buildQuotient) { + STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); + Partition initialPartition = getLabelBasedInitialPartition(model); + partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient); + } + + template + DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, std::string const& phiLabel, std::string const& psiLabel, 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::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bounded); + partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient); + } + + template + DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc const& model, std::string const& phiLabel, std::string const& psiLabel, 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::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bounded); + partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient); } template - std::shared_ptr> DeterministicModelBisimulationDecomposition::getQuotient() const { + std::shared_ptr> DeterministicModelStrongBisimulationDecomposition::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 - void DeterministicModelBisimulationDecomposition::buildQuotient(storm::models::Dtmc const& dtmc, Partition const& partition) { + template + void DeterministicModelStrongBisimulationDecomposition::buildQuotient(ModelType const& model, Partition const& partition) { // In order to create the quotient model, we need to construct // (a) the new transition matrix, // (b) the new labeling, @@ -496,8 +594,8 @@ namespace storm { storm::storage::SparseMatrixBuilder builder(this->size(), this->size()); // Prepare the new state labeling for (b). - storm::models::AtomicPropositionsLabeling newLabeling(this->size(), dtmc.getStateLabeling().getNumberOfAtomicPropositions()); - std::set atomicPropositionsSet = dtmc.getStateLabeling().getAtomicPropositions(); + 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); @@ -510,33 +608,50 @@ namespace storm { // 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(); - // Compute the outgoing transitions of the block. - std::map blockProbability; - for (auto const& entry : dtmc.getTransitionMatrix().getRow(representativeState)) { - storm::storage::sparse::state_type targetBlock = partition.getBlock(entry.getColumn()).getId(); - auto probIterator = blockProbability.find(targetBlock); - if (probIterator != blockProbability.end()) { - probIterator->second += entry.getValue(); - } else { - blockProbability[targetBlock] = entry.getValue(); - } - } - - // Now add them to the actual matrix. - for (auto const& probabilityEntry : blockProbability) { - builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second); - } + Block const& oldBlock = partition.getBlock(representativeState); - // Add all atomic propositions to the equivalence class that the representative state satisfies. - for (auto const& ap : atomicPropositions) { - if (dtmc.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) { - newLabeling.addAtomicPropositionToState(ap, blockIndex); + // If the block is absorbing, we simply add a self-loop. + if (oldBlock.isAbsorbing()) { + builder.addNextValue(blockIndex, blockIndex, storm::utility::constantOne()); + + if (oldBlock.hasLabel()) { + newLabeling.addAtomicPropositionToState(oldBlock.getLabel(), blockIndex); + } + } else { + // Compute the outgoing transitions of the block. + std::map blockProbability; + for (auto const& entry : model.getTransitionMatrix().getRow(representativeState)) { + storm::storage::sparse::state_type targetBlock = partition.getBlock(entry.getColumn()).getId(); + auto probIterator = blockProbability.find(targetBlock); + if (probIterator != blockProbability.end()) { + probIterator->second += entry.getValue(); + } else { + blockProbability[targetBlock] = entry.getValue(); + } + } + + // Now add them to the actual matrix. + for (auto const& probabilityEntry : blockProbability) { + builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second); + } + + // If the block has a special label, we only add that to the block. + if (oldBlock.hasLabel()) { + newLabeling.addAtomicPropositionToState(oldBlock.getLabel(), blockIndex); + } else { + // Otherwise 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); + } + } } } } // Now check which of the blocks of the partition contain at least one initial state. - for (auto initialState : dtmc.getInitialStates()) { + for (auto initialState : model.getInitialStates()) { Block const& initialBlock = partition.getBlock(initialState); newLabeling.addAtomicPropositionToState("init", initialBlock.getId()); } @@ -545,33 +660,21 @@ namespace storm { // If reward structures are allowed, the quotient structures need to be built here. // Finally construct the quotient model. - this->quotient = std::shared_ptr>(new storm::models::Dtmc(builder.build(), std::move(newLabeling))); + this->quotient = std::shared_ptr>(new ModelType(builder.build(), std::move(newLabeling))); } template - void DeterministicModelBisimulationDecomposition::computeBisimulationEquivalenceClasses(storm::models::Dtmc const& dtmc, bool weak, bool buildQuotient) { + template + void DeterministicModelStrongBisimulationDecomposition::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, bool buildQuotient) { 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()); - for (auto const& label : dtmc.getStateLabeling().getAtomicPropositions()) { - if (label == "init") { - continue; - } - partition.splitLabel(dtmc.getLabeledStates(label)); - } - // 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); + refinePartition(backwardTransitions, *splitterQueue.front(), partition, splitterQueue); splitterQueue.pop_front(); } @@ -579,12 +682,14 @@ namespace storm { // a way that maintains the block IDs as indices. this->blocks.resize(partition.size()); for (auto const& block : partition.getBlocks()) { + // We need to sort the states to allow for rapid construction of the blocks. + std::sort(partition.getBeginOfStates(block), partition.getEndOfStates(block)); this->blocks[block.getId()] = block_type(partition.getBeginOfStates(block), partition.getEndOfStates(block), true); } // If we are required to build the quotient model, do so now. if (buildQuotient) { - this->buildQuotient(dtmc, partition); + this->buildQuotient(model, partition); } std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart; @@ -595,7 +700,7 @@ namespace storm { } template - std::size_t DeterministicModelBisimulationDecomposition::splitBlockProbabilities(Block& block, Partition& partition, std::deque& splitterQueue) { + void DeterministicModelStrongBisimulationDecomposition::refineBlockProbabilities(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); } ); @@ -615,8 +720,7 @@ namespace storm { // Now we can check whether the block needs to be split, which is the case iff the probabilities for the // first and the last state are different. - std::size_t createdBlocks = 0; - while (std::abs(partition.getValueAtPosition(beginIndex) - partition.getValueAtPosition(endIndex - 1)) >= 1e-6) { + while (!comparator.isEqual(partition.getValueAtPosition(beginIndex), partition.getValueAtPosition(endIndex - 1))) { // Now we scan for the first state in the block that disagrees on the probability value. // Note that we do not have to check currentIndex for staying within bounds, because we know the matching // state is within bounds. @@ -624,13 +728,12 @@ namespace storm { typename std::vector::const_iterator valueIterator = partition.getValues().begin() + beginIndex + 1; ++currentIndex; - while (currentIndex < endIndex && std::abs(*valueIterator - currentValue) <= 1e-6) { + while (currentIndex < endIndex && comparator.isEqual(*valueIterator, currentValue)) { ++valueIterator; ++currentIndex; } // Now we split the block and mark it as a potential splitter. - ++createdBlocks; Block& newBlock = partition.splitBlock(block, currentIndex); if (!newBlock.isMarkedAsSplitter()) { splitterQueue.push_back(&newBlock); @@ -638,12 +741,10 @@ namespace storm { } beginIndex = currentIndex; } - - return createdBlocks; } template - std::size_t DeterministicModelBisimulationDecomposition::splitPartition(storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, std::deque& splitterQueue) { + void DeterministicModelStrongBisimulationDecomposition::refinePartition(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. @@ -658,7 +759,7 @@ namespace storm { Block& predecessorBlock = partition.getBlock(predecessor); // If the predecessor block has just one state, there is no point in splitting it. - if (predecessorBlock.getNumberOfStates() <= 1) { + if (predecessorBlock.getNumberOfStates() <= 1 || predecessorBlock.isAbsorbing()) { continue; } @@ -773,12 +874,31 @@ namespace storm { continue; } - splitBlockProbabilities(*blockPtr, partition, splitterQueue); + refineBlockProbabilities(*blockPtr, partition, splitterQueue); } - - return 0; } - template class DeterministicModelBisimulationDecomposition; + 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) { + 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); + return partition; + } + + template + template + typename DeterministicModelStrongBisimulationDecomposition::Partition DeterministicModelStrongBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model) { + Partition partition(model.getNumberOfStates()); + for (auto const& label : model.getStateLabeling().getAtomicPropositions()) { + if (label == "init") { + continue; + } + partition.splitLabel(model.getLabeledStates(label)); + } + return partition; + } + + template class DeterministicModelStrongBisimulationDecomposition; } } \ No newline at end of file diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelStrongBisimulationDecomposition.h similarity index 56% rename from src/storage/DeterministicModelBisimulationDecomposition.h rename to src/storage/DeterministicModelStrongBisimulationDecomposition.h index c1ca37c18..e5ac547db 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.h @@ -1,5 +1,5 @@ -#ifndef STORM_STORAGE_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ -#define STORM_STORAGE_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ +#ifndef STORM_STORAGE_DETERMINISTICMODELSTRONGBISIMULATIONDECOMPOSITION_H_ +#define STORM_STORAGE_DETERMINISTICMODELSTRONGBISIMULATIONDECOMPOSITION_H_ #include #include @@ -7,21 +7,59 @@ #include "src/storage/sparse/StateType.h" #include "src/storage/Decomposition.h" #include "src/models/Dtmc.h" +#include "src/models/Ctmc.h" #include "src/storage/Distribution.h" +#include "src/utility/ConstantsComparator.h" +#include "src/utility/OsDetection.h" namespace storm { namespace storage { /*! - * This class represents the decomposition model into its bisimulation quotient. + * This class represents the decomposition model into its (strong) bisimulation quotient. */ template - class DeterministicModelBisimulationDecomposition : public Decomposition { + class DeterministicModelStrongBisimulationDecomposition : public Decomposition { public: /*! - * Decomposes the given DTMC into equivalence classes under weak or strong bisimulation. + * Decomposes the given DTMC into equivalence classes under strong bisimulation. + * + * @param model The model to decompose. + * @param buildQuotient Sets whether or not the quotient model is to be built. + */ + DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, bool buildQuotient = false); + + /*! + * Decomposes the given CTMC into equivalence classes under strong bisimulation. + * + * @param model The model to decompose. + * @param buildQuotient Sets whether or not the quotient model is to be built. + */ + DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc const& model, bool buildQuotient = false); + + /*! + * Decomposes the given DTMC into equivalence classes under strong bisimulation in a way that onle safely + * preserves formulas of the form phi until psi. + * + * @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 bounded If set to true, also bounded until formulas are preserved. + * @param buildQuotient Sets whether or not the quotient model is to be built. */ - DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, bool weak = false, bool buildQuotient = false); + DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient = false); + + /*! + * Decomposes the given CTMC into equivalence classes under strong bisimulation in a way that onle safely + * preserves formulas of the form phi until psi. + * + * @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 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); /*! * Retrieves the quotient of the model under the previously computed bisimulation. @@ -37,7 +75,7 @@ namespace storm { public: typedef typename std::list::const_iterator const_iterator; - Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next); + Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr const& label = nullptr); // Prints the block. void print(Partition const& partition) const; @@ -138,6 +176,21 @@ namespace storm { // Removes the marking. void unmarkAsPredecessorBlock(); + // Sets whether or not the block is to be interpreted as absorbing. + void setAbsorbing(bool absorbing); + + // Retrieves whether the block is to be interpreted as absorbing. + bool isAbsorbing() const; + + // Retrieves whether the block has a special label. + bool hasLabel() const; + + // Retrieves the special label of the block if it has one. + std::string const& getLabel() const; + + // Retrieves a pointer to the label of the block (which is the nullptr if there is none). + std::shared_ptr const& getLabelPtr() const; + private: // An iterator to itself. This is needed to conveniently insert elements in the overall list of blocks // kept by the partition. @@ -160,8 +213,17 @@ namespace storm { // A position that can be used to store a certain position within the block. storm::storage::sparse::state_type markedPosition; + // A flag indicating whether the block is to be interpreted as absorbing or not. + bool absorbing; + // The ID of the block. This is only used for debugging purposes. std::size_t id; + + // The label of the block or nullptr if it has none. + std::shared_ptr label; + + // A counter for the IDs of the blocks. + static std::size_t blockId; }; class Partition { @@ -170,8 +232,31 @@ namespace storm { /*! * Creates a partition with one block consisting of all the states. + * + * @param numberOfStates The number of states the partition holds. */ Partition(std::size_t numberOfStates); + + /*! + * Creates a partition with three blocks: one with all phi states, one with all psi states and one with + * all other states. The former two blocks are marked as being absorbing, because their outgoing + * transitions shall not be taken into account for future refinement. + * + * @param numberOfStates The number of states the partition holds. + * @param prob0States The states which have probability 0 of satisfying phi until psi. + * @param prob1States The states which have probability 1 of satisfying phi until psi. + * @param otherLabel The label that is to be attached to all other states. + * @param prob1Label The label that is to be attached to all states with probability 1. + */ + Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label); + + Partition() = default; + Partition(Partition const& other) = default; + Partition& operator=(Partition const& other) = default; +#ifndef WINDOWS + Partition(Partition&& other) = default; + Partition& operator=(Partition&& other) = default; +#endif /*! * Splits all blocks of the partition such that afterwards all blocks contain only states with the label @@ -262,6 +347,8 @@ namespace storm { // Updates the block mapping for the given range of states to the specified block. void updateBlockMapping(Block& block, std::vector::iterator first, std::vector::iterator end); + // Retrieves the first block of the partition. + Block& getFirstBlock(); private: // The list of blocks in the partition. std::list blocks; @@ -280,18 +367,86 @@ namespace storm { std::vector values; }; - void computeBisimulationEquivalenceClasses(storm::models::Dtmc const& model, bool weak, bool buildQuotient); + /*! + * Performs the partition refinement on the model and thereby computes the equivalence classes under strong + * bisimulation equivalence. If required, the quotient model is built and may be retrieved using + * getQuotient(). + * + * @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 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 buildQuotient); - std::size_t splitPartition(storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, std::deque& splitterQueue); + /*! + * Refines the partition based on the provided splitter. After calling this method all blocks are stable + * with respect to the splitter. + * + * @param backwardTransitions A matrix that can be used to retrieve the predecessors (and their + * probabilities). + * @param splitter The splitter to use. + * @param partition The partition to split. + * @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& backwardTransitions, Block& splitter, Partition& partition, std::deque& splitterQueue); - std::size_t splitBlockProbabilities(Block& block, Partition& partition, 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 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 buildQuotient(storm::models::Dtmc const& dtmc, Partition const& partition); + /*! + * Builds the quotient model based on the previously computed equivalence classes (stored in the blocks + * of the decomposition. + * + * @param model The model whose state space was used for computing the equivalence classes. This is used for + * determining the transitions of each equivalence class. + * @param partition The previously computed partition. This is used for quickly retrieving the block of a + * state. + */ + template + void buildQuotient(ModelType const& model, Partition const& partition); + /*! + * Creates the measure-driven initial partition for reaching psi states from phi states. + * + * @param model The model whose state space is partitioned based on reachability of psi states from phi + * states. + * @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 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); + + /*! + * Creates the initial partition based on all the labels in the given model. + * + * @param model The model whose state space is partitioned based on its labels. + * @return The resulting partition. + */ + template + Partition getLabelBasedInitialPartition(ModelType const& model); + // If required, a quotient model is built and stored in this member. std::shared_ptr> quotient; + + // A comparator that is used for determining whether two probabilities are considered to be equal. + storm::utility::ConstantsComparator comparator; }; } } -#endif /* STORM_STORAGE_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_DETERMINISTICMODELSTRONGBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h new file mode 100644 index 000000000..fc46b251f --- /dev/null +++ b/src/utility/ConstantsComparator.h @@ -0,0 +1,84 @@ +#ifndef STORM_UTILITY_CONSTANTSCOMPARATOR_H_ +#define STORM_UTILITY_CONSTANTSCOMPARATOR_H_ + +#ifdef max +# undef max +#endif + +#ifdef min +# undef min +#endif + +#include +#include + +#include "src/settings/SettingsManager.h" + +namespace storm { + namespace utility { + + template + ValueType one() { + return ValueType(1); + } + + template + ValueType zero() { + return ValueType(0); + } + + template + ValueType infinity() { + return std::numeric_limits::infinity(); + } + + // A class that can be used for comparing constants. + template + class ConstantsComparator { + public: + bool isOne(ValueType const& value) { + return value == one(); + } + + bool isZero(ValueType const& value) { + return value == zero(); + } + + bool isEqual(ValueType const& value1, ValueType const& value2) { + return value1 == value2; + } + }; + + // For doubles we specialize this class and consider the comparison modulo some predefined precision. + template<> + class ConstantsComparator { + public: + ConstantsComparator() : precision(storm::settings::generalSettings().getPrecision()) { + // Intentionally left empty. + } + + ConstantsComparator(double precision) : precision(precision) { + // Intentionally left empty. + } + + bool isOne(double const& value) { + return std::abs(value - one()) <= precision; + } + + bool isZero(double const& value) { + return std::abs(value) <= precision; + } + + bool isEqual(double const& value1, double const& value2) { + return std::abs(value1 - value2) <= precision; + } + + private: + // The precision used for comparisons. + double precision; + }; + + } +} + +#endif /* STORM_UTILITY_CONSTANTSCOMPARATOR_H_ */ \ No newline at end of file diff --git a/src/utility/cli.h b/src/utility/cli.h index 813a6fa74..908d7dc52 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/DeterministicModelBisimulationDecomposition.h" +#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h" // Headers for counterexample generation. #include "src/counterexamples/MILPMinimalLabelSetGenerator.h" @@ -267,7 +267,7 @@ namespace storm { std::shared_ptr> dtmc = result->template as>(); STORM_PRINT(std::endl << "Performing bisimulation minimization..." << std::endl); - storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, false, true); + storm::storage::DeterministicModelStrongBisimulationDecomposition bisimulationDecomposition(*dtmc, true); result = bisimulationDecomposition.getQuotient(); @@ -285,7 +285,7 @@ namespace storm { std::shared_ptr> mdp = model->as>(); - // FIXME: re-parse the program. + // FIXME: do not re-parse the program. std::string const programFile = storm::settings::generalSettings().getSymbolicModelFilename(); std::string const constants = storm::settings::generalSettings().getConstantDefinitionString(); storm::prism::Program program = storm::parser::PrismParser::parse(programFile); diff --git a/src/utility/graph.h b/src/utility/graph.h index 21972adbc..3af235fe3 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -204,6 +204,25 @@ namespace storm { return result; } + /*! + * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a + * deterministic model. + * + * @param backwardTransitions The backward transitions of the model whose graph structure to search. + * @param phiStates The set of all states satisfying phi. + * @param psiStates The set of all states satisfying psi. + * @return A pair of bit vectors such that the first bit vector stores the indices of all states + * with probability 0 and the second stores all indices of states with probability 1. + */ + template + static std::pair performProb01(storm::storage::SparseMatrix backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + std::pair result; + result.first = performProbGreater0(backwardTransitions, phiStates, psiStates); + result.second = performProb1(backwardTransitions, phiStates, psiStates, result.first); + result.first.complement(); + return result; + } + /*! * Computes the sets of states that have probability greater 0 of satisfying phi until psi under at least * one possible resolution of non-determinism in a non-deterministic model. Stated differently,