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

went from deque to vector-based representation of splitter queue in bisimulation 

Former-commit-id: 7047192641
tempestpy_adaptions
dehnert 8 years ago
parent
8e565a2930
commit
cb97da887c
6 changed files with 22 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
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      src/storage/bisimulation/BisimulationDecomposition.cpp
  2. 4
      src/storage/bisimulation/BisimulationDecomposition.h
  3. 8
      src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
  4. 8
      src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h
  5. 26
      src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp
  6. 6
      src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h

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

@ -231,7 +231,7 @@ namespace storm {
template<typename ModelType, typename BlockDataType> template<typename ModelType, typename BlockDataType>
void BisimulationDecomposition<ModelType, BlockDataType>::performPartitionRefinement() { void BisimulationDecomposition<ModelType, BlockDataType>::performPartitionRefinement() {
// Insert all blocks into the splitter queue as a (potential) splitter. // Insert all blocks into the splitter queue as a (potential) splitter.
std::deque<Block<BlockDataType>*> splitterQueue;
std::vector<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()); } ); std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (std::unique_ptr<Block<BlockDataType>> const& block) { block->data().setSplitter(); splitterQueue.push_back(block.get()); } );
// Then perform the actual splitting until there are no more splitters. // Then perform the actual splitting until there are no more splitters.
@ -242,9 +242,9 @@ namespace storm {
// Get and prepare the next splitter. // Get and prepare the next splitter.
// Sort the splitters according to their sizes to prefer small splitters. That is just a heuristic, but // Sort the splitters according to their sizes to prefer small splitters. That is just a heuristic, but
// tends to work well. // 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(splitterQueue.begin(), splitterQueue.end(), [] (Block<BlockDataType> const* b1, Block<BlockDataType> const* b2) { return b1->getNumberOfStates() > b2->getNumberOfStates(); } );
Block<BlockDataType>* splitter = splitterQueue.back();
splitterQueue.pop_back();
splitter->data().setSplitter(false); splitter->data().setSplitter(false);
// Now refine the partition using the current splitter. // Now refine the partition using the current splitter.

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

@ -1,8 +1,6 @@
#ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ #ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
#define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ #define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
#include <deque>
#include "src/settings/SettingsManager.h" #include "src/settings/SettingsManager.h"
#include "src/settings/modules/BisimulationSettings.h" #include "src/settings/modules/BisimulationSettings.h"
#include "src/storage/sparse/StateType.h" #include "src/storage/sparse/StateType.h"
@ -224,7 +222,7 @@ namespace storm {
* @param splitter The splitter to use. * @param splitter The splitter to use.
* @param splitterQueue The queue into which to insert the newly discovered potential splitters. * @param splitterQueue The queue 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>*>& splitterQueue) = 0;
/*! /*!
* Builds the quotient model based on the previously computed equivalence classes (stored in the blocks * Builds the quotient model based on the previously computed equivalence classes (stored in the blocks

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

@ -157,7 +157,7 @@ namespace storm {
} }
template<typename ModelType> 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>*>& splitterQueue) {
for (auto block : predecessorBlocks) { for (auto block : predecessorBlocks) {
STORM_LOG_TRACE("Refining predecessor " << block->getId() << " of splitter"); STORM_LOG_TRACE("Refining predecessor " << block->getId() << " of splitter");
@ -378,7 +378,7 @@ namespace storm {
} }
template<typename ModelType> 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>*>& splitterQueue) {
// First, we need to turn the one-step probabilities to go to the splitter to the conditional probabilities // First, we need to turn the one-step probabilities to go to the splitter to the conditional probabilities
// for all non-silent states. // for all non-silent states.
computeConditionalProbabilitiesForNonSilentStates(block); computeConditionalProbabilitiesForNonSilentStates(block);
@ -416,7 +416,7 @@ namespace storm {
} }
template<typename ModelType> 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>*>& splitterQueue) {
for (auto block : predecessorBlocks) { for (auto block : predecessorBlocks) {
if (*block != splitter) { if (*block != splitter) {
refinePredecessorBlockOfSplitterWeak(*block, splitterQueue); refinePredecessorBlockOfSplitterWeak(*block, splitterQueue);
@ -439,7 +439,7 @@ namespace storm {
} }
template<typename ModelType> 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>*>& splitterQueue) {
STORM_LOG_TRACE("Refining partition based on splitter " << splitter.getId()); STORM_LOG_TRACE("Refining partition based on splitter " << splitter.getId());
// The outline of the refinement is as follows. // The outline of the refinement is as follows.

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

@ -39,11 +39,11 @@ namespace storm {
virtual void buildQuotient() override; 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>*>& splitterQueue) override;
private: private:
// Refines the predecessor blocks wrt. strong bisimulation. // 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>*>& splitterQueue);
/*! /*!
* Performs the necessary steps to compute a weak bisimulation on a DTMC. * Performs the necessary steps to compute a weak bisimulation on a DTMC.
@ -99,10 +99,10 @@ namespace storm {
void updateSilentProbabilitiesBasedOnTransitions(bisimulation::Block<BlockDataType>& block); void updateSilentProbabilitiesBasedOnTransitions(bisimulation::Block<BlockDataType>& block);
// Refines the predecessor blocks of the splitter wrt. weak bisimulation in DTMCs. // 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>*>& splitterQueue);
// Refines the given block wrt to weak bisimulation in DTMCs. // 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>*>& splitterQueue);
// Converts the one-step probabilities of going into the splitter into the conditional probabilities needed // Converts the one-step probabilities of going into the splitter into the conditional probabilities needed
// for weak bisimulation (on DTMCs). // for weak bisimulation (on DTMCs).

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

@ -198,7 +198,7 @@ namespace storm {
} }
template<typename ModelType> 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>*>& splitterQueue) {
uint_fast64_t lastState = 0; uint_fast64_t lastState = 0;
bool lastStateInitialized = false; bool lastStateInitialized = false;
@ -332,36 +332,23 @@ namespace storm {
} }
template<typename ModelType> 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>*>& splitterQueue) {
std::list<Block<BlockDataType>*> newBlocks; std::list<Block<BlockDataType>*> newBlocks;
bool split = this->partition.splitBlock(block, bool split = this->partition.splitBlock(block,
[this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { [this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
bool result = quotientDistributionsLess(state1, state2); bool result = quotientDistributionsLess(state1, state2);
// std::cout << state1 << " is " << (!result ? "not" : "") << " smaller than " << state2 << std::endl;
return result; return result;
}, },
[this, &block, &splitterQueue, &newBlocks] (Block<BlockDataType>& newBlock) { [this, &block, &splitterQueue, &newBlocks] (Block<BlockDataType>& newBlock) {
newBlocks.push_back(&newBlock); newBlocks.push_back(&newBlock);
// this->checkBlockStable(newBlock);
// this->checkDistributionsDifferent(block, block.getEndIndex());
// this->checkQuotientDistributions();
}); });
// The quotient distributions of the predecessors of block do not need to be updated, since the probability
// will go to the block with the same id as before.
// std::cout << "partition after split: " << std::endl;
// this->partition.print();
// defer updating the quotient distributions until *after* all splits, because
// Defer updating the quotient distributions until *after* all splits, because
// it otherwise influences the subsequent splits! // it otherwise influences the subsequent splits!
for (auto el : newBlocks) { for (auto el : newBlocks) {
this->updateQuotientDistributionsOfPredecessors(*el, block, splitterQueue); this->updateQuotientDistributionsOfPredecessors(*el, block, splitterQueue);
} }
// this->checkQuotientDistributions();
return split; return split;
} }
@ -370,11 +357,6 @@ namespace storm {
STORM_LOG_TRACE("Comparing the quotient distributions of state " << state1 << " and " << state2 << "."); STORM_LOG_TRACE("Comparing the quotient distributions of state " << state1 << " and " << state2 << ".");
std::vector<uint_fast64_t> nondeterministicChoiceIndices = this->model.getTransitionMatrix().getRowGroupIndices(); std::vector<uint_fast64_t> nondeterministicChoiceIndices = this->model.getTransitionMatrix().getRowGroupIndices();
// std::cout << "distributions of state " << state1 << std::endl;
// this->printDistributions(state1);
// std::cout << "distributions of state " << state2 << std::endl;
// this->printDistributions(state2);
auto firstIt = orderedQuotientDistributions.begin() + nondeterministicChoiceIndices[state1]; auto firstIt = orderedQuotientDistributions.begin() + nondeterministicChoiceIndices[state1];
auto firstIte = orderedQuotientDistributions.begin() + nondeterministicChoiceIndices[state1 + 1]; auto firstIte = orderedQuotientDistributions.begin() + nondeterministicChoiceIndices[state1 + 1];
auto secondIt = orderedQuotientDistributions.begin() + nondeterministicChoiceIndices[state2]; auto secondIt = orderedQuotientDistributions.begin() + nondeterministicChoiceIndices[state2];
@ -405,7 +387,7 @@ namespace storm {
} }
template<typename ModelType> 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>*>& splitterQueue) {
if (!possiblyNeedsRefinement(splitter)) { if (!possiblyNeedsRefinement(splitter)) {
return; return;
} }

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

@ -37,7 +37,7 @@ namespace storm {
virtual void buildQuotient() override; 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>*>& splitterQueue) override;
virtual void initialize() override; virtual void initialize() override;
@ -52,7 +52,7 @@ namespace storm {
bool possiblyNeedsRefinement(bisimulation::Block<BlockDataType> const& block) const; bool possiblyNeedsRefinement(bisimulation::Block<BlockDataType> const& block) const;
// Splits the given block according to the current quotient distributions. // 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>*>& splitterQueue);
// Retrieves whether the quotient distributions of state 1 are considered to be less than the ones of state 2. // 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; 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 // Updates the quotient distributions of the predecessors of the new block by taking the probability mass
// away from the old block. // 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>*>& splitterQueue);
bool checkQuotientDistributions() const; bool checkQuotientDistributions() const;
bool checkBlockStable(bisimulation::Block<BlockDataType> const& newBlock) const; bool checkBlockStable(bisimulation::Block<BlockDataType> const& newBlock) const;

Write Preview
Loading…
Cancel
Save