diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 88e0a396f..05d262b65 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -33,6 +33,7 @@ file(GLOB STORM_SETTINGS_FILES ${PROJECT_SOURCE_DIR}/src/settings/*.h ${PROJECT_ file(GLOB STORM_SETTINGS_MODULES_FILES ${PROJECT_SOURCE_DIR}/src/settings/modules/*.h ${PROJECT_SOURCE_DIR}/src/settings/modules/*.cpp) file(GLOB_RECURSE STORM_SOLVER_FILES ${PROJECT_SOURCE_DIR}/src/solver/*.h ${PROJECT_SOURCE_DIR}/src/solver/*.cpp) file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp) +file(GLOB STORM_STORAGE_BISIMULATION_FILES ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.h ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.cpp) file(GLOB_RECURSE STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp) file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp) file(GLOB_RECURSE STORM_STORAGE_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/*.cpp) @@ -77,6 +78,7 @@ source_group(settings FILES ${STORM_SETTINGS_FILES}) source_group(settings\\modules FILES ${STORM_SETTINGS_MODULES_FILES}) source_group(solver FILES ${STORM_SOLVER_FILES}) source_group(storage FILES ${STORM_STORAGE_FILES}) +source_group(storage\\bisimulation FILES ${STORM_STORAGE_BISIMULATION_FILES}) source_group(storage\\dd FILES ${STORM_STORAGE_DD_FILES}) source_group(storage\\expressions FILES ${STORM_STORAGE_EXPRESSIONS_FILES}) source_group(storage\\prism FILES ${STORM_STORAGE_PRISM_FILES}) diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp deleted file mode 100644 index b861f8f2c..000000000 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ /dev/null @@ -1,1538 +0,0 @@ -#include "src/storage/DeterministicModelBisimulationDecomposition.h" - -#include -#include -#include -#include -#include - -#include "src/adapters/CarlAdapter.h" -#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" -#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" - -#include "src/models/sparse/StandardRewardModel.h" - -#include "src/utility/graph.h" -#include "src/utility/constants.h" -#include "src/utility/ConstantsComparator.h" -#include "src/exceptions/IllegalFunctionCallException.h" -#include "src/exceptions/InvalidOptionException.h" -#include "src/exceptions/InvalidArgumentException.h" - -#include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" - -namespace storm { - namespace storage { - - template - DeterministicModelBisimulationDecomposition::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(id) { - if (next != nullptr) { - next->prev = this; - } - if (prev != nullptr) { - prev->next = this; - } - STORM_LOG_ASSERT(begin < end, "Unable to create block of illegal size."); - } - - template - void DeterministicModelBisimulationDecomposition::Block::print(Partition const& partition) const { - std::cout << "block " << this->getId() << " with marked position " << this->getMarkedPosition() << " and original begin " << this->getOriginalBegin() << std::endl; - std::cout << "begin: " << this->begin << " and end: " << this->end << " (number of states: " << this->getNumberOfStates() << ")" << std::endl; - std::cout << "states:" << std::endl; - for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) { - std::cout << partition.statesAndValues[index].first << " "; - } - std::cout << std::endl << "original: " << std::endl; - for (storm::storage::sparse::state_type index = this->getOriginalBegin(); index < this->end; ++index) { - std::cout << partition.statesAndValues[index].first << " "; - } - std::cout << std::endl << "values:" << std::endl; - for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) { - std::cout << std::setprecision(3) << partition.statesAndValues[index].second << " "; - } - if (partition.keepSilentProbabilities) { - std::cout << std::endl << "silent:" << std::endl; - for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) { - std::cout << std::setprecision(3) << partition.silentProbabilities[partition.statesAndValues[index].first] << " "; - } - } - std::cout << std::endl; - } - - template - 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 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 DeterministicModelBisimulationDecomposition::Block::incrementBegin() { - ++this->begin; - STORM_LOG_ASSERT(begin <= end, "Unable to resize block to illegal size."); - } - - template - storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getBegin() const { - return this->begin; - } - - template - storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getOriginalBegin() const { - if (this->hasPreviousBlock()) { - return this->getPreviousBlock().getEnd(); - } else { - return 0; - } - } - - template - storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getEnd() const { - return this->end; - } - - template - void DeterministicModelBisimulationDecomposition::Block::setIterator(iterator it) { - this->selfIt = it; - } - - template - typename DeterministicModelBisimulationDecomposition::Block::iterator DeterministicModelBisimulationDecomposition::Block::getIterator() const { - return this->selfIt; - } - - template - typename DeterministicModelBisimulationDecomposition::Block::iterator DeterministicModelBisimulationDecomposition::Block::getNextIterator() const { - return this->getNextBlock().getIterator(); - } - - template - typename DeterministicModelBisimulationDecomposition::Block::iterator DeterministicModelBisimulationDecomposition::Block::getPreviousIterator() const { - return this->getPreviousBlock().getIterator(); - } - - template - typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Block::getNextBlock() { - return *this->next; - } - - template - typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Block::getNextBlock() const { - return *this->next; - } - - template - bool DeterministicModelBisimulationDecomposition::Block::hasNextBlock() const { - return this->next != nullptr; - } - - template - typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Block::getPreviousBlock() { - return *this->prev; - } - - template - typename DeterministicModelBisimulationDecomposition::Block* DeterministicModelBisimulationDecomposition::Block::getPreviousBlockPointer() { - return this->prev; - } - - template - typename DeterministicModelBisimulationDecomposition::Block* DeterministicModelBisimulationDecomposition::Block::getNextBlockPointer() { - return this->next; - } - - template - typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Block::getPreviousBlock() const { - return *this->prev; - } - - template - bool DeterministicModelBisimulationDecomposition::Block::hasPreviousBlock() const { - return this->prev != nullptr; - } - - template - 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); - return true; - } - - template - 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 DeterministicModelBisimulationDecomposition::Block::isMarkedAsSplitter() const { - return this->markedAsSplitter; - } - - template - void DeterministicModelBisimulationDecomposition::Block::markAsSplitter() { - this->markedAsSplitter = true; - } - - template - void DeterministicModelBisimulationDecomposition::Block::unmarkAsSplitter() { - this->markedAsSplitter = false; - } - - template - std::size_t DeterministicModelBisimulationDecomposition::Block::getId() const { - return this->id; - } - - template - void DeterministicModelBisimulationDecomposition::Block::setAbsorbing(bool absorbing) { - this->absorbing = absorbing; - } - - template - bool DeterministicModelBisimulationDecomposition::Block::isAbsorbing() const { - return this->absorbing; - } - - template - void DeterministicModelBisimulationDecomposition::Block::setRepresentativeState(storm::storage::sparse::state_type representativeState) { - this->representativeState = representativeState; - } - - template - bool DeterministicModelBisimulationDecomposition::Block::hasRepresentativeState() const { - return static_cast(representativeState); - } - - template - storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getRepresentativeState() const { - STORM_LOG_THROW(representativeState, storm::exceptions::InvalidOperationException, "Unable to retrieve representative state for block."); - return representativeState.get(); - } - - template - storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getMarkedPosition() const { - return this->markedPosition; - } - - template - void DeterministicModelBisimulationDecomposition::Block::setMarkedPosition(storm::storage::sparse::state_type position) { - this->markedPosition = position; - } - - template - void DeterministicModelBisimulationDecomposition::Block::resetMarkedPosition() { - this->markedPosition = this->begin; - } - - template - void DeterministicModelBisimulationDecomposition::Block::incrementMarkedPosition() { - ++this->markedPosition; - } - - template - void DeterministicModelBisimulationDecomposition::Block::markAsPredecessorBlock() { - this->markedAsPredecessorBlock = true; - } - - template - void DeterministicModelBisimulationDecomposition::Block::unmarkAsPredecessorBlock() { - this->markedAsPredecessorBlock = false; - } - - template - bool DeterministicModelBisimulationDecomposition::Block::isMarkedAsPredecessor() const { - return markedAsPredecessorBlock; - } - - template - DeterministicModelBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates, bool keepSilentProbabilities) : numberOfBlocks(0), 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, numberOfBlocks++); - it->setIterator(it); - - // Set up the different parts of the internal structure. - for (storm::storage::sparse::state_type state = 0; state < numberOfStates; ++state) { - statesAndValues[state] = std::make_pair(state, storm::utility::zero()); - positions[state] = state; - stateToBlockMapping[state] = &blocks.back(); - } - - // If we are requested to store silent probabilities, we need to prepare the vector. - if (this->keepSilentProbabilities) { - silentProbabilities = std::vector(numberOfStates); - } - } - - template - DeterministicModelBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, boost::optional representativeProb1State, bool keepSilentProbabilities) : numberOfBlocks(0), stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() { - storm::storage::sparse::state_type position = 0; - Block* firstBlock = nullptr; - Block* secondBlock = nullptr; - Block* thirdBlock = nullptr; - if (!prob0States.empty()) { - typename std::list::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr, numberOfBlocks++); - firstBlock = &(*firstIt); - firstBlock->setIterator(firstIt); - - for (auto state : prob0States) { - statesAndValues[position] = std::make_pair(state, storm::utility::zero()); - positions[state] = position; - stateToBlockMapping[state] = firstBlock; - ++position; - } - firstBlock->setAbsorbing(true); - } - - if (!prob1States.empty()) { - typename std::list::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), firstBlock, nullptr, numberOfBlocks++); - secondBlock = &(*secondIt); - secondBlock->setIterator(secondIt); - - for (auto state : prob1States) { - statesAndValues[position] = std::make_pair(state, storm::utility::zero()); - positions[state] = position; - stateToBlockMapping[state] = secondBlock; - ++position; - } - secondBlock->setAbsorbing(true); - secondBlock->setRepresentativeState(representativeProb1State.get()); - } - - storm::storage::BitVector otherStates = ~(prob0States | prob1States); - if (!otherStates.empty()) { - typename std::list::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, secondBlock, nullptr, numberOfBlocks++); - thirdBlock = &(*thirdIt); - thirdBlock->setIterator(thirdIt); - - for (auto state : otherStates) { - statesAndValues[position] = std::make_pair(state, storm::utility::zero()); - positions[state] = position; - stateToBlockMapping[state] = thirdBlock; - ++position; - } - } - - // If we are requested to store silent probabilities, we need to prepare the vector. - if (this->keepSilentProbabilities) { - silentProbabilities = std::vector(numberOfStates); - } - } - - template - 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 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; - - std::swap(this->statesAndValues[position1], this->statesAndValues[position2]); - - this->positions[state1] = position2; - this->positions[state2] = position1; - } - - template - storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition::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) { - this->positions[state] = position; - } - - template - storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition::Partition::getState(storm::storage::sparse::state_type position) const { - return this->statesAndValues[position].first; - } - - template - ValueType const& DeterministicModelBisimulationDecomposition::Partition::getValue(storm::storage::sparse::state_type state) const { - return this->statesAndValues[this->positions[state]].second; - } - - template - ValueType const& DeterministicModelBisimulationDecomposition::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const { - return this->statesAndValues[position].second; - } - - template - void DeterministicModelBisimulationDecomposition::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) { - this->statesAndValues[this->positions[state]].second = value; - } - - template - void DeterministicModelBisimulationDecomposition::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) { - this->statesAndValues[this->positions[state]].second += value; - } - - template - 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 DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Partition::getFirstBlock() { - return *this->blocks.begin(); - } - - template - typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::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 { - return *this->stateToBlockMapping[state]; - } - - template - typename std::vector>::iterator DeterministicModelBisimulationDecomposition::Partition::getBegin(Block const& block) { - return this->statesAndValues.begin() + block.getBegin(); - } - - template - typename std::vector>::iterator DeterministicModelBisimulationDecomposition::Partition::getEnd(Block const& block) { - return this->statesAndValues.begin() + block.getEnd(); - } - - template - typename std::vector>::const_iterator DeterministicModelBisimulationDecomposition::Partition::getBegin(Block const& block) const { - return this->statesAndValues.begin() + block.getBegin(); - } - - template - typename std::vector>::const_iterator DeterministicModelBisimulationDecomposition::Partition::getEnd(Block const& block) const { - return this->statesAndValues.begin() + block.getEnd(); - } - - template - 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()) { - return block; - } - - // 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, numberOfBlocks++); - selfIt->setIterator(selfIt); - Block& newBlock = *selfIt; - - // Resize the current block appropriately. - block.setBegin(position); - - // Update the mapping of the states in the newly created block. - this->updateBlockMapping(newBlock, this->getBegin(newBlock), this->getEnd(newBlock)); - - return newBlock; - } - - template - typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Partition::insertBlock(Block& block) { - // Find the beginning of the new block. - storm::storage::sparse::state_type begin; - if (block.hasPreviousBlock()) { - begin = block.getPreviousBlock().getEnd(); - } else { - begin = 0; - } - - // Actually insert the new block. - typename std::list::iterator it = this->blocks.emplace(block.getIterator(), begin, block.getBegin(), block.getPreviousBlockPointer(), &block, numberOfBlocks++); - Block& newBlock = *it; - newBlock.setIterator(it); - - // Update the mapping of the states in the newly created block. - for (auto it = this->getBegin(newBlock), ite = this->getEnd(newBlock); it != ite; ++it) { - stateToBlockMapping[it->first] = &newBlock; - } - - return *it; - } - - template - 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; - - // Sort the range of the block such that all states that have the label are moved to the front. - std::sort(this->getBegin(block), this->getEnd(block), [&statesWithLabel] (std::pair const& a, std::pair const& b) { return statesWithLabel.get(a.first) && !statesWithLabel.get(b.first); } ); - - // Update the positions vector. - storm::storage::sparse::state_type position = block.getBegin(); - for (auto stateIt = this->getBegin(block), stateIte = this->getEnd(block); stateIt != stateIte; ++stateIt, ++position) { - this->positions[stateIt->first] = position; - } - - // Now we can find the first position in the block that does not have the label and create new blocks. - typename std::vector>::iterator it = std::find_if(this->getBegin(block), this->getEnd(block), [&] (std::pair const& a) { return !statesWithLabel.get(a.first); }); - - // If not all the states agreed on the validity of the label, we need to split the block. - if (it != this->getBegin(block) && it != this->getEnd(block)) { - auto cutPoint = std::distance(this->statesAndValues.begin(), it); - this->splitBlock(block, cutPoint); - } else { - // Otherwise, we simply proceed to the next block. - ++blockIterator; - } - } - } - - template - 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 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& 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 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; - } - } - - template - 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(); - } - } - - template - 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& DeterministicModelBisimulationDecomposition::Partition::getBlocks() const { - return this->blocks; - } - - template - std::vector>& DeterministicModelBisimulationDecomposition::Partition::getStatesAndValues() { - return this->statesAndValues; - } - - template - std::list::Block>& DeterministicModelBisimulationDecomposition::Partition::getBlocks() { - return this->blocks; - } - - template - 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); - } - } - for (auto const& block : this->blocks) { - assert(block.check()); - for (auto stateIt = this->getBegin(block), stateIte = this->getEnd(block); stateIt != stateIte; ++stateIt) { - if (this->stateToBlockMapping[stateIt->first] != &block) { - assert(false); - } - } - } - return true; - } - - template - void DeterministicModelBisimulationDecomposition::Partition::print() const { - for (auto const& block : this->blocks) { - block.print(*this); - } - std::cout << "states in partition" << std::endl; - for (auto const& stateValue : statesAndValues) { - std::cout << stateValue.first << " "; - } - std::cout << std::endl << "positions: " << std::endl; - for (auto const& index : positions) { - std::cout << index << " "; - } - std::cout << std::endl << "state to block mapping: " << std::endl; - for (auto const& block : stateToBlockMapping) { - std::cout << block << "[" << block->getId() <<"] "; - } - std::cout << std::endl; - if (this->keepSilentProbabilities) { - std::cout << "silent probabilities" << std::endl; - for (auto const& prob : silentProbabilities) { - std::cout << prob << " "; - } - std::cout << std::endl; - } - std::cout << "size: " << numberOfBlocks << std::endl; - assert(this->check()); - } - - template - std::size_t DeterministicModelBisimulationDecomposition::Partition::size() const { - return numberOfBlocks; - } - - template - DeterministicModelBisimulationDecomposition::Options::Options(storm::models::sparse::Model const& model, storm::logic::Formula const& formula) : Options() { - this->preserveSingleFormula(model, formula); - } - - template - DeterministicModelBisimulationDecomposition::Options::Options(storm::models::sparse::Model const& model, std::vector> const& formulas) : Options() { - if (formulas.size() == 1) { - this->preserveSingleFormula(model, *formulas.front()); - } else { - for (auto const& formula : formulas) { - std::vector> atomicExpressionFormulas = formula->getAtomicExpressionFormulas(); - std::vector> atomicLabelFormulas = formula->getAtomicLabelFormulas(); - - std::set labelsToRespect; - for (auto const& labelFormula : atomicLabelFormulas) { - labelsToRespect.insert(labelFormula->getLabel()); - } - for (auto const& expressionFormula : atomicExpressionFormulas) { - std::stringstream stream; - stream << *expressionFormula; - labelsToRespect.insert(stream.str()); - } - if (!respectedAtomicPropositions) { - respectedAtomicPropositions = labelsToRespect; - } else { - respectedAtomicPropositions.get().insert(labelsToRespect.begin(), labelsToRespect.end()); - } - } - } - } - - template - DeterministicModelBisimulationDecomposition::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(true), weak(false), bounded(true), buildQuotient(true) { - // Intentionally left empty. - } - - template - void DeterministicModelBisimulationDecomposition::Options::preserveSingleFormula(storm::models::sparse::Model const& model, storm::logic::Formula const& formula) { - if (!formula.containsRewardOperator()) { - this->keepRewards = false; - } - - // As a tradeoff, we compute a strong bisimulation, because that is typically much faster. If the number of - // states is to be minimized, this should be set to weak by the calling site. - weak = false; - - // We need to preserve bounded properties iff the formula contains a bounded until or a next subformula. - bounded = formula.containsBoundedUntilFormula() || formula.containsNextFormula(); - - std::vector> atomicExpressionFormulas = formula.getAtomicExpressionFormulas(); - std::vector> atomicLabelFormulas = formula.getAtomicLabelFormulas(); - - std::set labelsToRespect; - for (auto const& labelFormula : atomicLabelFormulas) { - labelsToRespect.insert(labelFormula->getLabel()); - } - for (auto const& expressionFormula : atomicExpressionFormulas) { - std::stringstream stream; - stream << *expressionFormula; - labelsToRespect.insert(stream.str()); - } - respectedAtomicPropositions = labelsToRespect; - - std::shared_ptr newFormula = formula.asSharedPointer(); - - if (formula.isProbabilityOperatorFormula()) { - newFormula = formula.asProbabilityOperatorFormula().getSubformula().asSharedPointer(); - } else if (formula.isRewardOperatorFormula()) { - newFormula = formula.asRewardOperatorFormula().getSubformula().asSharedPointer(); - } - - std::shared_ptr leftSubformula = std::make_shared(true); - std::shared_ptr rightSubformula; - if (newFormula->isUntilFormula()) { - leftSubformula = newFormula->asUntilFormula().getLeftSubformula().asSharedPointer(); - rightSubformula = newFormula->asUntilFormula().getRightSubformula().asSharedPointer(); - if (leftSubformula->isPropositionalFormula() && rightSubformula->isPropositionalFormula()) { - measureDrivenInitialPartition = true; - } - } else if (newFormula->isEventuallyFormula()) { - rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer(); - if (rightSubformula->isPropositionalFormula()) { - measureDrivenInitialPartition = true; - } - } else if (newFormula->isReachabilityRewardFormula()) { - rightSubformula = newFormula->asReachabilityRewardFormula().getSubformula().asSharedPointer(); - if (rightSubformula->isPropositionalFormula()) { - measureDrivenInitialPartition = true; - } - } - - if (measureDrivenInitialPartition) { - storm::modelchecker::SparsePropositionalModelChecker> checker(model); - std::unique_ptr phiStatesCheckResult = checker.check(*leftSubformula); - std::unique_ptr psiStatesCheckResult = checker.check(*rightSubformula); - phiStates = phiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector(); - psiStates = psiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector(); - } - } - - template - DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::sparse::Dtmc const& model, Options const& options) { - STORM_LOG_THROW(!model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model."); - STORM_LOG_THROW(!model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls)."); - STORM_LOG_THROW(!options.weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties."); - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - BisimulationType bisimulationType = options.weak ? BisimulationType::WeakDtmc : BisimulationType::Strong; - - std::set atomicPropositions; - if (options.respectedAtomicPropositions) { - atomicPropositions = options.respectedAtomicPropositions.get(); - } else { - atomicPropositions = model.getStateLabeling().getLabels(); - } - - Partition initialPartition; - storm::utility::ConstantsComparator comparator; - if (options.measureDrivenInitialPartition) { - STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi states."); - STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without psi states."); - initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStates.get(), options.psiStates.get(), bisimulationType, options.keepRewards, options.bounded, comparator); - } else { - initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards, comparator); - } - - partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, options.keepRewards, options.buildQuotient, comparator); - } - - template - DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::sparse::Ctmc const& model, Options const& options) { - STORM_LOG_THROW(!model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model."); - STORM_LOG_THROW(!model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls)."); - STORM_LOG_THROW(!options.weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties."); - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - BisimulationType bisimulationType = options.weak ? BisimulationType::WeakCtmc : BisimulationType::Strong; - - std::set atomicPropositions; - if (options.respectedAtomicPropositions) { - atomicPropositions = options.respectedAtomicPropositions.get(); - } else { - atomicPropositions = model.getStateLabeling().getLabels(); - } - - Partition initialPartition; - storm::utility::ConstantsComparator comparator; - if (options.measureDrivenInitialPartition) { - STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states."); - STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states."); - initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStates.get(), options.psiStates.get(), bisimulationType, options.keepRewards, options.bounded, comparator); - } else { - initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards, comparator); - } - - partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, options.keepRewards, options.buildQuotient, comparator); - } - - template - 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 DeterministicModelBisimulationDecomposition::buildQuotient(ModelType const& model, std::set const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards, storm::utility::ConstantsComparator const& comparator) { - // In order to create the quotient model, we need to construct - // (a) the new transition matrix, - // (b) the new labeling, - // (c) the new reward structures. - - // Prepare a matrix builder for (a). - storm::storage::SparseMatrixBuilder builder(this->size(), this->size()); - - // Prepare the new state labeling for (b). - storm::models::sparse::StateLabeling newLabeling(this->size()); - std::set atomicPropositionsSet = selectedAtomicPropositions; - atomicPropositionsSet.insert("init"); - std::vector atomicPropositions = std::vector(atomicPropositionsSet.begin(), atomicPropositionsSet.end()); - for (auto const& ap : atomicPropositions) { - newLabeling.addLabel(ap); - } - - // If the model had state rewards, we need to build the state rewards for the quotient as well. - boost::optional> stateRewards; - if (keepRewards && model.hasRewardModel()) { - stateRewards = std::vector(this->blocks.size()); - } - - // Now build (a) and (b) by traversing all blocks. - for (uint_fast64_t blockIndex = 0; blockIndex < this->blocks.size(); ++blockIndex) { - auto const& block = this->blocks[blockIndex]; - - // Pick one representative state. For strong bisimulation it doesn't matter which state it is, because - // they all behave equally. - 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 - // there is any such state). - if (bisimulationType == BisimulationType::WeakDtmc) { - for (auto const& state : block) { - if (!partition.isSilent(state, comparator)) { - representativeState = state; - break; - } - } - } - - Block const& oldBlock = partition.getBlock(representativeState); - - // If the block is absorbing, we simply add a self-loop. - if (oldBlock.isAbsorbing()) { - builder.addNextValue(blockIndex, blockIndex, storm::utility::one()); - - // If the block has a special representative state, we retrieve it now. - if (oldBlock.hasRepresentativeState()) { - representativeState = oldBlock.getRepresentativeState(); - } - - // Add all of the selected atomic propositions that hold in the representative state to the state - // representing the block. - for (auto const& ap : atomicPropositions) { - if (model.getStateLabeling().getStateHasLabel(ap, representativeState)) { - newLabeling.addLabelToState(ap, 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(); - - // If we are computing a weak bisimulation quotient, there is no need to add self-loops. - if ((bisimulationType == BisimulationType::WeakDtmc || bisimulationType == BisimulationType::WeakCtmc) && targetBlock == blockIndex) { - continue; - } - - 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) { - 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); - } - } - - // Otherwise add all atomic propositions to the equivalence class that the representative state - // satisfies. - for (auto const& ap : atomicPropositions) { - if (model.getStateLabeling().getStateHasLabel(ap, representativeState)) { - newLabeling.addLabelToState(ap, blockIndex); - } - } - } - - // If the model has state rewards, we simply copy the state reward of the representative state, because - // all states in a block are guaranteed to have the same state reward. - if (keepRewards && model.hasRewardModel()) { - typename std::unordered_map::const_iterator nameRewardModelPair = model.getUniqueRewardModel(); - stateRewards.get()[blockIndex] = nameRewardModelPair->second.getStateRewardVector()[representativeState]; - } - } - - // Now check which of the blocks of the partition contain at least one initial state. - for (auto initialState : model.getInitialStates()) { - Block const& initialBlock = partition.getBlock(initialState); - newLabeling.addLabelToState("init", initialBlock.getId()); - } - - // Construct the reward model mapping. - std::unordered_map rewardModels; - if (keepRewards && model.hasRewardModel()) { - typename std::unordered_map::const_iterator nameRewardModelPair = model.getUniqueRewardModel(); - rewardModels.insert(std::make_pair(nameRewardModelPair->first, typename ModelType::RewardModelType(stateRewards))); - } - - // Finally construct the quotient model. - this->quotient = std::shared_ptr>(new ModelType(builder.build(), std::move(newLabeling), std::move(rewardModels))); - } - - template - template - void DeterministicModelBisimulationDecomposition::partitionRefinement(ModelType const& model, std::set const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient, storm::utility::ConstantsComparator const& comparator) { - 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. - std::chrono::high_resolution_clock::time_point refinementStart = std::chrono::high_resolution_clock::now(); - std::deque splitterQueue; - std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); a.markAsSplitter(); }); - - // Then perform the actual splitting until there are no more splitters. - while (!splitterQueue.empty()) { - // Optionally: sort the splitter queue according to some criterion (here: prefer small splitters). - std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates() || (b1->getNumberOfStates() == b2->getNumberOfStates() && b1->getId() < b2->getId()); } ); - std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } ); - - // Get and prepare the next splitter. - Block* splitter = splitterQueue.front(); - splitterQueue.pop_front(); - splitter->unmarkAsSplitter(); - - // Now refine the partition using the current splitter. - refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitter, partition, bisimulationType, splitterQueue, comparator); - } - std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart; - - // Now move the states from the internal partition into their final place in the decomposition. We do so in - // a way that maintains the block IDs as indices. - std::chrono::high_resolution_clock::time_point extractionStart = std::chrono::high_resolution_clock::now(); - 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.getBegin(block), partition.getEnd(block), [] (std::pair const& a, std::pair const& b) { return a.first < b.first; }); - - // Convert the state-value-pairs to states only. - std::function const&)> projection = [] (std::pair const& a) -> storm::storage::sparse::state_type { return a.first; }; - this->blocks[block.getId()] = block_type(boost::make_transform_iterator(partition.getBegin(block), projection), boost::make_transform_iterator(partition.getEnd(block), projection), true); - } - - // If we are required to build the quotient model, do so now. - if (buildQuotient) { - this->buildQuotient(model, atomicPropositions, partition, bisimulationType, keepRewards, comparator); - } - - std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart; - std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart; - - if (storm::settings::generalSettings().isShowStatisticsSet()) { - std::chrono::milliseconds refinementTimeInMilliseconds = std::chrono::duration_cast(refinementTime); - std::chrono::milliseconds extractionTimeInMilliseconds = std::chrono::duration_cast(extractionTime); - std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast(totalTime); - std::cout << std::endl; - std::cout << "Time breakdown:" << std::endl; - std::cout << " * time for partitioning: " << refinementTimeInMilliseconds.count() << "ms" << std::endl; - std::cout << " * time for extraction: " << extractionTimeInMilliseconds.count() << "ms" << std::endl; - std::cout << "------------------------------------------" << std::endl; - std::cout << " * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl; - std::cout << std::endl; - } - } - - template - void DeterministicModelBisimulationDecomposition::refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator) { - // 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; } ); - - // 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, we need to scan the ranges of states that agree on the probability. - typename std::vector>::const_iterator begin = partition.getBegin(block); - typename std::vector>::const_iterator end = partition.getEnd(block) - 1; - storm::storage::sparse::state_type currentIndex = block.getBegin(); - - // 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. - bool blockSplit = !comparator.isEqual(begin->second, end->second); - while (!comparator.isEqual(begin->second, end->second)) { - // 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. - ValueType const& currentValue = begin->second; - - ++begin; - ++currentIndex; - while (begin != end && comparator.isEqual(begin->second, currentValue)) { - ++begin; - ++currentIndex; - } - - // Now we split the block and mark it as a potential splitter. - Block& newBlock = partition.splitBlock(block, currentIndex); - if (!newBlock.isMarkedAsSplitter()) { - splitterQueue.push_back(&newBlock); - newBlock.markAsSplitter(); - } - } - - // If the block was split, we also need to insert itself into the splitter queue. - if (blockSplit) { - if (!block.isMarkedAsSplitter()) { - splitterQueue.push_back(&block); - block.markAsSplitter(); - } - } - } - - template - void DeterministicModelBisimulationDecomposition::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator) { - std::vector splitPoints = getSplitPointsWeak(block, partition, comparator); - - // Restore the original begin of the block. - block.setBegin(block.getOriginalBegin()); - - // Now that we have the split points of the non-silent states, we perform a backward search from - // each non-silent state and label the predecessors with the class of the non-silent state. - std::vector stateLabels(block.getEnd() - block.getBegin(), storm::storage::BitVector(splitPoints.size() - 1)); - - std::vector stateStack; - stateStack.reserve(block.getEnd() - block.getBegin()); - for (uint_fast64_t stateClassIndex = 0; stateClassIndex < splitPoints.size() - 1; ++stateClassIndex) { - for (auto stateIt = partition.getStatesAndValues().begin() + splitPoints[stateClassIndex], stateIte = partition.getStatesAndValues().begin() + splitPoints[stateClassIndex + 1]; stateIt != stateIte; ++stateIt) { - - stateStack.push_back(stateIt->first); - stateLabels[partition.getPosition(stateIt->first) - block.getBegin()].set(stateClassIndex); - while (!stateStack.empty()) { - storm::storage::sparse::state_type currentState = stateStack.back(); - stateStack.pop_back(); - - for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { - if (comparator.isZero(predecessorEntry.getValue())) { - continue; - } - - storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); - - // Only if the state is in the same block, is a silent state and it has not yet been - // labeled with the current label. - if (&partition.getBlock(predecessor) == &block && partition.isSilent(predecessor, comparator) && !stateLabels[partition.getPosition(predecessor) - block.getBegin()].get(stateClassIndex)) { - stateStack.push_back(predecessor); - stateLabels[partition.getPosition(predecessor) - block.getBegin()].set(stateClassIndex); - } - } - } - } - } - - // Now that all states were appropriately labeled, we can sort the states according to their labels and then - // scan for ranges that agree on the label. - std::sort(partition.getBegin(block), partition.getEnd(block), [&] (std::pair const& a, std::pair const& b) { return stateLabels[partition.getPosition(a.first) - block.getBegin()] < stateLabels[partition.getPosition(b.first) - block.getBegin()]; }); - - // Note that we do not yet repair the positions vector, but for the sake of efficiency temporariliy keep the - // data structure in an inconsistent state. - - // Now we have everything in place to actually split the block by just scanning for ranges of equal label. - typename std::vector>::const_iterator begin = partition.getBegin(block); - typename std::vector>::const_iterator end = partition.getEnd(block) - 1; - storm::storage::sparse::state_type currentIndex = block.getBegin(); - - // Now we can check whether the block needs to be split, which is the case iff the labels for the first and - // the last state are different. Store the offset of the block seperately, because it will potentially - // modified by splits. - storm::storage::sparse::state_type blockOffset = block.getBegin(); - bool blockSplit = stateLabels[partition.getPosition(begin->first) - blockOffset] != stateLabels[partition.getPosition(end->first) - blockOffset]; - while (stateLabels[partition.getPosition(begin->first) - blockOffset] != stateLabels[partition.getPosition(end->first) - blockOffset]) { - // Now we scan for the first state in the block that disagrees on the labeling value. - // Note that we do not have to check currentIndex for staying within bounds, because we know the matching - // state is within bounds. - storm::storage::BitVector const& currentValue = stateLabels[partition.getPosition(begin->first) - blockOffset]; - - ++begin; - ++currentIndex; - while (begin != end && stateLabels[partition.getPosition(begin->first) - blockOffset] == currentValue) { - ++begin; - ++currentIndex; - } - - // Now we split the block and mark it as a potential splitter. - Block& newBlock = partition.splitBlock(block, currentIndex); - - // Update the silent probabilities for all the states in the new block. - for (auto stateIt = partition.getBegin(newBlock), stateIte = partition.getEnd(newBlock); stateIt != stateIte; ++stateIt) { - if (partition.hasSilentProbability(stateIt->first, comparator)) { - ValueType newSilentProbability = storm::utility::zero(); - for (auto const& successorEntry : forwardTransitions.getRow(stateIt->first)) { - if (&partition.getBlock(successorEntry.getColumn()) == &newBlock) { - newSilentProbability += successorEntry.getValue(); - } - } - partition.setSilentProbability(stateIt->first, newSilentProbability); - } - } - - if (!newBlock.isMarkedAsSplitter()) { - splitterQueue.push_back(&newBlock); - newBlock.markAsSplitter(); - } - } - - // If the block was split, we also need to insert itself into the splitter queue. - if (blockSplit) { - if (!block.isMarkedAsSplitter()) { - splitterQueue.push_back(&block); - block.markAsSplitter(); - } - - // Update the silent probabilities for all the states in the old block. - for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt) { - if (partition.hasSilentProbability(stateIt->first, comparator)) { - ValueType newSilentProbability = storm::utility::zero(); - for (auto const& successorEntry : forwardTransitions.getRow(stateIt->first)) { - if (&partition.getBlock(successorEntry.getColumn()) == &block) { - newSilentProbability += successorEntry.getValue(); - } - } - partition.setSilentProbability(stateIt->first, newSilentProbability); - } - } - } - - // Finally update the positions vector. - storm::storage::sparse::state_type position = blockOffset; - for (auto stateIt = partition.getStatesAndValues().begin() + blockOffset, stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) { - partition.setPosition(stateIt->first, position); - } - } - - template - std::vector DeterministicModelBisimulationDecomposition::getSplitPointsWeak(Block& block, Partition& partition, storm::utility::ConstantsComparator const& comparator) { - 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) { - ValueType const& silentProbability = partition.getSilentProbability(stateValuePair.first); - if (!comparator.isOne(silentProbability) && !comparator.isZero(silentProbability)) { - stateValuePair.second /= storm::utility::one() - silentProbability; - } - }); - - // Now sort the states based on their probabilities. - std::sort(partition.getStatesAndValues().begin() + block.getOriginalBegin(), partition.getStatesAndValues().begin() + block.getBegin(), [&partition] (std::pair const& a, std::pair const& b) { return a.second < b.second; } ); - - // Update the positions vector. - storm::storage::sparse::state_type position = block.getOriginalBegin(); - for (auto stateIt = partition.getStatesAndValues().begin() + block.getOriginalBegin(), stateIte = partition.getStatesAndValues().begin() + block.getBegin(); stateIt != stateIte; ++stateIt, ++position) { - partition.setPosition(stateIt->first, position); - } - - // Then, we scan for the ranges of states that agree on the probability. - typename std::vector>::const_iterator begin = partition.getStatesAndValues().begin() + block.getOriginalBegin(); - typename std::vector>::const_iterator end = partition.getStatesAndValues().begin() + block.getBegin() - 1; - storm::storage::sparse::state_type currentIndex = block.getOriginalBegin(); - result.push_back(currentIndex); - - // 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. - while (!comparator.isEqual(begin->second, end->second)) { - // 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. - ValueType const& currentValue = begin->second; - - ++begin; - ++currentIndex; - while (begin != end && comparator.isEqual(begin->second, currentValue)) { - ++begin; - ++currentIndex; - } - - // Remember the index at which the probabilities were different. - result.push_back(currentIndex); - } - - // Push a sentinel element and return result. - result.push_back(block.getBegin()); - return result; - } - - template - void DeterministicModelBisimulationDecomposition::refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator) { - std::list predecessorBlocks; - - // Iterate over all states of the splitter and check its predecessors. - bool splitterIsPredecessor = false; - storm::storage::sparse::state_type currentPosition = splitter.getBegin(); - for (auto stateIterator = partition.getBegin(splitter), stateIte = partition.getEnd(splitter); stateIterator != stateIte; ++stateIterator, ++currentPosition) { - storm::storage::sparse::state_type currentState = stateIterator->first; - - uint_fast64_t elementsToSkip = 0; - for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { - storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); - - // Get predecessor block and remember if the splitter was a predecessor of itself. - Block& predecessorBlock = partition.getBlock(predecessor); - if (&predecessorBlock == &splitter) { - splitterIsPredecessor = true; - } - - // If the predecessor block has just one state or is marked as being absorbing, we must not split it. - if (predecessorBlock.getNumberOfStates() <= 1 || predecessorBlock.isAbsorbing()) { - continue; - } - - storm::storage::sparse::state_type predecessorPosition = partition.getPosition(predecessor); - - // If we have not seen this predecessor before, we move it to a part near the beginning of the block. - if (predecessorPosition >= predecessorBlock.getBegin()) { - if (&predecessorBlock == &splitter) { - // If the predecessor we just found was already processed (in terms of visiting its predecessors), - // we swap it with the state that is currently at the beginning of the block and move the start - // of the block one step further. - if (predecessorPosition <= currentPosition + elementsToSkip) { - partition.swapStates(predecessor, partition.getState(predecessorBlock.getBegin())); - predecessorBlock.incrementBegin(); - } else { - // Otherwise, we need to move the predecessor, but we need to make sure that we explore its - // predecessors later. - if (predecessorBlock.getMarkedPosition() == predecessorBlock.getBegin()) { - partition.swapStatesAtPositions(predecessorBlock.getMarkedPosition(), predecessorPosition); - partition.swapStatesAtPositions(predecessorPosition, currentPosition + elementsToSkip + 1); - } else { - partition.swapStatesAtPositions(predecessorBlock.getMarkedPosition(), predecessorPosition); - partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.getBegin()); - partition.swapStatesAtPositions(predecessorPosition, currentPosition + elementsToSkip + 1); - } - - ++elementsToSkip; - predecessorBlock.incrementMarkedPosition(); - predecessorBlock.incrementBegin(); - } - } else { - partition.swapStates(predecessor, partition.getState(predecessorBlock.getBegin())); - predecessorBlock.incrementBegin(); - } - partition.setValue(predecessor, predecessorEntry.getValue()); - } else { - // Otherwise, we just need to update the probability for this predecessor. - partition.increaseValue(predecessor, predecessorEntry.getValue()); - } - - if (!predecessorBlock.isMarkedAsPredecessor()) { - predecessorBlocks.emplace_back(&predecessorBlock); - predecessorBlock.markAsPredecessorBlock(); - } - } - - // If we had to move some elements beyond the current element, we may have to skip them. - if (elementsToSkip > 0) { - stateIterator += elementsToSkip; - currentPosition += elementsToSkip; - } - } - - // Now we can traverse the list of states of the splitter whose predecessors we have not yet explored. - for (auto stateIterator = partition.getStatesAndValues().begin() + splitter.getOriginalBegin(), stateIte = partition.getStatesAndValues().begin() + splitter.getMarkedPosition(); stateIterator != stateIte; ++stateIterator) { - storm::storage::sparse::state_type currentState = stateIterator->first; - - for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { - storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); - Block& predecessorBlock = partition.getBlock(predecessor); - storm::storage::sparse::state_type predecessorPosition = partition.getPosition(predecessor); - - if (predecessorPosition >= predecessorBlock.getBegin()) { - partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.getBegin()); - predecessorBlock.incrementBegin(); - partition.setValue(predecessor, predecessorEntry.getValue()); - } else { - partition.increaseValue(predecessor, predecessorEntry.getValue()); - } - - if (!predecessorBlock.isMarkedAsPredecessor()) { - predecessorBlocks.emplace_back(&predecessorBlock); - predecessorBlock.markAsPredecessorBlock(); - } - } - } - - if (bisimulationType == BisimulationType::Strong || bisimulationType == BisimulationType::WeakCtmc) { - std::vector blocksToSplit; - - // Now, we can iterate over the predecessor blocks and see whether we have to create a new block for - // predecessors of the splitter. - for (auto blockPtr : predecessorBlocks) { - Block& block = *blockPtr; - - block.unmarkAsPredecessorBlock(); - block.resetMarkedPosition(); - - // If we have moved the begin of the block to somewhere in the middle of the block, we need to split it. - if (block.getBegin() != block.getEnd()) { - Block& newBlock = partition.insertBlock(block); - if (!newBlock.isMarkedAsSplitter()) { - splitterQueue.push_back(&newBlock); - newBlock.markAsSplitter(); - } - - // Schedule the block of predecessors for refinement based on probabilities. - blocksToSplit.emplace_back(&newBlock); - } else { - // In this case, we can keep the block by setting its begin to the old value. - block.setBegin(block.getOriginalBegin()); - blocksToSplit.emplace_back(&block); - } - } - - // Finally, we walk through the blocks that have a transition to the splitter and split them using - // probabilistic information. - for (auto blockPtr : blocksToSplit) { - if (blockPtr->getNumberOfStates() <= 1) { - continue; - } - - // 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, comparator); - } - } 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) { - partition.setSilentProbabilities(partition.getStatesAndValues().begin() + splitter.getOriginalBegin(), partition.getStatesAndValues().begin() + splitter.getBegin()); - partition.setSilentProbabilitiesToZero(partition.getStatesAndValues().begin() + splitter.getBegin(), partition.getStatesAndValues().begin() + splitter.getEnd()); - } - - // Now refine all predecessor blocks in a weak manner. That is, we split according to the criterion of - // weak bisimulation. - for (auto blockPtr : predecessorBlocks) { - Block& block = *blockPtr; - - // If the splitter is also the predecessor block, we must not refine it at this point. - if (&block != &splitter) { - refineBlockWeak(block, partition, forwardTransitions, backwardTransitions, splitterQueue, comparator); - } else { - // Restore the begin of the block. - block.setBegin(block.getOriginalBegin()); - } - - block.unmarkAsPredecessorBlock(); - block.resetMarkedPosition(); - } - } - - STORM_LOG_ASSERT(partition.check(), "Partition became inconsistent."); - } - - template - template - typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, BisimulationType bisimulationType, bool keepRewards, bool bounded, storm::utility::ConstantsComparator const& comparator) { - std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); - - boost::optional representativePsiState; - if (!psiStates.empty()) { - representativePsiState = *psiStates.begin(); - } - - Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded || keepRewards ? psiStates : statesWithProbability01.second, representativePsiState, bisimulationType == BisimulationType::WeakDtmc); - - // If the model has state rewards, we need to consider them, because otherwise reward properties are not - // preserved. - if (keepRewards && model.hasRewardModel()) { - this->splitRewards(model.getUniqueRewardModel()->second.getStateRewardVector(), partition, comparator); - } - - // 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 (bisimulationType == BisimulationType::WeakDtmc) { - this->splitOffDivergentStates(model, backwardTransitions, partition); - this->initializeSilentProbabilities(model, partition); - } - - return partition; - } - - template - template - 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; - } - - // 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); - - 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()); - } - } - } - } - } - - - 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. - 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); - } - } - } - - template - template - typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType, boost::optional> const& atomicPropositions, bool keepRewards, storm::utility::ConstantsComparator const& comparator) { - Partition partition(model.getNumberOfStates(), bisimulationType == BisimulationType::WeakDtmc); - - if (atomicPropositions) { - for (auto const& label : atomicPropositions.get()) { - if (label == "init") { - continue; - } - partition.splitLabel(model.getStates(label)); - } - } else { - for (auto const& label : model.getStateLabeling().getLabels()) { - if (label == "init") { - continue; - } - partition.splitLabel(model.getStates(label)); - } - } - - // If the model has state rewards, we need to consider them, because otherwise reward properties are not - // preserved. - if (keepRewards && model.hasRewardModel()) { - this->splitRewards(model.getUniqueRewardModel()->second.getStateRewardVector(), partition, comparator); - } - - // 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 (bisimulationType == BisimulationType::WeakDtmc) { - this->splitOffDivergentStates(model, backwardTransitions, partition); - this->initializeSilentProbabilities(model, partition); - } - return partition; - } - - template - template - 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(); - - for (auto const& successorEntry : model.getRows(stateIt->first)) { - if (&partition.getBlock(successorEntry.getColumn()) == &block) { - silentProbability += successorEntry.getValue(); - } - } - - partition.setSilentProbability(stateIt->first, silentProbability); - } - } - } - - template - void DeterministicModelBisimulationDecomposition::splitRewards(std::vector const& stateRewardVector, Partition& partition, storm::utility::ConstantsComparator const& comparator) { - for (auto& block : partition.getBlocks()) { - std::sort(partition.getBegin(block), partition.getEnd(block), [&stateRewardVector] (std::pair const& a, std::pair const& b) { return stateRewardVector[a.first] < stateRewardVector[b.first]; } ); - - // Update the positions vector and put the (state) reward values next to the states so we can easily compare them later. - 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); - stateIt->second = stateRewardVector[stateIt->first]; - } - - // Finally, we need to scan the ranges of states that agree on the probability. - typename std::vector>::const_iterator begin = partition.getBegin(block); - typename std::vector>::const_iterator end = partition.getEnd(block) - 1; - storm::storage::sparse::state_type currentIndex = block.getBegin(); - - // Now we can check whether the block needs to be split, which is the case iff the rewards for the first - // and the last state are different. - while (!comparator.isEqual(begin->second, end->second)) { - // Now we scan for the first state in the block that disagrees on the reward value. Note that we do - // not have to check currentIndex for staying within bounds, because we know the matching state is - // within bounds. - ValueType const& currentValue = begin->second; - - ++begin; - ++currentIndex; - while (begin != end && comparator.isEqual(begin->second, currentValue)) { - ++begin; - ++currentIndex; - } - - // Now we split the block. - partition.splitBlock(block, currentIndex); - } - } - } - - template class DeterministicModelBisimulationDecomposition; - -#ifdef STORM_HAVE_CARL - template class DeterministicModelBisimulationDecomposition; -#endif - } -} diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h deleted file mode 100644 index d66591f76..000000000 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ /dev/null @@ -1,590 +0,0 @@ -#ifndef STORM_STORAGE_DeterministicModelBisimulationDecomposition_H_ -#define STORM_STORAGE_DeterministicModelBisimulationDecomposition_H_ - -#include -#include - -#include "src/storage/sparse/StateType.h" -#include "src/storage/Decomposition.h" -#include "src/storage/StateBlock.h" -#include "src/logic/Formulas.h" -#include "src/models/sparse/Dtmc.h" -#include "src/models/sparse/Ctmc.h" -#include "src/storage/Distribution.h" -#include "src/utility/constants.h" -#include "src/utility/OsDetection.h" -#include "src/exceptions/InvalidOperationException.h" - -namespace storm { - namespace utility { - template class ConstantsComparator; - } - - namespace storage { - - /*! - * This class represents the decomposition model into its (strong) bisimulation quotient. - */ - template - class DeterministicModelBisimulationDecomposition : public Decomposition { - public: - // A class that offers the possibility to customize the bisimulation. - struct Options { - // Creates an object representing the default values for all options. - Options(); - - /*! - * Creates an object representing the options necessary to obtain the quotient while still preserving - * the given formula. - * - * @param The model for which the quotient model shall be computed. This needs to be given in order to - * derive a suitable initial partition. - * @param formula The formula that is to be preserved. - */ - Options(storm::models::sparse::Model const& model, storm::logic::Formula const& formula); - - /*! - * Creates an object representing the options necessary to obtain the smallest quotient while still - * preserving the given formula. - * - * @param The model for which the quotient model shall be computed. This needs to be given in order to - * derive a suitable initial partition. - * @param formulas The formula that is to be preserved. - */ - Options(storm::models::sparse::Model const& model, std::vector> const& formulas); - - // A flag that indicates whether a measure driven initial partition is to be used. If this flag is set - // to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the - // measure driven initial partition wrt. to the states phi and psi is taken. - bool measureDrivenInitialPartition; - boost::optional phiStates; - boost::optional psiStates; - - // An optional set of strings that indicate which of the atomic propositions of the model are to be - // respected and which may be ignored. If not given, all atomic propositions of the model are respected. - boost::optional> respectedAtomicPropositions; - - // A flag that indicates whether or not the state-rewards of the model are to be respected (and should - // be kept in the quotient model, if one is built). - bool keepRewards; - - // A flag that indicates whether a strong or a weak bisimulation is to be computed. - bool weak; - - // A flag that indicates whether step-bounded properties are to be preserved. This may only be set to tru - // when computing strong bisimulation equivalence. - bool bounded; - - // A flag that governs whether the quotient model is actually built or only the decomposition is computed. - bool buildQuotient; - - private: - /*! - * Sets the options under the assumption that the given formula is the only one that is to be checked. - * - * @param model The model for which to preserve the formula. - * @param formula The only formula to check. - */ - void preserveSingleFormula(storm::models::sparse::Model const& model, storm::logic::Formula const& formula); - }; - - /*! - * Decomposes the given DTMC into equivalance classes of a bisimulation. Which kind of bisimulation is - * computed, is customizable via the given options. - * - * @param model The model to decompose. - * @param options The options that customize the computed bisimulation. - */ - DeterministicModelBisimulationDecomposition(storm::models::sparse::Dtmc const& model, Options const& options = Options()); - - /*! - * Decomposes the given CTMC into equivalance classes of a bisimulation. Which kind of bisimulation is - * computed, is customizable via the given options. - * - * @param model The model to decompose. - * @param options The options that customize the computed bisimulation. - */ - DeterministicModelBisimulationDecomposition(storm::models::sparse::Ctmc const& model, Options const& options = Options()); - - /*! - * Retrieves the quotient of the model under the previously computed bisimulation. - * - * @return The quotient model. - */ - std::shared_ptr> getQuotient() const; - - private: - enum class BisimulationType { Strong, WeakDtmc, WeakCtmc }; - - class Partition; - - class Block { - public: - typedef typename std::list::iterator iterator; - typedef typename std::list::const_iterator const_iterator; - - // Creates a new block with the given begin and end. - Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id); - - // Prints the block. - void print(Partition const& partition) const; - - // Sets the beginning index of the block. - void setBegin(storm::storage::sparse::state_type begin); - - // Moves the beginning index of the block one step further. - void incrementBegin(); - - // Sets the end index of the block. - void setEnd(storm::storage::sparse::state_type end); - - // Returns the beginning index of the block. - storm::storage::sparse::state_type getBegin() const; - - // Returns the beginning index of the block. - storm::storage::sparse::state_type getEnd() const; - - // Retrieves the original beginning index of the block in case the begin index has been moved. - storm::storage::sparse::state_type getOriginalBegin() const; - - // Returns the iterator the block in the list of overall blocks. - iterator getIterator() const; - - // Returns the iterator the block in the list of overall blocks. - void setIterator(iterator it); - - // Returns the iterator the next block in the list of overall blocks if it exists. - iterator getNextIterator() const; - - // Returns the iterator the next block in the list of overall blocks if it exists. - iterator getPreviousIterator() const; - - // Gets the next block (if there is one). - Block& getNextBlock(); - - // Gets the next block (if there is one). - Block const& getNextBlock() const; - - // Gets a pointer to the next block (if there is one). - Block* getNextBlockPointer(); - - // Retrieves whether the block as a successor block. - bool hasNextBlock() const; - - // Gets the previous block (if there is one). - Block& getPreviousBlock(); - - // Gets a pointer to the previous block (if there is one). - Block* getPreviousBlockPointer(); - - // Gets the next block (if there is one). - Block const& getPreviousBlock() const; - - // Retrieves whether the block as a successor block. - bool hasPreviousBlock() const; - - // Checks consistency of the information in the block. - bool check() const; - - // Retrieves the number of states in this block. - std::size_t getNumberOfStates() const; - - // Checks whether the block is marked as a splitter. - bool isMarkedAsSplitter() const; - - // Marks the block as being a splitter. - void markAsSplitter(); - - // Removes the mark. - void unmarkAsSplitter(); - - // Retrieves the ID of the block. - std::size_t getId() const; - - // Retrieves the marked position in the block. - storm::storage::sparse::state_type getMarkedPosition() const; - - // Sets the marked position to the given value.. - void setMarkedPosition(storm::storage::sparse::state_type position); - - // Increases the marked position by one. - void incrementMarkedPosition(); - - // Resets the marked position to the begin of the block. - void resetMarkedPosition(); - - // Retrieves whether the block is marked as a predecessor. - bool isMarkedAsPredecessor() const; - - // Marks the block as being a predecessor block. - void markAsPredecessorBlock(); - - // 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; - - // Sets the representative state of this block - void setRepresentativeState(storm::storage::sparse::state_type representativeState); - - // Retrieves the representative state for this block. - bool hasRepresentativeState() const; - - // Retrieves the representative state for this block. - storm::storage::sparse::state_type getRepresentativeState() const; - - private: - // An iterator to itself. This is needed to conveniently insert elements in the overall list of blocks - // kept by the partition. - iterator selfIt; - - // Pointers to the next and previous block. - Block* next; - Block* prev; - - // The begin and end indices of the block in terms of the state vector of the partition. - storm::storage::sparse::state_type begin; - storm::storage::sparse::state_type end; - - // A field that can be used for marking the block. - bool markedAsSplitter; - - // A field that can be used for marking the block as a predecessor block. - bool markedAsPredecessorBlock; - - // 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; - - // 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. - boost::optional representativeState; - }; - - class Partition { - public: - friend class Block; - - /*! - * Creates a partition with one block consisting of all the states. - * - * @param numberOfStates The number of states the partition holds. - * @param keepSilentProbabilities A flag indicating whether or not silent probabilities are to be tracked. - */ - Partition(std::size_t numberOfStates, bool keepSilentProbabilities = false); - - /*! - * 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 representativeProb1State If the set of prob1States is non-empty, this needs to be a state - * that is representative for this block in the sense that the state representing this block in the quotient - * model will receive exactly the atomic propositions of the representative state. - * @param keepSilentProbabilities A flag indicating whether or not silent probabilities are to be tracked. - */ - Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, boost::optional representativeProb1State, bool keepSilentProbabilities = false); - - Partition() = default; - Partition(Partition const& other) = default; - Partition& operator=(Partition const& other) = default; - - // Define move-construct and move-assignment explicitly to make sure they exist (as they are vital to - // keep validity of pointers. - Partition(Partition&& other) : blocks(std::move(other.blocks)), numberOfBlocks(other.numberOfBlocks), stateToBlockMapping(std::move(other.stateToBlockMapping)), statesAndValues(std::move(other.statesAndValues)), positions(std::move(other.positions)), keepSilentProbabilities(other.keepSilentProbabilities), silentProbabilities(std::move(other.silentProbabilities)) { - // Intentionally left empty. - } - - Partition& operator=(Partition&& other) { - if (this != &other) { - blocks = std::move(other.blocks); - numberOfBlocks = other.numberOfBlocks; - stateToBlockMapping = std::move(other.stateToBlockMapping); - statesAndValues = std::move(other.statesAndValues); - positions = std::move(other.positions); - keepSilentProbabilities = other.keepSilentProbabilities; - silentProbabilities = std::move(other.silentProbabilities); - } - - return *this; - } - - /*! - * Splits all blocks of the partition such that afterwards all blocks contain only states with the label - * or no labeled state at all. - */ - void splitLabel(storm::storage::BitVector const& statesWithLabel); - - // Retrieves the size of the partition, i.e. the number of blocks. - std::size_t size() const; - - // Prints the partition to the standard output. - void print() const; - - // Splits the block at the given position and inserts a new block after the current one holding the rest - // of the states. - Block& splitBlock(Block& block, storm::storage::sparse::state_type position); - - // 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); - - // Retrieves the blocks of the partition. - std::list const& getBlocks() const; - - // Retrieves the blocks of the partition. - std::list& getBlocks(); - - // Checks the partition for internal consistency. - bool check() const; - - // Returns an iterator to the beginning of the states of the given block. - typename std::vector>::iterator getBegin(Block const& block); - - // Returns an iterator to the beginning of the states of the given block. - typename std::vector>::iterator getEnd(Block const& block); - - // Returns an iterator to the beginning of the states of the given block. - typename std::vector>::const_iterator getBegin(Block const& block) const; - - // Returns an iterator to the beginning of the states of the given block. - typename std::vector>::const_iterator getEnd(Block const& block) const; - - // Swaps the positions of the two given states. - void swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2); - - // Swaps the positions of the two states given by their positions. - void swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2); - - // Retrieves the block of the given state. - Block& getBlock(storm::storage::sparse::state_type state); - - // Retrieves the block of the given state. - Block const& getBlock(storm::storage::sparse::state_type state) const; - - // Retrieves the position of the given state. - storm::storage::sparse::state_type const& getPosition(storm::storage::sparse::state_type state) const; - - // Retrieves the position of the given state. - void setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position); - - // Sets the position of the state to the given position. - storm::storage::sparse::state_type const& getState(storm::storage::sparse::state_type position) const; - - // Retrieves the value for the given state. - ValueType const& getValue(storm::storage::sparse::state_type state) const; - - // Retrieves the value at the given position. - ValueType const& getValueAtPosition(storm::storage::sparse::state_type position) const; - - // Sets the given value for the given state. - void setValue(storm::storage::sparse::state_type state, ValueType value); - - // Retrieves the vector with the probabilities going into the current splitter. - std::vector>& getStatesAndValues(); - - // Increases the value for the given state by the specified amount. - void increaseValue(storm::storage::sparse::state_type state, ValueType value); - - // Updates the block mapping for the given range of states to the specified block. - void updateBlockMapping(Block& block, typename std::vector>::iterator first, typename std::vector>::iterator last); - - // Retrieves the first block of the partition. - Block& getFirstBlock(); - - // Retrieves whether the given state is fully silent (only in case the silent probabilities are tracked). - bool isSilent(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator const& comparator) const; - - // Retrieves whether the given state has a non-zero silent probability. - bool hasSilentProbability(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator const& comparator) const; - - // Retrieves the silent probability (i.e. the probability to stay within the own equivalence class). - ValueType const& getSilentProbability(storm::storage::sparse::state_type state) const; - - // Sets the silent probabilities for all the states in the range to their values in the range. - void setSilentProbabilities(typename std::vector>::iterator first, typename std::vector>::iterator last); - - // Sets the silent probabilities for all states in the range to zero. - void setSilentProbabilitiesToZero(typename std::vector>::iterator first, typename std::vector>::iterator last); - - // Sets the silent probability for the given state to the given value. - void setSilentProbability(storm::storage::sparse::state_type state, ValueType const& value); - - private: - // The list of blocks in the partition. - std::list blocks; - - // The number of blocks of the partition. Although this could be retrieved via block.size(), we want to - // guarantee constant access time (which is currently not guaranteed by gcc'c standard libary). - uint_fast64_t numberOfBlocks; - - // A mapping of states to their blocks. - std::vector stateToBlockMapping; - - // A vector containing all the states and their values. It is ordered in a special way such that the - // blocks only need to define their start/end indices. - std::vector> statesAndValues; - - // This vector keeps track of the position of each state in the state vector. - std::vector positions; - - // A flag that indicates whether or not the vector with silent probabilities exists. - bool keepSilentProbabilities; - - // This vector keeps track of the silent probabilities (i.e. the probabilities going into the very own - // equivalence class) of each state. This means that a state is silent iff its entry is non-zero. - std::vector silentProbabilities; - }; - - /*! - * 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 atomicPropositions The set of atomic propositions that the bisimulation considers. - * @param backwardTransitions The backward transitions of the model. - * @param The initial partition. - * @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. - * @param comparator A comparator used for comparing constants. - */ - template - void partitionRefinement(ModelType const& model, std::set const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient, storm::utility::ConstantsComparator const& comparator); - - /*! - * Refines the partition based on the provided splitter. After calling this method all blocks are stable - * with respect to the splitter. - * - * @param forwardTransitions The forward transitions of the model. - * @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 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. - * @param comparator A comparator used for comparing constants. - */ - void refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator); - - /*! - * 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. - * @param comparator A comparator used for comparing constants. - */ - void refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator); - - void refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator); - - /*! - * Determines the split offsets in the given block. - * - * @param block The block that is to be analyzed for splits. - * @param partition The partition that contains the block. - * @param comparator A comparator used for comparing constants. - */ - std::vector getSplitPointsWeak(Block& block, Partition& partition, storm::utility::ConstantsComparator const& comparator); - - /*! - * 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 selectedAtomicPropositions The set of atomic propositions that was considered by the bisimulation. - * The quotient will only have these atomic propositions. - * @param partition The previously computed partition. This is used for quickly retrieving the block of a - * state. - * @param bisimulationType The kind of bisimulation that is to be computed. - * @param comparator A comparator used for comparing constants. - */ - template - void buildQuotient(ModelType const& model, std::set const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards, storm::utility::ConstantsComparator const& comparator); - - /*! - * 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 phiStates The phi states in the model. - * @param psiStates The psi states in the model. - * @param bisimulationType The kind of bisimulation that 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. - * @param comparator A comparator used for comparing constants. - * @return The resulting partition. - */ - template - Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false, storm::utility::ConstantsComparator const& comparator = storm::utility::ConstantsComparator()); - - /*! - * 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. - * @param backwardTransitions The backward transitions of the model. - * @param bisimulationType The kind of bisimulation that is to be computed. - * @param atomicPropositions The set of atomic propositions to respect. If not given, then all atomic - * propositions of the model are respected. - * @param comparator A comparator used for comparing constants. - * @return The resulting partition. - */ - template - Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType, boost::optional> const& atomicPropositions = boost::optional>(), bool keepRewards = true, storm::utility::ConstantsComparator const& comparator = storm::utility::ConstantsComparator()); - - /*! - * 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. - * - * @param model The model from which to look-up the probabilities. - * @param partition The partition that holds the silent probabilities. - */ - template - void initializeSilentProbabilities(ModelType const& model, Partition& partition); - - /*! - * Splits all blocks of the partition in a way such that the states of each block agree on the rewards. - * - * @param stateRewardVector The state reward vector of the model. - * @param partition The partition that is to be split. - * @param comparator A comparator used for comparing constants. - */ - void splitRewards(std::vector const& stateRewardVector, Partition& partition, storm::utility::ConstantsComparator const& comparator); - - // If required, a quotient model is built and stored in this member. - std::shared_ptr> quotient; - }; - } -} - -#endif /* STORM_STORAGE_DeterministicModelBisimulationDecomposition_H_ */ \ No newline at end of file diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp new file mode 100644 index 000000000..06b33f55e --- /dev/null +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -0,0 +1,259 @@ +#include "src/storage/bisimulation/BisimulationDecomposition.h" + +#include + +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Ctmc.h" + +#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + +#include "src/utility/macros.h" +#include "src/exceptions/IllegalFunctionCallException.h" + +namespace storm { + namespace storage { + + using namespace bisimulation; + + template + BisimulationDecomposition::Options::Options(ModelType const& model, storm::logic::Formula const& formula) : Options() { + this->preserveSingleFormula(model, formula); + } + + template + BisimulationDecomposition::Options::Options(ModelType const& model, std::vector> const& formulas) : Options() { + if (formulas.size() == 1) { + this->preserveSingleFormula(model, *formulas.front()); + } else { + for (auto const& formula : formulas) { + preserveFormula(model, *formula); + } + } + } + + template + BisimulationDecomposition::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(false), type(BisimulationType::Strong), bounded(false), buildQuotient(true) { + // Intentionally left empty. + } + + template + void BisimulationDecomposition::Options::preserveFormula(ModelType const& model, storm::logic::Formula const& formula) { + // Disable the measure driven initial partition. + measureDrivenInitialPartition = false; + phiStates = boost::none; + psiStates = boost::none; + + // Preserve rewards if necessary. + keepRewards = keepRewards || formula.containsRewardOperator(); + + // Preserve bounded properties if necessary. + bounded = bounded || (formula.containsBoundedUntilFormula() || formula.containsNextFormula()); + + // Compute the relevant labels and expressions. + this->addToRespectedAtomicPropositions(formula.getAtomicExpressionFormulas(), formula.getAtomicLabelFormulas()); + } + + template + void BisimulationDecomposition::Options::preserveSingleFormula(ModelType const& model, storm::logic::Formula const& formula) { + keepRewards = formula.containsRewardOperator(); + + // We need to preserve bounded properties iff the formula contains a bounded until or a next subformula. + bounded = formula.containsBoundedUntilFormula() || formula.containsNextFormula(); + + // Compute the relevant labels and expressions. + this->addToRespectedAtomicPropositions(formula.getAtomicExpressionFormulas(), formula.getAtomicLabelFormulas()); + + // Check whether measure driven initial partition is possible and, if so, set it. + this->checkAndSetMeasureDrivenInitialPartition(model, formula); + } + + template + void BisimulationDecomposition::Options::checkAndSetMeasureDrivenInitialPartition(ModelType const& model, storm::logic::Formula const& formula) { + std::shared_ptr newFormula = formula.asSharedPointer(); + + if (formula.isProbabilityOperatorFormula()) { + newFormula = formula.asProbabilityOperatorFormula().getSubformula().asSharedPointer(); + } else if (formula.isRewardOperatorFormula()) { + newFormula = formula.asRewardOperatorFormula().getSubformula().asSharedPointer(); + } + + std::shared_ptr leftSubformula = std::make_shared(true); + std::shared_ptr rightSubformula; + if (newFormula->isUntilFormula()) { + leftSubformula = newFormula->asUntilFormula().getLeftSubformula().asSharedPointer(); + rightSubformula = newFormula->asUntilFormula().getRightSubformula().asSharedPointer(); + if (leftSubformula->isPropositionalFormula() && rightSubformula->isPropositionalFormula()) { + measureDrivenInitialPartition = true; + } + } else if (newFormula->isEventuallyFormula()) { + rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer(); + if (rightSubformula->isPropositionalFormula()) { + measureDrivenInitialPartition = true; + } + } else if (newFormula->isReachabilityRewardFormula()) { + rightSubformula = newFormula->asReachabilityRewardFormula().getSubformula().asSharedPointer(); + if (rightSubformula->isPropositionalFormula()) { + measureDrivenInitialPartition = true; + } + } + + if (measureDrivenInitialPartition) { + storm::modelchecker::SparsePropositionalModelChecker checker(model); + std::unique_ptr phiStatesCheckResult = checker.check(*leftSubformula); + std::unique_ptr psiStatesCheckResult = checker.check(*rightSubformula); + phiStates = phiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = psiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector(); + } + } + + template + void BisimulationDecomposition::Options::addToRespectedAtomicPropositions(std::vector> const& expressions, std::vector> const& labels) { + std::set labelsToRespect; + for (auto const& labelFormula : labels) { + labelsToRespect.insert(labelFormula->getLabel()); + } + for (auto const& expressionFormula : expressions) { + labelsToRespect.insert(expressionFormula->toString()); + } + if (!respectedAtomicPropositions) { + respectedAtomicPropositions = labelsToRespect; + } else { + respectedAtomicPropositions.get().insert(labelsToRespect.begin(), labelsToRespect.end()); + } + } + + template + BisimulationDecomposition::BisimulationDecomposition(ModelType const& model, Options const& options) : model(model), backwardTransitions(model.getBackwardTransitions()), options(options), partition(), comparator(), quotient(nullptr) { + // Fix the respected atomic propositions if they were not explicitly given. + if (!this->options.respectedAtomicPropositions) { + this->options.respectedAtomicPropositions = model.getStateLabeling().getLabels(); + } + } + + template + void BisimulationDecomposition::computeBisimulationDecomposition() { + std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); + + std::chrono::high_resolution_clock::time_point refinementStart = std::chrono::high_resolution_clock::now(); + this->performPartitionRefinement(); + std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart; + + std::chrono::high_resolution_clock::time_point extractionStart = std::chrono::high_resolution_clock::now(); + this->extractDecompositionBlocks(); + std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart; + + std::chrono::high_resolution_clock::time_point quotientBuildStart = std::chrono::high_resolution_clock::now(); + if (options.buildQuotient) { + this->buildQuotient(); + } + std::chrono::high_resolution_clock::duration quotientBuildTime = std::chrono::high_resolution_clock::now() - quotientBuildStart; + + std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart; + + if (storm::settings::generalSettings().isShowStatisticsSet()) { + std::chrono::milliseconds refinementTimeInMilliseconds = std::chrono::duration_cast(refinementTime); + std::chrono::milliseconds extractionTimeInMilliseconds = std::chrono::duration_cast(extractionTime); + std::chrono::milliseconds quotientBuildTimeInMilliseconds = std::chrono::duration_cast(quotientBuildTime); + std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast(totalTime); + std::cout << std::endl; + std::cout << "Time breakdown:" << std::endl; + std::cout << " * time for partitioning: " << refinementTimeInMilliseconds.count() << "ms" << std::endl; + std::cout << " * time for extraction: " << extractionTimeInMilliseconds.count() << "ms" << std::endl; + std::cout << " * time for building quotient: " << quotientBuildTimeInMilliseconds.count() << "ms" << std::endl; + std::cout << "------------------------------------------" << std::endl; + std::cout << " * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl; + std::cout << std::endl; + } + } + + template + void BisimulationDecomposition::performPartitionRefinement() { + // Insert all blocks into the splitter queue that are initially marked as being a (potential) splitter. + std::deque splitterQueue; + std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { if (a.isMarkedAsSplitter()) { splitterQueue.push_back(&a); } } ); + + // Then perform the actual splitting until there are no more splitters. + while (!splitterQueue.empty()) { + // Optionally: sort the splitter queue according to some criterion (here: prefer small splitters). + std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } ); + + // Get and prepare the next splitter. + Block* splitter = splitterQueue.front(); + splitterQueue.pop_front(); + splitter->unmarkAsSplitter(); + + // Now refine the partition using the current splitter. + refinePartitionBasedOnSplitter(*splitter, splitterQueue); + } + } + + template + std::shared_ptr BisimulationDecomposition::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 BisimulationDecomposition::splitInitialPartitionBasedOnStateRewards() { + std::vector const& stateRewardVector = model.getUniqueRewardModel()->second.getStateRewardVector(); + partition.split([&stateRewardVector] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return stateRewardVector[a] < stateRewardVector[b]; }, + [&stateRewardVector] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return stateRewardVector[a] != stateRewardVector[b]; }); + } + + template + void BisimulationDecomposition::initializeLabelBasedPartition() { + + partition = storm::storage::bisimulation::Partition(model.getNumberOfStates()); + for (auto const& label : options.respectedAtomicPropositions.get()) { + if (label == "init") { + continue; + } + partition.splitStates(model.getStates(label)); + } + + // If the model has state rewards, we need to consider them, because otherwise reward properties are not + // preserved. + if (options.keepRewards && model.hasRewardModel()) { + this->splitInitialPartitionBasedOnStateRewards(); + } + } + + template + void BisimulationDecomposition::initializeMeasureDrivenPartition() { + std::pair statesWithProbability01 = this->getStatesWithProbability01(backwardTransitions, options.phiStates.get(), options.psiStates.get()); + + boost::optional representativePsiState; + if (!options.psiStates.get().empty()) { + representativePsiState = *options.psiStates.get().begin(); + } + + partition = storm::storage::bisimulation::Partition(model.getNumberOfStates(), statesWithProbability01.first, options.bounded || options.keepRewards ? options.psiStates.get() : statesWithProbability01.second, representativePsiState); + + // If the model has state rewards, we need to consider them, because otherwise reward properties are not + // preserved. + if (options.keepRewards && model.hasRewardModel()) { + this->splitInitialPartitionBasedOnStateRewards(); + } + } + + template + void BisimulationDecomposition::extractDecompositionBlocks() { + // Now move the states from the internal partition into their final place in the decomposition. We do so in + // a way that maintains the block IDs as indices. + this->blocks.resize(partition.size()); + for (auto const& block : partition.getBlocks()) { + // We need to sort the states to allow for rapid construction of the blocks. + partition.sortBlock(block); + + // Convert the state-value-pairs to states only. + this->blocks[block.getId()] = block_type(partition.begin(block), partition.end(block), true); + } + } + + template class BisimulationDecomposition>; + } +} diff --git a/src/storage/bisimulation/BisimulationDecomposition.h b/src/storage/bisimulation/BisimulationDecomposition.h new file mode 100644 index 000000000..8796b5267 --- /dev/null +++ b/src/storage/bisimulation/BisimulationDecomposition.h @@ -0,0 +1,222 @@ +#ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ +#define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ + +#include + +#include "src/storage/sparse/StateType.h" +#include "src/storage/Decomposition.h" +#include "src/storage/StateBlock.h" +#include "src/storage/bisimulation/Partition.h" + +#include "src/logic/Formulas.h" + +#include "src/utility/constants.h" +#include "src/utility/ConstantsComparator.h" + +namespace storm { + namespace utility { + template class ConstantsComparator; + } + + namespace logic { + class Formula; + } + + namespace storage { + + enum class BisimulationType { Strong, Weak }; + + /*! + * This class is the superclass of all decompositions of a sparse model into its bisimulation quotient. + */ + template + class BisimulationDecomposition : public Decomposition { + public: + typedef typename ModelType::ValueType ValueType; + typedef typename ModelType::RewardModelType RewardModelType; + + // A class that offers the possibility to customize the bisimulation. + struct Options { + // Creates an object representing the default values for all options. + Options(); + + /*! + * Creates an object representing the options necessary to obtain the quotient while still preserving + * the given formula. + * + * @param The model for which the quotient model shall be computed. This needs to be given in order to + * derive a suitable initial partition. + * @param formula The formula that is to be preserved. + */ + Options(ModelType const& model, storm::logic::Formula const& formula); + + /*! + * Creates an object representing the options necessary to obtain the smallest quotient while still + * preserving the given formulas. + * + * @param The model for which the quotient model shall be computed. This needs to be given in order to + * derive a suitable initial partition. + * @param formulas The formulas that need to be preserved. + */ + Options(ModelType const& model, std::vector> const& formulas); + + /*! + * Changes the options in a way that the given formula is preserved. + * + * @param model The model for which to preserve the formula. + * @param formula The only formula to check. + */ + void preserveFormula(ModelType const& model, storm::logic::Formula const& formula); + + // A flag that indicates whether a measure driven initial partition is to be used. If this flag is set + // to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the + // measure driven initial partition wrt. to the states phi and psi is taken. + bool measureDrivenInitialPartition; + boost::optional phiStates; + boost::optional psiStates; + + // An optional set of strings that indicate which of the atomic propositions of the model are to be + // respected and which may be ignored. If not given, all atomic propositions of the model are respected. + boost::optional> respectedAtomicPropositions; + + // A flag that indicates whether or not the state-rewards of the model are to be respected (and should + // be kept in the quotient model, if one is built). + bool keepRewards; + + // A flag that indicates whether a strong or a weak bisimulation is to be computed. + BisimulationType type; + + // A flag that indicates whether step-bounded properties are to be preserved. This may only be set to tru + // when computing strong bisimulation equivalence. + bool bounded; + + // A flag that governs whether the quotient model is actually built or only the decomposition is computed. + bool buildQuotient; + + private: + /*! + * Sets the options under the assumption that the given formula is the only one that is to be checked. + * + * @param model The model for which to preserve the formula. + * @param formula The only formula to check. + */ + void preserveSingleFormula(ModelType const& model, storm::logic::Formula const& formula); + + /*! + * Adds the given expressions and labels to the set of respected atomic propositions. + * + * @param expressions The expressions to respect. + * @param labels The labels to respect. + */ + void addToRespectedAtomicPropositions(std::vector> const& expressions, std::vector> const& labels); + + /* + * Checks whether a measure driven partition is possible with the given formula and sets the necessary + * data if this is the case. + * + * @param model The model for which to derive the data. + * @param formula The formula for which to derive the data for the measure driven initial partition (if + * applicable). + */ + void checkAndSetMeasureDrivenInitialPartition(ModelType const& model, storm::logic::Formula const& formula); + }; + + /*! + * Decomposes the given model into equivalance classes of a bisimulation. + * + * @param model The model to decompose. + * @param type The type of the bisimulation to compute. + * @param buildQuotient A flag specifying whether the quotient is to be build. + */ + BisimulationDecomposition(ModelType const& model, Options const& options); + + /*! + * Retrieves the quotient of the model under the computed bisimulation. + * + * @return The quotient model. + */ + std::shared_ptr getQuotient() const; + + protected: + /*! + * Computes the decomposition of the model into bisimulation equivalence classes. If requested, a quotient + * model is built. + */ + void computeBisimulationDecomposition(); + + /*! + * 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(). + */ + void performPartitionRefinement(); + + /*! + * Refines the partition by considering the given splitter. All blocks that become potential splitters + * because of this refinement, are marked as splitters and inserted into the splitter queue. + * + * @param splitter The splitter to use. + * @param splitterQueue The queue into which to insert the newly discovered potential splitters. + */ + virtual void refinePartitionBasedOnSplitter(bisimulation::Block const& splitter, std::deque& splitterQueue); + + /*! + * Builds the quotient model based on the previously computed equivalence classes (stored in the blocks + * of the decomposition. + */ + virtual void buildQuotient() = 0; + + /*! + * Initializes the initial partition based on all respected labels. + */ + virtual void initializeLabelBasedPartition(); + + /*! + * Creates the measure-driven initial partition for reaching psi states from phi states. + */ + virtual void initializeMeasureDrivenPartition(); + + /*! + * Computes the set of states with probability 0/1 for satisfying phi until psi. This is used for the measure + * driven initial partition. + * + * @param backwardTransitions The backward transitions of the model. + * @param phiStates The phi states. + * @param psiStates The psi states. + * @return The states with probability 0 and 1. + */ + virtual std::pair getStatesWithProbability01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) = 0; + + /*! + * Splits the initial partition based on the (unique) state reward vector of the model. + */ + virtual void splitInitialPartitionBasedOnStateRewards(); + + /*! + * Constructs the blocks of the decomposition object based on the current partition. + */ + void extractDecompositionBlocks(); + + // The model to decompose. + ModelType const& model; + + // The backward transitions of the model. + storm::storage::SparseMatrix backwardTransitions; + + // The options used during construction. + Options options; + + // The current partition (used by partition refinement). + storm::storage::bisimulation::Partition partition; + + // A comparator used for comparing the distances of constants. + storm::utility::ConstantsComparator comparator; + + // The quotient, if it was build. Otherwhise a null pointer. + std::shared_ptr quotient; + }; + } +} + + +#endif /* STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ */ diff --git a/src/storage/bisimulation/Block.cpp b/src/storage/bisimulation/Block.cpp new file mode 100644 index 000000000..66183764c --- /dev/null +++ b/src/storage/bisimulation/Block.cpp @@ -0,0 +1,132 @@ +#include "src/storage/bisimulation/Block.h" + +#include +#include + +#include "src/storage/bisimulation/Partition.h" + +#include "src/utility/macros.h" + +namespace storm { + namespace storage { + namespace bisimulation { + + 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), markedAsSplitter(false), markedAsPredecessorBlock(false), absorbing(false), id(id) { + if (nextBlock != nullptr) { + nextBlock->previousBlock = this; + } + if (previousBlock != nullptr) { + previousBlock->nextBlock = this; + } + STORM_LOG_ASSERT(this->beginIndex < this->endIndex, "Unable to create block of illegal size."); + } + + void Block::print(Partition const& partition) const { + std::cout << "block " << this->id << " from " << this->beginIndex << " to " << this->endIndex; + } + + void Block::setBeginIndex(storm::storage::sparse::state_type beginIndex) { + this->beginIndex = beginIndex; + STORM_LOG_ASSERT(beginIndex < endIndex, "Unable to resize block to illegal size."); + } + + void Block::setEndIndex(storm::storage::sparse::state_type endIndex) { + this->endIndex = endIndex; + STORM_LOG_ASSERT(beginIndex < endIndex, "Unable to resize block to illegal size."); + } + + storm::storage::sparse::state_type Block::getBeginIndex() const { + return this->beginIndex; + } + + storm::storage::sparse::state_type Block::getEndIndex() const { + return this->endIndex; + } + + Block const& Block::getNextBlock() const { + return *this->nextBlock; + } + + bool Block::hasNextBlock() const { + return this->nextBlock != nullptr; + } + + Block const* Block::getNextBlockPointer() const { + return this->nextBlock; + } + + Block const& Block::getPreviousBlock() const { + return *this->previousBlock; + } + + Block const* Block::getPreviousBlockPointer() const { + return this->previousBlock; + } + + bool Block::hasPreviousBlock() const { + return this->previousBlock != nullptr; + } + + 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; + } + + std::size_t Block::getNumberOfStates() const { + return (this->endIndex - this->beginIndex); + } + + bool Block::isMarkedAsSplitter() const { + return this->markedAsSplitter; + } + + void Block::markAsSplitter() { + this->markedAsSplitter = true; + } + + void Block::unmarkAsSplitter() { + this->markedAsSplitter = false; + } + + std::size_t Block::getId() const { + return this->id; + } + + void Block::setAbsorbing(bool absorbing) { + this->absorbing = absorbing; + } + + bool Block::isAbsorbing() const { + return this->absorbing; + } + + void Block::setRepresentativeState(storm::storage::sparse::state_type representativeState) { + this->representativeState = representativeState; + } + + bool Block::hasRepresentativeState() const { + return static_cast(representativeState); + } + + storm::storage::sparse::state_type Block::getRepresentativeState() const { + STORM_LOG_THROW(representativeState, storm::exceptions::InvalidOperationException, "Unable to retrieve representative state for block."); + return representativeState.get(); + } + + void Block::markAsPredecessorBlock() { + this->markedAsPredecessorBlock = true; + } + + void Block::unmarkAsPredecessorBlock() { + this->markedAsPredecessorBlock = false; + } + + bool Block::isMarkedAsPredecessor() const { + return markedAsPredecessorBlock; + } + + } + } +} \ No newline at end of file diff --git a/src/storage/bisimulation/Block.h b/src/storage/bisimulation/Block.h new file mode 100644 index 000000000..0758b1658 --- /dev/null +++ b/src/storage/bisimulation/Block.h @@ -0,0 +1,132 @@ +#ifndef STORM_STORAGE_BISIMULATION_BLOCK_H_ +#define STORM_STORAGE_BISIMULATION_BLOCK_H_ + +#include +#include + +#include "src/storage/sparse/StateType.h" + +namespace storm { + namespace storage { + namespace bisimulation { + // Forward-declare partition class. + class Partition; + + class Block { + public: + friend class Partition; + + // Creates a new block with the given begin and end. + Block(storm::storage::sparse::state_type beginIndex, storm::storage::sparse::state_type endIndex, Block* previous, Block* next, std::size_t id); + + Block() = default; + Block(Block const& other) = default; + Block& operator=(Block const& other) = default; + Block(Block&& other) = default; + Block& operator=(Block&& other) = default; + + // Prints the block to the standard output. + void print(Partition const& partition) const; + + // Returns the beginning index of the block. + storm::storage::sparse::state_type getBeginIndex() const; + + // Returns the beginning index of the block. + storm::storage::sparse::state_type getEndIndex() const; + + // Gets the next block (if there is one). + Block const& getNextBlock() const; + + // Gets a pointer to the next block (if there is one). + Block const* getNextBlockPointer() const; + + // Retrieves whether the block as a successor block. + bool hasNextBlock() const; + + // Gets the next block (if there is one). + Block const& getPreviousBlock() const; + + // Gets a pointer to the previous block (if there is one). + Block const* getPreviousBlockPointer() const; + + // Retrieves whether the block as a successor block. + bool hasPreviousBlock() const; + + // Checks consistency of the information in the block. + bool check() const; + + // Retrieves the number of states in this block. + std::size_t getNumberOfStates() const; + + // Checks whether the block is marked as a splitter. + bool isMarkedAsSplitter() const; + + // Marks the block as being a splitter. + void markAsSplitter(); + + // Removes the mark. + void unmarkAsSplitter(); + + // Retrieves the ID of the block. + std::size_t getId() const; + + // Retrieves whether the block is marked as a predecessor. + bool isMarkedAsPredecessor() const; + + // Marks the block as being a predecessor block. + void markAsPredecessorBlock(); + + // 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; + + // Sets the representative state of this block + void setRepresentativeState(storm::storage::sparse::state_type representativeState); + + // Retrieves whether this block has a representative state. + bool hasRepresentativeState() const; + + // Retrieves the representative state for this block. + storm::storage::sparse::state_type getRepresentativeState() const; + + private: + // Sets the beginning index of the block. + void setBeginIndex(storm::storage::sparse::state_type beginIndex); + + // Sets the end index of the block. + void setEndIndex(storm::storage::sparse::state_type endIndex); + + // Pointers to the next and previous block. + Block* nextBlock; + Block* previousBlock; + + // The begin and end indices of the block in terms of the state vector of the partition. + storm::storage::sparse::state_type beginIndex; + storm::storage::sparse::state_type endIndex; + + // A field that can be used for marking the block. + bool markedAsSplitter; + + // A field that can be used for marking the block as a predecessor block. + bool markedAsPredecessorBlock; + + // 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; + + // 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. + boost::optional representativeState; + }; + } + } +} + +#endif /* STORM_STORAGE_BISIMULATION_BLOCK_H_ */ diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp new file mode 100644 index 000000000..a60262a15 --- /dev/null +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -0,0 +1,681 @@ +#include "src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h" + +#include +#include +#include +#include +#include + +#include "src/adapters/CarlAdapter.h" +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" + +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Ctmc.h" +#include "src/models/sparse/StandardRewardModel.h" + +#include "src/utility/graph.h" +#include "src/utility/constants.h" +#include "src/utility/ConstantsComparator.h" +#include "src/exceptions/IllegalFunctionCallException.h" +#include "src/exceptions/InvalidOptionException.h" +#include "src/exceptions/InvalidArgumentException.h" + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + +namespace storm { + namespace storage { + + using namespace bisimulation; + + template + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition::Options const& options) : BisimulationDecomposition(model, options.weak ? BisimulationType::Weak : BisimulationType::Strong) { + STORM_LOG_THROW(!model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model."); + STORM_LOG_THROW(!model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls)."); + STORM_LOG_THROW(!options.weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties."); + + // Extract the set of respected atomic propositions from the options. + if (options.respectedAtomicPropositions) { + this->selectedAtomicPropositions = options.respectedAtomicPropositions.get(); + } else { + this->selectedAtomicPropositions = model.getStateLabeling().getLabels(); + } + + // initialize the initial partition. + if (options.measureDrivenInitialPartition) { + STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi states."); + STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without psi states."); + this->initializeMeasureDrivenPartition(); + } else { + this->initializeLabelBasedPartition(); + } + + this->computeBisimulationDecomposition(); + } + + template + std::pair DeterministicModelBisimulationDecomposition::getStatesWithProbability01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + return storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); + } + + template + void DeterministicModelBisimulationDecomposition::splitOffDivergentStates() { + std::vector stateStack; + stateStack.reserve(this->model.getNumberOfStates()); + storm::storage::BitVector nondivergentStates(this->model.getNumberOfStates()); + + for (auto& block : this->partition.getBlocks()) { + nondivergentStates.clear(); + + for (auto stateIt = this->partition.begin(block), stateIte = this->partition.end(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 : this->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 (&this->partition.getBlock(successor.getColumn()) != &block) { + isDirectlyNonDivergent = true; + break; + } + } + + if (isDirectlyNonDivergent) { + stateStack.push_back(stateIt->first); + + while (!stateStack.empty()) { + storm::storage::sparse::state_type currentState = stateStack.back(); + stateStack.pop_back(); + nondivergentStates.set(currentState); + + for (auto const& predecessor : this->backwardTransitions.getRow(currentState)) { + if (&this->partition.getBlock(predecessor.getColumn()) == &block && !nondivergentStates.get(predecessor.getColumn())) { + stateStack.push_back(predecessor.getColumn()); + } + } + } + } + } + + + if (nondivergentStates.getNumberOfSetBits() > 0 && nondivergentStates.getNumberOfSetBits() != block.getNumberOfStates()) { + // After performing the split, the current block will contain the divergent states only. + this->partition.splitStates(block, nondivergentStates); + + // 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 + void DeterministicModelBisimulationDecomposition::initializeSilentProbabilities() { + silentProbabilities.resize(this->model.getNumberOfStates(), storm::utility::zero()); + for (storm::storage::sparse::state_type state = 0; state < this->model.getNumberOfStates(); ++state) { + Block const* currentBlockPtr = &this->partition.getBlock(state); + for (auto const& successorEntry : this->model.getRows(state)) { + if (&this->partition.getBlock(successorEntry.getColumn()) == currentBlockPtr) { + silentProbabilities[state] += successorEntry.getValue(); + } + } + } + } + + template + void DeterministicModelBisimulationDecomposition::initializeWeakDtmcBisimulation() { + // If we are creating the initial partition for weak bisimulation on DTMCs, we need to (a) split off all + // divergent states of each initial block and (b) initialize the vector of silent probabilities. + this->splitOffDivergentStates(); + this->initializeSilentProbabilities(); + } + + template + void DeterministicModelBisimulationDecomposition::initializeMeasureDrivenPartition() { + BisimulationDecomposition::initializeMeasureDrivenPartition(); + + if (this->options.type == BisimulationType::Weak && this->model.getModelType() == ModelType::Dtmc) { + this->initializeWeakDtmcBisimulation(); + } + } + + template + void DeterministicModelBisimulationDecomposition::initializeLabelBasedPartition() { + BisimulationDecomposition::initializeLabelBasedPartition(); + + if (this->options.type == BisimulationType::Weak && this->model.getModelType() == ModelType::Dtmc) { + this->initializeWeakDtmcBisimulation(); + } + } + + + + template + void DeterministicModelBisimulationDecomposition::buildQuotient() { + // In order to create the quotient model, we need to construct + // (a) the new transition matrix, + // (b) the new labeling, + // (c) the new reward structures. + + // Prepare a matrix builder for (a). + storm::storage::SparseMatrixBuilder builder(this->size(), this->size()); + + // Prepare the new state labeling for (b). + storm::models::sparse::StateLabeling newLabeling(this->size()); + std::set atomicPropositionsSet = this->options.selectedAtomicPropositions.get(); + atomicPropositionsSet.insert("init"); + std::vector atomicPropositions = std::vector(atomicPropositionsSet.begin(), atomicPropositionsSet.end()); + for (auto const& ap : atomicPropositions) { + newLabeling.addLabel(ap); + } + + // If the model had state rewards, we need to build the state rewards for the quotient as well. + boost::optional> stateRewards; + if (this->options.keepRewards && this->model.hasRewardModel()) { + stateRewards = std::vector(this->blocks.size()); + } + + // Now build (a) and (b) by traversing all blocks. + for (uint_fast64_t blockIndex = 0; blockIndex < this->blocks.size(); ++blockIndex) { + auto const& block = this->blocks[blockIndex]; + + // Pick one representative state. For strong bisimulation it doesn't matter which state it is, because + // they all behave equally. + 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 + // there is any such state). + if (this->options.type == BisimulationType::Weak) { + for (auto const& state : block) { + if (!partition.isSilent(state, comparator)) { + representativeState = state; + break; + } + } + } + + Block const& oldBlock = partition.getBlock(representativeState); + + // If the block is absorbing, we simply add a self-loop. + if (oldBlock.isAbsorbing()) { + builder.addNextValue(blockIndex, blockIndex, storm::utility::one()); + + // If the block has a special representative state, we retrieve it now. + if (oldBlock.hasRepresentativeState()) { + representativeState = oldBlock.getRepresentativeState(); + } + + // Add all of the selected atomic propositions that hold in the representative state to the state + // representing the block. + for (auto const& ap : atomicPropositions) { + if (model.getStateLabeling().getStateHasLabel(ap, representativeState)) { + newLabeling.addLabelToState(ap, 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(); + + // If we are computing a weak bisimulation quotient, there is no need to add self-loops. + if ((bisimulationType == BisimulationType::WeakDtmc || bisimulationType == BisimulationType::WeakCtmc) && targetBlock == blockIndex) { + continue; + } + + 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) { + 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); + } + } + + // Otherwise add all atomic propositions to the equivalence class that the representative state + // satisfies. + for (auto const& ap : atomicPropositions) { + if (model.getStateLabeling().getStateHasLabel(ap, representativeState)) { + newLabeling.addLabelToState(ap, blockIndex); + } + } + } + + // If the model has state rewards, we simply copy the state reward of the representative state, because + // all states in a block are guaranteed to have the same state reward. + if (keepRewards && model.hasRewardModel()) { + typename std::unordered_map::const_iterator nameRewardModelPair = model.getUniqueRewardModel(); + stateRewards.get()[blockIndex] = nameRewardModelPair->second.getStateRewardVector()[representativeState]; + } + } + + // Now check which of the blocks of the partition contain at least one initial state. + for (auto initialState : model.getInitialStates()) { + Block const& initialBlock = partition.getBlock(initialState); + newLabeling.addLabelToState("init", initialBlock.getId()); + } + + // Construct the reward model mapping. + std::unordered_map rewardModels; + if (keepRewards && model.hasRewardModel()) { + typename std::unordered_map::const_iterator nameRewardModelPair = model.getUniqueRewardModel(); + rewardModels.insert(std::make_pair(nameRewardModelPair->first, typename ModelType::RewardModelType(stateRewards))); + } + + // Finally construct the quotient model. + this->quotient = std::shared_ptr>(new ModelType(builder.build(), std::move(newLabeling), std::move(rewardModels))); + } + + template + void DeterministicModelBisimulationDecomposition::refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator) { + // 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; } ); + + // 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, we need to scan the ranges of states that agree on the probability. + typename std::vector>::const_iterator begin = partition.getBegin(block); + typename std::vector>::const_iterator end = partition.getEnd(block) - 1; + storm::storage::sparse::state_type currentIndex = block.getBegin(); + + // 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. + bool blockSplit = !comparator.isEqual(begin->second, end->second); + while (!comparator.isEqual(begin->second, end->second)) { + // 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. + ValueType const& currentValue = begin->second; + + ++begin; + ++currentIndex; + while (begin != end && comparator.isEqual(begin->second, currentValue)) { + ++begin; + ++currentIndex; + } + + // Now we split the block and mark it as a potential splitter. + Block& newBlock = partition.splitBlock(block, currentIndex); + if (!newBlock.isMarkedAsSplitter()) { + splitterQueue.push_back(&newBlock); + newBlock.markAsSplitter(); + } + } + + // If the block was split, we also need to insert itself into the splitter queue. + if (blockSplit) { + if (!block.isMarkedAsSplitter()) { + splitterQueue.push_back(&block); + block.markAsSplitter(); + } + } + } + + template + void DeterministicModelBisimulationDecomposition::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator) { + std::vector splitPoints = getSplitPointsWeak(block, partition, comparator); + + // Restore the original begin of the block. + block.setBegin(block.getOriginalBegin()); + + // Now that we have the split points of the non-silent states, we perform a backward search from + // each non-silent state and label the predecessors with the class of the non-silent state. + std::vector stateLabels(block.getEnd() - block.getBegin(), storm::storage::BitVector(splitPoints.size() - 1)); + + std::vector stateStack; + stateStack.reserve(block.getEnd() - block.getBegin()); + for (uint_fast64_t stateClassIndex = 0; stateClassIndex < splitPoints.size() - 1; ++stateClassIndex) { + for (auto stateIt = partition.getStatesAndValues().begin() + splitPoints[stateClassIndex], stateIte = partition.getStatesAndValues().begin() + splitPoints[stateClassIndex + 1]; stateIt != stateIte; ++stateIt) { + + stateStack.push_back(stateIt->first); + stateLabels[partition.getPosition(stateIt->first) - block.getBegin()].set(stateClassIndex); + while (!stateStack.empty()) { + storm::storage::sparse::state_type currentState = stateStack.back(); + stateStack.pop_back(); + + for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { + if (comparator.isZero(predecessorEntry.getValue())) { + continue; + } + + storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); + + // Only if the state is in the same block, is a silent state and it has not yet been + // labeled with the current label. + if (&partition.getBlock(predecessor) == &block && partition.isSilent(predecessor, comparator) && !stateLabels[partition.getPosition(predecessor) - block.getBegin()].get(stateClassIndex)) { + stateStack.push_back(predecessor); + stateLabels[partition.getPosition(predecessor) - block.getBegin()].set(stateClassIndex); + } + } + } + } + } + + // Now that all states were appropriately labeled, we can sort the states according to their labels and then + // scan for ranges that agree on the label. + std::sort(partition.getBegin(block), partition.getEnd(block), [&] (std::pair const& a, std::pair const& b) { return stateLabels[partition.getPosition(a.first) - block.getBegin()] < stateLabels[partition.getPosition(b.first) - block.getBegin()]; }); + + // Note that we do not yet repair the positions vector, but for the sake of efficiency temporariliy keep the + // data structure in an inconsistent state. + + // Now we have everything in place to actually split the block by just scanning for ranges of equal label. + typename std::vector>::const_iterator begin = partition.getBegin(block); + typename std::vector>::const_iterator end = partition.getEnd(block) - 1; + storm::storage::sparse::state_type currentIndex = block.getBegin(); + + // Now we can check whether the block needs to be split, which is the case iff the labels for the first and + // the last state are different. Store the offset of the block seperately, because it will potentially + // modified by splits. + storm::storage::sparse::state_type blockOffset = block.getBegin(); + bool blockSplit = stateLabels[partition.getPosition(begin->first) - blockOffset] != stateLabels[partition.getPosition(end->first) - blockOffset]; + while (stateLabels[partition.getPosition(begin->first) - blockOffset] != stateLabels[partition.getPosition(end->first) - blockOffset]) { + // Now we scan for the first state in the block that disagrees on the labeling value. + // Note that we do not have to check currentIndex for staying within bounds, because we know the matching + // state is within bounds. + storm::storage::BitVector const& currentValue = stateLabels[partition.getPosition(begin->first) - blockOffset]; + + ++begin; + ++currentIndex; + while (begin != end && stateLabels[partition.getPosition(begin->first) - blockOffset] == currentValue) { + ++begin; + ++currentIndex; + } + + // Now we split the block and mark it as a potential splitter. + Block& newBlock = partition.splitBlock(block, currentIndex); + + // Update the silent probabilities for all the states in the new block. + for (auto stateIt = partition.getBegin(newBlock), stateIte = partition.getEnd(newBlock); stateIt != stateIte; ++stateIt) { + if (partition.hasSilentProbability(stateIt->first, comparator)) { + ValueType newSilentProbability = storm::utility::zero(); + for (auto const& successorEntry : forwardTransitions.getRow(stateIt->first)) { + if (&partition.getBlock(successorEntry.getColumn()) == &newBlock) { + newSilentProbability += successorEntry.getValue(); + } + } + partition.setSilentProbability(stateIt->first, newSilentProbability); + } + } + + if (!newBlock.isMarkedAsSplitter()) { + splitterQueue.push_back(&newBlock); + newBlock.markAsSplitter(); + } + } + + // If the block was split, we also need to insert itself into the splitter queue. + if (blockSplit) { + if (!block.isMarkedAsSplitter()) { + splitterQueue.push_back(&block); + block.markAsSplitter(); + } + + // Update the silent probabilities for all the states in the old block. + for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt) { + if (partition.hasSilentProbability(stateIt->first, comparator)) { + ValueType newSilentProbability = storm::utility::zero(); + for (auto const& successorEntry : forwardTransitions.getRow(stateIt->first)) { + if (&partition.getBlock(successorEntry.getColumn()) == &block) { + newSilentProbability += successorEntry.getValue(); + } + } + partition.setSilentProbability(stateIt->first, newSilentProbability); + } + } + } + + // Finally update the positions vector. + storm::storage::sparse::state_type position = blockOffset; + for (auto stateIt = partition.getStatesAndValues().begin() + blockOffset, stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) { + partition.setPosition(stateIt->first, position); + } + } + + template + std::vector DeterministicModelBisimulationDecomposition::getSplitPointsWeak(Block& block, Partition& partition, storm::utility::ConstantsComparator const& comparator) { + 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) { + ValueType const& silentProbability = partition.getSilentProbability(stateValuePair.first); + if (!comparator.isOne(silentProbability) && !comparator.isZero(silentProbability)) { + stateValuePair.second /= storm::utility::one() - silentProbability; + } + }); + + // Now sort the states based on their probabilities. + std::sort(partition.getStatesAndValues().begin() + block.getOriginalBegin(), partition.getStatesAndValues().begin() + block.getBegin(), [&partition] (std::pair const& a, std::pair const& b) { return a.second < b.second; } ); + + // Update the positions vector. + storm::storage::sparse::state_type position = block.getOriginalBegin(); + for (auto stateIt = partition.getStatesAndValues().begin() + block.getOriginalBegin(), stateIte = partition.getStatesAndValues().begin() + block.getBegin(); stateIt != stateIte; ++stateIt, ++position) { + partition.setPosition(stateIt->first, position); + } + + // Then, we scan for the ranges of states that agree on the probability. + typename std::vector>::const_iterator begin = partition.getStatesAndValues().begin() + block.getOriginalBegin(); + typename std::vector>::const_iterator end = partition.getStatesAndValues().begin() + block.getBegin() - 1; + storm::storage::sparse::state_type currentIndex = block.getOriginalBegin(); + result.push_back(currentIndex); + + // 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. + while (!comparator.isEqual(begin->second, end->second)) { + // 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. + ValueType const& currentValue = begin->second; + + ++begin; + ++currentIndex; + while (begin != end && comparator.isEqual(begin->second, currentValue)) { + ++begin; + ++currentIndex; + } + + // Remember the index at which the probabilities were different. + result.push_back(currentIndex); + } + + // Push a sentinel element and return result. + result.push_back(block.getBegin()); + return result; + } + + template + void DeterministicModelBisimulationDecomposition::refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator) { + std::list predecessorBlocks; + + // Iterate over all states of the splitter and check its predecessors. + bool splitterIsPredecessor = false; + storm::storage::sparse::state_type currentPosition = splitter.getBegin(); + for (auto stateIterator = partition.getBegin(splitter), stateIte = partition.getEnd(splitter); stateIterator != stateIte; ++stateIterator, ++currentPosition) { + storm::storage::sparse::state_type currentState = stateIterator->first; + + uint_fast64_t elementsToSkip = 0; + for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { + storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); + + // Get predecessor block and remember if the splitter was a predecessor of itself. + Block& predecessorBlock = partition.getBlock(predecessor); + if (&predecessorBlock == &splitter) { + splitterIsPredecessor = true; + } + + // If the predecessor block has just one state or is marked as being absorbing, we must not split it. + if (predecessorBlock.getNumberOfStates() <= 1 || predecessorBlock.isAbsorbing()) { + continue; + } + + storm::storage::sparse::state_type predecessorPosition = partition.getPosition(predecessor); + + // If we have not seen this predecessor before, we move it to a part near the beginning of the block. + if (predecessorPosition >= predecessorBlock.getBegin()) { + if (&predecessorBlock == &splitter) { + // If the predecessor we just found was already processed (in terms of visiting its predecessors), + // we swap it with the state that is currently at the beginning of the block and move the start + // of the block one step further. + if (predecessorPosition <= currentPosition + elementsToSkip) { + partition.swapStates(predecessor, partition.getState(predecessorBlock.getBegin())); + predecessorBlock.incrementBegin(); + } else { + // Otherwise, we need to move the predecessor, but we need to make sure that we explore its + // predecessors later. + if (predecessorBlock.getMarkedPosition() == predecessorBlock.getBegin()) { + partition.swapStatesAtPositions(predecessorBlock.getMarkedPosition(), predecessorPosition); + partition.swapStatesAtPositions(predecessorPosition, currentPosition + elementsToSkip + 1); + } else { + partition.swapStatesAtPositions(predecessorBlock.getMarkedPosition(), predecessorPosition); + partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.getBegin()); + partition.swapStatesAtPositions(predecessorPosition, currentPosition + elementsToSkip + 1); + } + + ++elementsToSkip; + predecessorBlock.incrementMarkedPosition(); + predecessorBlock.incrementBegin(); + } + } else { + partition.swapStates(predecessor, partition.getState(predecessorBlock.getBegin())); + predecessorBlock.incrementBegin(); + } + partition.setValue(predecessor, predecessorEntry.getValue()); + } else { + // Otherwise, we just need to update the probability for this predecessor. + partition.increaseValue(predecessor, predecessorEntry.getValue()); + } + + if (!predecessorBlock.isMarkedAsPredecessor()) { + predecessorBlocks.emplace_back(&predecessorBlock); + predecessorBlock.markAsPredecessorBlock(); + } + } + + // If we had to move some elements beyond the current element, we may have to skip them. + if (elementsToSkip > 0) { + stateIterator += elementsToSkip; + currentPosition += elementsToSkip; + } + } + + // Now we can traverse the list of states of the splitter whose predecessors we have not yet explored. + for (auto stateIterator = partition.getStatesAndValues().begin() + splitter.getOriginalBegin(), stateIte = partition.getStatesAndValues().begin() + splitter.getMarkedPosition(); stateIterator != stateIte; ++stateIterator) { + storm::storage::sparse::state_type currentState = stateIterator->first; + + for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { + storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); + Block& predecessorBlock = partition.getBlock(predecessor); + storm::storage::sparse::state_type predecessorPosition = partition.getPosition(predecessor); + + if (predecessorPosition >= predecessorBlock.getBegin()) { + partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.getBegin()); + predecessorBlock.incrementBegin(); + partition.setValue(predecessor, predecessorEntry.getValue()); + } else { + partition.increaseValue(predecessor, predecessorEntry.getValue()); + } + + if (!predecessorBlock.isMarkedAsPredecessor()) { + predecessorBlocks.emplace_back(&predecessorBlock); + predecessorBlock.markAsPredecessorBlock(); + } + } + } + + if (bisimulationType == BisimulationType::Strong || bisimulationType == BisimulationType::WeakCtmc) { + std::vector blocksToSplit; + + // Now, we can iterate over the predecessor blocks and see whether we have to create a new block for + // predecessors of the splitter. + for (auto blockPtr : predecessorBlocks) { + Block& block = *blockPtr; + + block.unmarkAsPredecessorBlock(); + block.resetMarkedPosition(); + + // If we have moved the begin of the block to somewhere in the middle of the block, we need to split it. + if (block.getBegin() != block.getEnd()) { + Block& newBlock = partition.insertBlock(block); + if (!newBlock.isMarkedAsSplitter()) { + splitterQueue.push_back(&newBlock); + newBlock.markAsSplitter(); + } + + // Schedule the block of predecessors for refinement based on probabilities. + blocksToSplit.emplace_back(&newBlock); + } else { + // In this case, we can keep the block by setting its begin to the old value. + block.setBegin(block.getOriginalBegin()); + blocksToSplit.emplace_back(&block); + } + } + + // Finally, we walk through the blocks that have a transition to the splitter and split them using + // probabilistic information. + for (auto blockPtr : blocksToSplit) { + if (blockPtr->getNumberOfStates() <= 1) { + continue; + } + + // 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, comparator); + } + } 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) { + partition.setSilentProbabilities(partition.getStatesAndValues().begin() + splitter.getOriginalBegin(), partition.getStatesAndValues().begin() + splitter.getBegin()); + partition.setSilentProbabilitiesToZero(partition.getStatesAndValues().begin() + splitter.getBegin(), partition.getStatesAndValues().begin() + splitter.getEnd()); + } + + // Now refine all predecessor blocks in a weak manner. That is, we split according to the criterion of + // weak bisimulation. + for (auto blockPtr : predecessorBlocks) { + Block& block = *blockPtr; + + // If the splitter is also the predecessor block, we must not refine it at this point. + if (&block != &splitter) { + refineBlockWeak(block, partition, forwardTransitions, backwardTransitions, splitterQueue, comparator); + } else { + // Restore the begin of the block. + block.setBegin(block.getOriginalBegin()); + } + + block.unmarkAsPredecessorBlock(); + block.resetMarkedPosition(); + } + } + + STORM_LOG_ASSERT(partition.check(), "Partition became inconsistent."); + } + + template class DeterministicModelBisimulationDecomposition; + +#ifdef STORM_HAVE_CARL + template class DeterministicModelBisimulationDecomposition; +#endif + } +} diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h new file mode 100644 index 000000000..9bdb1dd48 --- /dev/null +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h @@ -0,0 +1,142 @@ +#ifndef STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ +#define STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ + +#include "src/storage/bisimulation/BisimulationDecomposition.h" + +namespace storm { + namespace utility { + template class ConstantsComparator; + } + + namespace storage { + + /*! + * This class represents the decomposition of a deterministic model into its bisimulation quotient. + */ + template + class DeterministicModelBisimulationDecomposition : public BisimulationDecomposition { + public: + typedef typename ModelType::ValueType ValueType; + typedef typename ModelType::RewardModelType RewardModelType; + + /*! + * Computes the bisimulation relation for the given model. Which kind of bisimulation is computed, is + * customizable via the given options. + * + * @param model The model to decompose. + * @param options The options that customize the computed bisimulation. + */ + DeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition::Options const& options = Options()); + + private: + virtual std::pair getStatesWithProbability01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) override; + + virtual void initializeLabelBasedPartition() override; + + /*! + * Performs the necessary steps to compute a weak bisimulation on a DTMC. + */ + void initializeWeakDtmcBisimulation(); + + /*! + * Splits all blocks of the current partition into a block that contains all divergent states and another + * block containing the non-divergent states. + */ + void splitOffDivergentStates(); + + /*! + * Initializes the vector of silent probabilities. + */ + void initializeSilentProbabilities(); + + virtual void initializeMeasureDrivenPartition() override; + + virtual void initializeLabelBasedPartition() override; + + virtual void buildQuotient() override; + + /*! + * Refines the partition based on the provided splitter. After calling this method all blocks are stable + * with respect to the splitter. + * + * @param forwardTransitions The forward transitions of the model. + * @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 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. + * @param comparator A comparator used for comparing constants. + */ + void refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator); + + /*! + * 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. + * @param comparator A comparator used for comparing constants. + */ + void refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator); + + void refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator); + + /*! + * Determines the split offsets in the given block. + * + * @param block The block that is to be analyzed for splits. + * @param partition The partition that contains the block. + * @param comparator A comparator used for comparing constants. + */ + std::vector getSplitPointsWeak(Block& block, Partition& partition, storm::utility::ConstantsComparator const& comparator); + + + + + + + + + + /*! + * 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 phiStates The phi states in the model. + * @param psiStates The psi states in the model. + * @param bisimulationType The kind of bisimulation that 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. + * @param comparator A comparator used for comparing constants. + * @return The resulting partition. + */ + template + Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false, storm::utility::ConstantsComparator const& comparator = storm::utility::ConstantsComparator()); + + /*! + * 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. + * @param backwardTransitions The backward transitions of the model. + * @param bisimulationType The kind of bisimulation that is to be computed. + * @param atomicPropositions The set of atomic propositions to respect. If not given, then all atomic + * propositions of the model are respected. + * @param comparator A comparator used for comparing constants. + * @return The resulting partition. + */ + template + Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType, std::set const& atomicPropositions, bool keepRewards = true, storm::utility::ConstantsComparator const& comparator = storm::utility::ConstantsComparator()); + + // A vector mapping each state to its silent probability. + std::vector silentProbabilities; + }; + } +} + +#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file diff --git a/src/storage/bisimulation/Partition.cpp b/src/storage/bisimulation/Partition.cpp new file mode 100644 index 000000000..eade12b0d --- /dev/null +++ b/src/storage/bisimulation/Partition.cpp @@ -0,0 +1,273 @@ +#include "src/storage/bisimulation/Partition.h" + +#include + +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace storage { + namespace bisimulation { + Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates) { + blocks.emplace_back(0, numberOfStates, nullptr, nullptr, blocks.size()); + + // Set up the different parts of the internal structure. + for (storm::storage::sparse::state_type state = 0; state < numberOfStates; ++state) { + states[state] = state; + positions[state] = state; + stateToBlockMapping[state] = &blocks.back(); + } + } + + Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, boost::optional representativeProb1State) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates) { + storm::storage::sparse::state_type position = 0; + Block* firstBlock = nullptr; + Block* secondBlock = nullptr; + Block* thirdBlock = nullptr; + if (!prob0States.empty()) { + blocks.emplace_back(0, prob0States.getNumberOfSetBits(), nullptr, nullptr, blocks.size()); + firstBlock = &blocks[0]; + + for (auto state : prob0States) { + states[position] = state; + positions[state] = position; + stateToBlockMapping[state] = firstBlock; + ++position; + } + firstBlock->setAbsorbing(true); + } + + if (!prob1States.empty()) { + blocks.emplace_back(position, position + prob1States.getNumberOfSetBits(), firstBlock, nullptr, blocks.size()); + secondBlock = &blocks[1]; + + for (auto state : prob1States) { + states[position] = state; + positions[state] = position; + stateToBlockMapping[state] = secondBlock; + ++position; + } + secondBlock->setAbsorbing(true); + secondBlock->setRepresentativeState(representativeProb1State.get()); + } + + storm::storage::BitVector otherStates = ~(prob0States | prob1States); + if (!otherStates.empty()) { + blocks.emplace_back(position, numberOfStates, secondBlock, nullptr, blocks.size()); + thirdBlock = &blocks[2]; + + for (auto state : otherStates) { + states[position] = state; + positions[state] = position; + stateToBlockMapping[state] = thirdBlock; + ++position; + } + } + } + + void 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->positions[state1], this->positions[state2]); + } + + void Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) { + storm::storage::sparse::state_type state1 = this->states[position1]; + storm::storage::sparse::state_type state2 = this->states[position2]; + + std::swap(this->states[position1], this->states[position2]); + this->positions[state1] = position2; + this->positions[state2] = position1; + } + + storm::storage::sparse::state_type const& Partition::getPosition(storm::storage::sparse::state_type state) const { + return this->positions[state]; + } + + void Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) { + this->positions[state] = position; + } + + storm::storage::sparse::state_type const& Partition::getState(storm::storage::sparse::state_type position) const { + return this->states[position]; + } + + void Partition::mapStatesToBlock(Block& block, std::vector::iterator first, std::vector::iterator last) { + for (; first != last; ++first) { + this->stateToBlockMapping[*first] = █ + } + } + + void Partition::mapStatesToPositions(Block const& block) { + storm::storage::sparse::state_type position = block.getBeginIndex(); + for (auto stateIt = this->begin(block), stateIte = this->end(block); stateIt != stateIte; ++stateIt, ++position) { + this->positions[*stateIt] = position; + } + } + + Block& Partition::getBlock(storm::storage::sparse::state_type state) { + return *this->stateToBlockMapping[state]; + } + + Block const& Partition::getBlock(storm::storage::sparse::state_type state) const { + return *this->stateToBlockMapping[state]; + } + + std::vector::const_iterator Partition::begin(Block const& block) const { + return this->states.begin() + block.getBeginIndex(); + } + + std::vector::const_iterator Partition::end(Block const& block) const { + return this->states.begin() + block.getEndIndex(); + } + + Block& 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."); + + // 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.getBeginIndex() || position == block.getEndIndex()) { + return block; + } + + // Actually create the new block. + blocks.emplace_back(block.getBeginIndex(), position, block.getPreviousBlockPointer(), &block, blocks.size()); + Block& newBlock = blocks.back(); + + // Resize the current block appropriately. + block.setBeginIndex(position); + + // Mark both blocks as splitters. + block.markAsSplitter(); + newBlock.markAsSplitter(); + + // Update the mapping of the states in the newly created block. + this->mapStatesToBlock(newBlock, this->begin(newBlock), this->end(newBlock)); + + return newBlock; + } + + void Partition::splitBlock(Block& block, std::function const& lessFunction, std::function const& changedFunction) { + // Sort the range of the block such that all states that have the label are moved to the front. + std::sort(this->begin(block), this->end(block), lessFunction); + + // Update the positions vector. + mapStatesToPositions(block); + + // Now we can check whether the block needs to be split, which is the case iff the changed function returns + // true for the first and last element of the remaining state range. + storm::storage::sparse::state_type begin = block.getBeginIndex(); + storm::storage::sparse::state_type end = block.getEndIndex() - 1; + while (changedFunction(begin, end)) { + // Now we scan for the first state in the block for which the changed function returns true. + // Note that we do not have to check currentIndex for staying within bounds, because we know the matching + // state is within bounds. + storm::storage::sparse::state_type currentIndex = begin + 1; + while (begin != end && !changedFunction(states[begin], states[currentIndex])) { + ++currentIndex; + } + begin = currentIndex; + + this->splitBlock(block, currentIndex); + } + } + + void Partition::split(std::function const& lessFunction, std::function const& changedFunction) { + for (auto& block : blocks) { + splitBlock(block, lessFunction, changedFunction); + } + } + + Block& Partition::splitStates(Block& block, storm::storage::BitVector const& states) { + // Sort the range of the block such that all states that have the label are moved to the front. + std::sort(this->begin(block), this->end(block), [&states] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return states.get(a) && !states.get(b); } ); + + // Update the positions vector. + mapStatesToPositions(block); + + // Now we can find the first position in the block that does not have the label and create new blocks. + std::vector::const_iterator it = std::find_if(this->begin(block), this->end(block), [&states] (storm::storage::sparse::state_type const& a) { return !states.get(a); }); + + if (it != this->begin(block) && it != this->end(block)) { + auto cutPoint = std::distance(this->states.cbegin(), it); + return this->splitBlock(block, cutPoint); + } else { + return block; + } + } + + void Partition::splitStates(storm::storage::BitVector const& states) { + for (auto& block : blocks) { + splitStates(block, states); + } + } + + void Partition::sortBlock(Block const& block) { + std::sort(this->begin(block), this->end(block), [] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return a < b; }); + mapStatesToPositions(block); + } + + 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(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; + } + + std::vector const& Partition::getBlocks() const { + return this->blocks; + } + + std::vector& Partition::getBlocks() { + return this->blocks; + } + + bool Partition::check() const { + for (uint_fast64_t state = 0; state < this->positions.size(); ++state) { + STORM_LOG_ASSERT(this->states[this->positions[state]] == state, "Position mapping corrupted."); + } + for (auto const& block : this->blocks) { + STORM_LOG_ASSERT(block.check(), "Block corrupted."); + for (auto stateIt = this->begin(block), stateIte = this->end(block); stateIt != stateIte; ++stateIt) { + STORM_LOG_ASSERT(this->stateToBlockMapping[*stateIt] == &block, "Block mapping corrupted."); + } + } + return true; + } + + void Partition::print() const { + for (auto const& block : this->blocks) { + block.print(*this); + } + std::cout << "states in partition" << std::endl; + for (auto const& state : states) { + std::cout << state << " "; + } + std::cout << std::endl << "positions: " << std::endl; + for (auto const& index : positions) { + std::cout << index << " "; + } + std::cout << std::endl << "state to block mapping: " << std::endl; + for (auto const& block : stateToBlockMapping) { + std::cout << block << "[" << block->getId() <<"] "; + } + std::cout << std::endl; + std::cout << "size: " << blocks.size() << std::endl; + STORM_LOG_ASSERT(this->check(), "Partition corrupted."); + } + + std::size_t Partition::size() const { + return blocks.size(); + } + + } + } +} \ No newline at end of file diff --git a/src/storage/bisimulation/Partition.h b/src/storage/bisimulation/Partition.h new file mode 100644 index 000000000..6bd2cd8e1 --- /dev/null +++ b/src/storage/bisimulation/Partition.h @@ -0,0 +1,142 @@ +#ifndef STORM_STORAGE_BISIMULATION_PARTITION_H_ +#define STORM_STORAGE_BISIMULATION_PARTITION_H_ + +#include +#include + +#include "src/storage/bisimulation/Block.h" + +#include "src/storage/BitVector.h" + +namespace storm { + namespace storage { + namespace bisimulation { + + class Partition { + public: + /*! + * 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 representativeProb1State If the set of prob1States is non-empty, this needs to be a state + * that is representative for this block in the sense that the state representing this block in the quotient + * model will receive exactly the atomic propositions of the representative state. + */ + Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, boost::optional representativeProb1State); + + Partition() = default; + Partition(Partition const& other) = default; + Partition& operator=(Partition const& other) = default; + Partition(Partition&& other) = default; + Partition& operator=(Partition&& other) = default; + + // Retrieves the size of the partition, i.e. the number of blocks. + std::size_t size() const; + + // Prints the partition to the standard output. + void print() const; + + // Splits the block at the given position and inserts a new block after the current one holding the rest + // of the states. + Block& splitBlock(Block& block, storm::storage::sparse::state_type position); + + // Splits the block by sorting the states according to the given function and then identifying the split + // points via the changed-function. + void splitBlock(Block& block, std::function const& lessFunction, std::function const& changedFunction); + + // Splits all blocks by using the sorting-based splitting. + void split(std::function const& lessFunction, std::function const& changedFunction); + + // Splits the block such that the resulting blocks contain only states in the given set or none at all. + // If the block is split, the given block will contain the states *not* in the given set and the newly + // created block will contain the states *in* the given set. + Block& splitStates(Block& block, storm::storage::BitVector const& states); + + /*! + * Splits all blocks of the partition such that afterwards all blocks contain only states within the given + * set of states or no such state at all. + */ + void splitStates(storm::storage::BitVector const& states); + + // Sorts the block based on the state indices. + void sortBlock(Block const& block); + + // Retrieves the blocks of the partition. + std::vector const& getBlocks() const; + + // Retrieves the blocks of the partition. + std::vector& getBlocks(); + + // Checks the partition for internal consistency. + bool check() const; + + // Returns an iterator to the beginning of the states of the given block. + std::vector::const_iterator begin(Block const& block) const; + + // Returns an iterator to the beginning of the states of the given block. + std::vector::const_iterator end(Block const& block) const; + + // Swaps the positions of the two given states. + void swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2); + + // Retrieves the block of the given state. + Block& getBlock(storm::storage::sparse::state_type state); + + // Retrieves the block of the given state. + Block const& getBlock(storm::storage::sparse::state_type state) const; + + // Retrieves the position of the given state. + storm::storage::sparse::state_type const& getPosition(storm::storage::sparse::state_type state) const; + + // Sets the position of the state to the given position. + storm::storage::sparse::state_type const& getState(storm::storage::sparse::state_type position) const; + + // Updates the block mapping for the given range of states to the specified block. + void mapStatesToBlock(Block& block, std::vector::iterator first, std::vector::iterator last); + + // Update the state to position for the states in the given block. + void mapStatesToPositions(Block const& block); + + private: + // FIXME: necessary? + // Swaps the positions of the two states given by their positions. + void swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2); + + // 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; + + // A mapping of states to their blocks. + std::vector stateToBlockMapping; + + // A vector containing all the states. It is ordered in a way such that the blocks only need to define + // their start/end indices. + std::vector states; + + // This vector keeps track of the position of each state in the state vector. + std::vector positions; + }; + } + } +} + +#endif /* STORM_STORAGE_BISIMULATION_PARTITION_H_ */ diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 725a41392..96cf57a31 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -162,6 +162,12 @@ namespace storm { return this->getBaseExpression().accept(visitor); } + std::string Expression::toString() { + std::stringstream stream; + stream << *this; + return stream.str(); + } + std::ostream& operator<<(std::ostream& stream, Expression const& expression) { stream << expression.getBaseExpression(); return stream; diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index c6ecdcbec..e8fe0e60b 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -292,6 +292,13 @@ namespace storm { */ boost::any accept(ExpressionVisitor& visitor) const; + /*! + * Converts the expression into a string. + * + * @return The string representation of the expression. + */ + std::string toString(); + friend std::ostream& operator<<(std::ostream& stream, Expression const& expression); private: diff --git a/src/utility/storm.h b/src/utility/storm.h index be76720fe..3281d342b 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -43,7 +43,7 @@ #include "src/builder/DdPrismModelBuilder.h" // Headers for model processing. -#include "src/storage/DeterministicModelBisimulationDecomposition.h" +#include "src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h" // Headers for model checking. #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" diff --git a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp index 5081e9e02..eeb7298b7 100644 --- a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp +++ b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/parser/AutoParser.h" -#include "src/storage/DeterministicModelBisimulationDecomposition.h" +#include "src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h" #include "src/models/sparse/StandardRewardModel.h" TEST(DeterministicModelBisimulationDecomposition, Die) {