diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index e42b56228..178b5a965 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -160,9 +160,6 @@ namespace storm { this->performPartitionRefinement(); std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart; - std::cout << "final partition: " << std::endl; - this->partition.print(); - 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; @@ -197,7 +194,7 @@ namespace storm { void BisimulationDecomposition::performPartitionRefinement() { // Insert all blocks into the splitter queue as a (potential) splitter. std::deque*> splitterQueue; - std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (std::unique_ptr> const& block) { splitterQueue.push_back(block.get()); } ); + std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (std::unique_ptr> const& block) { block->data().setSplitter(); splitterQueue.push_back(block.get()); } ); // Then perform the actual splitting until there are no more splitters. uint_fast64_t iterations = 0; diff --git a/src/storage/bisimulation/Block.cpp b/src/storage/bisimulation/Block.cpp index bb38b5f86..812e3b89b 100644 --- a/src/storage/bisimulation/Block.cpp +++ b/src/storage/bisimulation/Block.cpp @@ -37,6 +37,11 @@ namespace storm { template void Block::print(Partition const& partition) const { std::cout << "block [" << this << "] " << this->id << " from " << this->beginIndex << " to " << this->endIndex << " with data [" << this->data() << "]" << std::endl; + std::cout << "states "; + for (auto stateIt = partition.begin(*this), stateIte = partition.end(*this); stateIt != stateIte; ++stateIt) { + std::cout << *stateIt << ", "; + } + std::cout << std::endl; } template diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index 58296b254..5805fe15d 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -256,7 +256,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::exploreRemainingStatesOfSplitter(bisimulation::Block& splitter) { + void DeterministicModelBisimulationDecomposition::exploreRemainingStatesOfSplitter(bisimulation::Block& splitter, std::list*>& predecessorBlocks) { for (auto splitterIt = this->partition.begin(splitter), splitterIte = this->partition.begin(splitter) + (splitter.data().marker2() - splitter.getBeginIndex()); splitterIt != splitterIte; ++splitterIt) { storm::storage::sparse::state_type currentState = *splitterIt; @@ -268,7 +268,7 @@ namespace storm { if (!possiblyNeedsRefinement(predecessorBlock)) { continue; } - + // We keep track of the probability of the predecessor moving to the splitter. increaseProbabilityToSplitter(predecessor, predecessorBlock, predecessorEntry.getValue()); @@ -277,6 +277,8 @@ namespace storm { if (predecessorPosition >= predecessorBlock.data().marker1()) { moveStateToMarker1(predecessor, predecessorBlock); } + + insertIntoPredecessorList(predecessorBlock, predecessorBlocks); } } @@ -286,14 +288,14 @@ namespace storm { template void DeterministicModelBisimulationDecomposition::updateSilentProbabilitiesBasedOnProbabilitiesToSplitter(bisimulation::Block& block) { - // For all states that do not have a successor in the block itself, we need to set the silent probability to 0. - std::for_each(silentProbabilities.begin() + block.data().marker1(), silentProbabilities.begin() + block.getEndIndex(), [] (ValueType& val) { val = storm::utility::zero(); } ); - - // For all states that do have a successor in the block, we set the silent probability to the probability - // stored in the vector of probabilities going to the splitter. - auto it = boost::make_zip_iterator(boost::make_tuple(silentProbabilities.begin() + block.getBeginIndex(), probabilitiesToCurrentSplitter.begin() + block.getBeginIndex())); - auto ite = boost::make_zip_iterator(boost::make_tuple(silentProbabilities.begin() + block.data().marker1(), probabilitiesToCurrentSplitter.begin() + block.data().marker1())); - std::for_each(it, ite, [] (boost::tuple const& tuple) { boost::get<0>(tuple) = boost::get<1>(tuple); } ); + // For all predecessors, we can set the probability to the current probability of moving to the splitter. + for (auto stateIt = this->partition.begin(block), stateIte = this->partition.begin() + block.data().marker1(); stateIt != stateIte; ++stateIt) { + silentProbabilities[*stateIt] = probabilitiesToCurrentSplitter[*stateIt]; + } + // All non-predecessors have a silent probability of zero. + for (auto stateIt = this->partition.begin() + block.data().marker1(), stateIte = this->partition.end(block); stateIt != stateIte; ++stateIt) { + silentProbabilities[*stateIt] = storm::utility::zero(); + } } template @@ -313,13 +315,11 @@ namespace storm { template void DeterministicModelBisimulationDecomposition::computeConditionalProbabilitiesForNonSilentStates(bisimulation::Block& block) { - auto it = boost::make_zip_iterator(boost::make_tuple(silentProbabilities.begin() + block.getBeginIndex(), probabilitiesToCurrentSplitter.begin() + block.getBeginIndex())); - auto ite = boost::make_zip_iterator(boost::make_tuple(silentProbabilities.begin() + block.data().marker1(), probabilitiesToCurrentSplitter.begin() + block.data().marker1())); - std::for_each(it, ite, [this] (boost::tuple const& tuple) { - if (!this->comparator.isZero(boost::get<0>(tuple))) { - boost::get<1>(tuple) /= storm::utility::one() - boost::get<0>(tuple); + for (auto stateIt = this->partition.begin() + block.getBeginIndex(), stateIte = this->partition.begin() + block.data().marker1(); stateIt != stateIte; ++stateIt) { + if (!this->comparator.isOne(getSilentProbability(*stateIt))) { + probabilitiesToCurrentSplitter[*stateIt] /= storm::utility::one() - getSilentProbability(*stateIt); } - } ); + } } template @@ -334,13 +334,11 @@ namespace storm { // 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.getNumberOfStates(), storm::storage::BitVector(nonSilentBlockIndices.size() - 1)); - std::cout << "creating " << block.getNumberOfStates() << " labels " << std::endl; std::vector stateStack; stateStack.reserve(block.getNumberOfStates()); for (uint_fast64_t stateClassIndex = 0; stateClassIndex < nonSilentBlockIndices.size() - 1; ++stateClassIndex) { for (auto stateIt = this->partition.begin() + nonSilentBlockIndices[stateClassIndex], stateIte = this->partition.begin() + nonSilentBlockIndices[stateClassIndex + 1]; stateIt != stateIte; ++stateIt) { - std::cout << "moving backward from state " << *stateIt << std::endl; stateStack.push_back(*stateIt); stateLabels[this->partition.getPosition(*stateIt) - block.getBeginIndex()].set(stateClassIndex); @@ -351,20 +349,13 @@ namespace storm { for (auto const& predecessorEntry : this->backwardTransitions.getRow(currentState)) { storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); - std::cout << " found pred " << predecessor << " with value " << predecessorEntry.getValue() << std::endl; if (this->comparator.isZero(predecessorEntry.getValue())) { continue; } - + // Only if the state is in the same block, is a silent state and it has not yet been // labeled with the current label. - std::cout << "pred is at " << this->partition.getPosition(predecessor) << std::endl; - std::cout << "begin of block " << block.getBeginIndex() << std::endl; - std::cout << "accessing index " << (this->partition.getPosition(predecessor) - block.getBeginIndex()) << " of " << stateLabels.size() << std::endl; - std::cout << predecessor << " is in the same block as " << block.getId() << " ? " << (this->partition.getBlock(predecessor) == block) << std::endl; -// std::cout << isSilent(predecessor) << ", " << stateLabels[this->partition.getPosition(predecessor) - block.getBeginIndex()].get(stateClassIndex) << std::endl; if (this->partition.getBlock(predecessor) == block && isSilent(predecessor) && !stateLabels[this->partition.getPosition(predecessor) - block.getBeginIndex()].get(stateClassIndex)) { - std::cout << "assigning label " << stateClassIndex << std::endl; stateStack.push_back(predecessor); stateLabels[this->partition.getPosition(predecessor) - block.getBeginIndex()].set(stateClassIndex); } @@ -378,38 +369,20 @@ namespace storm { template void DeterministicModelBisimulationDecomposition::refinePredecessorBlockOfSplitterWeak(bisimulation::Block& block, std::deque*>& splitterQueue) { + // First, we need to turn the one-step probabilities to go to the splitter to the conditional probabilities + // for all non-silent states. computeConditionalProbabilitiesForNonSilentStates(block); - // First, we need to compute a labeling of the states that expresses which of the non-silent blocks they can reach. - std::vector nonSilentBlockIndices = computeNonSilentBlocks(block); - std::cout << "indices: " << std::endl; - for (auto el : nonSilentBlockIndices) { - std::cout << el << std::endl; - } - - for (int ind = 0; ind < nonSilentBlockIndices.size() - 1; ++ind) { - for (int inner = nonSilentBlockIndices[ind]; inner < nonSilentBlockIndices[ind + 1]; ++inner) { - std::cout << this->partition.getState(inner) << " is in class " << ind << std::endl; - } - } + // Then, we need to compute a labeling of the states that expresses which of the non-silent blocks they can reach. + std::vector nonSilentBlockIndices = computeNonSilentBlocks(block); std::vector weakStateLabels = computeWeakStateLabelingBasedOnNonSilentBlocks(block, nonSilentBlockIndices); - std::cout << "labels: " << std::endl; - for (auto el : weakStateLabels) { - std::cout << el << std::endl; - } - // Then split the block according to this labeling. // CAUTION: that this assumes that the positions of the states in the partition are not update until after // the sorting is over. Otherwise, this interferes with the data used in the sorting process. storm::storage::sparse::state_type originalBlockIndex = block.getBeginIndex(); - auto result = this->partition.splitBlock(block, + auto split = this->partition.splitBlock(block, [&weakStateLabels,&block,originalBlockIndex,this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { - std::cout << "comparing states " << state1 << " and " << state2 << std::endl; - std::cout << (this->partition.getPosition(state1) - originalBlockIndex) << " and " << (this->partition.getPosition(state2) - originalBlockIndex) << std::endl; - std::cout << "size: " << weakStateLabels.size() << std::endl; - std::cout << "begin is " << block.getBeginIndex() << std::endl; - std::cout << "orig begin " << originalBlockIndex << std::endl; return weakStateLabels[this->partition.getPosition(state1) - originalBlockIndex] < weakStateLabels[this->partition.getPosition(state2) - originalBlockIndex]; }, [this, &splitterQueue] (bisimulation::Block& block) { @@ -420,33 +393,41 @@ namespace storm { splitterQueue.emplace_back(&block); }); - // If the block was split, we also update the silent probabilities of the - if (result) { + // If the block was split, we also update the silent probabilities. + if (split) { updateSilentProbabilitiesBasedOnTransitions(block); - // Insert the new block as a splitter. - block.data().setSplitter(); - splitterQueue.emplace_back(&block); - } else { - block.resetMarkers(); + if (!block.data().splitter()) { + // Insert the new block as a splitter. + block.data().setSplitter(); + splitterQueue.emplace_back(&block); + } } } template void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::deque*>& splitterQueue) { for (auto block : predecessorBlocks) { - std::cout << "found predecessor block " << block->getId() << std::endl; if (*block != splitter) { refinePredecessorBlockOfSplitterWeak(*block, splitterQueue); } else { // If the block to split is the splitter itself, we must not do any splitting here. - block->resetMarkers(); } + block->resetMarkers(); block->data().setNeedsRefinement(false); } } + template + void DeterministicModelBisimulationDecomposition::insertIntoPredecessorList(bisimulation::Block& predecessorBlock, std::list*>& predecessorBlocks) { + // Insert the block into the list of blocks to refine (if that has not already happened). + if (!predecessorBlock.data().needsRefinement()) { + predecessorBlocks.emplace_back(&predecessorBlock); + predecessorBlock.data().setNeedsRefinement(); + } + } + template void DeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) { // The outline of the refinement is as follows. @@ -464,11 +445,6 @@ namespace storm { // // Finally, we use the information obtained in the first part for the actual splitting process in which all // predecessor blocks of the splitter are split based on the probabilities computed earlier. - - std::cout << "current partition is" << std::endl; - this->partition.print(); - std::cout << "refining using splitter " << splitter.getId() << std::endl; - std::list*> predecessorBlocks; storm::storage::sparse::state_type currentPosition = splitter.getBeginIndex(); bool splitterIsPredecessorBlock = false; @@ -500,11 +476,7 @@ namespace storm { moveStateInSplitter(predecessor, predecessorBlock, currentPosition, elementsToSkip); } - // Insert the block into the list of blocks to refine (if that has not already happened). - if (!predecessorBlock.data().needsRefinement()) { - predecessorBlocks.emplace_back(&predecessorBlock); - predecessorBlock.data().setNeedsRefinement(); - } + insertIntoPredecessorList(predecessorBlock, predecessorBlocks); } } @@ -516,7 +488,7 @@ namespace storm { // If the splitter was a predecessor block of itself, we potentially need to explore some states that have // not been explored yet. if (splitterIsPredecessorBlock) { - exploreRemainingStatesOfSplitter(splitter); + exploreRemainingStatesOfSplitter(splitter, predecessorBlocks); } // Finally, we split the block based on the precomputed probabilities and the chosen bisimulation type. diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h index 4f0c5dd76..b49390659 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h @@ -88,7 +88,7 @@ namespace storm { void increaseProbabilityToSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block const& predecessorBlock, ValueType const& value); // Explores the remaining predecessors of the splitter. - void exploreRemainingStatesOfSplitter(bisimulation::Block& splitter); + void exploreRemainingStatesOfSplitter(bisimulation::Block& splitter, std::list*>& predecessorBlocks); // Updates the silent probabilities of the states in the block based on the probabilities of going to the splitter. void updateSilentProbabilitiesBasedOnProbabilitiesToSplitter(bisimulation::Block& block); @@ -113,6 +113,9 @@ namespace storm { // Computes a labeling for all states of the block that identifies in which block they need to end up. std::vector computeWeakStateLabelingBasedOnNonSilentBlocks(bisimulation::Block const& block, std::vector const& nonSilentBlockIndices); + // Inserts the block into the list of predecessors if it is not already contained. + void insertIntoPredecessorList(bisimulation::Block& predecessorBlock, std::list*>& predecessorBlocks); + // A vector that holds the probabilities of states going into the splitter. This is used by the method that // refines a block based on probabilities. std::vector probabilitiesToCurrentSplitter; diff --git a/src/storage/bisimulation/Partition.cpp b/src/storage/bisimulation/Partition.cpp index ff432fa11..d72fe80cc 100644 --- a/src/storage/bisimulation/Partition.cpp +++ b/src/storage/bisimulation/Partition.cpp @@ -211,8 +211,6 @@ namespace storm { std::pair>>::iterator, bool> Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) { STORM_LOG_THROW(position >= block.getBeginIndex() && position <= block.getEndIndex(), storm::exceptions::InvalidArgumentException, "Cannot split block at illegal position."); - std::cout << "splitting block " << block.getId() << " at pos " << position << std::endl; - // 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()) { @@ -242,21 +240,13 @@ namespace storm { auto originalBegin = block.getBeginIndex(); auto originalEnd = block.getEndIndex(); - std::cout << "sorted block:" << std::endl; - for (auto stateIt = this->begin(block), stateIte = this->end(block); stateIt != stateIte; ++stateIt) { - std::cout << *stateIt << std::endl; - } - auto it = this->states.cbegin() + block.getBeginIndex(); auto ite = this->states.cbegin() + block.getEndIndex(); - std::cout << "splitting between " << block.getBeginIndex() << " and " << block.getEndIndex() << std::endl; bool wasSplit = false; std::vector::const_iterator upperBound; do { - std::cout << "it (" << *it << ") less than ite-1 (" << *(ite-1) << "? " << less(*it, *(ite - 1)) << std::endl; upperBound = std::upper_bound(it, ite, *it, less); - std::cout << "upper bound is " << std::distance(this->states.cbegin(), upperBound); if (upperBound != ite) { wasSplit = true; auto result = this->splitBlock(block, std::distance(this->states.cbegin(), upperBound));