diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp
index cfd43923b..2c57a65ed 100644
--- a/src/storage/bisimulation/BisimulationDecomposition.cpp
+++ b/src/storage/bisimulation/BisimulationDecomposition.cpp
@@ -231,7 +231,7 @@ 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::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()); } );
// Then perform the actual splitting until there are no more splitters.
@@ -242,9 +242,9 @@ namespace storm {
// 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(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);
// Now refine the partition using the current splitter.
diff --git a/src/storage/bisimulation/BisimulationDecomposition.h b/src/storage/bisimulation/BisimulationDecomposition.h
index 6507e3b07..e3322444c 100644
--- a/src/storage/bisimulation/BisimulationDecomposition.h
+++ b/src/storage/bisimulation/BisimulationDecomposition.h
@@ -1,8 +1,6 @@
#ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
#define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
-#include <deque>
-
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/BisimulationSettings.h"
#include "src/storage/sparse/StateType.h"
@@ -224,7 +222,7 @@ namespace storm {
* @param splitter The splitter to use.
* @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
diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
index 0b0574737..b030b7cee 100644
--- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
+++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
@@ -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>*>& splitterQueue) {
for (auto block : predecessorBlocks) {
STORM_LOG_TRACE("Refining predecessor " << block->getId() << " of splitter");
@@ -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>*>& 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);
@@ -416,7 +416,7 @@ namespace storm {
}
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) {
if (*block != splitter) {
refinePredecessorBlockOfSplitterWeak(*block, splitterQueue);
@@ -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>*>& splitterQueue) {
STORM_LOG_TRACE("Refining partition based on splitter " << splitter.getId());
// The outline of the refinement is as follows.
diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h
index b9f2a2a5a..b4db574cb 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<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) override;
+ virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) 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>*>& splitterQueue);
/*!
* 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>*>& splitterQueue);
// 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
// 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 547d4dc29..1a82e5976 100644
--- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp
+++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp
@@ -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>*>& splitterQueue) {
uint_fast64_t lastState = 0;
bool lastStateInitialized = false;
@@ -332,36 +332,23 @@ 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>*>& splitterQueue) {
std::list<Block<BlockDataType>*> newBlocks;
bool split = this->partition.splitBlock(block,
[this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
bool result = quotientDistributionsLess(state1, state2);
-// std::cout << state1 << " is " << (!result ? "not" : "") << " smaller than " << state2 << std::endl;
return result;
},
[this, &block, &splitterQueue, &newBlocks] (Block<BlockDataType>& 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!
for (auto el : newBlocks) {
this->updateQuotientDistributionsOfPredecessors(*el, block, splitterQueue);
}
-// this->checkQuotientDistributions();
-
return split;
}
@@ -369,11 +356,6 @@ namespace storm {
bool NondeterministicModelBisimulationDecomposition<ModelType>::quotientDistributionsLess(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) const {
STORM_LOG_TRACE("Comparing the quotient distributions of state " << state1 << " and " << state2 << ".");
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 firstIte = orderedQuotientDistributions.begin() + nondeterministicChoiceIndices[state1 + 1];
@@ -405,7 +387,7 @@ 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>*>& splitterQueue) {
if (!possiblyNeedsRefinement(splitter)) {
return;
}
diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h
index 18a6e8e58..6c25d6cf9 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<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;
@@ -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>*>& splitterQueue);
// 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>*>& splitterQueue);
bool checkQuotientDistributions() const;
bool checkBlockStable(bisimulation::Block<BlockDataType> 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_ */