diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index 4b31551f9..33d4cffcc 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -230,25 +230,25 @@ namespace storm { template 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) { block->data().setSplitter(); splitterQueue.push_back(block.get()); } ); + // Insert all blocks into the splitter vector as a (potential) splitter. + std::vector*> splitterVector; + std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (std::unique_ptr> const& block) { block->data().setSplitter(); splitterVector.push_back(block.get()); } ); // Then perform the actual splitting until there are no more splitters. uint_fast64_t iterations = 0; - while (!splitterQueue.empty()) { + while (!splitterVector.empty()) { ++iterations; // Get and prepare the next splitter. // Sort the splitters according to their sizes to prefer small splitters. That is just a heuristic, but // tends to work well. - std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } ); - Block* splitter = splitterQueue.front(); - splitterQueue.pop_front(); + std::sort(splitterVector.begin(), splitterVector.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() > b2->getNumberOfStates(); } ); + Block* splitter = splitterVector.back(); + splitterVector.pop_back(); splitter->data().setSplitter(false); // Now refine the partition using the current splitter. - refinePartitionBasedOnSplitter(*splitter, splitterQueue); + refinePartitionBasedOnSplitter(*splitter, splitterVector); } } diff --git a/src/storage/bisimulation/BisimulationDecomposition.h b/src/storage/bisimulation/BisimulationDecomposition.h index 6d86f2df9..df951bce3 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.h +++ b/src/storage/bisimulation/BisimulationDecomposition.h @@ -1,7 +1,7 @@ #ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ #define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ -#include +#include #include "src/settings/SettingsManager.h" #include "src/settings/modules/BisimulationSettings.h" @@ -219,12 +219,12 @@ namespace storm { /*! * 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. + * because of this refinement, are marked as splitters and inserted into the splitter vector. * * @param splitter The splitter to use. - * @param splitterQueue The queue into which to insert the newly discovered potential splitters. + * @param splitterVector The vector into which to insert the newly discovered potential splitters. */ - virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) = 0; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::vector*>& splitterVector) = 0; /*! * Builds the quotient model based on the previously computed equivalence classes (stored in the blocks diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index e968c98cd..dcc12fbfb 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -157,7 +157,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::deque*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::vector*>& splitterVector) { for (auto block : predecessorBlocks) { STORM_LOG_TRACE("Refining predecessor " << block->getId() << " of splitter"); @@ -176,15 +176,15 @@ namespace storm { [this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { return this->comparator.isLess(getProbabilityToSplitter(state1), getProbabilityToSplitter(state2)); }, - [&splitterQueue] (Block& block) { - splitterQueue.emplace_back(&block); block.data().setSplitter(); + [&splitterVector] (Block& block) { + splitterVector.emplace_back(&block); block.data().setSplitter(); }); - // If the predecessor block was split, we need to insert it into the splitter queue if it is not already + // If the predecessor block was split, we need to insert it into the splitter vector if it is not already // marked as a splitter. if (split && !blockToRefineProbabilistically->data().splitter()) { - splitterQueue.emplace_back(blockToRefineProbabilistically); + splitterVector.emplace_back(blockToRefineProbabilistically); blockToRefineProbabilistically->data().setSplitter(); } @@ -378,7 +378,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::refinePredecessorBlockOfSplitterWeak(bisimulation::Block& block, std::deque*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePredecessorBlockOfSplitterWeak(bisimulation::Block& block, std::vector*>& splitterVector) { // 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); @@ -395,12 +395,12 @@ namespace storm { [&weakStateLabels,&block,originalBlockIndex,this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { return weakStateLabels[this->partition.getPosition(state1) - originalBlockIndex] < weakStateLabels[this->partition.getPosition(state2) - originalBlockIndex]; }, - [this, &splitterQueue] (bisimulation::Block& block) { + [this, &splitterVector] (bisimulation::Block& block) { updateSilentProbabilitiesBasedOnTransitions(block); // Insert the new block as a splitter. block.data().setSplitter(); - splitterQueue.emplace_back(&block); + splitterVector.emplace_back(&block); }); // If the block was split, we also update the silent probabilities. @@ -410,16 +410,16 @@ namespace storm { if (!block.data().splitter()) { // Insert the new block as a splitter. block.data().setSplitter(); - splitterQueue.emplace_back(&block); + splitterVector.emplace_back(&block); } } } template - void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::deque*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::vector*>& splitterVector) { for (auto block : predecessorBlocks) { if (*block != splitter) { - refinePredecessorBlockOfSplitterWeak(*block, splitterQueue); + refinePredecessorBlockOfSplitterWeak(*block, splitterVector); } else { // If the block to split is the splitter itself, we must not do any splitting here. } @@ -439,7 +439,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::vector*>& splitterVector) { STORM_LOG_TRACE("Refining partition based on splitter " << splitter.getId()); // The outline of the refinement is as follows. @@ -513,7 +513,7 @@ namespace storm { if (this->options.getType() == BisimulationType::Strong || this->model.getType() == storm::models::ModelType::Ctmc) { // In the case of CTMCs and weak bisimulation, we still call the "splitStrong" method, but we already have // taken care of not adding the splitter to the predecessor blocks, so this is safe. - refinePredecessorBlocksOfSplitterStrong(predecessorBlocks, splitterQueue); + refinePredecessorBlocksOfSplitterStrong(predecessorBlocks, splitterVector); } else { // If the splitter is a predecessor of we can use the computed probabilities to update the silent // probabilities. @@ -521,7 +521,7 @@ namespace storm { updateSilentProbabilitiesBasedOnProbabilitiesToSplitter(splitter); } - refinePredecessorBlocksOfSplitterWeak(splitter, predecessorBlocks, splitterQueue); + refinePredecessorBlocksOfSplitterWeak(splitter, predecessorBlocks, splitterVector); } } diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h index b9f2a2a5a..b460dfa5d 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h @@ -39,11 +39,11 @@ namespace storm { virtual void buildQuotient() override; - virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) override; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::vector*>& splitterVector) override; private: // Refines the predecessor blocks wrt. strong bisimulation. - void refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::deque*>& splitterQueue); + void refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::vector*>& splitterVector); /*! * Performs the necessary steps to compute a weak bisimulation on a DTMC. @@ -99,10 +99,10 @@ namespace storm { void updateSilentProbabilitiesBasedOnTransitions(bisimulation::Block& block); // Refines the predecessor blocks of the splitter wrt. weak bisimulation in DTMCs. - void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::deque*>& splitterQueue); + void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::vector*>& splitterVector); // Refines the given block wrt to weak bisimulation in DTMCs. - void refinePredecessorBlockOfSplitterWeak(bisimulation::Block& block, std::deque*>& splitterQueue); + void refinePredecessorBlockOfSplitterWeak(bisimulation::Block& block, std::vector*>& splitterVector); // Converts the one-step probabilities of going into the splitter into the conditional probabilities needed // for weak bisimulation (on DTMCs). @@ -127,4 +127,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp index 2e7d54113..fe53c6602 100644 --- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp @@ -198,7 +198,7 @@ namespace storm { } template - void NondeterministicModelBisimulationDecomposition::updateQuotientDistributionsOfPredecessors(Block const& newBlock, Block const& oldBlock, std::deque*>& splitterQueue) { + void NondeterministicModelBisimulationDecomposition::updateQuotientDistributionsOfPredecessors(Block const& newBlock, Block const& oldBlock, std::vector*>& splitterVector) { uint_fast64_t lastState = 0; bool lastStateInitialized = false; @@ -220,7 +220,7 @@ namespace storm { // If the predecessor block is not marked as to-refined, we do so now. if (!predecessorBlock.data().splitter()) { predecessorBlock.data().setSplitter(); - splitterQueue.push_back(&predecessorBlock); + splitterVector.push_back(&predecessorBlock); } if (lastStateInitialized) { @@ -332,7 +332,7 @@ namespace storm { } template - bool NondeterministicModelBisimulationDecomposition::splitBlockAccordingToCurrentQuotientDistributions(Block& block, std::deque*>& splitterQueue) { + bool NondeterministicModelBisimulationDecomposition::splitBlockAccordingToCurrentQuotientDistributions(Block& block, std::vector*>& splitterVector) { std::list*> newBlocks; bool split = this->partition.splitBlock(block, [this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { @@ -340,7 +340,7 @@ namespace storm { // std::cout << state1 << " is " << (!result ? "not" : "") << " smaller than " << state2 << std::endl; return result; }, - [this, &block, &splitterQueue, &newBlocks] (Block& newBlock) { + [this, &block, &splitterVector, &newBlocks] (Block& newBlock) { newBlocks.push_back(&newBlock); // this->checkBlockStable(newBlock); @@ -357,7 +357,7 @@ namespace storm { // defer updating the quotient distributions until *after* all splits, because // it otherwise influences the subsequent splits! for (auto el : newBlocks) { - this->updateQuotientDistributionsOfPredecessors(*el, block, splitterQueue); + this->updateQuotientDistributionsOfPredecessors(*el, block, splitterVector); } // this->checkQuotientDistributions(); @@ -405,14 +405,14 @@ namespace storm { } template - void NondeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) { + void NondeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::vector*>& splitterVector) { if (!possiblyNeedsRefinement(splitter)) { return; } STORM_LOG_TRACE("Refining block " << splitter.getId()); - splitBlockAccordingToCurrentQuotientDistributions(splitter, splitterQueue); + splitBlockAccordingToCurrentQuotientDistributions(splitter, splitterVector); } template class NondeterministicModelBisimulationDecomposition>; diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h index 18a6e8e58..38feaf36a 100644 --- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h @@ -37,7 +37,7 @@ namespace storm { virtual void buildQuotient() override; - virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) override; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::vector*>& splitterVector) override; virtual void initialize() override; @@ -52,7 +52,7 @@ namespace storm { bool possiblyNeedsRefinement(bisimulation::Block const& block) const; // Splits the given block according to the current quotient distributions. - bool splitBlockAccordingToCurrentQuotientDistributions(bisimulation::Block& block, std::deque*>& splitterQueue); + bool splitBlockAccordingToCurrentQuotientDistributions(bisimulation::Block& block, std::vector*>& splitterVector); // Retrieves whether the quotient distributions of state 1 are considered to be less than the ones of state 2. bool quotientDistributionsLess(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) const; @@ -62,7 +62,7 @@ namespace storm { // Updates the quotient distributions of the predecessors of the new block by taking the probability mass // away from the old block. - void updateQuotientDistributionsOfPredecessors(bisimulation::Block const& newBlock, bisimulation::Block const& oldBlock, std::deque*>& splitterQueue); + void updateQuotientDistributionsOfPredecessors(bisimulation::Block const& newBlock, bisimulation::Block const& oldBlock, std::vector*>& splitterVector); bool checkQuotientDistributions() const; bool checkBlockStable(bisimulation::Block const& newBlock) const; @@ -81,4 +81,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */