From f90ac5c8c39fa26407cf432eba6369c18397a016 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 25 Oct 2014 17:03:37 +0200 Subject: [PATCH] First working version of weak bisimulation for DTMCs. Former-commit-id: 8a7d76de4fc182b487c40199c78a338aede88bd9 --- ...inisticModelStrongBisimulationDecomposition.cpp | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp index f057b4406..4cc536c1b 100644 --- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp @@ -576,7 +576,7 @@ namespace storm { } template - DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, bool weak, bool buildQuotient) { + DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, bool weak, bool buildQuotient) : comparator(0) { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, weak); @@ -732,12 +732,19 @@ namespace storm { std::chrono::high_resolution_clock::time_point refinementStart = std::chrono::high_resolution_clock::now(); std::deque splitterQueue; std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); a.markAsSplitter(); }); - + // Then perform the actual splitting until there are no more splitters. while (!splitterQueue.empty()) { + // 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(); } ); - refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitterQueue.front(), partition, weak, splitterQueue); + + // Get and prepare the next splitter. + Block* splitter = splitterQueue.front(); splitterQueue.pop_front(); + splitter->unmarkAsSplitter(); + + // Now refine the partition using the current splitter. + refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitter, partition, weak, splitterQueue); } std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart; @@ -770,7 +777,6 @@ namespace storm { std::cout << "------------------------------------------" << std::endl; std::cout << " * total time: " << std::chrono::duration_cast(totalTime).count() << "ms" << std::endl; std::cout << std::endl; - std::cout << "Number of equivalence classes: " << this->size() << std::endl; } }