diff --git a/src/storm/storage/bisimulation/DeterministicBlockData.cpp b/src/storm/storage/bisimulation/DeterministicBlockData.cpp index a5c4f3a17..db9e3ba3a 100644 --- a/src/storm/storage/bisimulation/DeterministicBlockData.cpp +++ b/src/storm/storage/bisimulation/DeterministicBlockData.cpp @@ -13,7 +13,7 @@ namespace storm { // Intentionally left empty. } - DeterministicBlockData::DeterministicBlockData(uint_fast64_t marker1, uint_fast64_t marker2) : valMarker1(marker1), valMarker2(marker2), splitterFlag(false), needsRefinementFlag(false), absorbingFlag(false), valRepresentativeState() { + DeterministicBlockData::DeterministicBlockData(uint_fast64_t marker1, uint_fast64_t marker2) : valMarker1(marker1), valMarker2(marker2), flags(0), valRepresentativeState() { // Intentionally left empty. } @@ -56,19 +56,27 @@ namespace storm { } bool DeterministicBlockData::splitter() const { - return this->splitterFlag; + return getFlag(SPLITTER_FLAG); } void DeterministicBlockData::setSplitter(bool value) { - this->splitterFlag = value; + setFlag(SPLITTER_FLAG, value); } void DeterministicBlockData::setAbsorbing(bool absorbing) { - this->absorbingFlag = absorbing; + setFlag(ABSORBING_FLAG, absorbing); } bool DeterministicBlockData::absorbing() const { - return this->absorbingFlag; + return getFlag(ABSORBING_FLAG); + } + + void DeterministicBlockData::setHasRewards(bool value) { + setFlag(REWARD_FLAG, value); + } + + bool DeterministicBlockData::hasRewards() const { + return getFlag(REWARD_FLAG); } void DeterministicBlockData::setRepresentativeState(storm::storage::sparse::state_type representativeState) { @@ -85,15 +93,27 @@ namespace storm { } bool DeterministicBlockData::needsRefinement() const { - return needsRefinementFlag; + return getFlag(REFINEMENT_FLAG); } void DeterministicBlockData::setNeedsRefinement(bool value) { - needsRefinementFlag = value; + setFlag(REFINEMENT_FLAG, value); + } + + bool DeterministicBlockData::getFlag(uint64_t flag) const { + return (this->flags & flag) != 0ull; + } + + void DeterministicBlockData::setFlag(uint64_t flag, bool value) { + if (value) { + this->flags |= flag; + } else { + this->flags &= ~flag; + } } std::ostream& operator<<(std::ostream& out, DeterministicBlockData const& data) { - out << "m1: " << data.marker1() << ", m2: " << data.marker2(); + out << "m1: " << data.marker1() << ", m2: " << data.marker2() << ", r: " << data.hasRewards(); return out; } } diff --git a/src/storm/storage/bisimulation/DeterministicBlockData.h b/src/storm/storage/bisimulation/DeterministicBlockData.h index bc4ed1abc..020c5e9fb 100644 --- a/src/storm/storage/bisimulation/DeterministicBlockData.h +++ b/src/storm/storage/bisimulation/DeterministicBlockData.h @@ -49,6 +49,12 @@ namespace storm { // Retrieves whether the block is to be interpreted as absorbing. bool absorbing() const; + // Sets whether the states in the block have rewards. + void setHasRewards(bool value = true); + + // Retrieves whether the states in the block have rewards. + bool hasRewards() const; + // Sets the representative state of this block void setRepresentativeState(storm::storage::sparse::state_type representativeState); @@ -61,19 +67,21 @@ namespace storm { friend std::ostream& operator<<(std::ostream& out, DeterministicBlockData const& data); public: + // Helpers to set/retrieve flags. + bool getFlag(uint64_t flag) const; + void setFlag(uint64_t flag, bool value); + // Two markers that can be used for various purposes. Whenever the block is split, both the markers are // set to the beginning index of the block. uint_fast64_t valMarker1; uint_fast64_t valMarker2; - // A flag that can be used for marking the block as being a splitter. - bool splitterFlag; - - // A flag that can be used for marking the block as needing refinement. - bool needsRefinementFlag; - - // A flag indicating whether the block is to be interpreted as absorbing or not. - bool absorbingFlag; + // Some bits to store flags: splitter flag, refinement flag, absorbing flag. + static const uint64_t SPLITTER_FLAG = 1ull; + static const uint64_t REFINEMENT_FLAG = 1ull << 1; + static const uint64_t ABSORBING_FLAG = 1ull << 2; + static const uint64_t REWARD_FLAG = 1ull << 3; + uint8_t flags; // An optional representative state for the block. If this is set, this state is used to derive the // atomic propositions of the meta state in the quotient model. diff --git a/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index 27e5fd806..39ad3db45 100644 --- a/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -118,22 +118,37 @@ namespace storm { this->initializeSilentProbabilities(); } + template - void DeterministicModelBisimulationDecomposition::initializeMeasureDrivenPartition() { - BisimulationDecomposition::initializeMeasureDrivenPartition(); - + void DeterministicModelBisimulationDecomposition::postProcessInitialPartition() { if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) { this->initializeWeakDtmcBisimulation(); } + + if (this->options.getKeepRewards() && this->model.hasRewardModel() && this->options.getType() == BisimulationType::Weak) { + // For a weak bisimulation that is to preserve reward properties, we have to flag all blocks of states + // with non-zero reward as reward blocks to they can be refined wrt. strong bisimulation. + + // Here, we assume that the initial partition already respects state rewards. Therefore, it suffices to + // check the first state of each block for a non-zero reward. + std::vector const& stateRewardVector = this->model.getUniqueRewardModel().getStateRewardVector(); + for (auto& block : this->partition.getBlocks()) { + auto state = *this->partition.begin(*block); + block->data().setHasRewards(!storm::utility::isZero(stateRewardVector[state])); + } + } + } + + template + void DeterministicModelBisimulationDecomposition::initializeMeasureDrivenPartition() { + BisimulationDecomposition::initializeMeasureDrivenPartition(); + postProcessInitialPartition(); } template void DeterministicModelBisimulationDecomposition::initializeLabelBasedPartition() { BisimulationDecomposition::initializeLabelBasedPartition(); - - if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) { - this->initializeWeakDtmcBisimulation(); - } + postProcessInitialPartition(); } template @@ -156,37 +171,49 @@ namespace storm { return silentProbabilities[state]; } + template + void DeterministicModelBisimulationDecomposition::refinePredecessorBlockOfSplitterStrong(bisimulation::Block& block, std::vector*>& splitterQueue) { + STORM_LOG_TRACE("Refining predecessor " << block.getId() << " of splitter"); + + // Depending on the actions we need to take, the block to refine changes, so we need to keep track of it. + Block* blockToRefineProbabilistically = █ + + bool split = false; + // If the new begin index has shifted to a non-trivial position, we need to split the block. + if (block.getBeginIndex() != block.data().marker1() && block.getEndIndex() != block.data().marker1()) { + split = true; + this->partition.splitBlock(block, block.data().marker1()); + blockToRefineProbabilistically = block.getPreviousBlockPointer(); + + // Keep track of whether this is a block with reward states. + blockToRefineProbabilistically->data().setHasRewards(block.data().hasRewards()); + } + + split |= this->partition.splitBlock(*blockToRefineProbabilistically, + [this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { + return this->comparator.isLess(getProbabilityToSplitter(state1), getProbabilityToSplitter(state2)); + }, + [&splitterQueue,&block] (Block& newBlock) { + splitterQueue.emplace_back(&newBlock); + newBlock.data().setSplitter(); + + // Keep track of whether this is a block with reward states. + newBlock.data().setHasRewards(block.data().hasRewards()); + }); + + + // If the predecessor block was split, we need to insert it into the splitter vector if it is not already + // marked as a splitter. + if (split && !blockToRefineProbabilistically->data().splitter()) { + splitterQueue.emplace_back(blockToRefineProbabilistically); + blockToRefineProbabilistically->data().setSplitter(); + } + } + template void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::vector*>& splitterQueue) { for (auto block : predecessorBlocks) { - STORM_LOG_TRACE("Refining predecessor " << block->getId() << " of splitter"); - - // Depending on the actions we need to take, the block to refine changes, so we need to keep track of it. - Block* blockToRefineProbabilistically = block; - - bool split = false; - // If the new begin index has shifted to a non-trivial position, we need to split the block. - if (block->getBeginIndex() != block->data().marker1() && block->getEndIndex() != block->data().marker1()) { - split = true; - this->partition.splitBlock(*block, block->data().marker1()); - blockToRefineProbabilistically = block->getPreviousBlockPointer(); - } - - split |= this->partition.splitBlock(*blockToRefineProbabilistically, - [this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { - return this->comparator.isLess(getProbabilityToSplitter(state1), getProbabilityToSplitter(state2)); - }, - [&splitterQueue] (Block& block) { - splitterQueue.emplace_back(&block); block.data().setSplitter(); - }); - - - // If the predecessor block was split, we need to insert it into the splitter vector if it is not already - // marked as a splitter. - if (split && !blockToRefineProbabilistically->data().splitter()) { - splitterQueue.emplace_back(blockToRefineProbabilistically); - blockToRefineProbabilistically->data().setSplitter(); - } + refinePredecessorBlockOfSplitterStrong(*block, splitterQueue); // If the block was *not* split, we need to reset the markers by notifying the data. block->resetMarkers(); @@ -395,12 +422,15 @@ namespace storm { [&weakStateLabels,&block,originalBlockIndex,this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { return weakStateLabels[this->partition.getPosition(state1) - originalBlockIndex] < weakStateLabels[this->partition.getPosition(state2) - originalBlockIndex]; }, - [this, &splitterQueue] (bisimulation::Block& block) { - updateSilentProbabilitiesBasedOnTransitions(block); + [this, &splitterQueue, &block] (bisimulation::Block& newBlock) { + updateSilentProbabilitiesBasedOnTransitions(newBlock); // Insert the new block as a splitter. - block.data().setSplitter(); - splitterQueue.emplace_back(&block); + newBlock.data().setSplitter(); + splitterQueue.emplace_back(&newBlock); + + // Keep track of whether this is a block with reward states. + newBlock.data().setHasRewards(block.data().hasRewards()); }); // If the block was split, we also update the silent probabilities. @@ -418,10 +448,14 @@ namespace storm { template void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::vector*>& splitterQueue) { for (auto block : predecessorBlocks) { - if (*block != splitter) { - refinePredecessorBlockOfSplitterWeak(*block, splitterQueue); + if (block->data().hasRewards()) { + refinePredecessorBlockOfSplitterStrong(*block, splitterQueue); } else { - // If the block to split is the splitter itself, we must not do any splitting here. + if (*block != splitter) { + refinePredecessorBlockOfSplitterWeak(*block, splitterQueue); + } else { + // If the block to split is the splitter itself, we must not do any splitting here. + } } block->resetMarkers(); @@ -594,7 +628,7 @@ namespace storm { storm::storage::sparse::state_type targetBlock = this->partition.getBlock(entry.getColumn()).getId(); // If we are computing a weak bisimulation quotient, there is no need to add self-loops. - if ((this->options.getType() == BisimulationType::Weak) && targetBlock == blockIndex) { + if ((this->options.getType() == BisimulationType::Weak) && targetBlock == blockIndex && !oldBlock.data().hasRewards()) { continue; } @@ -608,7 +642,7 @@ namespace storm { // Now add them to the actual matrix. for (auto const& probabilityEntry : blockProbability) { - if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) { + if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc && !oldBlock.data().hasRewards()) { builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second / (storm::utility::one() - getSilentProbability(representativeState))); } else { builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second); diff --git a/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h b/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h index 468e39ef3..0605474bb 100644 --- a/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h +++ b/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h @@ -42,6 +42,12 @@ namespace storm { virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::vector*>& splitterQueue) override; private: + // Post-processes the initial partition to properly initialize it. + void postProcessInitialPartition(); + + // Refines the given block wrt to strong bisimulation. + void refinePredecessorBlockOfSplitterStrong(bisimulation::Block& block, std::vector*>& splitterQueue); + // Refines the predecessor blocks wrt. strong bisimulation. void refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::vector*>& splitterQueue); @@ -98,11 +104,11 @@ namespace storm { // of the states. void updateSilentProbabilitiesBasedOnTransitions(bisimulation::Block& block); - // Refines the predecessor blocks of the splitter wrt. weak bisimulation in DTMCs. - void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::vector*>& splitterQueue); - // Refines the given block wrt to weak bisimulation in DTMCs. void refinePredecessorBlockOfSplitterWeak(bisimulation::Block& block, std::vector*>& splitterQueue); + + // Refines the predecessor blocks of the splitter wrt. weak bisimulation in DTMCs. + void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::vector*>& splitterQueue); // Converts the one-step probabilities of going into the splitter into the conditional probabilities needed // for weak bisimulation (on DTMCs). diff --git a/src/storm/storage/bisimulation/Partition.cpp b/src/storm/storage/bisimulation/Partition.cpp index a98aa4ba7..d2904027b 100644 --- a/src/storm/storage/bisimulation/Partition.cpp +++ b/src/storm/storage/bisimulation/Partition.cpp @@ -89,11 +89,6 @@ namespace storm { return this->positions[state]; } - template - void 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& Partition::getState(storm::storage::sparse::state_type position) const { return this->states[position]; @@ -214,7 +209,7 @@ namespace storm { template std::pair>>::iterator, bool> Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) { - STORM_LOG_THROW(position >= block.getBeginIndex() && position <= block.getEndIndex(), storm::exceptions::InvalidArgumentException, "Cannot split block at illegal position."); + STORM_LOG_ASSERT(position >= block.getBeginIndex() && position <= block.getEndIndex(), "Cannot split block at illegal position."); STORM_LOG_TRACE("Splitting " << block.getId() << " at position " << position << " (begin was " << block.getBeginIndex() << ")."); // In case one of the resulting blocks would be empty, we simply return the current block and do not create @@ -308,23 +303,6 @@ namespace storm { mapStatesToPositions(block); } - template - Block& Partition::insertBlock(Block& block) { - // Find the beginning of the new block. - storm::storage::sparse::state_type begin = block.hasPreviousBlock() ? block.getPreviousBlock().getEndIndex() : 0; - - // Actually insert the new block. - blocks.emplace_back(new Block(begin, block.getBeginIndex(), block.getPreviousBlockPointer(), &block, blocks.size())); - Block& newBlock = *blocks.back(); - - // Update the mapping of the states in the newly created block. - for (auto it = this->begin(newBlock), ite = this->end(newBlock); it != ite; ++it) { - stateToBlockMapping[*it] = &newBlock; - } - - return newBlock; - } - template std::vector>> const& Partition::getBlocks() const { return this->blocks; diff --git a/src/storm/storage/bisimulation/Partition.h b/src/storm/storage/bisimulation/Partition.h index 0a6f7eabc..3ace9b2e1 100644 --- a/src/storm/storage/bisimulation/Partition.h +++ b/src/storm/storage/bisimulation/Partition.h @@ -152,15 +152,6 @@ namespace storm { void swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2); private: - // FIXME: necessary? - // Inserts a block before the given block. The new block will cover all states between the beginning - // of the given block and the end of the previous block. - Block& insertBlock(Block& block); - - // FIXME: necessary? - // Sets the position of the given state. - void setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position); - // The of blocks in the partition. std::vector>> blocks;