#include "storm/storage/bisimulation/Block.h" #include #include #include "storm/storage/bisimulation/Partition.h" #include "storm/storage/bisimulation/DeterministicBlockData.h" #include "storm/utility/macros.h" namespace storm { namespace storage { namespace bisimulation { template Block::Block(storm::storage::sparse::state_type beginIndex, storm::storage::sparse::state_type endIndex, Block* previousBlock, Block* nextBlock, std::size_t id) : nextBlock(nextBlock), previousBlock(previousBlock), beginIndex(beginIndex), endIndex(endIndex), id(id), mData() { if (nextBlock != nullptr) { nextBlock->previousBlock = this; } if (previousBlock != nullptr) { previousBlock->nextBlock = this; } data().resetMarkers(*this); STORM_LOG_ASSERT(this->beginIndex < this->endIndex, "Unable to create block of illegal size."); } template bool Block::operator==(Block const& other) const { return this == &other; } template bool Block::operator!=(Block const& other) const { return this != &other; } template void Block::print(Partition const& partition) const { std::cout << "block [" << this << "] " << this->id << " from " << this->beginIndex << " to " << this->endIndex << " with data [" << this->data() << "]" << std::endl; std::cout << "states "; for (auto stateIt = partition.begin(*this), stateIte = partition.end(*this); stateIt != stateIte; ++stateIt) { std::cout << *stateIt << ", "; } std::cout << std::endl; } template void Block::setBeginIndex(storm::storage::sparse::state_type beginIndex) { this->beginIndex = beginIndex; data().resetMarkers(*this); STORM_LOG_ASSERT(beginIndex < endIndex, "Unable to resize block to illegal size."); } template void Block::setEndIndex(storm::storage::sparse::state_type endIndex) { this->endIndex = endIndex; data().resetMarkers(*this); STORM_LOG_ASSERT(beginIndex < endIndex, "Unable to resize block to illegal size."); } template std::size_t Block::getId() const { return this->id; } template storm::storage::sparse::state_type Block::getBeginIndex() const { return this->beginIndex; } template storm::storage::sparse::state_type Block::getEndIndex() const { return this->endIndex; } template Block const& Block::getNextBlock() const { return *this->nextBlock; } template bool Block::hasNextBlock() const { return this->nextBlock != nullptr; } template Block* Block::getNextBlockPointer() { return this->nextBlock; } template Block const* Block::getNextBlockPointer() const { return this->nextBlock; } template Block const& Block::getPreviousBlock() const { return *this->previousBlock; } template Block* Block::getPreviousBlockPointer() { return this->previousBlock; } template Block const* Block::getPreviousBlockPointer() const { return this->previousBlock; } template bool Block::hasPreviousBlock() const { return this->previousBlock != nullptr; } template bool Block::check() const { STORM_LOG_ASSERT(this->beginIndex < this->endIndex, "Block has negative size."); STORM_LOG_ASSERT(!this->hasPreviousBlock() || this->getPreviousBlock().getNextBlockPointer() == this, "Illegal previous block."); STORM_LOG_ASSERT(!this->hasNextBlock() || this->getNextBlock().getPreviousBlockPointer() == this, "Illegal next block."); return true; } template std::size_t Block::getNumberOfStates() const { return (this->endIndex - this->beginIndex); } template DataType& Block::data() { return mData; } template DataType const& Block::data() const { return mData; } template void Block::resetMarkers() { mData.resetMarkers(*this); } template class Block; } } }