From bc43ce52ab25c5548d77fe1dfc14532d0a88baec Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 12 Oct 2014 22:51:33 +0200 Subject: [PATCH] Eliminated two bugs, more to come. Former-commit-id: 3ea21c66b946aae54cf62990d8f3e9687d2c0c15 --- src/storage/BisimulationDecomposition.cpp | 2 +- src/storage/BisimulationDecomposition2.cpp | 26 +++++++++++++--------- src/utility/cli.h | 2 +- 3 files changed, 18 insertions(+), 12 deletions(-) diff --git a/src/storage/BisimulationDecomposition.cpp b/src/storage/BisimulationDecomposition.cpp index 342914601..0d7abc44a 100644 --- a/src/storage/BisimulationDecomposition.cpp +++ b/src/storage/BisimulationDecomposition.cpp @@ -16,7 +16,7 @@ namespace storm { std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); // We start by computing the initial partition. In particular, we also keep a mapping of states to their blocks. std::vector stateToBlockMapping(dtmc.getNumberOfStates()); - storm::storage::BitVector labeledStates = dtmc.getLabeledStates("observe0Greater1"); + storm::storage::BitVector labeledStates = dtmc.getLabeledStates("elected"); this->blocks.emplace_back(labeledStates.begin(), labeledStates.end()); std::for_each(labeledStates.begin(), labeledStates.end(), [&] (storm::storage::sparse::state_type const& state) { stateToBlockMapping[state] = 0; } ); labeledStates.complement(); diff --git a/src/storage/BisimulationDecomposition2.cpp b/src/storage/BisimulationDecomposition2.cpp index abda69f66..38d02ae90 100644 --- a/src/storage/BisimulationDecomposition2.cpp +++ b/src/storage/BisimulationDecomposition2.cpp @@ -11,7 +11,7 @@ namespace storm { static std::size_t globalId = 0; template - BisimulationDecomposition2::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedPosition(begin), id(globalId++) { + BisimulationDecomposition2::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), id(globalId++) { if (next != nullptr) { next->prev = this; } @@ -232,11 +232,10 @@ namespace storm { template void BisimulationDecomposition2::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { - std::cout << "swapping states " << state1 << " and " << state2 << std::endl; + std::cout << "swapping states " << state1 << " and " << state2 << " at positions " << this->positions[state1] << " and " << this->positions[state2] << std::endl; std::swap(this->states[this->positions[state1]], this->states[this->positions[state2]]); std::swap(this->values[this->positions[state1]], this->values[this->positions[state2]]); std::swap(this->positions[state1], this->positions[state2]); - assert(this->check()); } template @@ -252,7 +251,6 @@ namespace storm { this->positions[state2] = position1; std::cout << "pos of " << state1 << " is now " << position2 << " and pos of " << state2 << " is now " << position1 << std::endl; std::cout << this->states[position1] << " vs " << state2 << " and " << this->states[position2] << " vs " << state1 << std::endl; - assert(this->check()); } template @@ -559,7 +557,7 @@ namespace storm { // Now we can check whether the block needs to be split, which is the case iff the probabilities for the // first and the last state are different. std::size_t createdBlocks = 0; - while (std::abs(partition.getValueAtPosition(beginIndex) - partition.getValueAtPosition(endIndex)) >= 1e-6) { + while (std::abs(partition.getValueAtPosition(beginIndex) - partition.getValueAtPosition(endIndex - 1)) >= 1e-6) { // Now we scan for the first state in the block that disagrees on the probability value. // Note that we do not have to check currentIndex for staying within bounds, because we know the matching // state is within bounds. @@ -575,9 +573,9 @@ namespace storm { // Now we split the block and mark it as a potential splitter. ++createdBlocks; Block& newBlock = partition.splitBlock(block, currentIndex); - if (!newBlock.isMarkedAsPredecessor()) { - newBlock.markAsSplitter(); + if (!newBlock.isMarkedAsSplitter()) { splitterQueue.push_back(&newBlock); + newBlock.markAsSplitter(); } beginIndex = currentIndex; } @@ -658,8 +656,11 @@ namespace storm { } if (!predecessorBlock.isMarkedAsPredecessor()) { + std::cout << "not already in there" << std::endl; predecessorBlocks.emplace_back(&predecessorBlock); predecessorBlock.markAsPredecessorBlock(); + } else { + std::cout << "already in there" << std::endl; } } @@ -671,6 +672,8 @@ namespace storm { } } + std::cout << "(1)having " << predecessorBlocks.size() << " pred blocks " << std::endl; + // Now we can traverse the list of states of the splitter whose predecessors we have not yet explored. for (auto stateIterator = partition.getStates().begin() + splitter.getOriginalBegin(), stateIte = partition.getStates().begin() + splitter.getMarkedPosition(); stateIterator != stateIte; ++stateIterator) { storm::storage::sparse::state_type currentState = *stateIterator; @@ -699,7 +702,7 @@ namespace storm { std::list blocksToSplit; - std::cout << "having " << predecessorBlocks.size() << " pred blocks " << std::endl; + std::cout << "(2)having " << predecessorBlocks.size() << " pred blocks " << std::endl; // Now, we can iterate over the predecessor blocks and see whether we have to create a new block for // predecessors of the splitter. @@ -714,9 +717,12 @@ namespace storm { std::cout << "moved begin of block " << block.getId() << " to " << block.getBegin() << " and end to " << block.getEnd() << std::endl; Block& newBlock = partition.insertBlock(block); - std::cout << "created new block " << std::endl; + std::cout << "created new block " << newBlock.getId() << " from block " << block.getId() << std::endl; newBlock.print(partition); - splitterQueue.push_back(&newBlock); + if (!newBlock.isMarkedAsSplitter()) { + splitterQueue.push_back(&newBlock); + newBlock.markAsSplitter(); + } } else { std::cout << "all states are predecessors" << std::endl; diff --git a/src/utility/cli.h b/src/utility/cli.h index 70d4e75af..6996736a4 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -261,7 +261,7 @@ namespace storm { if (settings.isBisimulationSet()) { STORM_LOG_THROW(result->getType() == storm::models::DTMC, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only compatible with DTMCs."); std::shared_ptr> dtmc = result->template as>(); -// storm::storage::BisimulationDecomposition bisimulationDecomposition(*dtmc); + storm::storage::BisimulationDecomposition bisimulationDecomposition(*dtmc); storm::storage::BisimulationDecomposition2 bisimulationDecomposition2(*dtmc); }