sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Changed deque to vector in bisimulation to gain performance boost 

Former-commit-id: 5db8e917b4
tempestpy_adaptions
Mavo 8 years ago
parent
82a3964e5d
commit
d1d77ff4df
6 changed files with 42 additions and 42 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 16
      src/storage/bisimulation/BisimulationDecomposition.cpp
  2. 8
      src/storage/bisimulation/BisimulationDecomposition.h
  3. 28
      src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
  4. 10
      src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h
  5. 14
      src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp
  6. 8
      src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h

16
src/storage/bisimulation/BisimulationDecomposition.cpp
View File

@ -230,25 +230,25 @@ namespace storm {
template<typename ModelType, typename BlockDataType>
void BisimulationDecomposition<ModelType, BlockDataType>::performPartitionRefinement() {
// Insert all blocks into the splitter queue as a (potential) splitter.
std::deque<Block<BlockDataType>*> splitterQueue;
std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (std::unique_ptr<Block<BlockDataType>> const& block) { block->data().setSplitter(); splitterQueue.push_back(block.get()); } );
// Insert all blocks into the splitter vector as a (potential) splitter.
std::vector<Block<BlockDataType>*> splitterVector;
std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (std::unique_ptr<Block<BlockDataType>> 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<BlockDataType> const* b1, Block<BlockDataType> const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } );
Block<BlockDataType>* splitter = splitterQueue.front();
splitterQueue.pop_front();
std::sort(splitterVector.begin(), splitterVector.end(), [] (Block<BlockDataType> const* b1, Block<BlockDataType> const* b2) { return b1->getNumberOfStates() > b2->getNumberOfStates(); } );
Block<BlockDataType>* splitter = splitterVector.back();
splitterVector.pop_back();
splitter->data().setSplitter(false);
// Now refine the partition using the current splitter.
refinePartitionBasedOnSplitter(*splitter, splitterQueue);
refinePartitionBasedOnSplitter(*splitter, splitterVector);
}
}

8
src/storage/bisimulation/BisimulationDecomposition.h
View File

@ -1,7 +1,7 @@
#ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
#define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
#include <deque>
#include <vector>
#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<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) = 0;
virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterVector) = 0;
/*!
* Builds the quotient model based on the previously computed equivalence classes (stored in the blocks

28
src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
View File

@ -157,7 +157,7 @@ namespace storm {
}
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterStrong(std::list<Block<BlockDataType>*> const& predecessorBlocks, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) {
void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterStrong(std::list<Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& 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<BlockDataType>& block) {
splitterQueue.emplace_back(&block); block.data().setSplitter();
[&splitterVector] (Block<BlockDataType>& 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<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlockOfSplitterWeak(bisimulation::Block<BlockDataType>& block, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) {
void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlockOfSplitterWeak(bisimulation::Block<BlockDataType>& block, std::vector<bisimulation::Block<BlockDataType>*>& 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<BlockDataType>& block) {
[this, &splitterVector] (bisimulation::Block<BlockDataType>& 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<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) {
void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& 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<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) {
void DeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& 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);
}
}

10
src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h
View File

@ -39,11 +39,11 @@ namespace storm {
virtual void buildQuotient() override;
virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) override;
virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterVector) override;
private:
// Refines the predecessor blocks wrt. strong bisimulation.
void refinePredecessorBlocksOfSplitterStrong(std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue);
void refinePredecessorBlocksOfSplitterStrong(std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterVector);
/*!
* Performs the necessary steps to compute a weak bisimulation on a DTMC.
@ -99,10 +99,10 @@ namespace storm {
void updateSilentProbabilitiesBasedOnTransitions(bisimulation::Block<BlockDataType>& block);
// Refines the predecessor blocks of the splitter wrt. weak bisimulation in DTMCs.
void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue);
void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterVector);
// Refines the given block wrt to weak bisimulation in DTMCs.
void refinePredecessorBlockOfSplitterWeak(bisimulation::Block<BlockDataType>& block, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue);
void refinePredecessorBlockOfSplitterWeak(bisimulation::Block<BlockDataType>& block, std::vector<bisimulation::Block<BlockDataType>*>& 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_ */
#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */

14
src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp
View File

@ -198,7 +198,7 @@ namespace storm {
}
template<typename ModelType>
void NondeterministicModelBisimulationDecomposition<ModelType>::updateQuotientDistributionsOfPredecessors(Block<BlockDataType> const& newBlock, Block<BlockDataType> const& oldBlock, std::deque<Block<BlockDataType>*>& splitterQueue) {
void NondeterministicModelBisimulationDecomposition<ModelType>::updateQuotientDistributionsOfPredecessors(Block<BlockDataType> const& newBlock, Block<BlockDataType> const& oldBlock, std::vector<Block<BlockDataType>*>& 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<typename ModelType>
bool NondeterministicModelBisimulationDecomposition<ModelType>::splitBlockAccordingToCurrentQuotientDistributions(Block<BlockDataType>& block, std::deque<Block<BlockDataType>*>& splitterQueue) {
bool NondeterministicModelBisimulationDecomposition<ModelType>::splitBlockAccordingToCurrentQuotientDistributions(Block<BlockDataType>& block, std::vector<Block<BlockDataType>*>& splitterVector) {
std::list<Block<BlockDataType>*> 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<BlockDataType>& newBlock) {
[this, &block, &splitterVector, &newBlocks] (Block<BlockDataType>& 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<typename ModelType>
void NondeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) {
void NondeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterVector) {
if (!possiblyNeedsRefinement(splitter)) {
return;
}
STORM_LOG_TRACE("Refining block " << splitter.getId());
splitBlockAccordingToCurrentQuotientDistributions(splitter, splitterQueue);
splitBlockAccordingToCurrentQuotientDistributions(splitter, splitterVector);
}
template class NondeterministicModelBisimulationDecomposition<storm::models::sparse::Mdp<double>>;

8
src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h
View File

@ -37,7 +37,7 @@ namespace storm {
virtual void buildQuotient() override;
virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) override;
virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterVector) override;
virtual void initialize() override;
@ -52,7 +52,7 @@ namespace storm {
bool possiblyNeedsRefinement(bisimulation::Block<BlockDataType> const& block) const;
// Splits the given block according to the current quotient distributions.
bool splitBlockAccordingToCurrentQuotientDistributions(bisimulation::Block<BlockDataType>& block, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue);
bool splitBlockAccordingToCurrentQuotientDistributions(bisimulation::Block<BlockDataType>& block, std::vector<bisimulation::Block<BlockDataType>*>& 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<BlockDataType> const& newBlock, bisimulation::Block<BlockDataType> const& oldBlock, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue);
void updateQuotientDistributionsOfPredecessors(bisimulation::Block<BlockDataType> const& newBlock, bisimulation::Block<BlockDataType> const& oldBlock, std::vector<bisimulation::Block<BlockDataType>*>& splitterVector);
bool checkQuotientDistributions() const;
bool checkBlockStable(bisimulation::Block<BlockDataType> const& newBlock) const;
@ -81,4 +81,4 @@ namespace storm {
}
}
#endif /* STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */
#endif /* STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */
Write Preview
Loading…
Cancel
Save