Browse Source

Next splitter is now chosen more deterministically.

Former-commit-id: 7f92208d1c
tempestpy_adaptions
dehnert 10 years ago
parent
commit
4b8f2e7a0b
  1. 2
      src/storage/DeterministicModelBisimulationDecomposition.cpp

2
src/storage/DeterministicModelBisimulationDecomposition.cpp

@ -757,7 +757,7 @@ namespace storm {
// Then perform the actual splitting until there are no more splitters. // Then perform the actual splitting until there are no more splitters.
while (!splitterQueue.empty()) { while (!splitterQueue.empty()) {
// Optionally: sort the splitter queue according to some criterion (here: prefer small splitters). // Optionally: sort the splitter queue according to some criterion (here: prefer small splitters).
std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } );
std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates() || (b1->getNumberOfStates() == b2->getNumberOfStates() && b1->getId() < b2->getId()); } );
// Get and prepare the next splitter. // Get and prepare the next splitter.
Block* splitter = splitterQueue.front(); Block* splitter = splitterQueue.front();

Loading…
Cancel
Save